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<storm::expressions::Variable> Module::getAllExpressionVariables() const {
+ std::set<storm::expressions::Variable> 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<storm::prism::IntegerVariable> const& getIntegerVariables() const;
+ /*!
+ * Retrieves the set of all expression variables declared in this module.
+ *
+ * @return The set of all expression variables.
+ */
+ std::set<storm::expressions::Variable> 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<IntegerVariable> const& Program::getGlobalIntegerVariables() const {
return this->globalIntegerVariables;
}
+
+ std::set<storm::expressions::Variable> Program::getAllExpressionVariables() const {
+ std::set<storm::expressions::Variable> 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<storm::expressions::Variable> 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 <storm::dd::DdType DdType, typename ValueType>
- AbstractCommand<DdType, ValueType>::AbstractCommand(storm::expressions::ExpressionManager& expressionManager, storm::prism::Command const& command, std::vector<storm::expressions::Expression> const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : expressionManager(expressionManager), smtSolver(smtSolverFactory.create(expressionManager)), predicates(initialPredicates), command(command) {
+ AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.expressionManager)), expressionInformation(expressionInformation), ddInformation(ddInformation), command(command) {
// Intentionally left empty.
}
+ template <storm::dd::DdType DdType, typename ValueType>
+ std::pair<std::set<uint_fast64_t>, std::set<uint_fast64_t>> AbstractCommand<DdType, ValueType>::computeRelevantPredicates(std::vector<storm::prism::Assignment> const& assignments) const {
+ std::pair<std::set<uint_fast64_t>, std::set<uint_fast64_t>> result;
+
+ // To start with, all predicates related to the guard are relevant source predicates.
+ result.first = variablePartition.getExpressionsUsingVariables(command.get().getGuardExpression().getVariables());
+
+ std::set<storm::expressions::Variable> 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<storm::dd::DdType::CUDD, double>;
}
}
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 <memory>
+#include <set>
+
+#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 <storm::dd::DdType DdType, typename ValueType>
+ class AbstractionDdInformation;
+
+ class AbstractionExpressionInformation;
+
template <storm::dd::DdType DdType, typename ValueType>
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<storm::expressions::Expression> const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
+ AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> 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<uint_fast64_t>, std::set<uint_fast64_t>> computeRelevantPredicates(std::vector<storm::prism::Assignment> const& assignments) const;
// An SMT responsible for this abstract command.
std::unique_ptr<storm::solver::SmtSolver> smtSolver;
+
+ // The expression-related information.
+ AbstractionExpressionInformation const& expressionInformation;
- // The current set of predicates used in the abstraction.
- std::vector<storm::expressions::Expression> predicates;
+ // The DD-related information.
+ AbstractionDdInformation<DdType, ValueType> const& ddInformation;
// The concrete command this abstract command refers to.
std::reference_wrapper<Command const> 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 <storm::dd::DdType DdType, typename ValueType>
- AbstractModule<DdType, ValueType>::AbstractModule(storm::expressions::ExpressionManager& expressionManager, storm::prism::Module const& module, std::vector<storm::expressions::Expression> const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : expressionManager(expressionManager), smtSolverFactory(smtSolverFactory), predicates(initialPredicates), commands(), module(module) {
+ AbstractModule<DdType, ValueType>::AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> 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 <storm::dd::DdType DdType, typename ValueType>
+ class AbstractionDdInformation;
+
+ class AbstractionExpressionInformation;
+
template <storm::dd::DdType DdType, typename ValueType>
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<storm::expressions::Expression> const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
+ AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> 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 <storm::dd::DdType DdType, typename ValueType>
- AbstractProgram<DdType, ValueType>::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory, bool addAllGuards) : expressionManager(expressionManager), smtSolverFactory(std::move(smtSolverFactory)), predicates(initialPredicates), ddManager(new storm::dd::DdManager<DdType>()), predicateDdVariables(), commandDdVariable(), optionDdVariables(), modules(), program(program) {
+ AbstractProgram<DdType, ValueType>::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared<storm::dd::DdManager<DdType>>(new storm::dd::DdManager<DdType>())), 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<storm::expressions::Variable> 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<uint_fast64_t>(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 <storm::dd::DdType DdType>
- class DdManager;
+ namespace utility {
+ namespace solver {
+ class SmtSolverFactory;
+ }
}
namespace prism {
@@ -20,6 +21,7 @@ namespace storm {
class Program;
namespace menu_games {
+
template <storm::dd::DdType DdType, typename ValueType>
class AbstractProgram {
public:
@@ -35,26 +37,15 @@ namespace storm {
AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory = std::unique_ptr<storm::utility::solver::SmtSolverFactory>(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<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
- // The current set of predicates used in the abstraction.
- std::vector<storm::expressions::Expression> predicates;
-
- // The manager responsible for the DDs.
- std::shared_ptr<storm::dd::DdManager<DdType>> ddManager;
-
- // The DD variables corresponding to the predicates.
- std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> predicateDdVariables;
-
- // The DD variable encoding the command (i.e., the nondeterministic choices of player 1).
- std::pair<storm::expressions::Variable, storm::expressions::Variable> commandDdVariable;
+ // A struct containing all DD-related information like variables and managers.
+ AbstractionDdInformation<DdType, ValueType> ddInformation;
- // The DD variables encoding the nondeterministic choices of player 2.
- std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> 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<AbstractModule<DdType, ValueType>> 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 <storm::dd::DdType DdType, typename ValueType>
+ AbstractionDdInformation<DdType, ValueType>::AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> 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 <memory>
+#include <vector>
+
+#include "src/storage/dd/DdType.h"
+#include "src/storage/expressions/Variable.h"
+
+namespace storm {
+ namespace dd {
+ template <storm::dd::DdType DdType>
+ class DdManager;
+ }
+
+ namespace prism {
+ namespace menu_games {
+
+ template <storm::dd::DdType DdType, typename ValueType>
+ struct AbstractionDdInformation {
+ public:
+ /*!
+ * Creates a new DdInformation that uses the given manager.
+ *
+ * @param manager The manager to use.
+ */
+ AbstractionDdInformation(std::shared_ptr<storm::dd::DdManager<DdType>> const& manager);
+
+ // The manager responsible for the DDs.
+ std::shared_ptr<storm::dd::DdManager<DdType>> ddManager;
+
+ // The DD variables corresponding to the predicates.
+ std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> 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<storm::expressions::Variable> 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<storm::expressions::Expression> const& predicates, std::set<storm::expressions::Variable> 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 <vector>
+#include <set>
+
+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<storm::expressions::Expression> const& predicates = std::vector<storm::expressions::Expression>(), std::set<storm::expressions::Variable> const& variables = std::set<storm::expressions::Variable>());
+
+ // 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<storm::expressions::Expression> predicates;
+
+ // The set of all variables.
+ std::set<storm::expressions::Variable> 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<uint_fast64_t> VariablePartition::getExpressionsUsingVariables(std::set<storm::expressions::Variable> const& variables) const {
+ std::set<uint_fast64_t> 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<uint_fast64_t> 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<uint_fast64_t> getExpressionsUsingVariables(std::set<storm::expressions::Variable> const& variables) const;
/*!
* Retrieves the expression with the given index.