more work on game-stuff

Former-commit-id: 62a56c9ba7

src/storage/prism/Program.cpp

@@ -360,11 +360,11 @@ namespace storm {
             return this->labels;
         }
         
-        std::vector<storm::expressions::Expression> Program::getAllGuards() const {
+        std::vector<storm::expressions::Expression> Program::getAllGuards(bool negated) const {
             std::vector<storm::expressions::Expression> allGuards;
             for (auto const& module : modules) {
                 for (auto const& command : module.getCommands()) {
-                    allGuards.push_back(command.getGuardExpression());
+                    allGuards.push_back(negated ? !command.getGuardExpression() : command.getGuardExpression());
                 }
             }
             return allGuards;

src/storage/prism/Program.h

@@ -363,9 +363,10 @@ namespace storm {
             /*!
              * Retrieves all guards appearing in the program.
              *
+             * @param negated A flag indicating whether the guards should be negated.
              * @return All guards appearing in the program.
              */
-            std::vector<storm::expressions::Expression> getAllGuards() const;
+            std::vector<storm::expressions::Expression> getAllGuards(bool negated = false) const;
             
             /*!
              * Retrieves the expression associated with the given label, if it exists.

src/storage/prism/menu_games/AbstractProgram.cpp

@@ -17,7 +17,7 @@ namespace storm {
         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>>(), initialPredicates), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(expressionInformation, ddInformation, program.getAllGuards(), *this->smtSolverFactory), currentGame(nullptr) {
+            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>>(), initialPredicates), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(expressionInformation, ddInformation, program.getAllGuards(true), *this->smtSolverFactory), currentGame(nullptr) {
                 
                 // 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.
@@ -71,7 +71,7 @@ namespace storm {
                 
                 // Add the predicates to the global list of predicates.
                 uint_fast64_t firstNewPredicateIndex = expressionInformation.predicates.size();
-                expressionInformation.predicates.insert(expressionInformation.predicates.end(), predicates.begin(), predicates.end());
+                expressionInformation.addPredicates(predicates);
                 
                 // Create DD variables and some auxiliary data structures for the new predicates.
                 for (auto const& predicate : predicates) {
@@ -140,10 +140,11 @@ namespace storm {
                 if (addedAllGuards) {
                     bottomStates = ddInformation.manager->getBddZero();
                 } else {
-                    // bottomStates = bottomStateAbstractor.getAbstractStates();
+                    bottomStateAbstractor.constrain(reachableStates);
+                    bottomStates = bottomStateAbstractor.getAbstractStates();
                 }
                 
-                // std::cout << "found " << (reachableStates && bottomStates).getNonZeroCount() << " reachable bottom states" << std::endl;
+                std::cout << "found " << (reachableStates && bottomStates).getNonZeroCount() << " reachable bottom states" << std::endl;
                 
                 // Find the deadlock states in the model.
                 storm::dd::Bdd<DdType> deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables);

src/storage/prism/menu_games/AbstractionDdInformation.cpp

@@ -16,7 +16,7 @@ namespace storm {
         namespace menu_games {
             
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractionDdInformation<DdType, ValueType>::AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> const& manager, std::vector<storm::expressions::Expression> const& initialPredicates) : manager(manager), allPredicateIdentities(manager->getBddOne()) {
+            AbstractionDdInformation<DdType, ValueType>::AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> const& manager, std::vector<storm::expressions::Expression> const& initialPredicates) : manager(manager), allPredicateIdentities(manager->getBddOne()), bddVariableIndexToPredicateMap() {
                 for (auto const& predicate : initialPredicates) {
                     this->addPredicate(predicate);
                 }
@@ -58,6 +58,7 @@ namespace storm {
                 sourceVariables.insert(newMetaVariable.first);
                 successorVariables.insert(newMetaVariable.second);
                 expressionToBddMap[predicate] = predicateBdds.back().first;
+                bddVariableIndexToPredicateMap[predicateIdentities.back().getIndex()] = predicate;
             }
          
             template <storm::dd::DdType DdType, typename ValueType>

src/storage/prism/menu_games/AbstractionDdInformation.h

@@ -5,6 +5,7 @@
 #include <vector>
 #include <set>
 #include <map>
+#include <unordered_map>
 
 #include "src/storage/dd/DdType.h"
 #include "src/storage/expressions/Variable.h"
@@ -105,6 +106,9 @@ namespace storm {
                 
                 // A mapping from the predicates to the BDDs.
                 std::map<storm::expressions::Expression, storm::dd::Bdd<DdType>> expressionToBddMap;
+                
+                // A mapping from the indices of the BDD variables to the predicates.
+                std::unordered_map<uint_fast64_t, storm::expressions::Expression> bddVariableIndexToPredicateMap;
             };
             
         }

src/storage/prism/menu_games/AbstractionExpressionInformation.cpp

@@ -11,6 +11,16 @@ namespace storm {
                 // Intentionally left empty.
             }
             
+            void AbstractionExpressionInformation::addPredicate(storm::expressions::Expression const& predicate) {
+                predicates.push_back(predicate);
+            }
+            
+            void AbstractionExpressionInformation::addPredicates(std::vector<storm::expressions::Expression> const& predicates) {
+                for (auto const& predicate : predicates) {
+                    this->addPredicate(predicate);
+                }
+            }
+            
         }
     }
 }

src/storage/prism/menu_games/AbstractionExpressionInformation.h

@@ -26,6 +26,20 @@ namespace storm {
                  */
                 AbstractionExpressionInformation(storm::expressions::ExpressionManager& manager, std::vector<storm::expressions::Expression> const& predicates = std::vector<storm::expressions::Expression>(), std::set<storm::expressions::Variable> const& variables = std::set<storm::expressions::Variable>(), std::vector<storm::expressions::Expression> const& rangeExpressions = std::vector<storm::expressions::Expression>());
                 
+                /*!
+                 * Adds the given predicate.
+                 *
+                 * @param predicate The predicate to add.
+                 */
+                void addPredicate(storm::expressions::Expression const& predicate);
+
+                /*!
+                 * Adds the given predicates.
+                 *
+                 * @param predicates The predicates to add.
+                 */
+                void addPredicates(std::vector<storm::expressions::Expression> const& predicates);
+                
                 // The manager responsible for the expressions of the program and the SMT solvers.
                 storm::expressions::ExpressionManager& manager;
                 

src/storage/prism/menu_games/StateSetAbstractor.cpp

@@ -13,7 +13,7 @@ namespace storm {
         namespace menu_games {
             
             template <storm::dd::DdType DdType, typename ValueType>
-            StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, std::vector<storm::expressions::Expression> const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.manager)), expressionInformation(expressionInformation), ddInformation(ddInformation), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(ddInformation.manager->getBddZero()), constraintBdd(ddInformation.manager->getBddOne()) {
+            StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, std::vector<storm::expressions::Expression> const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.manager)), expressionInformation(expressionInformation), ddInformation(ddInformation), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(ddInformation.manager->getBddZero()), constraint(ddInformation.manager->getBddOne()) {
                 
                 // Assert all range expressions to enforce legal variable values.
                 for (auto const& rangeExpression : expressionInformation.rangeExpressions) {
@@ -52,12 +52,21 @@ namespace storm {
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            void StateSetAbstractor<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& newPredicates, boost::optional<storm::dd::Bdd<DdType>> const& constraintBdd) {
+            void StateSetAbstractor<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& newPredicates) {
                 // Make the partition aware of the new predicates, which may make more predicates relevant to the abstraction.
                 for (auto const& predicateIndex : newPredicates) {
                     variablePartition.addExpression(expressionInformation.predicates[predicateIndex]);
                 }
-                this->recomputeCachedBdd();
+                needsRecomputation = true;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void StateSetAbstractor<DdType, ValueType>::constrain(storm::dd::Bdd<DdType> const& newConstraint) {
+                // If the constraint is different from the last one, we add it to the solver.
+                if (newConstraint != this->constraint) {
+                    constraint = newConstraint;
+                    this->pushConstraintBdd();
+                }
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
@@ -90,11 +99,17 @@ namespace storm {
                 if (!recomputeBdd) {
                     return;
                 }
-
+                
+                // Before adding the missing predicates, we need to remove the constraint BDD.
+                this->popConstraintBdd();
+                
                 // If we need to recompute the BDD, we start by introducing decision variables and the corresponding
                 // constraints in the SMT problem.
                 addMissingPredicates(newRelevantPredicateIndices);
                 
+                // Then re-add the constraint BDD.
+                this->pushConstraintBdd();
+                
                 STORM_LOG_TRACE("Recomputing BDD for state set abstraction.");
                 
                 storm::dd::Bdd<DdType> result = ddInformation.manager->getBddZero();
@@ -104,8 +119,34 @@ namespace storm {
                 cachedBdd = result;
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            void StateSetAbstractor<DdType, ValueType>::popConstraintBdd() {
+                // If the last constraint was not the constant one BDD, we need to pop the constraint from the solver.
+                if (!this->constraint.isOne()) {
+                    smtSolver->pop();
+                }
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void StateSetAbstractor<DdType, ValueType>::pushConstraintBdd() {
+                // Create a new backtracking point before adding the constraint.
+                smtSolver->push();
+                
+                // Then add the constraint.
+                std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> result = constraint.toExpression(expressionInformation.manager, ddInformation.bddVariableIndexToPredicateMap);
+                
+                std::cout << "adding expressions... " << std::endl;
+                for (auto const& expression : result.first) {
+                    std::cout << expression << std::endl;
+                    smtSolver->add(expression);
+                }
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> StateSetAbstractor<DdType, ValueType>::getAbstractStates() {
+                if (needsRecomputation) {
+                    this->recomputeCachedBdd();
+                }
                 return cachedBdd;
             }
             

src/storage/prism/menu_games/StateSetAbstractor.h

@@ -65,7 +65,14 @@ namespace storm {
                  *
                  * @param newPredicateIndices The indices of the new predicates.
                  */
-                void refine(std::vector<uint_fast64_t> const& newPredicateIndices, boost::optional<storm::dd::Bdd<DdType>> const& constraintBdd = boost::none);
+                void refine(std::vector<uint_fast64_t> const& newPredicateIndices);
+                
+                /*!
+                 * Constraints the abstract states with the given BDD.
+                 *
+                 * @param newConstraint The BDD used as the constraint.
+                 */
+                void constrain(storm::dd::Bdd<DdType> const& newConstraint);
                 
                 /*!
                  * Retrieves the set of abstract states matching all predicates added to this abstractor.
@@ -82,6 +89,16 @@ namespace storm {
                  */
                 void addMissingPredicates(std::set<uint_fast64_t> const& newRelevantPredicateIndices);
                 
+                /*!
+                 * Adds the current constraint BDD to the solver.
+                 */
+                void pushConstraintBdd();
+
+                /*!
+                 * Removes the current constraint BDD (if any) from the solver.
+                 */
+                void popConstraintBdd();
+                
                 /*!
                  * Recomputes the cached BDD. This needs to be triggered if any relevant predicates change.
                  */
@@ -124,7 +141,7 @@ namespace storm {
                 storm::dd::Bdd<DdType> cachedBdd;
                 
                 // This BDD currently constrains the search for solutions.
-                storm::dd::Bdd<DdType> constraintBdd;
+                storm::dd::Bdd<DdType> constraint;
             };
         }
     }