From b28f36bb347ba69ca8ee720d304e9fc830bcdb75 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 11 Sep 2015 18:54:02 +0200 Subject: [PATCH] work on game-based abstraction Former-commit-id: 4635199f84146d2f97f0e395c956948ef38f8e3e --- src/storage/prism/Module.cpp | 11 +++++ src/storage/prism/Module.h | 7 +++ src/storage/prism/Program.cpp | 22 ++++++++- src/storage/prism/Program.h | 7 +++ .../prism/menu_games/AbstractCommand.cpp | 33 ++++++++++++- .../prism/menu_games/AbstractCommand.h | 37 +++++++++++--- .../prism/menu_games/AbstractModule.cpp | 7 ++- src/storage/prism/menu_games/AbstractModule.h | 14 +++--- .../prism/menu_games/AbstractProgram.cpp | 29 +++++++---- .../prism/menu_games/AbstractProgram.h | 31 +++++------- .../menu_games/AbstractionDdInformation.cpp | 16 ++++++ .../menu_games/AbstractionDdInformation.h | 49 +++++++++++++++++++ .../AbstractionExpressionInformation.cpp | 16 ++++++ .../AbstractionExpressionInformation.h | 39 +++++++++++++++ .../prism/menu_games/VariablePartition.cpp | 12 +++++ .../prism/menu_games/VariablePartition.h | 8 +++ 16 files changed, 289 insertions(+), 49 deletions(-) create mode 100644 src/storage/prism/menu_games/AbstractionDdInformation.cpp create mode 100644 src/storage/prism/menu_games/AbstractionDdInformation.h create mode 100644 src/storage/prism/menu_games/AbstractionExpressionInformation.cpp create mode 100644 src/storage/prism/menu_games/AbstractionExpressionInformation.h diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 47d44269a..08c8b6dc6 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -43,6 +43,17 @@ namespace storm { return this->integerVariables; } + std::set Module::getAllExpressionVariables() const { + std::set result; + for (auto const& var : this->getBooleanVariables()) { + result.insert(var.getExpressionVariable()); + } + for (auto const& var : this->getIntegerVariables()) { + result.insert(var.getExpressionVariable()); + } + return result; + } + std::size_t Module::getNumberOfCommands() const { return this->commands.size(); } diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h index bb8c3b8d4..9c22cd7d1 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -97,6 +97,13 @@ namespace storm { */ std::vector const& getIntegerVariables() const; + /*! + * Retrieves the set of all expression variables declared in this module. + * + * @return The set of all expression variables. + */ + std::set getAllExpressionVariables() const; + /*! * Retrieves the number of commands of this module. * diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 9ac73881e..a0ce6132a 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -194,6 +194,26 @@ namespace storm { std::vector const& Program::getGlobalIntegerVariables() const { return this->globalIntegerVariables; } + + std::set Program::getAllExpressionVariables() const { + std::set result; + + for (auto const& constant : constants) { + result.insert(constant.getExpressionVariable()); + } + for (auto const& variable : globalBooleanVariables) { + result.insert(variable.getExpressionVariable()); + } + for (auto const& variable : globalIntegerVariables) { + result.insert(variable.getExpressionVariable()); + } + for (auto const& module : modules) { + auto const& moduleVariables = module.getAllExpressionVariables(); + result.insert(moduleVariables.begin(), moduleVariables.end()); + } + + return result; + } bool Program::globalBooleanVariableExists(std::string const& variableName) const { return this->globalBooleanVariableToIndexMap.count(variableName) > 0; @@ -202,8 +222,6 @@ namespace storm { bool Program::globalIntegerVariableExists(std::string const& variableName) const { return this->globalIntegerVariableToIndexMap.count(variableName) > 0; } - - BooleanVariable const& Program::getGlobalBooleanVariable(std::string const& variableName) const { auto const& nameIndexPair = this->globalBooleanVariableToIndexMap.find(variableName); diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index f2b13781d..de3e18fc9 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -166,6 +166,13 @@ namespace storm { */ IntegerVariable const& getGlobalIntegerVariable(std::string const& variableName) const; + /*! + * Retrieves the set of all expression variables declared in this module. + * + * @return The set of all expression variables. + */ + std::set getAllExpressionVariables() const; + /*! * Retrieves the number of global boolean variables of the program. * diff --git a/src/storage/prism/menu_games/AbstractCommand.cpp b/src/storage/prism/menu_games/AbstractCommand.cpp index 558d1e77c..52c344a65 100644 --- a/src/storage/prism/menu_games/AbstractCommand.cpp +++ b/src/storage/prism/menu_games/AbstractCommand.cpp @@ -1,5 +1,8 @@ #include "src/storage/prism/menu_games/AbstractCommand.h" +#include "src/storage/prism/menu_games/AbstractionExpressionInformation.h" +#include "src/storage/prism/menu_games/AbstractionDdInformation.h" + #include "src/storage/prism/Command.h" #include "src/storage/prism/Update.h" @@ -7,10 +10,38 @@ namespace storm { namespace prism { namespace menu_games { template - AbstractCommand::AbstractCommand(storm::expressions::ExpressionManager& expressionManager, storm::prism::Command const& command, std::vector const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : expressionManager(expressionManager), smtSolver(smtSolverFactory.create(expressionManager)), predicates(initialPredicates), command(command) { + 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) { // Intentionally left empty. } + template + std::pair, std::set> AbstractCommand::computeRelevantPredicates(std::vector const& assignments) const { + std::pair, std::set> result; + + // To start with, all predicates related to the guard are relevant source predicates. + result.first = variablePartition.getExpressionsUsingVariables(command.get().getGuardExpression().getVariables()); + + std::set assignedVariables; + for (auto const& assignment : assignments) { + // Also, variables appearing on the right-hand side of an assignment are relevant for source state. + auto const& rightHandSidePredicates = variablePartition.getExpressionsUsingVariables(assignment.getExpression().getVariables()); + result.first.insert(rightHandSidePredicates.begin(), rightHandSidePredicates.end()); + + // Variables that are being assigned are relevant for the target state. + storm::expressions::Variable const& assignedVariable = assignment.getVariable(); + auto const& leftHandSidePredicates = variablePartition.getExpressionsUsingVariable(assignedVariable); + result.second.insert(leftHandSidePredicates.begin(), leftHandSidePredicates.end()); + + // Keep track of all assigned variables, so we can find the related predicates later. + assignedVariables.insert(assignedVariable); + } + + auto const& predicatesRelatedToAssignedVariable = variablePartition.getRelatedExpressions(assignedVariables); + result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end()); + + return result; + } + template class AbstractCommand; } } diff --git a/src/storage/prism/menu_games/AbstractCommand.h b/src/storage/prism/menu_games/AbstractCommand.h index a380bc4f6..1b773f477 100644 --- a/src/storage/prism/menu_games/AbstractCommand.h +++ b/src/storage/prism/menu_games/AbstractCommand.h @@ -2,6 +2,9 @@ #define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTCOMMAND_H_ #include +#include + +#include "src/storage/prism/menu_games/VariablePartition.h" #include "src/storage/dd/DdType.h" #include "src/storage/expressions/Expression.h" @@ -11,35 +14,53 @@ namespace storm { namespace prism { - // Forward-declare concrete command and update classes. + // Forward-declare concrete command and assignment classes. class Command; + class Assignment; namespace menu_games { + template + class AbstractionDdInformation; + + class AbstractionExpressionInformation; + template class AbstractCommand { public: /*! * Constructs an abstract command from the given command and the initial predicates. * - * @param expressionManager The manager responsible for the expressions of the command. * @param command The concrete command for which to build the abstraction. - * @param initialPredicates The initial set of predicates. + * @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 is to be used for creating new SMT solvers. */ - AbstractCommand(storm::expressions::ExpressionManager& expressionManager, storm::prism::Command const& command, std::vector const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); private: - // The manager responsible for the expressions of the command and the SMT solvers. - storm::expressions::ExpressionManager& expressionManager; + /*! + * Determines the relevant predicates for source as well as target states. + * + * @param assignments The assignments that are to be considered. + * @return A pair whose first component represents the relevant source predicates and whose second + * component represents the relevant target state predicates. + */ + std::pair, std::set> computeRelevantPredicates(std::vector const& assignments) const; // An SMT responsible for this abstract command. std::unique_ptr smtSolver; + + // The expression-related information. + AbstractionExpressionInformation const& expressionInformation; - // The current set of predicates used in the abstraction. - std::vector predicates; + // The DD-related information. + AbstractionDdInformation const& ddInformation; // The concrete command this abstract command refers to. std::reference_wrapper command; + + // The partition of variables and expressions. + VariablePartition variablePartition; }; } } diff --git a/src/storage/prism/menu_games/AbstractModule.cpp b/src/storage/prism/menu_games/AbstractModule.cpp index 8252d450c..860512da7 100644 --- a/src/storage/prism/menu_games/AbstractModule.cpp +++ b/src/storage/prism/menu_games/AbstractModule.cpp @@ -1,5 +1,8 @@ #include "src/storage/prism/menu_games/AbstractModule.h" +#include "src/storage/prism/menu_games/AbstractionExpressionInformation.h" +#include "src/storage/prism/menu_games/AbstractionDdInformation.h" + #include "src/storage/prism/Module.h" namespace storm { @@ -7,11 +10,11 @@ namespace storm { namespace menu_games { template - AbstractModule::AbstractModule(storm::expressions::ExpressionManager& expressionManager, storm::prism::Module const& module, std::vector const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : expressionManager(expressionManager), smtSolverFactory(smtSolverFactory), predicates(initialPredicates), commands(), module(module) { + AbstractModule::AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), commands(), module(module) { // For each concrete command, we create an abstract counterpart. for (auto const& command : module.getCommands()) { - commands.emplace_back(expressionManager, command, initialPredicates, smtSolverFactory); + commands.emplace_back(command, expressionInformation, ddInformation, smtSolverFactory); } } diff --git a/src/storage/prism/menu_games/AbstractModule.h b/src/storage/prism/menu_games/AbstractModule.h index 3d292203d..fc1e002e8 100644 --- a/src/storage/prism/menu_games/AbstractModule.h +++ b/src/storage/prism/menu_games/AbstractModule.h @@ -15,23 +15,25 @@ namespace storm { class Module; namespace menu_games { + template + class AbstractionDdInformation; + + class AbstractionExpressionInformation; + template class AbstractModule { public: /*! * Constructs an abstract module from the given module and the initial predicates. * - * @param expressionManager The manager responsible for the expressions of the command. * @param module The concrete module for which to build the abstraction. - * @param initialPredicates The initial set of predicates. + * @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 is to be used for creating new SMT solvers. */ - AbstractModule(storm::expressions::ExpressionManager& expressionManager, storm::prism::Module const& module, std::vector const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); private: - // The manager responsible for the expressions of the module and the SMT solvers. - storm::expressions::ExpressionManager& expressionManager; - // A factory that can be used to create new SMT solvers. storm::utility::solver::SmtSolverFactory const& smtSolverFactory; diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp index 801805054..f45a9f8d1 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -7,6 +7,7 @@ #include "src/storage/dd/CuddDdManager.h" #include "src/utility/macros.h" +#include "src/utility/solver.h" #include "src/exceptions/WrongFormatException.h" namespace storm { @@ -14,45 +15,53 @@ 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) : expressionManager(expressionManager), smtSolverFactory(std::move(smtSolverFactory)), predicates(initialPredicates), ddManager(new storm::dd::DdManager()), predicateDdVariables(), commandDdVariable(), optionDdVariables(), 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>(new storm::dd::DdManager())), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables()), modules(), program(program) { // 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. STORM_LOG_THROW(program.getNumberOfModules() == 1, storm::exceptions::WrongFormatException, "Cannot create abstract program from program containing too many modules."); + std::set allVariables; + + uint_fast64_t totalNumberOfCommands = 0; + uint_fast64_t maximalUpdateCount = 0; for (auto const& module : program.getModules()) { // If we were requested to add all guards to the set of predicates, we do so now. - if (addAllGuards) { - for (auto const& command : module.getCommands()) { - predicates.push_back(command.getGuardExpression()); + for (auto const& command : module.getCommands()) { + if (addAllGuards) { + expressionInformation.predicates.push_back(command.getGuardExpression()); } + maximalUpdateCount = std::max(maximalUpdateCount, static_cast(command.getNumberOfUpdates())); } - + totalNumberOfCommands += module.getNumberOfCommands(); } // Create DD variables for all predicates. - for (auto const& predicate : predicates) { + for (auto const& predicate : expressionInformation.predicates) { std::stringstream stream; stream << predicate; - predicateDdVariables.push_back(ddManager->addMetaVariable(stream.str())); + ddInformation.predicateDdVariables.push_back(ddInformation.ddManager->addMetaVariable(stream.str())); } // Create DD variable for the command encoding. - commandDdVariable = ddManager->addMetaVariable("command", 0, totalNumberOfCommands - 1); + ddInformation.commandDdVariable = ddInformation.ddManager->addMetaVariable("command", 0, totalNumberOfCommands - 1).first; + + // Create DD variable for update encoding. + ddInformation.updateDdVariable = ddInformation.ddManager->addMetaVariable("update", 0, maximalUpdateCount - 1).first; // Create DD variables encoding the nondeterministic choices of player 2. // NOTE: currently we assume that 100 variables suffice, which corresponds to 2^100 possible choices. // If for some reason this should not be enough, we could grow this vector dynamically, but odds are // that it's impossible to treat such models in any event. for (uint_fast64_t index = 0; index < 100; ++index) { - optionDdVariables.push_back(ddManager->addMetaVariable("opt" + std::to_string(index))); + ddInformation.optionDdVariables.push_back(ddInformation.ddManager->addMetaVariable("opt" + std::to_string(index)).first); } // For each module of the concrete program, we create an abstract counterpart. for (auto const& module : program.getModules()) { - modules.emplace_back(expressionManager, module, predicates, *smtSolverFactory); + modules.emplace_back(module, expressionInformation, ddInformation, *smtSolverFactory); } } diff --git a/src/storage/prism/menu_games/AbstractProgram.h b/src/storage/prism/menu_games/AbstractProgram.h index e00f4e8f1..1ed11dc16 100644 --- a/src/storage/prism/menu_games/AbstractProgram.h +++ b/src/storage/prism/menu_games/AbstractProgram.h @@ -3,16 +3,17 @@ #include "src/storage/dd/DdType.h" +#include "src/storage/prism/menu_games/AbstractionDdInformation.h" +#include "src/storage/prism/menu_games/AbstractionExpressionInformation.h" #include "src/storage/prism/menu_games/AbstractModule.h" #include "src/storage/expressions/Expression.h" -#include "src/utility/solver.h" - namespace storm { - namespace dd { - template - class DdManager; + namespace utility { + namespace solver { + class SmtSolverFactory; + } } namespace prism { @@ -20,6 +21,7 @@ namespace storm { class Program; namespace menu_games { + template class AbstractProgram { public: @@ -35,26 +37,15 @@ namespace storm { AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory = std::unique_ptr(new storm::utility::solver::SmtSolverFactory()), bool addAllGuards = false); private: - // The manager responsible for the expressions of the program and the SMT solvers. - storm::expressions::ExpressionManager& expressionManager; // A factory that can be used to create new SMT solvers. std::unique_ptr smtSolverFactory; - // The current set of predicates used in the abstraction. - std::vector predicates; - - // The manager responsible for the DDs. - std::shared_ptr> ddManager; - - // The DD variables corresponding to the predicates. - std::vector> predicateDdVariables; - - // The DD variable encoding the command (i.e., the nondeterministic choices of player 1). - std::pair commandDdVariable; + // A struct containing all DD-related information like variables and managers. + AbstractionDdInformation ddInformation; - // The DD variables encoding the nondeterministic choices of player 2. - std::vector> optionDdVariables; + // A struct containing all expression-related information like variables, managers and the predicates. + AbstractionExpressionInformation expressionInformation; // The abstract modules of the abstract program. std::vector> modules; diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.cpp b/src/storage/prism/menu_games/AbstractionDdInformation.cpp new file mode 100644 index 000000000..105126772 --- /dev/null +++ b/src/storage/prism/menu_games/AbstractionDdInformation.cpp @@ -0,0 +1,16 @@ +#include "src/storage/prism/menu_games/AbstractionDdInformation.h" + +#include "src/storage/dd/DdManager.h" + +namespace storm { + namespace prism { + namespace menu_games { + + template + AbstractionDdInformation::AbstractionDdInformation(std::shared_ptr> const& manager) : ddManager(manager) { + // Intentionally left empty. + } + + } + } +} \ No newline at end of file diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.h b/src/storage/prism/menu_games/AbstractionDdInformation.h new file mode 100644 index 000000000..9944c7e00 --- /dev/null +++ b/src/storage/prism/menu_games/AbstractionDdInformation.h @@ -0,0 +1,49 @@ +#ifndef STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTIONDDINFORMATION_H_ +#define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTIONDDINFORMATION_H_ + +#include +#include + +#include "src/storage/dd/DdType.h" +#include "src/storage/expressions/Variable.h" + +namespace storm { + namespace dd { + template + class DdManager; + } + + namespace prism { + namespace menu_games { + + template + struct AbstractionDdInformation { + public: + /*! + * Creates a new DdInformation that uses the given manager. + * + * @param manager The manager to use. + */ + AbstractionDdInformation(std::shared_ptr> const& manager); + + // The manager responsible for the DDs. + std::shared_ptr> ddManager; + + // The DD variables corresponding to the predicates. + std::vector> predicateDdVariables; + + // The DD variable encoding the command (i.e., the nondeterministic choices of player 1). + storm::expressions::Variable commandDdVariable; + + // The DD variable encoding the update IDs for all actions. + storm::expressions::Variable updateDdVariable; + + // The DD variables encoding the nondeterministic choices of player 2. + std::vector optionDdVariables; + }; + + } + } +} + +#endif /* STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTIONDDINFORMATION_H_ */ diff --git a/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp b/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp new file mode 100644 index 000000000..9530bd96f --- /dev/null +++ b/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp @@ -0,0 +1,16 @@ +#include "src/storage/prism/menu_games/AbstractionExpressionInformation.h" + +#include "src/storage/expressions/ExpressionManager.h" +#include "src/storage/expressions/Expression.h" + +namespace storm { + namespace prism { + namespace menu_games { + + AbstractionExpressionInformation::AbstractionExpressionInformation(storm::expressions::ExpressionManager& expressionManager, std::vector const& predicates, std::set const& variables) : expressionManager(expressionManager), predicates(predicates), variables(variables) { + // Intentionally left empty. + } + + } + } +} \ No newline at end of file diff --git a/src/storage/prism/menu_games/AbstractionExpressionInformation.h b/src/storage/prism/menu_games/AbstractionExpressionInformation.h new file mode 100644 index 000000000..d56c6c72d --- /dev/null +++ b/src/storage/prism/menu_games/AbstractionExpressionInformation.h @@ -0,0 +1,39 @@ +#ifndef STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTIONEXPRESSIONINFORMATION_H_ +#define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTIONEXPRESSIONINFORMATION_H_ + +#include +#include + +namespace storm { + namespace expressions { + class ExpressionManager; + class Expression; + class Variable; + } + + namespace prism { + namespace menu_games { + + struct AbstractionExpressionInformation { + public: + /*! + * Creates an expression information object with the given expression manager. + * + * @param expressionManager The expression manager to use. + */ + AbstractionExpressionInformation(storm::expressions::ExpressionManager& expressionManager, std::vector const& predicates = std::vector(), std::set const& variables = std::set()); + + // The manager responsible for the expressions of the program and the SMT solvers. + storm::expressions::ExpressionManager& expressionManager; + + // The current set of predicates used in the abstraction. + std::vector predicates; + + // The set of all variables. + std::set variables; + }; + } + } +} + +#endif /* STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTIONEXPRESSIONINFORMATION_H_ */ \ No newline at end of file diff --git a/src/storage/prism/menu_games/VariablePartition.cpp b/src/storage/prism/menu_games/VariablePartition.cpp index 53c0d2a61..92738dfb8 100644 --- a/src/storage/prism/menu_games/VariablePartition.cpp +++ b/src/storage/prism/menu_games/VariablePartition.cpp @@ -124,6 +124,18 @@ namespace storm { return this->variableToExpressionsMapping.find(variable)->second; } + std::set VariablePartition::getExpressionsUsingVariables(std::set const& variables) const { + std::set result; + + for (auto const& variable : variables) { + STORM_LOG_ASSERT(this->relevantVariables.find(variable) != this->relevantVariables.end(), "Illegal variable '" << variable.getName() << "' for partition."); + auto it = this->variableToExpressionsMapping.find(variable); + result.insert(it->second.begin(), it->second.end()); + } + + return result; + } + storm::expressions::Expression const& VariablePartition::getExpression(uint_fast64_t expressionIndex) const { return this->expressions[expressionIndex]; } diff --git a/src/storage/prism/menu_games/VariablePartition.h b/src/storage/prism/menu_games/VariablePartition.h index 46651fe8f..ae6637943 100644 --- a/src/storage/prism/menu_games/VariablePartition.h +++ b/src/storage/prism/menu_games/VariablePartition.h @@ -111,6 +111,14 @@ namespace storm { * @return The indices of all expressions using the given variable. */ std::set const& getExpressionsUsingVariable(storm::expressions::Variable const& variable) const; + + /*! + * Retrieves the indices of the expressions in which the given variables appear. + * + * @param variables The variables for which to retrieve the expressions. + * @return The indices of all expressions using the given variables. + */ + std::set getExpressionsUsingVariables(std::set const& variables) const; /*! * Retrieves the expression with the given index.