diff --git a/src/storage/prism/menu_games/AbstractCommand.cpp b/src/storage/prism/menu_games/AbstractCommand.cpp index 4e8c2abc2..3acf648ec 100644 --- a/src/storage/prism/menu_games/AbstractCommand.cpp +++ b/src/storage/prism/menu_games/AbstractCommand.cpp @@ -11,13 +11,14 @@ #include "src/storage/prism/Command.h" #include "src/storage/prism/Update.h" +#include "src/utility/solver.h" #include "src/utility/macros.h" namespace storm { namespace prism { namespace menu_games { template - AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.expressionManager)), expressionInformation(expressionInformation), ddInformation(ddInformation), command(command), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), cachedDd(std::make_pair(ddInformation.manager->getBddZero(), 0)), decisionVariables() { + AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.manager)), expressionInformation(expressionInformation), ddInformation(ddInformation), command(command), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), cachedDd(std::make_pair(ddInformation.manager->getBddZero(), 0)), decisionVariables() { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates()); @@ -98,7 +99,7 @@ namespace storm { resultBdd &= computeMissingSourceStateIdentities(); resultBdd &= ddInformation.manager->getEncoding(ddInformation.commandDdVariable, command.get().getGlobalIndex()); - // Cache the result before returning it. + // Cache the result. cachedDd = std::make_pair(resultBdd, numberOfVariablesNeeded); } @@ -158,26 +159,10 @@ namespace storm { return false; } - template - std::vector> AbstractCommand::declareNewVariables(std::vector> const& oldRelevantPredicates, std::set const& newRelevantPredicates) { - std::vector> result; - - auto oldIt = oldRelevantPredicates.begin(); - auto oldIte = oldRelevantPredicates.end(); - for (auto newIt = newRelevantPredicates.begin(), newIte = newRelevantPredicates.end(); newIt != newIte; ++newIt) { - // If the new variable does not yet exist as a source variable, we create it now. - if (oldIt == oldIte || oldIt->second != *newIt) { - result.push_back(std::make_pair(expressionInformation.expressionManager.declareFreshBooleanVariable(), *newIt)); - } - } - - return result; - } - template void AbstractCommand::addMissingPredicates(std::pair, std::vector>> const& newRelevantPredicates) { // Determine and add new relevant source predicates. - std::vector> newSourceVariables = declareNewVariables(relevantPredicatesAndVariables.first, newRelevantPredicates.first); + std::vector> newSourceVariables = AbstractionDdInformation::declareNewVariables(expressionInformation.manager, relevantPredicatesAndVariables.first, newRelevantPredicates.first); for (auto const& element : newSourceVariables) { smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second])); decisionVariables.push_back(element.first); @@ -189,7 +174,7 @@ namespace storm { // Do the same for every update. for (uint_fast64_t index = 0; index < command.get().getNumberOfUpdates(); ++index) { - std::vector> newSuccessorVariables = declareNewVariables(relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]); + std::vector> newSuccessorVariables = AbstractionDdInformation::declareNewVariables(expressionInformation.manager, relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]); for (auto const& element : newSuccessorVariables) { smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second].substitute(command.get().getUpdate(index).getAsVariableToExpressionMap()))); decisionVariables.push_back(element.first); diff --git a/src/storage/prism/menu_games/AbstractCommand.h b/src/storage/prism/menu_games/AbstractCommand.h index 5d8765053..844231edb 100644 --- a/src/storage/prism/menu_games/AbstractCommand.h +++ b/src/storage/prism/menu_games/AbstractCommand.h @@ -12,9 +12,22 @@ #include "src/storage/expressions/Expression.h" #include "src/solver/SmtSolver.h" -#include "src/utility/solver.h" namespace storm { + namespace utility { + namespace solver { + class SmtSolverFactory; + } + } + + namespace dd { + template + class Bdd; + + template + class Add; + } + namespace prism { // Forward-declare concrete command and assignment classes. class Command; @@ -22,9 +35,9 @@ namespace storm { namespace menu_games { template - class AbstractionDdInformation; + struct AbstractionDdInformation; - class AbstractionExpressionInformation; + struct AbstractionExpressionInformation; template class AbstractCommand { @@ -86,15 +99,7 @@ namespace storm { * @param newRelevantPredicates The new relevant predicates. */ bool relevantPredicatesChanged(std::pair, std::vector>> const& newRelevantPredicates) const; - - /*! - * Declares variables for the predicates that were added. - * - * @param oldRelevantPredicates The old relevant predicates (and the corresponding variables). - * @return Pairs of variable and predicate (indices) for the new relevant predicates. - */ - std::vector> declareNewVariables(std::vector> const& oldRelevantPredicates, std::set const& newRelevantPredicates); - + /*! * Takes the new relevant predicates and creates the appropriate variables and assertions for the ones * that are currently missing. diff --git a/src/storage/prism/menu_games/AbstractModule.cpp b/src/storage/prism/menu_games/AbstractModule.cpp index 2a6fde0b2..514af9c2b 100644 --- a/src/storage/prism/menu_games/AbstractModule.cpp +++ b/src/storage/prism/menu_games/AbstractModule.cpp @@ -29,7 +29,7 @@ namespace storm { } template - storm::dd::Bdd AbstractModule::getAbstractBdd() { + std::pair, uint_fast64_t> AbstractModule::getAbstractBdd() { // First, we retrieve the abstractions of all commands. std::vector, uint_fast64_t>> commandDdsAndUsedOptionVariableCounts; uint_fast64_t maximalNumberOfUsedOptionVariables = 0; @@ -44,7 +44,7 @@ namespace storm { for (auto const& commandDd : commandDdsAndUsedOptionVariableCounts) { result |= commandDd.first && ddInformation.getMissingOptionVariableCube(commandDd.second, maximalNumberOfUsedOptionVariables); } - return result; + return std::make_pair(result, maximalNumberOfUsedOptionVariables); } template diff --git a/src/storage/prism/menu_games/AbstractModule.h b/src/storage/prism/menu_games/AbstractModule.h index b345613bf..ee0ad5b74 100644 --- a/src/storage/prism/menu_games/AbstractModule.h +++ b/src/storage/prism/menu_games/AbstractModule.h @@ -16,9 +16,9 @@ namespace storm { namespace menu_games { template - class AbstractionDdInformation; + struct AbstractionDdInformation; - class AbstractionExpressionInformation; + struct AbstractionExpressionInformation; template class AbstractModule { @@ -43,9 +43,9 @@ namespace storm { /*! * Computes the abstraction of the module wrt. to the current set of predicates. * - * @return The abstraction of the module in the form of a BDD. + * @return The abstraction of the module in the form of a BDD together with how many option variables were used. */ - storm::dd::Bdd getAbstractBdd(); + std::pair, uint_fast64_t> getAbstractBdd(); /*! * Retrieves an ADD that maps the encodings of commands and their updates to their probabilities. diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp index 2fe2e593b..a9c0f7aa5 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -14,7 +14,7 @@ namespace storm { namespace menu_games { template - AbstractProgram::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program) { + AbstractProgram::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, *this->smtSolverFactory) { // 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. @@ -59,14 +59,51 @@ namespace storm { modules.emplace_back(module, expressionInformation, ddInformation, *this->smtSolverFactory); } + // Add the initial state expression to the initial state abstractor. + initialStateAbstractor.addPredicate(program.getInitialConstruct().getInitialStatesExpression()); + // Finally, retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later. commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd(); } + template + void AbstractProgram::refine(std::vector const& predicates) { + // 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()); + + // Create a list of indices of the predicates, so we can refine the abstract modules and the state set abstractors. + std::vector newPredicateIndices; + for (uint_fast64_t index = firstNewPredicateIndex; expressionInformation.predicates.size(); ++index) { + newPredicateIndices.push_back(index); + } + + // Refine all abstract modules. + for (auto& module : modules) { + module.refine(newPredicateIndices); + } + + // Refine initial state abstractor. + initialStateAbstractor.refine(newPredicateIndices); + } + template storm::dd::Add AbstractProgram::getAbstractAdd() { - // As long as there is only one module, we build its game representation and return it. - return modules.front().getAbstractBdd().toAdd() * commandUpdateProbabilitiesAdd; + // As long as there is only one module, we only build its game representation. + std::pair, uint_fast64_t> gameBdd = modules.front().getAbstractBdd(); + + // Construct a set of all unnecessary variables, so we can abstract from it. + std::set variablesToAbstract = {ddInformation.commandDdVariable, ddInformation.updateDdVariable}; + for (uint_fast64_t index = 0; index < gameBdd.second; ++index) { + variablesToAbstract.insert(ddInformation.optionDdVariables[index].first); + } + + // Do a reachability analysis on the raw transition relation. + storm::dd::Bdd transitionRelation = gameBdd.first.existsAbstract(variablesToAbstract); + storm::dd::Bdd reachableStates = this->getReachableStates(initialStateAbstractor.getAbstractStates(), transitionRelation); + + // Construct the final game by cutting away the transitions of unreachable states. + return (gameBdd.first && reachableStates).toAdd() * commandUpdateProbabilitiesAdd; } template @@ -74,9 +111,14 @@ namespace storm { storm::dd::Bdd frontier = initialStates; storm::dd::Bdd reachableStates = initialStates; + uint_fast64_t reachabilityIteration = 0; while (!frontier.isZero()) { - frontier = frontier.andExists(transitionRelation, ddInformation.successorVariables); + ++reachabilityIteration; + frontier = frontier.andExists(transitionRelation, ddInformation.sourceVariables); + frontier = frontier.swapVariables(ddInformation.predicateDdVariables); + frontier &= !reachableStates; reachableStates |= frontier; + STORM_LOG_TRACE("Iteration " << reachabilityIteration << " of reachability analysis."); } return reachableStates; diff --git a/src/storage/prism/menu_games/AbstractProgram.h b/src/storage/prism/menu_games/AbstractProgram.h index 801acab62..d9cf6b4ad 100644 --- a/src/storage/prism/menu_games/AbstractProgram.h +++ b/src/storage/prism/menu_games/AbstractProgram.h @@ -5,6 +5,7 @@ #include "src/storage/prism/menu_games/AbstractionDdInformation.h" #include "src/storage/prism/menu_games/AbstractionExpressionInformation.h" +#include "src/storage/prism/menu_games/StateSetAbstractor.h" #include "src/storage/prism/menu_games/AbstractModule.h" #include "src/storage/expressions/Expression.h" @@ -43,6 +44,13 @@ namespace storm { */ storm::dd::Add getAbstractAdd(); + /*! + * Refines the abstract module with the given predicates. + * + * @param predicates The new predicates. + */ + void refine(std::vector const& predicates); + private: /*! * Computes the reachable states of the transition relation. @@ -69,6 +77,9 @@ namespace storm { // The concrete program this abstract program refers to. std::reference_wrapper program; + // A state-set abstractor used to determine the initial states of the abstraction. + StateSetAbstractor initialStateAbstractor; + // An ADD characterizing the probabilities of commands and their updates. storm::dd::Add commandUpdateProbabilitiesAdd; }; diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.cpp b/src/storage/prism/menu_games/AbstractionDdInformation.cpp index 01a673d96..0848ceffb 100644 --- a/src/storage/prism/menu_games/AbstractionDdInformation.cpp +++ b/src/storage/prism/menu_games/AbstractionDdInformation.cpp @@ -2,6 +2,7 @@ #include +#include "src/storage/expressions/ExpressionManager.h" #include "src/storage/expressions/Expression.h" #include "src/storage/dd/CuddDdManager.h" @@ -54,6 +55,22 @@ namespace storm { return result; } + template + std::vector> AbstractionDdInformation::declareNewVariables(storm::expressions::ExpressionManager& manager, std::vector> const& oldRelevantPredicates, std::set const& newRelevantPredicates) { + std::vector> result; + + auto oldIt = oldRelevantPredicates.begin(); + auto oldIte = oldRelevantPredicates.end(); + for (auto newIt = newRelevantPredicates.begin(), newIte = newRelevantPredicates.end(); newIt != newIte; ++newIt) { + // If the new variable does not yet exist as a source variable, we create it now. + if (oldIt == oldIte || oldIt->second != *newIt) { + result.push_back(std::make_pair(manager.declareFreshBooleanVariable(), *newIt)); + } + } + + return result; + } + template struct AbstractionDdInformation; } diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.h b/src/storage/prism/menu_games/AbstractionDdInformation.h index b013589a8..cc20253da 100644 --- a/src/storage/prism/menu_games/AbstractionDdInformation.h +++ b/src/storage/prism/menu_games/AbstractionDdInformation.h @@ -60,6 +60,17 @@ namespace storm { */ storm::dd::Bdd getMissingOptionVariableCube(uint_fast64_t lastUsed, uint_fast64_t lastToBe) const; + /*! + * Examines the old and new relevant predicates and declares decision variables for the missing relevant + * predicates. + * + * @param manager The manager in which to declare the decision variable. + * @param oldRelevantPredicates The previously relevant predicates. + * @param newRelevantPredicates The new relevant predicates. + * @return Pairs of decision variables and their index for the missing predicates. + */ + static std::vector> declareNewVariables(storm::expressions::ExpressionManager& manager, std::vector> const& oldRelevantPredicates, std::set const& newRelevantPredicates); + // The manager responsible for the DDs. std::shared_ptr> manager; diff --git a/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp b/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp index b3b927d70..d82401545 100644 --- a/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp +++ b/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp @@ -7,7 +7,7 @@ namespace storm { namespace prism { namespace menu_games { - AbstractionExpressionInformation::AbstractionExpressionInformation(storm::expressions::ExpressionManager& expressionManager, std::vector const& predicates, std::set const& variables, std::vector const& rangeExpressions) : expressionManager(expressionManager), predicates(predicates), variables(variables), rangeExpressions(rangeExpressions) { + AbstractionExpressionInformation::AbstractionExpressionInformation(storm::expressions::ExpressionManager& manager, std::vector const& predicates, std::set const& variables, std::vector const& rangeExpressions) : manager(manager), predicates(predicates), variables(variables), rangeExpressions(rangeExpressions) { // Intentionally left empty. } diff --git a/src/storage/prism/menu_games/AbstractionExpressionInformation.h b/src/storage/prism/menu_games/AbstractionExpressionInformation.h index 0e03b4d72..b2961b7a1 100644 --- a/src/storage/prism/menu_games/AbstractionExpressionInformation.h +++ b/src/storage/prism/menu_games/AbstractionExpressionInformation.h @@ -19,12 +19,15 @@ namespace storm { /*! * Creates an expression information object with the given expression manager. * - * @param expressionManager The expression manager to use. + * @param manager The expression manager to use. + * @param predicates The initial set of predicates. + * @param variables The variables. + * @param rangeExpressions A set of expressions that enforce the variable bounds. */ - AbstractionExpressionInformation(storm::expressions::ExpressionManager& expressionManager, std::vector const& predicates = std::vector(), std::set const& variables = std::set(), std::vector const& rangeExpressions = std::vector()); + AbstractionExpressionInformation(storm::expressions::ExpressionManager& manager, std::vector const& predicates = std::vector(), std::set const& variables = std::set(), std::vector const& rangeExpressions = std::vector()); // The manager responsible for the expressions of the program and the SMT solvers. - storm::expressions::ExpressionManager& expressionManager; + storm::expressions::ExpressionManager& manager; // The current set of predicates used in the abstraction. std::vector predicates; diff --git a/src/storage/prism/menu_games/StateSetAbstractor.cpp b/src/storage/prism/menu_games/StateSetAbstractor.cpp new file mode 100644 index 000000000..da5219043 --- /dev/null +++ b/src/storage/prism/menu_games/StateSetAbstractor.cpp @@ -0,0 +1,114 @@ +#include "src/storage/prism/menu_games/StateSetAbstractor.h" + +#include "src/storage/prism/menu_games/AbstractionExpressionInformation.h" +#include "src/storage/prism/menu_games/AbstractionDdInformation.h" + +#include "src/storage/dd/CuddDdManager.h" + +#include "src/utility/macros.h" +#include "src/utility/solver.h" + +namespace storm { + namespace prism { + namespace menu_games { + + template + StateSetAbstractor::StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation 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()) { + + // Assert all range expressions to enforce legal variable values. + for (auto const& rangeExpression : expressionInformation.rangeExpressions) { + smtSolver->add(rangeExpression); + } + + // Refine the command based on all initial predicates. + std::vector allPredicateIndices(expressionInformation.predicates.size()); + for (auto index = 0; index < expressionInformation.predicates.size(); ++index) { + allPredicateIndices[index] = index; + } + this->refine(allPredicateIndices); + } + + template + void StateSetAbstractor::addPredicate(storm::expressions::Expression const& predicate) { + smtSolver->add(predicate); + + // Extract the variables of the predicate, so we know which variables were used when abstracting. + std::set usedVariables = predicate.getVariables(); + 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(); + } + + template + void StateSetAbstractor::addMissingPredicates(std::set const& newRelevantPredicateIndices) { + std::vector> newPredicateVariables = AbstractionDdInformation::declareNewVariables(expressionInformation.manager, relevantPredicatesAndVariables, newRelevantPredicateIndices); + + for (auto const& element : newPredicateVariables) { + smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second])); + decisionVariables.push_back(element.first); + } + + relevantPredicatesAndVariables.insert(relevantPredicatesAndVariables.end(), newPredicateVariables.begin(), newPredicateVariables.end()); + std::sort(relevantPredicatesAndVariables.begin(), relevantPredicatesAndVariables.end(), [] (std::pair const& firstPair, std::pair const& secondPair) { return firstPair.second < secondPair.second; } ); + } + + template + void StateSetAbstractor::refine(std::vector 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]); + } + + // Now check whether we need to recompute the cached BDD. + std::set newRelevantPredicateIndices = variablePartition.getRelatedExpressions(concretePredicateVariables); + STORM_LOG_TRACE("Found " << newRelevantPredicateIndices.size() << " relevant predicates in abstractor."); + + // Since the number of relevant predicates is monotonic, we can simply check for the size here. + STORM_LOG_ASSERT(newRelevantPredicateIndices.size() >= relevantPredicatesAndVariables.size(), "Illegal size of relevant predicates."); + bool recomputeDd = newRelevantPredicateIndices.size() > relevantPredicatesAndVariables.size(); + + if (recomputeDd) { + // If we need to recompute the BDD, we start by introducing decision variables and the corresponding + // constraints in the SMT problem. + addMissingPredicates(newRelevantPredicateIndices); + + // Finally recompute the cached BDD. + this->recomputeCachedBdd(); + } + } + + template + storm::dd::Bdd StateSetAbstractor::getStateBdd(storm::solver::SmtSolver::ModelReference const& model) const { + STORM_LOG_TRACE("Building source state BDD."); + storm::dd::Bdd result = ddInformation.manager->getBddOne(); + for (auto const& variableIndexPair : relevantPredicatesAndVariables) { + if (model.getBooleanValue(variableIndexPair.first)) { + result &= ddInformation.predicateBdds[variableIndexPair.second].first; + } else { + result &= !ddInformation.predicateBdds[variableIndexPair.second].first; + } + } + return result; + } + + template + void StateSetAbstractor::recomputeCachedBdd() { + STORM_LOG_TRACE("Recomputing BDD for state set abstraction."); + + storm::dd::Bdd result = ddInformation.manager->getBddZero(); + smtSolver->allSat(decisionVariables, [&result,this] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); return true; } ); + + cachedBdd = result; + } + + template + storm::dd::Bdd StateSetAbstractor::getAbstractStates() const { + return cachedBdd; + } + + template class StateSetAbstractor; + } + } +} diff --git a/src/storage/prism/menu_games/StateSetAbstractor.h b/src/storage/prism/menu_games/StateSetAbstractor.h new file mode 100644 index 000000000..7e5b17178 --- /dev/null +++ b/src/storage/prism/menu_games/StateSetAbstractor.h @@ -0,0 +1,117 @@ +#ifndef STORM_STORAGE_PRISM_MENU_GAMES_STATESETABSTRACTOR_H_ +#define STORM_STORAGE_PRISM_MENU_GAMES_STATESETABSTRACTOR_H_ + +#include +#include + +#include "src/storage/dd/DdType.h" + +#include "src/solver/SmtSolver.h" + +#include "src/storage/prism/menu_games/VariablePartition.h" + +namespace storm { + namespace utility { + namespace solver { + class SmtSolverFactory; + } + } + + namespace dd { + template + class Bdd; + + template + class Add; + } + + namespace prism { + namespace menu_games { + template + class AbstractionDdInformation; + + class AbstractionExpressionInformation; + + template + class StateSetAbstractor { + public: + /*! + * Creates a state set abstractor. + * + * @param expressionInformation The expression-related information including the manager and the predicates. + * @param ddInformation The DD-related information including the manager. + * @param smtSolverFactory A factory that can create new SMT solvers. + */ + StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + + /*! + * Adds the given (concrete) predicate to the abstractor and therefore restricts the abstraction to + * abstract states that contain at least some states satisfying the predicate. + */ + void addPredicate(storm::expressions::Expression const& predicate); + + /*! + * Refines the abstractor by making the given predicates new abstract predicates. + * + * @param newPredicateIndices The indices of the new predicates. + */ + void refine(std::vector const& newPredicateIndices = std::vector()); + + /*! + * Retrieves the set of abstract states matching all predicates added to this abstractor. + * + * @return The set of matching abstract states in the form of a BDD + */ + storm::dd::Bdd getAbstractStates() const; + + private: + /*! + * Creates decision variables and the corresponding constraints for the missing predicates. + * + * @param newRelevantPredicateIndices The set of all relevant predicate indices. + */ + void addMissingPredicates(std::set const& newRelevantPredicateIndices); + + /*! + * Recomputes the cached BDD. This needs to be triggered if any relevant predicates change. + */ + void recomputeCachedBdd(); + + /*! + * Translates the given model to a state DD. + * + * @param model The model to translate. + * @return The state encoded as a DD. + */ + storm::dd::Bdd getStateBdd(storm::solver::SmtSolver::ModelReference const& model) const; + + // The SMT solver used for abstracting the set of states. + std::unique_ptr smtSolver; + + // The expression-related information. + AbstractionExpressionInformation const& expressionInformation; + + // The DD-related information. + AbstractionDdInformation const& ddInformation; + + // The partition of the variables. + VariablePartition variablePartition; + + // The set of relevant predicates and the corresponding decision variables. + std::vector> relevantPredicatesAndVariables; + + // The set of all variables appearing in the concrete predicates. + std::set concretePredicateVariables; + + // The set of all decision variables over which to perform the all-sat enumeration. + std::vector decisionVariables; + + // The cached BDD representing the abstraction. This variable is written to in refinement steps (if work + // needed to be done). + storm::dd::Bdd cachedBdd; + }; + } + } +} + +#endif /* STORM_STORAGE_PRISM_MENU_GAMES_STATESETABSTRACTOR_H_ */ diff --git a/src/storage/prism/menu_games/VariablePartition.cpp b/src/storage/prism/menu_games/VariablePartition.cpp index a8705e599..a5058db1d 100644 --- a/src/storage/prism/menu_games/VariablePartition.cpp +++ b/src/storage/prism/menu_games/VariablePartition.cpp @@ -27,8 +27,13 @@ namespace storm { for (auto const& variable : expressionVariables) { variableToExpressionsMapping[variable].insert(this->expressions.size()); } + + // Add the expression to the block of the first variable. When relating the variables, the blocks will + // get merged (if necessary). + STORM_LOG_ASSERT(!expressionVariables.empty(), "Found no variables in expression."); + expressionBlocks[getBlockIndexOfVariable(*expressionVariables.begin())].insert(this->expressions.size()); - // Add aexpression and relate all the appearing variables. + // Add expression and relate all the appearing variables. this->expressions.push_back(expression); return this->relate(expressionVariables); }