Browse Source

work on game-based abstraction

Former-commit-id: 4635199f84
main
dehnert 10 years ago
parent
commit
b28f36bb34
  1. 11
      src/storage/prism/Module.cpp
  2. 7
      src/storage/prism/Module.h
  3. 22
      src/storage/prism/Program.cpp
  4. 7
      src/storage/prism/Program.h
  5. 33
      src/storage/prism/menu_games/AbstractCommand.cpp
  6. 37
      src/storage/prism/menu_games/AbstractCommand.h
  7. 7
      src/storage/prism/menu_games/AbstractModule.cpp
  8. 14
      src/storage/prism/menu_games/AbstractModule.h
  9. 29
      src/storage/prism/menu_games/AbstractProgram.cpp
  10. 31
      src/storage/prism/menu_games/AbstractProgram.h
  11. 16
      src/storage/prism/menu_games/AbstractionDdInformation.cpp
  12. 49
      src/storage/prism/menu_games/AbstractionDdInformation.h
  13. 16
      src/storage/prism/menu_games/AbstractionExpressionInformation.cpp
  14. 39
      src/storage/prism/menu_games/AbstractionExpressionInformation.h
  15. 12
      src/storage/prism/menu_games/VariablePartition.cpp
  16. 8
      src/storage/prism/menu_games/VariablePartition.h

11
src/storage/prism/Module.cpp

