deadlock states now get fixed in abstract game

Former-commit-id: efaa5d007e

src/storage/prism/menu_games/AbstractProgram.cpp

@@ -14,7 +14,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) {
+            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()) {
                 
                 // 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.
@@ -92,6 +92,14 @@ namespace storm {
                 // As long as there is only one module, we only build its game representation.
                 std::pair<storm::dd::Bdd<DdType>, uint_fast64_t> gameBdd = modules.front().getAbstractBdd();
                 
+                // If the abstraction did not change, we can return the most recenty obtained ADD.
+                if (gameBdd.first == lastAbstractBdd) {
+                    return lastAbstractAdd;
+                }
+                
+                // Otherwise, we remember that the abstract BDD changed and perform a reachability analysis.
+                lastAbstractBdd = gameBdd.first;
+
                 // Construct a set of all unnecessary variables, so we can abstract from it.
                 std::set<storm::expressions::Variable> variablesToAbstract = {ddInformation.commandDdVariable, ddInformation.updateDdVariable};
                 for (uint_fast64_t index = 0; index < gameBdd.second; ++index) {
@@ -99,11 +107,22 @@ namespace storm {
                 }
 
                 // Do a reachability analysis on the raw transition relation.
-                storm::dd::Bdd<DdType> transitionRelation = gameBdd.first.existsAbstract(variablesToAbstract);
+                storm::dd::Bdd<DdType> transitionRelation = lastAbstractBdd.existsAbstract(variablesToAbstract);
                 storm::dd::Bdd<DdType> reachableStates = this->getReachableStates(initialStateAbstractor.getAbstractStates(), transitionRelation);
                 
+                // Find the deadlock states in the model.
+                storm::dd::Bdd<DdType> deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables);
+                deadlockStates = reachableStates && !deadlockStates;
+                
+                // If there are deadlock states, we fix them now.
+                storm::dd::Add<DdType> deadlockTransitions = ddInformation.manager->getAddZero();
+                if (!deadlockStates.isZero()) {
+                    deadlockTransitions = (deadlockStates && ddInformation.allPredicateIdentities && ddInformation.manager->getEncoding(ddInformation.commandDdVariable, 0)  && ddInformation.manager->getEncoding(ddInformation.updateDdVariable, 0) && ddInformation.getMissingOptionVariableCube(0, gameBdd.second)).toAdd();
+                }
+                
                 // Construct the final game by cutting away the transitions of unreachable states.
-                return (gameBdd.first && reachableStates).toAdd() * commandUpdateProbabilitiesAdd;
+                lastAbstractAdd = (lastAbstractBdd && reachableStates).toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions;
+                return lastAbstractAdd;
             }
             
             template <storm::dd::DdType DdType, typename ValueType>

src/storage/prism/menu_games/AbstractProgram.h

@@ -82,6 +82,12 @@ namespace storm {
                 
                 // An ADD characterizing the probabilities of commands and their updates.
                 storm::dd::Add<DdType> commandUpdateProbabilitiesAdd;
+                
+                // A BDD that is the result of the last abstraction of the system.
+                storm::dd::Bdd<DdType> lastAbstractBdd;
+
+                // An ADD that is the result of the last abstraction of the system.
+                storm::dd::Add<DdType> lastAbstractAdd;
             };
         }
     }

src/storage/prism/menu_games/AbstractionDdInformation.cpp

@@ -14,7 +14,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) : manager(manager) {
+            AbstractionDdInformation<DdType, ValueType>::AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> const& manager) : manager(manager), allPredicateIdentities(manager->getBddOne()) {
                 // Intentionally left empty.
             }
             
@@ -40,6 +40,7 @@ namespace storm {
                 predicateDdVariables.push_back(newMetaVariable);
                 predicateBdds.emplace_back(manager->getEncoding(newMetaVariable.first, 1), manager->getEncoding(newMetaVariable.second, 1));
                 predicateIdentities.push_back(manager->getIdentity(newMetaVariable.first).equals(manager->getIdentity(newMetaVariable.second)).toBdd());
+                allPredicateIdentities &= predicateIdentities.back();
                 sourceVariables.insert(newMetaVariable.first);
                 successorVariables.insert(newMetaVariable.second);
             }

src/storage/prism/menu_games/AbstractionDdInformation.h

@@ -89,6 +89,9 @@ namespace storm {
                 // The BDDs representing the predicate identities (i.e. source and successor variable have the same truth value).
                 std::vector<storm::dd::Bdd<DdType>> predicateIdentities;
                 
+                // A BDD that represents the identity of all predicate variables.
+                storm::dd::Bdd<DdType> allPredicateIdentities;
+                
                 // The DD variable encoding the command (i.e., the nondeterministic choices of player 1).
                 storm::expressions::Variable commandDdVariable;