From e8794dee22b83e61642794c6e9c0e39f078c9c82 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 18 Sep 2015 16:58:09 +0200 Subject: [PATCH] added more tests, not working yet, however Former-commit-id: 2badd7ce35cfc4ac92f236dd6c28f0b4d252bd94 --- .../prism/menu_games/AbstractCommand.cpp | 15 +- .../prism/menu_games/AbstractProgram.cpp | 16 ++- .../prism/menu_games/AbstractProgram.h | 13 +- .../prism/menu_games/VariablePartition.cpp | 2 + .../abstraction/PrismMenuGameTest.cpp | 128 ++++++++++++++++-- 5 files changed, 160 insertions(+), 14 deletions(-) diff --git a/src/storage/prism/menu_games/AbstractCommand.cpp b/src/storage/prism/menu_games/AbstractCommand.cpp index 3b91eb01e..267ee38b6 100644 --- a/src/storage/prism/menu_games/AbstractCommand.cpp +++ b/src/storage/prism/menu_games/AbstractCommand.cpp @@ -71,11 +71,12 @@ namespace storm { template void AbstractCommand::recomputeCachedBdd() { STORM_LOG_TRACE("Recomputing BDD for command " << command.get()); + std::cout << "recomputing " << command.get() << std::endl; // Create a mapping from source state DDs to their distributions. std::unordered_map, std::vector>> sourceToDistributionsMap; uint_fast64_t modelCounter = 0; - smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model)); ++modelCounter; return true; } ); + smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model)); ++modelCounter; std::cout << "model cnt: " << modelCounter << std::endl; return true; } ); // Now we search for the maximal number of choices of player 2 to determine how many DD variables we // need to encode the nondeterminism. @@ -121,6 +122,11 @@ namespace storm { // To start with, all predicates related to the guard are relevant source predicates. result.first = variablePartition.getExpressionsUsingVariables(command.get().getGuardExpression().getVariables()); + std::cout << "using" << std::endl; + for (auto const& el : result.first) { + std::cout << expressionInformation.predicates[el] << std::endl; + } + std::set assignedVariables; for (auto const& assignment : assignments) { // Also, variables appearing on the right-hand side of an assignment are relevant for source state. @@ -137,6 +143,13 @@ namespace storm { } auto const& predicatesRelatedToAssignedVariable = variablePartition.getRelatedExpressions(assignedVariables); + + std::cout << variablePartition << std::endl; + std::cout << "related" << std::endl; + for (auto const& el : predicatesRelatedToAssignedVariable) { + std::cout << expressionInformation.predicates[el] << std::endl; + } + result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end()); return result; diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp index 792efc323..c515a9074 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -8,13 +8,14 @@ #include "src/utility/macros.h" #include "src/utility/solver.h" #include "src/exceptions/WrongFormatException.h" +#include "src/exceptions/InvalidArgumentException.h" namespace storm { namespace prism { namespace menu_games { template - AbstractProgram::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, *this->smtSolverFactory), lastAbstractBdd(ddInformation.manager->getBddZero()), lastAbstractAdd(ddInformation.manager->getAddZero()) { + AbstractProgram::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, *this->smtSolverFactory), lastAbstractBdd(ddInformation.manager->getBddZero()), lastAbstractAdd(ddInformation.manager->getAddZero()), lastReachableStates(ddInformation.manager->getBddZero()) { // For now, we assume that there is a single module. If the program has more than one module, it needs // to be flattened before the procedure. @@ -74,6 +75,7 @@ namespace storm { // Create DD variables and some auxiliary data structures for the new predicates. for (auto const& predicate : predicates) { + STORM_LOG_THROW(predicate.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expecting a predicate of type bool."); ddInformation.addPredicate(predicate); } @@ -113,11 +115,11 @@ namespace storm { // Do a reachability analysis on the raw transition relation. storm::dd::Bdd transitionRelation = lastAbstractBdd.existsAbstract(variablesToAbstract); - storm::dd::Bdd reachableStates = this->getReachableStates(initialStateAbstractor.getAbstractStates(), transitionRelation); + lastReachableStates = this->getReachableStates(initialStateAbstractor.getAbstractStates(), transitionRelation); // Find the deadlock states in the model. storm::dd::Bdd deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables); - deadlockStates = reachableStates && !deadlockStates; + deadlockStates = lastReachableStates && !deadlockStates; // If there are deadlock states, we fix them now. storm::dd::Add deadlockTransitions = ddInformation.manager->getAddZero(); @@ -126,10 +128,16 @@ namespace storm { } // Construct the final game by cutting away the transitions of unreachable states. - lastAbstractAdd = (lastAbstractBdd && reachableStates).toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; + lastAbstractAdd = (lastAbstractBdd && lastReachableStates).toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; return lastAbstractAdd; } + + template + storm::dd::Bdd AbstractProgram::getReachableStates() { + return lastReachableStates; + } + template storm::dd::Bdd AbstractProgram::getReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitionRelation) { storm::dd::Bdd frontier = initialStates; diff --git a/src/storage/prism/menu_games/AbstractProgram.h b/src/storage/prism/menu_games/AbstractProgram.h index 88094a632..c1f54b585 100644 --- a/src/storage/prism/menu_games/AbstractProgram.h +++ b/src/storage/prism/menu_games/AbstractProgram.h @@ -44,6 +44,14 @@ namespace storm { */ storm::dd::Add getAbstractAdd(); + /*! + * Retrieves the reachable state space of the abstract game (that was previously retrieved via the + * appropriate method. + * + * @return The reachable state space in the form of a BDD. + */ + storm::dd::Bdd getReachableStates(); + /*! * Refines the abstract module with the given predicates. * @@ -85,9 +93,12 @@ namespace storm { // A BDD that is the result of the last abstraction of the system. storm::dd::Bdd lastAbstractBdd; - + // An ADD that is the result of the last abstraction of the system. storm::dd::Add lastAbstractAdd; + + // A BDD that is the result of the reachability analysis on the abstraction of the system. + storm::dd::Bdd lastReachableStates; }; } } diff --git a/src/storage/prism/menu_games/VariablePartition.cpp b/src/storage/prism/menu_games/VariablePartition.cpp index a5058db1d..fc69ac1a4 100644 --- a/src/storage/prism/menu_games/VariablePartition.cpp +++ b/src/storage/prism/menu_games/VariablePartition.cpp @@ -10,9 +10,11 @@ namespace storm { VariablePartition::VariablePartition(std::set const& relevantVariables, std::vector const& expressions) : relevantVariables(relevantVariables), expressionBlocks(relevantVariables.size()) { // Assign each variable to a new block. uint_fast64_t currentBlock = 0; + variableBlocks.resize(relevantVariables.size()); for (auto const& variable : relevantVariables) { this->variableToBlockMapping[variable] = currentBlock; this->variableToExpressionsMapping[variable] = std::set(); + variableBlocks[currentBlock].insert(variable); } // Add all expressions, which might relate some variables. diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp index 466f7693a..8fdd03cdd 100644 --- a/test/functional/abstraction/PrismMenuGameTest.cpp +++ b/test/functional/abstraction/PrismMenuGameTest.cpp @@ -15,7 +15,7 @@ #include "src/utility/solver.h" -TEST(PrismMenuGame, DieProgramAbstractionTest) { +TEST(PrismMenuGame, DieAbstractionTest) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); std::vector initialPredicates; @@ -31,7 +31,7 @@ TEST(PrismMenuGame, DieProgramAbstractionTest) { EXPECT_EQ(19, abstraction.getNodeCount()); } -TEST(PrismMenuGame, DieProgramAbstractionAndRefinementTest) { +TEST(PrismMenuGame, DieAbstractionAndRefinementTest) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); std::vector initialPredicates; @@ -50,7 +50,43 @@ TEST(PrismMenuGame, DieProgramAbstractionAndRefinementTest) { EXPECT_EQ(26, abstraction.getNodeCount()); } -TEST(PrismMenuGame, CrowdsProgramAbstractionTest) { +TEST(PrismMenuGame, DieFullAbstractionTest) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + + std::vector initialPredicates; + storm::expressions::ExpressionManager& manager = program.getManager(); + + initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(6)); + initialPredicates.push_back(manager.getVariableExpression("s") == manager.integer(7)); + + initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(5)); + initialPredicates.push_back(manager.getVariableExpression("d") == manager.integer(6)); + + storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + + storm::dd::Add abstraction; + ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); + + EXPECT_EQ(313, abstraction.getNodeCount()); + + storm::dd::Bdd reachableStatesInAbstraction; + ASSERT_NO_THROW(reachableStatesInAbstraction = abstractProgram.getReachableStates()); + + EXPECT_EQ(13, reachableStatesInAbstraction.getNonZeroCount()); +} + +TEST(PrismMenuGame, CrowdsAbstractionTest) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); program = program.substituteConstants(); @@ -67,7 +103,7 @@ TEST(PrismMenuGame, CrowdsProgramAbstractionTest) { EXPECT_EQ(46, abstraction.getNodeCount()); } -TEST(PrismMenuGame, CrowdsProgramAbstractionAndRefinementTest) { +TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); program = program.substituteConstants(); @@ -89,7 +125,83 @@ TEST(PrismMenuGame, CrowdsProgramAbstractionAndRefinementTest) { EXPECT_EQ(75, abstraction.getNodeCount()); } -TEST(PrismMenuGame, TwoDiceProgramAbstractionTest) { +TEST(PrismMenuGame, CrowdsFullAbstractionTest) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + program = program.substituteConstants(); + + std::vector initialPredicates; + storm::expressions::ExpressionManager& manager = program.getManager(); + + initialPredicates.push_back(manager.getVariableExpression("phase") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("phase") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("phase") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("phase") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("phase") == manager.integer(4)); + + initialPredicates.push_back(manager.getVariableExpression("good")); + + initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("runCount") == manager.integer(5)); + + initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("observe0") == manager.integer(5)); + + initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("observe1") == manager.integer(5)); + + initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("observe2") == manager.integer(5)); + + initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("observe3") == manager.integer(5)); + + initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(4)); + initialPredicates.push_back(manager.getVariableExpression("observe4") == manager.integer(5)); + + initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(0)); + initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(1)); + initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(2)); + initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(3)); + initialPredicates.push_back(manager.getVariableExpression("lastSeen") == manager.integer(4)); + + storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + + storm::dd::Add abstraction; + ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd()); + + EXPECT_EQ(46, abstraction.getNodeCount()); + + storm::dd::Bdd reachableStatesInAbstraction; + ASSERT_NO_THROW(reachableStatesInAbstraction = abstractProgram.getReachableStates()); + + EXPECT_EQ(13, reachableStatesInAbstraction.getNonZeroCount()); +} + +TEST(PrismMenuGame, TwoDiceAbstractionTest) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_unique()); @@ -108,7 +220,7 @@ TEST(PrismMenuGame, TwoDiceProgramAbstractionTest) { EXPECT_EQ(38, abstraction.getNodeCount()); } -TEST(PrismMenuGame, TwoDiceProgramAbstractionAndRefinementTest) { +TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_unique()); @@ -132,7 +244,7 @@ TEST(PrismMenuGame, TwoDiceProgramAbstractionAndRefinementTest) { EXPECT_EQ(107, abstraction.getNodeCount()); } -TEST(PrismMenuGame, WlanProgramAbstractionTest) { +TEST(PrismMenuGame, WlanAbstractionTest) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_unique()); @@ -152,7 +264,7 @@ TEST(PrismMenuGame, WlanProgramAbstractionTest) { EXPECT_EQ(219, abstraction.getNodeCount()); } -TEST(PrismMenuGame, WlanProgramAbstractionAndRefinementTest) { +TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); program = program.substituteConstants(); program = program.flattenModules(std::make_unique());