added support for computation of bottom states. not yet done

Former-commit-id: 49c2a28b28

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>>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, *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>>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(expressionInformation, ddInformation, *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.
@@ -30,6 +30,10 @@ namespace storm {
                     for (auto const& command : module.getCommands()) {
                         if (addAllGuards) {
                             expressionInformation.predicates.push_back(command.getGuardExpression());
+                        } else {
+                            // If not all guards were added, we also need to populate the bottom state abstractor.
+                            std::cout << "adding " << !command.getGuardExpression() << std::endl;
+                            bottomStateAbstractor.addPredicate(!command.getGuardExpression());
                         }
                         maximalUpdateCount = std::max(maximalUpdateCount, static_cast<uint_fast64_t>(command.getNumberOfUpdates()));
                     }
@@ -100,7 +104,10 @@ namespace storm {
                 // Refine initial state abstractor.
                 initialStateAbstractor.refine(newPredicateIndices);
                 
-                // Finally, we rebuild the game.
+                // Refine bottom state abstractor.
+                bottomStateAbstractor.refine(newPredicateIndices);
+                
+                // Finally, we rebuild the game..
                 currentGame = buildGame();
             }
             
@@ -139,6 +146,16 @@ namespace storm {
                 storm::dd::Bdd<DdType> initialStates = initialStateAbstractor.getAbstractStates();
                 storm::dd::Bdd<DdType> reachableStates = this->getReachableStates(initialStates, transitionRelation);
 
+                // Determine the bottom states.
+                storm::dd::Bdd<DdType> bottomStates;
+                if (addedAllGuards) {
+                    bottomStates = ddInformation.manager->getBddZero();
+                } else {
+                    bottomStates = bottomStateAbstractor.getAbstractStates();
+                }
+                
+                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);
                 deadlockStates = reachableStates && !deadlockStates;
@@ -160,7 +177,7 @@ namespace storm {
                 std::set<storm::expressions::Variable> allNondeterminismVariables = usedPlayer2Variables;
                 allNondeterminismVariables.insert(ddInformation.commandDdVariable);
                 
-                return std::unique_ptr<MenuGame<DdType>>(new MenuGame<DdType>(ddInformation.manager, reachableStates, initialStates, transitionMatrix, ddInformation.sourceVariables, ddInformation.successorVariables, ddInformation.predicateDdVariables, {ddInformation.commandDdVariable}, usedPlayer2Variables, allNondeterminismVariables, ddInformation.updateDdVariable, ddInformation.expressionToBddMap));
+                return std::unique_ptr<MenuGame<DdType>>(new MenuGame<DdType>(ddInformation.manager, reachableStates, initialStates, transitionMatrix, bottomStates, ddInformation.sourceVariables, ddInformation.successorVariables, ddInformation.predicateDdVariables, {ddInformation.commandDdVariable}, usedPlayer2Variables, allNondeterminismVariables, ddInformation.updateDdVariable, ddInformation.expressionToBddMap));
             }
             
             template <storm::dd::DdType DdType, typename ValueType>

src/storage/prism/menu_games/AbstractProgram.h

@@ -104,6 +104,12 @@ namespace storm {
                 // A state-set abstractor used to determine the initial states of the abstraction.
                 StateSetAbstractor<DdType, ValueType> initialStateAbstractor;
                 
+                // A flag that stores whether all guards were added (which is relevant for determining the bottom states).
+                bool addedAllGuards;
+
+                // A state-set abstractor used to determine the bottom states if not all guards were added.
+                StateSetAbstractor<DdType, ValueType> bottomStateAbstractor;
+                
                 // An ADD characterizing the probabilities of commands and their updates.
                 storm::dd::Add<DdType> commandUpdateProbabilitiesAdd;
                 

src/storage/prism/menu_games/MenuGame.cpp

@@ -17,6 +17,7 @@ namespace storm {
                                      storm::dd::Bdd<Type> reachableStates,
                                      storm::dd::Bdd<Type> initialStates,
                                      storm::dd::Add<Type> transitionMatrix,
+                                     storm::dd::Bdd<Type> bottomStates,
                                      std::set<storm::expressions::Variable> const& rowVariables,
                                      std::set<storm::expressions::Variable> const& columnVariables,
                                      std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
@@ -24,7 +25,7 @@ namespace storm {
                                      std::set<storm::expressions::Variable> const& player2Variables,
                                      std::set<storm::expressions::Variable> const& allNondeterminismVariables,
                                      storm::expressions::Variable const& updateVariable,
-                                     std::map<storm::expressions::Expression, storm::dd::Bdd<Type>> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame<Type>(manager, reachableStates, initialStates, transitionMatrix.sumAbstract({updateVariable}), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), updateVariable(updateVariable), expressionToBddMap(expressionToBddMap) {
+                                     std::map<storm::expressions::Expression, storm::dd::Bdd<Type>> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame<Type>(manager, reachableStates, initialStates, transitionMatrix.sumAbstract({updateVariable}), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), updateVariable(updateVariable), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) {
                 // Intentionally left empty.
             }
             
@@ -49,6 +50,11 @@ namespace storm {
                 }
             }
             
+            template<storm::dd::DdType Type>
+            storm::dd::Bdd<Type> MenuGame<Type>::getBottomStates() const {
+                return bottomStates;
+            }
+            
             template<storm::dd::DdType Type>
             bool MenuGame<Type>::hasLabel(std::string const& label) const {
                 return false;

src/storage/prism/menu_games/MenuGame.h

@@ -31,9 +31,10 @@ namespace storm {
                  * Constructs a model from the given data.
                  *
                  * @param manager The manager responsible for the decision diagrams.
-                 * @param reachableStates A DD representing the reachable states.
-                 * @param initialStates A DD representing the initial states of the model.
+                 * @param reachableStates The reachable states of the model.
+                 * @param initialStates The initial states of the model.
                  * @param transitionMatrix The matrix representing the transitions in the model.
+                 * @param bottomStates The bottom states of the model.
                  * @param rowVariables The set of row meta variables used in the DDs.
                  * @param columVariables The set of column meta variables used in the DDs.
                  * @param rowColumnMetaVariablePairs All pairs of row/column meta variables.
@@ -48,6 +49,7 @@ namespace storm {
                          storm::dd::Bdd<Type> reachableStates,
                          storm::dd::Bdd<Type> initialStates,
                          storm::dd::Add<Type> transitionMatrix,
+                         storm::dd::Bdd<Type> bottomStates,
                          std::set<storm::expressions::Variable> const& rowVariables,
                          std::set<storm::expressions::Variable> const& columnVariables,
                          std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
@@ -78,6 +80,13 @@ namespace storm {
                  */
                 storm::dd::Bdd<Type> getStates(storm::expressions::Expression const& expression, bool negated) const;
                 
+                /*!
+                 * Retrieves the bottom states of the model.
+                 *
+                 * @return The bottom states of the model.
+                 */
+                storm::dd::Bdd<Type> getBottomStates() const;
+                
                 virtual bool hasLabel(std::string const& label) const override;
                 
             private:
@@ -86,6 +95,9 @@ namespace storm {
                 
                 // A mapping from expressions that were used in the abstraction process to the the BDDs representing them.
                 std::map<storm::expressions::Expression, storm::dd::Bdd<Type>> expressionToBddMap;
+                
+                // The bottom states of the model.
+                storm::dd::Bdd<Type> bottomStates;
             };
             
         } // namespace menu_games

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, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.manager)), expressionInformation(expressionInformation), ddInformation(ddInformation), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), concretePredicateVariables(), cachedBdd(ddInformation.manager->getBddZero()) {
+            StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, 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()) {
                 
                 // Assert all range expressions to enforce legal variable values.
                 for (auto const& rangeExpression : expressionInformation.rangeExpressions) {
@@ -37,8 +37,8 @@ namespace storm {
                 concretePredicateVariables.insert(usedVariables.begin(), usedVariables.end());
                 variablePartition.relate(usedVariables);
 
-                // Since the new predicate might have changed the abstractions, we need to recompute it.
-                this->refine();
+                // Remember that we have to recompute the BDD.
+                this->needsRecomputation = true;
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
@@ -82,11 +82,14 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> StateSetAbstractor<DdType, ValueType>::getStateBdd(storm::solver::SmtSolver::ModelReference const& model) const {
                 STORM_LOG_TRACE("Building source state BDD.");
+                std::cout << "new model: " << std::endl;
                 storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne();
                 for (auto const& variableIndexPair : relevantPredicatesAndVariables) {
                     if (model.getBooleanValue(variableIndexPair.first)) {
+                        std::cout << expressionInformation.predicates[variableIndexPair.second] << " is true" << std::endl;
                         result &= ddInformation.predicateBdds[variableIndexPair.second].first;
                     } else {
+                        std::cout << expressionInformation.predicates[variableIndexPair.second] << " is false" << std::endl;
                         result &= !ddInformation.predicateBdds[variableIndexPair.second].first;
                     }
                 }
@@ -98,13 +101,17 @@ namespace storm {
                 STORM_LOG_TRACE("Recomputing BDD for state set abstraction.");
                 
                 storm::dd::Bdd<DdType> result = ddInformation.manager->getBddZero();
-                smtSolver->allSat(decisionVariables, [&result,this] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); return true; } );
+                uint_fast64_t modelCounter = 0;
+                smtSolver->allSat(decisionVariables, [&result,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); ++modelCounter; std::cout << "found " << modelCounter << " models" << std::endl; return modelCounter < 10000 ? true : false; } );
                 
                 cachedBdd = result;
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            storm::dd::Bdd<DdType> StateSetAbstractor<DdType, ValueType>::getAbstractStates() const {
+            storm::dd::Bdd<DdType> StateSetAbstractor<DdType, ValueType>::getAbstractStates() {
+                if (needsRecomputation) {
+                    this->refine();
+                }
                 return cachedBdd;
             }
             

src/storage/prism/menu_games/StateSetAbstractor.h

@@ -62,7 +62,7 @@ namespace storm {
                  *
                  * @return The set of matching abstract states in the form of a BDD
                  */
-                storm::dd::Bdd<DdType> getAbstractStates() const;
+                storm::dd::Bdd<DdType> getAbstractStates();
                 
             private:
                 /*!
@@ -106,6 +106,9 @@ namespace storm {
                 // The set of all decision variables over which to perform the all-sat enumeration.
                 std::vector<storm::expressions::Variable> decisionVariables;
                 
+                // A flag indicating whether the cached BDD needs recomputation.
+                bool needsRecomputation;
+                
                 // The cached BDD representing the abstraction. This variable is written to in refinement steps (if work
                 // needed to be done).
                 storm::dd::Bdd<DdType> cachedBdd;