@ -43,6 +43,17 @@ namespace storm {
return this->integerVariables; 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 { std::size_t Module::getNumberOfCommands() const {
return this->commands.size(); return this->commands.size();
} }

7
src/storage/prism/Module.h

@ -97,6 +97,13 @@ namespace storm {
*/ */
std::vector<storm::prism::IntegerVariable> const& getIntegerVariables() const; 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. * Retrieves the number of commands of this module.
* *

22
src/storage/prism/Program.cpp

@ -194,6 +194,26 @@ namespace storm {
std::vector<IntegerVariable> const& Program::getGlobalIntegerVariables() const { std::vector<IntegerVariable> const& Program::getGlobalIntegerVariables() const {
return this->globalIntegerVariables; 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 { bool Program::globalBooleanVariableExists(std::string const& variableName) const {
return this->globalBooleanVariableToIndexMap.count(variableName) > 0; return this->globalBooleanVariableToIndexMap.count(variableName) > 0;
@ -202,8 +222,6 @@ namespace storm {
bool Program::globalIntegerVariableExists(std::string const& variableName) const { bool Program::globalIntegerVariableExists(std::string const& variableName) const {
return this->globalIntegerVariableToIndexMap.count(variableName) > 0; return this->globalIntegerVariableToIndexMap.count(variableName) > 0;
} }
BooleanVariable const& Program::getGlobalBooleanVariable(std::string const& variableName) const { BooleanVariable const& Program::getGlobalBooleanVariable(std::string const& variableName) const {
auto const& nameIndexPair = this->globalBooleanVariableToIndexMap.find(variableName); auto const& nameIndexPair = this->globalBooleanVariableToIndexMap.find(variableName);

7
src/storage/prism/Program.h

@ -166,6 +166,13 @@ namespace storm {
*/ */
IntegerVariable const& getGlobalIntegerVariable(std::string const& variableName) const; 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. * Retrieves the number of global boolean variables of the program.
* *

33
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/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/Command.h"
#include "src/storage/prism/Update.h" #include "src/storage/prism/Update.h"
@ -7,10 +10,38 @@ namespace storm {
namespace prism { namespace prism {
namespace menu_games { namespace menu_games {
template <storm::dd::DdType DdType, typename ValueType> 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. // 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>; template class AbstractCommand<storm::dd::DdType::CUDD, double>;
} }
} }

37
src/storage/prism/menu_games/AbstractCommand.h

@ -2,6 +2,9 @@
#define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTCOMMAND_H_ #define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTCOMMAND_H_
#include <memory> #include <memory>
#include <set>
#include "src/storage/prism/menu_games/VariablePartition.h"
#include "src/storage/dd/DdType.h" #include "src/storage/dd/DdType.h"
#include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Expression.h"
@ -11,35 +14,53 @@
namespace storm { namespace storm {
namespace prism { namespace prism {
// Forward-declare concrete command and update classes. // Forward-declare concrete command and assignment classes.
class Command; class Command;
class Assignment;
namespace menu_games { namespace menu_games {
template <storm::dd::DdType DdType, typename ValueType>
class AbstractionDdInformation;
class AbstractionExpressionInformation;
template <storm::dd::DdType DdType, typename ValueType> template <storm::dd::DdType DdType, typename ValueType>
class AbstractCommand { class AbstractCommand {
public: public:
/*! /*!
* Constructs an abstract command from the given command and the initial predicates. * 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 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. * @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: 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. // An SMT responsible for this abstract command.
std::unique_ptr<storm::solver::SmtSolver> smtSolver; std::unique_ptr<storm::solver::SmtSolver> smtSolver;
// The expression-related information.
AbstractionExpressionInformation const& expressionInformation;
// The current set of predicates used in the abstraction. // The DD-related information.
std::vector<storm::expressions::Expression> predicates; AbstractionDdInformation<DdType, ValueType> const& ddInformation;
// The concrete command this abstract command refers to. // The concrete command this abstract command refers to.
std::reference_wrapper<Command const> command; std::reference_wrapper<Command const> command;
// The partition of variables and expressions.
VariablePartition variablePartition;
}; };
} }
} }

7
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/AbstractModule.h"
#include "src/storage/prism/menu_games/AbstractionExpressionInformation.h"
#include "src/storage/prism/menu_games/AbstractionDdInformation.h"
#include "src/storage/prism/Module.h" #include "src/storage/prism/Module.h"
namespace storm { namespace storm {
@ -7,11 +10,11 @@ namespace storm {
namespace menu_games { namespace menu_games {
template <storm::dd::DdType DdType, typename ValueType> 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 each concrete command, we create an abstract counterpart.
for (auto const& command : module.getCommands()) { for (auto const& command : module.getCommands()) {
commands.emplace_back(expressionManager, command, initialPredicates, smtSolverFactory); commands.emplace_back(command, expressionInformation, ddInformation, smtSolverFactory);
} }
} }

14
src/storage/prism/menu_games/AbstractModule.h

@ -15,23 +15,25 @@ namespace storm {
class Module; class Module;
namespace menu_games { namespace menu_games {
template <storm::dd::DdType DdType, typename ValueType>
class AbstractionDdInformation;
class AbstractionExpressionInformation;
template <storm::dd::DdType DdType, typename ValueType> template <storm::dd::DdType DdType, typename ValueType>
class AbstractModule { class AbstractModule {
public: public:
/*! /*!
* Constructs an abstract module from the given module and the initial predicates. * 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 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. * @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: 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. // A factory that can be used to create new SMT solvers.
storm::utility::solver::SmtSolverFactory const& smtSolverFactory; storm::utility::solver::SmtSolverFactory const& smtSolverFactory;

29
src/storage/prism/menu_games/AbstractProgram.cpp

@ -7,6 +7,7 @@
#include "src/storage/dd/CuddDdManager.h" #include "src/storage/dd/CuddDdManager.h"
#include "src/utility/macros.h" #include "src/utility/macros.h"
#include "src/utility/solver.h"
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
namespace storm { namespace storm {
@ -14,45 +15,53 @@ namespace storm {
namespace menu_games { namespace menu_games {
template <storm::dd::DdType DdType, typename ValueType> 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 // 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. // 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."); 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 totalNumberOfCommands = 0;
uint_fast64_t maximalUpdateCount = 0;
for (auto const& module : program.getModules()) { for (auto const& module : program.getModules()) {
// If we were requested to add all guards to the set of predicates, we do so now. // 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()) {
for (auto const& command : module.getCommands()) { if (addAllGuards) {
predicates.push_back(command.getGuardExpression()); expressionInformation.predicates.push_back(command.getGuardExpression());
} }
maximalUpdateCount = std::max(maximalUpdateCount, static_cast<uint_fast64_t>(command.getNumberOfUpdates()));
} }
totalNumberOfCommands += module.getNumberOfCommands(); totalNumberOfCommands += module.getNumberOfCommands();
} }
// Create DD variables for all predicates. // Create DD variables for all predicates.
for (auto const& predicate : predicates) { for (auto const& predicate : expressionInformation.predicates) {
std::stringstream stream; std::stringstream stream;
stream << predicate; 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. // 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. // 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. // 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 // 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. // that it's impossible to treat such models in any event.
for (uint_fast64_t index = 0; index < 100; ++index) { 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 each module of the concrete program, we create an abstract counterpart.
for (auto const& module : program.getModules()) { for (auto const& module : program.getModules()) {
modules.emplace_back(expressionManager, module, predicates, *smtSolverFactory); modules.emplace_back(module, expressionInformation, ddInformation, *smtSolverFactory);
} }
} }

31
src/storage/prism/menu_games/AbstractProgram.h

@ -3,16 +3,17 @@
#include "src/storage/dd/DdType.h" #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/prism/menu_games/AbstractModule.h"
#include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Expression.h"
#include "src/utility/solver.h"
namespace storm { namespace storm {
namespace dd { namespace utility {
template <storm::dd::DdType DdType> namespace solver {
class DdManager; class SmtSolverFactory;
}
} }
namespace prism { namespace prism {
@ -20,6 +21,7 @@ namespace storm {
class Program; class Program;
namespace menu_games { namespace menu_games {
template <storm::dd::DdType DdType, typename ValueType> template <storm::dd::DdType DdType, typename ValueType>
class AbstractProgram { class AbstractProgram {
public: 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); 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: 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. // A factory that can be used to create new SMT solvers.
std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory; std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
// The current set of predicates used in the abstraction. // A struct containing all DD-related information like variables and managers.
std::vector<storm::expressions::Expression> predicates; AbstractionDdInformation<DdType, ValueType> ddInformation;
// 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;
// The DD variables encoding the nondeterministic choices of player 2. // A struct containing all expression-related information like variables, managers and the predicates.
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> optionDdVariables; AbstractionExpressionInformation expressionInformation;
// The abstract modules of the abstract program. // The abstract modules of the abstract program.
std::vector<AbstractModule<DdType, ValueType>> modules; std::vector<AbstractModule<DdType, ValueType>> modules;

16
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.
}
}
}
}

49
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_ */

16
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.
}
}
}
}

39
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_ */

12
src/storage/prism/menu_games/VariablePartition.cpp

@ -124,6 +124,18 @@ namespace storm {
return this->variableToExpressionsMapping.find(variable)->second; 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 { storm::expressions::Expression const& VariablePartition::getExpression(uint_fast64_t expressionIndex) const {
return this->expressions[expressionIndex]; return this->expressions[expressionIndex];
} }

8
src/storage/prism/menu_games/VariablePartition.h

@ -111,6 +111,14 @@ namespace storm {
* @return The indices of all expressions using the given variable. * @return The indices of all expressions using the given variable.
*/ */
std::set<uint_fast64_t> const& getExpressionsUsingVariable(storm::expressions::Variable const& variable) const; 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. * Retrieves the expression with the given index.

|||||||
100:0
Loading…
Cancel
Save