From d4ed882795ecc824c04f0357d10a8c6990ecddba Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 10 Sep 2015 16:36:18 +0200 Subject: [PATCH] more work on menu-game abstraction PRISM programs Former-commit-id: acc54b7f159e1c15fd801eec05c7a254e83b5b80 --- src/CMakeLists.txt | 4 +- src/adapters/Z3ExpressionAdapter.h | 2 + .../prism/menu_games/AbstractCommand.cpp | 17 +++++ .../prism/menu_games/AbstractCommand.h | 48 +++++++++++++ .../prism/menu_games/AbstractModule.cpp | 21 ++++++ src/storage/prism/menu_games/AbstractModule.h | 51 ++++++++++++++ .../prism/menu_games/AbstractProgram.cpp | 64 +++++++++++++++++ .../prism/menu_games/AbstractProgram.h | 69 +++++++++++++++++++ .../prism/menu_games/VariablePartition.cpp | 0 .../prism/menu_games/VariablePartition.h | 0 10 files changed, 275 insertions(+), 1 deletion(-) create mode 100644 src/storage/prism/menu_games/AbstractCommand.cpp create mode 100644 src/storage/prism/menu_games/AbstractCommand.h create mode 100644 src/storage/prism/menu_games/AbstractModule.cpp create mode 100644 src/storage/prism/menu_games/AbstractModule.h create mode 100644 src/storage/prism/menu_games/AbstractProgram.cpp create mode 100644 src/storage/prism/menu_games/AbstractProgram.h create mode 100644 src/storage/prism/menu_games/VariablePartition.cpp create mode 100644 src/storage/prism/menu_games/VariablePartition.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 454fe8262..5671ce4c6 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -35,7 +35,8 @@ file(GLOB_RECURSE STORM_SOLVER_FILES ${PROJECT_SOURCE_DIR}/src/solver/*.h ${PROJ file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp) file(GLOB_RECURSE STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp) file(GLOB_RECURSE STORM_STORAGE_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.h ${PROJECT_SOURCE_DIR}/src/storage/expressions/*.cpp) -file(GLOB_RECURSE STORM_STORAGE_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/*.cpp) +file(GLOB STORM_STORAGE_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/*.cpp) +file(GLOB STORM_STORAGE_PRISM_MENU_GAME_FILES ${PROJECT_SOURCE_DIR}/src/storage/prism/menu_games/*.h ${PROJECT_SOURCE_DIR}/src/storage/prism/menu_games/*.cpp) file(GLOB_RECURSE STORM_STORAGE_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.h ${PROJECT_SOURCE_DIR}/src/storage/sparse/*.cpp) file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp) @@ -80,6 +81,7 @@ source_group(storage FILES ${STORM_STORAGE_FILES}) source_group(storage\\dd FILES ${STORM_STORAGE_DD_FILES}) source_group(storage\\expressions FILES ${STORM_STORAGE_EXPRESSIONS_FILES}) source_group(storage\\prism FILES ${STORM_STORAGE_PRISM_FILES}) +source_group(storage\\prism\\menu_games FILES ${STORM_STORAGE_PRISM_MENU_GAME_FILES}) source_group(storage\\sparse FILES ${STORM_STORAGE_SPARSE_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES}) diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 4fc60c8a5..7ab8de742 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -47,6 +47,7 @@ namespace storm { z3::expr translateExpression(storm::expressions::Variable const& variable); storm::expressions::Expression translateExpression(z3::expr const& expr); + /*! * Finds the counterpart to the given z3 variable declaration. * @@ -82,6 +83,7 @@ namespace storm { * @param variable The variable for which to create a Z3 counterpart. */ z3::expr createVariable(storm::expressions::Variable const& variable); + // The manager that can be used to build expressions. storm::expressions::ExpressionManager& manager; diff --git a/src/storage/prism/menu_games/AbstractCommand.cpp b/src/storage/prism/menu_games/AbstractCommand.cpp new file mode 100644 index 000000000..558d1e77c --- /dev/null +++ b/src/storage/prism/menu_games/AbstractCommand.cpp @@ -0,0 +1,17 @@ +#include "src/storage/prism/menu_games/AbstractCommand.h" + +#include "src/storage/prism/Command.h" +#include "src/storage/prism/Update.h" + +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) { + // Intentionally left empty. + } + + template class AbstractCommand; + } + } +} \ No newline at end of file diff --git a/src/storage/prism/menu_games/AbstractCommand.h b/src/storage/prism/menu_games/AbstractCommand.h new file mode 100644 index 000000000..a380bc4f6 --- /dev/null +++ b/src/storage/prism/menu_games/AbstractCommand.h @@ -0,0 +1,48 @@ +#ifndef STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTCOMMAND_H_ +#define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTCOMMAND_H_ + +#include + +#include "src/storage/dd/DdType.h" +#include "src/storage/expressions/Expression.h" + +#include "src/solver/SmtSolver.h" +#include "src/utility/solver.h" + +namespace storm { + namespace prism { + // Forward-declare concrete command and update classes. + class Command; + + namespace menu_games { + 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 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); + + private: + // The manager responsible for the expressions of the command and the SMT solvers. + storm::expressions::ExpressionManager& expressionManager; + + // An SMT responsible for this abstract command. + std::unique_ptr smtSolver; + + // The current set of predicates used in the abstraction. + std::vector predicates; + + // The concrete command this abstract command refers to. + std::reference_wrapper command; + }; + } + } +} + +#endif /* STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTCOMMAND_H_ */ \ No newline at end of file diff --git a/src/storage/prism/menu_games/AbstractModule.cpp b/src/storage/prism/menu_games/AbstractModule.cpp new file mode 100644 index 000000000..8252d450c --- /dev/null +++ b/src/storage/prism/menu_games/AbstractModule.cpp @@ -0,0 +1,21 @@ +#include "src/storage/prism/menu_games/AbstractModule.h" + +#include "src/storage/prism/Module.h" + +namespace storm { + namespace prism { + 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) { + + // For each concrete command, we create an abstract counterpart. + for (auto const& command : module.getCommands()) { + commands.emplace_back(expressionManager, command, initialPredicates, smtSolverFactory); + } + } + + template class AbstractModule; + } + } +} \ No newline at end of file diff --git a/src/storage/prism/menu_games/AbstractModule.h b/src/storage/prism/menu_games/AbstractModule.h new file mode 100644 index 000000000..3d292203d --- /dev/null +++ b/src/storage/prism/menu_games/AbstractModule.h @@ -0,0 +1,51 @@ +#ifndef STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTMODULE_H_ +#define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTMODULE_H_ + +#include "src/storage/dd/DdType.h" + +#include "src/storage/prism/menu_games/AbstractCommand.h" + +#include "src/storage/expressions/Expression.h" + +#include "src/utility/solver.h" + +namespace storm { + namespace prism { + // Forward-declare concrete module class. + class Module; + + namespace menu_games { + 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 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); + + 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; + + // The current set of predicates used in the abstraction. + std::vector predicates; + + // The abstract commands of the abstract module. + std::vector> commands; + + // The concrete module this abstract module refers to. + std::reference_wrapper module; + }; + } + } +} + +#endif /* STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTMODULE_H_ */ \ No newline at end of file diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp new file mode 100644 index 000000000..801805054 --- /dev/null +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -0,0 +1,64 @@ +#include "src/storage/prism/menu_games/AbstractProgram.h" + +#include + +#include "src/storage/prism/Program.h" + +#include "src/storage/dd/CuddDdManager.h" + +#include "src/utility/macros.h" +#include "src/exceptions/WrongFormatException.h" + +namespace storm { + namespace prism { + 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) { + + // 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."); + + uint_fast64_t totalNumberOfCommands = 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()); + } + } + + totalNumberOfCommands += module.getNumberOfCommands(); + } + + // Create DD variables for all predicates. + for (auto const& predicate : predicates) { + std::stringstream stream; + stream << predicate; + predicateDdVariables.push_back(ddManager->addMetaVariable(stream.str())); + } + + // Create DD variable for the command encoding. + commandDdVariable = ddManager->addMetaVariable("command", 0, totalNumberOfCommands - 1); + + // 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))); + } + + // 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); + } + } + + // Explicitly instantiate the class. + template class AbstractProgram; + + } + } +} \ No newline at end of file diff --git a/src/storage/prism/menu_games/AbstractProgram.h b/src/storage/prism/menu_games/AbstractProgram.h new file mode 100644 index 000000000..e00f4e8f1 --- /dev/null +++ b/src/storage/prism/menu_games/AbstractProgram.h @@ -0,0 +1,69 @@ +#ifndef STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTPROGRAM_H_ +#define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTPROGRAM_H_ + +#include "src/storage/dd/DdType.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 prism { + // Forward-declare concrete Program class. + class Program; + + namespace menu_games { + template + class AbstractProgram { + public: + /*! + * Constructs an abstract program from the given program and the initial predicates. + * + * @param expressionManager The manager responsible for the expressions of the program. + * @param program The concrete program for which to build the abstraction. + * @param initialPredicates The initial set of predicates. + * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. + * @param addAllGuards A flag that indicates whether all guards of the program should be added to the initial set of predicates. + */ + 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; + + // The DD variables encoding the nondeterministic choices of player 2. + std::vector> optionDdVariables; + + // The abstract modules of the abstract program. + std::vector> modules; + + // The concrete program this abstract program refers to. + std::reference_wrapper program; + }; + } + } +} + +#endif /* STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTPROGRAM_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 new file mode 100644 index 000000000..e69de29bb diff --git a/src/storage/prism/menu_games/VariablePartition.h b/src/storage/prism/menu_games/VariablePartition.h new file mode 100644 index 000000000..e69de29bb