added more tests, not working yet, however

Former-commit-id: 2badd7ce35

src/storage/prism/menu_games/AbstractCommand.cpp

@@ -71,11 +71,12 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             void AbstractCommand<DdType, ValueType>::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<storm::dd::Bdd<DdType>, std::vector<storm::dd::Bdd<DdType>>> 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<storm::expressions::Variable> 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;

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 <storm::dd::DdType DdType, typename ValueType>
-            AbstractProgram<DdType, ValueType>::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared<storm::dd::DdManager<DdType>>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, *this->smtSolverFactory), lastAbstractBdd(ddInformation.manager->getBddZero()), lastAbstractAdd(ddInformation.manager->getAddZero()) {
+            AbstractProgram<DdType, ValueType>::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared<storm::dd::DdManager<DdType>>()), 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<DdType> transitionRelation = lastAbstractBdd.existsAbstract(variablesToAbstract);
-                storm::dd::Bdd<DdType> reachableStates = this->getReachableStates(initialStateAbstractor.getAbstractStates(), transitionRelation);
+                lastReachableStates = this->getReachableStates(initialStateAbstractor.getAbstractStates(), transitionRelation);
 
                 // Find the deadlock states in the model.
                 storm::dd::Bdd<DdType> deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables);
-                deadlockStates = reachableStates && !deadlockStates;
+                deadlockStates = lastReachableStates && !deadlockStates;
                 
                 // If there are deadlock states, we fix them now.
                 storm::dd::Add<DdType> 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::DdType DdType, typename ValueType>
+            storm::dd::Bdd<DdType> AbstractProgram<DdType, ValueType>::getReachableStates() {
+                return lastReachableStates;
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> AbstractProgram<DdType, ValueType>::getReachableStates(storm::dd::Bdd<DdType> const& initialStates, storm::dd::Bdd<DdType> const& transitionRelation) {
                 storm::dd::Bdd<storm::dd::DdType::CUDD> frontier = initialStates;

src/storage/prism/menu_games/AbstractProgram.h

@@ -44,6 +44,14 @@ namespace storm {
                  */
                 storm::dd::Add<DdType> 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<DdType> getReachableStates();
+                
                 /*!
                  * Refines the abstract module with the given predicates.
                  *
@@ -88,6 +96,9 @@ namespace storm {
                 
                 // An ADD that is the result of the last abstraction of the system.
                 storm::dd::Add<DdType> lastAbstractAdd;
+                
+                // A BDD that is the result of the reachability analysis on the abstraction of the system.
+                storm::dd::Bdd<DdType> lastReachableStates;
             };
         }
     }

src/storage/prism/menu_games/VariablePartition.cpp

@@ -10,9 +10,11 @@ namespace storm {
             VariablePartition::VariablePartition(std::set<storm::expressions::Variable> const& relevantVariables, std::vector<storm::expressions::Expression> 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<uint_fast64_t>();
+                    variableBlocks[currentBlock].insert(variable);
                 }
                 
                 // Add all expressions, which might relate some variables.

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<storm::expressions::Expression> 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<storm::expressions::Expression> 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<storm::expressions::Expression> 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<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+    ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+    
+    EXPECT_EQ(313, abstraction.getNodeCount());
+    
+    storm::dd::Bdd<storm::dd::DdType::CUDD> 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<storm::expressions::Expression> 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<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+    ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+    
+    EXPECT_EQ(46, abstraction.getNodeCount());
+    
+    storm::dd::Bdd<storm::dd::DdType::CUDD> 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<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -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<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -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<storm::utility::solver::MathsatSmtSolverFactory>());
@@ -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<storm::utility::solver::MathsatSmtSolverFactory>());