diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.cpp b/src/storm/abstraction/jani/AutomatonAbstractor.cpp index 21481f00c..5d399fc56 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.cpp +++ b/src/storm/abstraction/jani/AutomatonAbstractor.cpp @@ -24,12 +24,12 @@ namespace storm { using storm::settings::modules::AbstractionSettings; template - AutomatonAbstractor::AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), edges(), automaton(automaton) { + AutomatonAbstractor::AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool addPredicatesForValidBlocks, bool debug) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), edges(), automaton(automaton) { // For each concrete command, we create an abstract counterpart. uint64_t edgeId = 0; for (auto const& edge : automaton.getEdges()) { - edges.emplace_back(edgeId, edge, abstractionInformation, smtSolverFactory, useDecomposition, debug); + edges.emplace_back(edgeId, edge, abstractionInformation, smtSolverFactory, useDecomposition, addPredicatesForValidBlocks, debug); ++edgeId; } diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.h b/src/storm/abstraction/jani/AutomatonAbstractor.h index 3053de3c4..9b58ba9c1 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.h +++ b/src/storm/abstraction/jani/AutomatonAbstractor.h @@ -35,7 +35,7 @@ namespace storm { * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param useDecomposition A flag indicating whether to use the decomposition during abstraction. */ - AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug); + AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool addPredicatesForValidBlocks, bool debug); AutomatonAbstractor(AutomatonAbstractor const&) = default; AutomatonAbstractor& operator=(AutomatonAbstractor const&) = default; diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp index 950221dcd..ee52cae71 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.cpp +++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp @@ -23,7 +23,7 @@ namespace storm { namespace abstraction { namespace jani { template - EdgeAbstractor::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), edgeId(edgeId), edge(edge), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!edge.getGuard()}, smtSolverFactory), debug(debug) { + EdgeAbstractor::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool addPredicatesForValidBlocks, bool debug) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), edgeId(edgeId), edge(edge), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), addPredicatesForValidBlocks(addPredicatesForValidBlocks), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!edge.getGuard()}, smtSolverFactory), debug(debug) { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(edge.getNumberOfDestinations()); @@ -43,6 +43,11 @@ namespace storm { assignedVariables.insert(assignment.getExpressionVariable()); } } + + // Log whether or not predicates are added to ensure valid blocks. + if (this->addPredicatesForValidBlocks) { + STORM_LOG_DEBUG("Adding more predicates to ensure valid blocks."); + } } template @@ -489,6 +494,12 @@ namespace storm { storm::expressions::Variable const& assignedVariable = assignment.getExpressionVariable(); auto const& leftHandSidePredicates = localExpressionInformation.getExpressionsUsingVariable(assignedVariable); result.second.insert(leftHandSidePredicates.begin(), leftHandSidePredicates.end()); + + // Predicates that are indirectly related to the assigned variables are relevant for the source state (if requested). + if (this->addPredicatesForValidBlocks) { + auto const& assignedVariableBlock = localExpressionInformation.getRelatedExpressions(assignedVariable); + result.first.insert(assignedVariableBlock.begin(), assignedVariableBlock.end()); + } } return result; diff --git a/src/storm/abstraction/jani/EdgeAbstractor.h b/src/storm/abstraction/jani/EdgeAbstractor.h index 3c8c1d21b..8c02e8b76 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.h +++ b/src/storm/abstraction/jani/EdgeAbstractor.h @@ -58,7 +58,7 @@ namespace storm { * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param useDecomposition A flag indicating whether to use an edge decomposition during abstraction. */ - EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug); + EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool addPredicatesForValidBlocks, bool debug); /*! * Refines the abstract edge with the given predicates. @@ -246,6 +246,9 @@ namespace storm { // A flag indicating whether to use the decomposition when abstracting. bool useDecomposition; + + // Whether or not to add predicates indirectly related to assignment variables to relevant source predicates. + bool addPredicatesForValidBlocks; // A flag indicating whether the computation of bottom states can be skipped (for example, if the bottom // states become empty at some point). diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index a71d78f04..991870ede 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -35,7 +35,7 @@ namespace storm { using storm::settings::modules::AbstractionSettings; template - JaniMenuGameAbstractor::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr const& smtSolverFactory, MenuGameAbstractorOptions const& options) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager()), AbstractionInformationOptions(options.constraints)), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(true) { + JaniMenuGameAbstractor::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr const& smtSolverFactory, MenuGameAbstractorOptions const& options) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager()), AbstractionInformationOptions(options.constraints)), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), restrictToValidBlocks(false), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(true) { // Check whether the model is linear as the abstraction requires this. STORM_LOG_WARN_COND(model.isLinear(), "The model appears to contain non-linear expressions, which may cause malfunctioning of the abstraction."); @@ -70,9 +70,11 @@ namespace storm { // For each module of the concrete program, we create an abstract counterpart. auto const& settings = storm::settings::getModule(); bool useDecomposition = settings.isUseDecompositionSet(); + restrictToValidBlocks = settings.getValidBlockMode() == storm::settings::modules::AbstractionSettings::ValidBlockMode::BlockEnumeration; + bool addPredicatesForValidBlocks = !restrictToValidBlocks; bool debug = settings.isDebugSet(); for (auto const& automaton : model.getAutomata()) { - automata.emplace_back(automaton, abstractionInformation, this->smtSolverFactory, useDecomposition, debug); + automata.emplace_back(automaton, abstractionInformation, this->smtSolverFactory, useDecomposition, addPredicatesForValidBlocks, debug); } // Retrieve global BDDs/ADDs so we can multiply them in the abstraction process. @@ -97,8 +99,10 @@ namespace storm { // Refine initial state abstractor. initialStateAbstractor.refine(predicateIndices); - // Refine the valid blocks. - validBlockAbstractor.refine(predicateIndices); + if (this->restrictToValidBlocks) { + // Refine the valid blocks. + validBlockAbstractor.refine(predicateIndices); + } refinementPerformed |= !command.getPredicates().empty(); } @@ -183,15 +187,22 @@ namespace storm { } relevantStatesWatch.stop(); - storm::dd::Bdd validBlocks = validBlockAbstractor.getValidBlocks(); + storm::dd::Bdd extendedTransitionRelation = nonTerminalStates && game.bdd; + storm::dd::Bdd initialStates = initialLocationsBdd && initialStateAbstractor.getAbstractStates(); + if (this->restrictToValidBlocks) { + STORM_LOG_DEBUG("Restricting to valid blocks."); + storm::dd::Bdd validBlocks = validBlockAbstractor.getValidBlocks(); - // Compute the choices with only valid successors so we can restrict the game to these. - auto choicesWithOnlyValidSuccessors = !game.bdd.andExists(!validBlocks.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs()), successorAndAuxVariables) && game.bdd.existsAbstract(successorAndAuxVariables); + // Compute the choices with only valid successors so we can restrict the game to these. + auto choicesWithOnlyValidSuccessors = !game.bdd.andExists(!validBlocks.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs()), successorAndAuxVariables) && game.bdd.existsAbstract(successorAndAuxVariables); + + // Restrict the proper parts. + extendedTransitionRelation &= validBlocks && choicesWithOnlyValidSuccessors; + initialStates &= validBlocks; + } // Do a reachability analysis on the raw transition relation. - storm::dd::Bdd extendedTransitionRelation = validBlocks && nonTerminalStates && game.bdd && choicesWithOnlyValidSuccessors; storm::dd::Bdd transitionRelation = extendedTransitionRelation.existsAbstract(variablesToAbstract); - storm::dd::Bdd initialStates = initialLocationsBdd && initialStateAbstractor.getAbstractStates() && validBlocks; initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables()); storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h index d9f04f828..2017b2c17 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.h +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.h @@ -159,6 +159,9 @@ namespace storm { // A state-set abstractor used to determine the initial states of the abstraction. StateSetAbstractor initialStateAbstractor; + // A flag indicating whether the valid blocks need to be computed and the game restricted to these. + bool restrictToValidBlocks; + // An object that is used to compute the valid blocks. ValidBlockAbstractor validBlockAbstractor; diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index a57c990c7..ecb415655 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -13,9 +13,6 @@ #include "storm/storage/prism/Command.h" #include "storm/storage/prism/Update.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/AbstractionSettings.h" - #include "storm/utility/solver.h" #include "storm/utility/macros.h" @@ -26,7 +23,7 @@ namespace storm { namespace abstraction { namespace prism { template - CommandAbstractor::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), addAssignmentRelatedVariablesToSourcePredicates(false), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!command.getGuardExpression()}, smtSolverFactory), debug(debug) { + CommandAbstractor::CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool addPredicatesForValidBlocks, bool debug) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), useDecomposition(useDecomposition), addPredicatesForValidBlocks(addPredicatesForValidBlocks), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!command.getGuardExpression()}, smtSolverFactory), debug(debug) { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates()); @@ -47,8 +44,10 @@ namespace storm { } } - auto const& abstractionSettings = storm::settings::getModule(); - addAssignmentRelatedVariablesToSourcePredicates = abstractionSettings.getValidBlockMode() == storm::settings::modules::AbstractionSettings::ValidBlockMode::MorePredicates; + // Log whether or not predicates are added to ensure valid blocks. + if (this->addPredicatesForValidBlocks) { + STORM_LOG_DEBUG("Adding more predicates to ensure valid blocks."); + } } template @@ -497,7 +496,7 @@ namespace storm { result.second.insert(leftHandSidePredicates.begin(), leftHandSidePredicates.end()); // Predicates that are indirectly related to the assigned variables are relevant for the source state (if requested). - if (this->addAssignmentRelatedVariablesToSourcePredicates) { + if (this->addPredicatesForValidBlocks) { auto const& assignedVariableBlock = localExpressionInformation.getRelatedExpressions(assignedVariable); result.first.insert(assignedVariableBlock.begin(), assignedVariableBlock.end()); } diff --git a/src/storm/abstraction/prism/CommandAbstractor.h b/src/storm/abstraction/prism/CommandAbstractor.h index f37abbdb5..e6f8f6a6f 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.h +++ b/src/storm/abstraction/prism/CommandAbstractor.h @@ -56,7 +56,7 @@ namespace storm { * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param useDecomposition A flag indicating whether to use the decomposition during abstraction. */ - CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug); + CommandAbstractor(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool addPredicatesForValidBlocks, bool debug); /*! * Refines the abstract command with the given predicates. @@ -248,7 +248,7 @@ namespace storm { bool useDecomposition; // Whether or not to add predicates indirectly related to assignment variables to relevant source predicates. - bool addAssignmentRelatedVariablesToSourcePredicates; + bool addPredicatesForValidBlocks; // A flag indicating whether the guard of the command was added as a predicate. If this is true, there // is no need to compute bottom states. diff --git a/src/storm/abstraction/prism/ModuleAbstractor.cpp b/src/storm/abstraction/prism/ModuleAbstractor.cpp index ab031eeab..f17d47df3 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.cpp +++ b/src/storm/abstraction/prism/ModuleAbstractor.cpp @@ -23,11 +23,11 @@ namespace storm { using storm::settings::modules::AbstractionSettings; template - ModuleAbstractor::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) { + ModuleAbstractor::ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool addPredicatesForValidBlocks, bool debug) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) { // For each concrete command, we create an abstract counterpart. for (auto const& command : module.getCommands()) { - commands.emplace_back(command, abstractionInformation, smtSolverFactory, useDecomposition, debug); + commands.emplace_back(command, abstractionInformation, smtSolverFactory, useDecomposition, addPredicatesForValidBlocks, debug); } } diff --git a/src/storm/abstraction/prism/ModuleAbstractor.h b/src/storm/abstraction/prism/ModuleAbstractor.h index 9771347c6..72a7bb492 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.h +++ b/src/storm/abstraction/prism/ModuleAbstractor.h @@ -38,7 +38,7 @@ namespace storm { * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. * @param useDecomposition A flag that governs whether to use the decomposition in the abstraction. */ - ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool debug); + ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool useDecomposition, bool addPredicatesForValidBlocks, bool debug); ModuleAbstractor(ModuleAbstractor const&) = default; ModuleAbstractor& operator=(ModuleAbstractor const&) = default; diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 4db02a199..9e018ce3e 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -67,9 +67,10 @@ namespace storm { auto const& settings = storm::settings::getModule(); bool useDecomposition = settings.isUseDecompositionSet(); restrictToValidBlocks = settings.getValidBlockMode() == storm::settings::modules::AbstractionSettings::ValidBlockMode::BlockEnumeration; + bool addPredicatesForValidBlocks = !restrictToValidBlocks; bool debug = settings.isDebugSet(); for (auto const& module : program.getModules()) { - this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, useDecomposition, debug); + this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, useDecomposition, addPredicatesForValidBlocks, debug); } // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later. @@ -181,6 +182,7 @@ namespace storm { storm::dd::Bdd extendedTransitionRelation = nonTerminalStates && game.bdd; storm::dd::Bdd initialStates = initialStateAbstractor.getAbstractStates(); if (restrictToValidBlocks) { + STORM_LOG_DEBUG("Restricting to valid blocks."); storm::dd::Bdd validBlocks = validBlockAbstractor.getValidBlocks(); // Compute the choices with only valid successors so we can restrict the game to these.