diff --git a/src/storm/abstraction/MenuGameAbstractor.cpp b/src/storm/abstraction/MenuGameAbstractor.cpp index 7ce40950b..f68694c30 100644 --- a/src/storm/abstraction/MenuGameAbstractor.cpp +++ b/src/storm/abstraction/MenuGameAbstractor.cpp @@ -4,6 +4,9 @@ #include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/AbstractionSettings.h" + #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" #include "storm/utility/dd.h" @@ -15,6 +18,11 @@ namespace storm { namespace abstraction { + template + MenuGameAbstractor::MenuGameAbstractor() : restrictToRelevantStates(storm::settings::getModule().isRestrictToRelevantStatesSet()) { + // Intentionally left empty. + } + template std::string getStateName(std::pair const& stateValue, std::set const& locationVariables, std::set const& predicateVariables, storm::expressions::Variable const& bottomVariable) { std::stringstream stateName; @@ -45,6 +53,11 @@ namespace storm { return stateName.str(); } + template + bool MenuGameAbstractor::isRestrictToRelevantStatesSet() const { + return restrictToRelevantStates; + } + template void MenuGameAbstractor::exportToDot(storm::abstraction::MenuGame const& currentGame, std::string const& filename, storm::dd::Bdd const& highlightStatesBdd, storm::dd::Bdd const& filter) const { @@ -135,6 +148,21 @@ namespace storm { storm::utility::closeFile(out); } + template + void MenuGameAbstractor::setTargetStates(storm::expressions::Expression const& targetStateExpression) { + this->targetStateExpression = targetStateExpression; + } + + template + storm::expressions::Expression const& MenuGameAbstractor::getTargetStateExpression() const { + return this->targetStateExpression; + } + + template + bool MenuGameAbstractor::hasTargetStateExpression() const { + return this->targetStateExpression.isInitialized(); + } + template class MenuGameAbstractor; template class MenuGameAbstractor; diff --git a/src/storm/abstraction/MenuGameAbstractor.h b/src/storm/abstraction/MenuGameAbstractor.h index 646292106..35fc75c42 100644 --- a/src/storm/abstraction/MenuGameAbstractor.h +++ b/src/storm/abstraction/MenuGameAbstractor.h @@ -24,6 +24,7 @@ namespace storm { template class MenuGameAbstractor { public: + MenuGameAbstractor(); virtual ~MenuGameAbstractor() = default; /// Retrieves the abstraction. @@ -58,8 +59,25 @@ namespace storm { */ virtual void addTerminalStates(storm::expressions::Expression const& expression) = 0; + /*! + * Sets the expression characterizing the target states. For this to work, appropriate predicates must have + * been used to refine the abstraction, otherwise this will fail. + */ + void setTargetStates(storm::expressions::Expression const& targetStateExpression); + + storm::expressions::Expression const& getTargetStateExpression() const; + bool hasTargetStateExpression() const; + protected: + bool isRestrictToRelevantStatesSet() const; + void exportToDot(storm::abstraction::MenuGame const& currentGame, std::string const& filename, storm::dd::Bdd const& highlightStatesBdd, storm::dd::Bdd const& filter) const; + + private: + bool restrictToRelevantStates; + + // An expression characterizing the target states. + storm::expressions::Expression targetStateExpression; }; } diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index 0e63bc0a5..09782e9fd 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -17,6 +17,7 @@ #include "storm/settings/SettingsManager.h" +#include "storm/utility/Stopwatch.h" #include "storm/utility/dd.h" #include "storm/utility/macros.h" #include "storm/utility/solver.h" @@ -154,18 +155,48 @@ namespace storm { auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount()); variablesToAbstract.insert(auxVariables.begin(), auxVariables.end()); - // Compute which states are non-terminal. + storm::utility::Stopwatch relevantStatesWatch(true); storm::dd::Bdd nonTerminalStates = this->abstractionInformation.getDdManager().getBddOne(); - for (auto const& expression : this->terminalStateExpressions) { - nonTerminalStates &= !this->getStates(expression); + if (this->isRestrictToRelevantStatesSet()) { + // Compute which states are non-terminal. + for (auto const& expression : this->terminalStateExpressions) { + nonTerminalStates &= !this->getStates(expression); + } + if (this->hasTargetStateExpression()) { + nonTerminalStates &= !this->getStates(this->getTargetStateExpression()); + } } - + relevantStatesWatch.stop(); + // Do a reachability analysis on the raw transition relation. storm::dd::Bdd transitionRelation = nonTerminalStates && game.bdd.existsAbstract(variablesToAbstract); storm::dd::Bdd initialStates = initialLocationsBdd && initialStateAbstractor.getAbstractStates(); initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables()); storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); + relevantStatesWatch.start(); + if (this->isRestrictToRelevantStatesSet() && this->hasTargetStateExpression()) { + // Cut transition relation to the reachable states for backward search. + transitionRelation &= reachableStates; + + // Get the target state BDD. + storm::dd::Bdd targetStates = reachableStates && this->getStates(this->getTargetStateExpression()); + + // In the presence of target states, we keep only states that can reach the target states. + reachableStates = storm::utility::dd::computeBackwardsReachableStates(targetStates, reachableStates && !initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()) || initialStates; + + // Cut the transition relation to the 'extended backward reachable states', so we have the appropriate self- + // loops of (now) deadlock states. + transitionRelation &= reachableStates; + + // Include all successors of reachable states, because the backward search otherwise potentially + // cuts probability 0 choices of these states. + reachableStates |= reachableStates.relationalProduct(transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); + relevantStatesWatch.stop(); + + STORM_LOG_TRACE("Restricting to relevant states took " << relevantStatesWatch.getTimeInMilliseconds() << "ms."); + } + // Find the deadlock states in the model. Note that this does not find the 'deadlocks' in bottom states, // as the bottom states are not contained in the reachable states. storm::dd::Bdd deadlockStates = transitionRelation.existsAbstract(abstractionInformation.getSuccessorVariables()); @@ -223,7 +254,7 @@ namespace storm { void JaniMenuGameAbstractor::addTerminalStates(storm::expressions::Expression const& expression) { terminalStateExpressions.emplace_back(expression); } - + // Explicitly instantiate the class. template class JaniMenuGameAbstractor; template class JaniMenuGameAbstractor; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index e5f2580b4..9da47fee3 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -15,6 +15,7 @@ #include "storm/settings/SettingsManager.h" +#include "storm/utility/Stopwatch.h" #include "storm/utility/dd.h" #include "storm/utility/macros.h" #include "storm/utility/solver.h" @@ -147,11 +148,18 @@ namespace storm { auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount()); variablesToAbstract.insert(auxVariables.begin(), auxVariables.end()); - // Compute which states are non-terminal. + storm::utility::Stopwatch relevantStatesWatch(true); storm::dd::Bdd nonTerminalStates = this->abstractionInformation.getDdManager().getBddOne(); - for (auto const& expression : this->terminalStateExpressions) { - nonTerminalStates &= !this->getStates(expression); + if (this->isRestrictToRelevantStatesSet()) { + // Compute which states are non-terminal. + for (auto const& expression : this->terminalStateExpressions) { + nonTerminalStates &= !this->getStates(expression); + } + if (this->hasTargetStateExpression()) { + nonTerminalStates &= !this->getStates(this->getTargetStateExpression()); + } } + relevantStatesWatch.stop(); // Do a reachability analysis on the raw transition relation. storm::dd::Bdd transitionRelation = nonTerminalStates && game.bdd.existsAbstract(variablesToAbstract); @@ -159,6 +167,29 @@ namespace storm { initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables()); storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); + relevantStatesWatch.start(); + if (this->isRestrictToRelevantStatesSet() && this->hasTargetStateExpression()) { + // Cut transition relation to the reachable states for backward search. + transitionRelation &= reachableStates; + + // Get the target state BDD. + storm::dd::Bdd targetStates = reachableStates && this->getStates(this->getTargetStateExpression()); + + // In the presence of target states, we keep only states that can reach the target states. + reachableStates = storm::utility::dd::computeBackwardsReachableStates(targetStates, reachableStates && !initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()) || initialStates; + + // Cut the transition relation to the 'extended backward reachable states', so we have the appropriate self- + // loops of (now) deadlock states. + transitionRelation &= reachableStates; + + // Include all successors of reachable states, because the backward search otherwise potentially + // cuts probability 0 choices of these states. + reachableStates |= reachableStates.relationalProduct(transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); + relevantStatesWatch.stop(); + + STORM_LOG_TRACE("Restricting to relevant states took " << relevantStatesWatch.getTimeInMilliseconds() << "ms."); + } + // Find the deadlock states in the model. Note that this does not find the 'deadlocks' in bottom states, // as the bottom states are not contained in the reachable states. storm::dd::Bdd deadlockStates = transitionRelation.existsAbstract(abstractionInformation.getSuccessorVariables()); diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 7a58e4f39..f2cb7a3d2 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -346,6 +346,7 @@ namespace storm { abstractor->addTerminalStates(!constraintExpression); } abstractor->addTerminalStates(targetStateExpression); + abstractor->setTargetStates(targetStateExpression); // Create a refiner that can be used to refine the abstraction when needed. storm::abstraction::MenuGameRefiner refiner(*abstractor, smtSolverFactory->create(preprocessedModel.getManager())); diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index fd384321f..9570810f1 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -21,6 +21,7 @@ namespace storm { const std::string AbstractionSettings::precisionOptionName = "precision"; const std::string AbstractionSettings::pivotHeuristicOptionName = "pivot-heuristic"; const std::string AbstractionSettings::reuseResultsOptionName = "reuse"; + const std::string AbstractionSettings::restrictToRelevantStatesOptionName = "relevant"; AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) { std::vector methods = {"games", "bisimulation", "bisim"}; @@ -64,6 +65,11 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(reuseModes)) .setDefaultValueString("all").build()) .build()); + + this->addOption(storm::settings::OptionBuilder(moduleName, restrictToRelevantStatesOptionName, true, "Sets whether to restrict to relevant states during the abstraction.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff)) + .setDefaultValueString("off").build()) + .build()); } AbstractionSettings::Method AbstractionSettings::getAbstractionRefinementMethod() const { @@ -104,6 +110,10 @@ namespace storm { return this->getOption(useInterpolationOptionName).getArgumentByName("value").getValueAsString() == "on"; } + bool AbstractionSettings::isRestrictToRelevantStatesSet() const { + return this->getOption(restrictToRelevantStatesOptionName).getArgumentByName("value").getValueAsString() == "on"; + } + double AbstractionSettings::getPrecision() const { return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble(); } diff --git a/src/storm/settings/modules/AbstractionSettings.h b/src/storm/settings/modules/AbstractionSettings.h index 4d5827187..7c2a98f66 100644 --- a/src/storm/settings/modules/AbstractionSettings.h +++ b/src/storm/settings/modules/AbstractionSettings.h @@ -93,6 +93,13 @@ namespace storm { */ ReuseMode getReuseMode() const; + /*! + * Retrieves whether only relevant states are to be considered. + * + * @return True iff the option was set. + */ + bool isRestrictToRelevantStatesSet() const; + const static std::string moduleName; private: @@ -104,6 +111,7 @@ namespace storm { const static std::string precisionOptionName; const static std::string pivotHeuristicOptionName; const static std::string reuseResultsOptionName; + const static std::string restrictToRelevantStatesOptionName; }; } diff --git a/src/storm/utility/dd.cpp b/src/storm/utility/dd.cpp index 626dc845f..3ecbef7d6 100644 --- a/src/storm/utility/dd.cpp +++ b/src/storm/utility/dd.cpp @@ -45,6 +45,38 @@ namespace storm { return reachableStates; } + template + storm::dd::Bdd computeBackwardsReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables) { + STORM_LOG_TRACE("Computing backwards reachable states: transition matrix BDD has " << transitions.getNodeCount() << " node(s) and " << transitions.getNonZeroCount() << " non-zero(s), " << initialStates.getNonZeroCount() << " initial states)."); + + auto start = std::chrono::high_resolution_clock::now(); + storm::dd::Bdd reachableStates = initialStates; + + // Perform the BFS to discover all reachable states. + bool changed = true; + uint_fast64_t iteration = 0; + do { + changed = false; + storm::dd::Bdd tmp = reachableStates.inverseRelationalProduct(transitions, rowMetaVariables, columnMetaVariables); + storm::dd::Bdd newReachableStates = tmp && (!reachableStates) && constraintStates; + + // Check whether new states were indeed discovered. + if (!newReachableStates.isZero()) { + changed = true; + } + + reachableStates |= newReachableStates; + + ++iteration; + STORM_LOG_TRACE("Iteration " << iteration << " of (backward) reachability computation completed: " << reachableStates.getNonZeroCount() << " reachable states found."); + } while (changed); + + auto end = std::chrono::high_resolution_clock::now(); + STORM_LOG_TRACE("Backward reachability computation completed in " << iteration << " iterations (" << std::chrono::duration_cast(end - start).count() << "ms)."); + + return reachableStates; + } + template storm::dd::Bdd getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs) { return ddManager.getIdentity(rowColumnMetaVariablePairs, false); @@ -53,6 +85,9 @@ namespace storm { template storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); template storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); + template storm::dd::Bdd computeBackwardsReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); + template storm::dd::Bdd computeBackwardsReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); + template storm::dd::Bdd getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs); template storm::dd::Bdd getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs); diff --git a/src/storm/utility/dd.h b/src/storm/utility/dd.h index 65e079bf3..679e1bd50 100644 --- a/src/storm/utility/dd.h +++ b/src/storm/utility/dd.h @@ -25,7 +25,10 @@ namespace storm { template storm::dd::Bdd computeReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); - + + template + storm::dd::Bdd computeBackwardsReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& constraintStates, storm::dd::Bdd const& transitions, std::set const& rowMetaVariables, std::set const& columnMetaVariables); + template storm::dd::Add getRowColumnDiagonal(storm::dd::DdManager const& ddManager, std::vector> const& rowColumnMetaVariablePairs);