diff --git a/src/storage/prism/IntegerVariable.cpp b/src/storage/prism/IntegerVariable.cpp index 8ab2f9678..b2306ece0 100644 --- a/src/storage/prism/IntegerVariable.cpp +++ b/src/storage/prism/IntegerVariable.cpp @@ -14,6 +14,10 @@ namespace storm { return this->upperBoundExpression; } + storm::expressions::Expression IntegerVariable::getRangeExpression() const { + return this->getLowerBoundExpression() <= this->getExpressionVariable() && this->getExpressionVariable() <= this->getUpperBoundExpression(); + } + IntegerVariable IntegerVariable::substitute(std::map const& substitution) const { return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); } diff --git a/src/storage/prism/IntegerVariable.h b/src/storage/prism/IntegerVariable.h index 024e1d214..eac97235b 100644 --- a/src/storage/prism/IntegerVariable.h +++ b/src/storage/prism/IntegerVariable.h @@ -45,6 +45,13 @@ namespace storm { */ storm::expressions::Expression const& getUpperBoundExpression() const; + /*! + * Retrieves an expression that characterizes the valid range of the variable. + * + * @return An expression that characterizes the valid range of the variable. + */ + storm::expressions::Expression getRangeExpression() const; + /*! * Substitutes all identifiers in the boolean variable according to the given map. * diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 08c8b6dc6..76eb9ff42 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -54,6 +54,14 @@ namespace storm { return result; } + std::vector Module::getAllRangeExpressions() const { + std::vector result; + for (auto const& integerVariable : this->integerVariables) { + result.push_back(integerVariable.getRangeExpression()); + } + 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 9c22cd7d1..7ea7ee54e 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -104,6 +104,13 @@ namespace storm { */ std::set getAllExpressionVariables() const; + /*! + * Retrieves a set of expressions characterizing the legal ranges of all variables declared in the module. + * + * @return The expressions characterizing the legal ranges of all variables declared in the module. + */ + std::vector getAllRangeExpressions() const; + /*! * Retrieves the number of commands of this module. * diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index a0ce6132a..7d1486501 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -215,6 +215,20 @@ namespace storm { return result; } + std::vector Program::getAllRangeExpressions() const { + std::vector result; + for (auto const& globalIntegerVariable : this->globalIntegerVariables) { + result.push_back(globalIntegerVariable.getRangeExpression()); + } + + for (auto const& module : modules) { + std::vector moduleRangeExpressions = module.getAllRangeExpressions(); + result.insert(result.end(), moduleRangeExpressions.begin(), moduleRangeExpressions.end()); + } + + return result; + } + bool Program::globalBooleanVariableExists(std::string const& variableName) const { return this->globalBooleanVariableToIndexMap.count(variableName) > 0; } diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index de3e18fc9..8185472ee 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -173,6 +173,13 @@ namespace storm { */ std::set getAllExpressionVariables() const; + /*! + * Retrieves a set of expressions characterizing the legal ranges of all variables. + * + * @return The expressions characterizing the legal ranges of all variables. + */ + std::vector getAllRangeExpressions() const; + /*! * Retrieves the number of global boolean variables of the program. * diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp index 4c3432fde..811a4a426 100644 --- a/src/storage/prism/Update.cpp +++ b/src/storage/prism/Update.cpp @@ -31,6 +31,16 @@ namespace storm { return this->getAssignments()[variableIndexPair->second]; } + std::map Update::getAsVariableToExpressionMap() const { + std::map result; + + for (auto const& assignment : this->getAssignments()) { + result.emplace(assignment.getVariable(), assignment.getExpression()); + } + + return result; + } + uint_fast64_t Update::getGlobalIndex() const { return this->globalIndex; } diff --git a/src/storage/prism/Update.h b/src/storage/prism/Update.h index 7b9ebdbc1..69e918cd3 100644 --- a/src/storage/prism/Update.h +++ b/src/storage/prism/Update.h @@ -59,6 +59,13 @@ namespace storm { */ storm::prism::Assignment const& getAssignment(std::string const& variableName) const; + /*! + * Creates a mapping representation of this update. + * + * @return A mapping from variables to expressions. + */ + std::map getAsVariableToExpressionMap() const; + /*! * Retrieves the global index of the update, that is, a unique index over all modules. * @@ -73,6 +80,7 @@ namespace storm { * @return The resulting update. */ Update substitute(std::map const& substitution) const; + /*! * Removes all assignments which do not change the variable. * diff --git a/src/storage/prism/menu_games/AbstractCommand.cpp b/src/storage/prism/menu_games/AbstractCommand.cpp index 52c344a65..7e6263067 100644 --- a/src/storage/prism/menu_games/AbstractCommand.cpp +++ b/src/storage/prism/menu_games/AbstractCommand.cpp @@ -3,6 +3,9 @@ #include "src/storage/prism/menu_games/AbstractionExpressionInformation.h" #include "src/storage/prism/menu_games/AbstractionDdInformation.h" +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddAdd.h" + #include "src/storage/prism/Command.h" #include "src/storage/prism/Update.h" @@ -10,8 +13,15 @@ namespace storm { namespace prism { namespace menu_games { template - AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.expressionManager)), expressionInformation(expressionInformation), ddInformation(ddInformation), command(command) { - // Intentionally left empty. + AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.expressionManager)), expressionInformation(expressionInformation), ddInformation(ddInformation), command(command), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), cachedDd(std::make_pair(ddInformation.ddManager->getAddZero(), 0)) { + + // Make the second component of relevant predicates have the right size. + relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates()); + + // Assert all range expressions to enforce legal variable values. + for (auto const& rangeExpression : expressionInformation.rangeExpressions) { + smtSolver->add(rangeExpression); + } } template @@ -42,6 +52,94 @@ namespace storm { return result; } + template + std::pair, std::vector>> AbstractCommand::computeRelevantPredicates() const { + std::pair, std::vector>> result; + + for (auto const& update : command.get().getUpdates()) { + std::pair, std::set> relevantUpdatePredicates = computeRelevantPredicates(update.getAssignments()); + result.first.insert(relevantUpdatePredicates.first.begin(), relevantUpdatePredicates.first.end()); + result.second.push_back(relevantUpdatePredicates.second); + } + + return result; + } + + template + bool AbstractCommand::relevantPredicatesChanged(std::pair, std::vector>> const& newRelevantPredicates) const { + if (newRelevantPredicates.first.size() > relevantPredicatesAndVariables.first.size()) { + return true; + } + + for (uint_fast64_t index = 0; index < command.get().getNumberOfUpdates(); ++index) { + if (newRelevantPredicates.second[index].size() > relevantPredicatesAndVariables.second[index].size()) { + return true; + } + } + + return false; + } + + template + std::vector> AbstractCommand::declareNewVariables(std::vector> const& oldRelevantPredicates, std::set const& newRelevantPredicates) { + std::vector> result; + + auto oldIt = oldRelevantPredicates.begin(); + auto oldIte = oldRelevantPredicates.end(); + for (auto newIt = newRelevantPredicates.begin(), newIte = newRelevantPredicates.end(); newIt != newIte; ++newIt) { + // If the new variable does not yet exist as a source variable, we create it now. + if (oldIt == oldIte || oldIt->second != *newIt) { + result.push_back(std::make_pair(expressionInformation.expressionManager.declareFreshBooleanVariable(), *newIt)); + } + } + + return result; + } + + template + void AbstractCommand::addMissingPredicates(std::pair, std::vector>> const& newRelevantPredicates) { + // Determine and add new relevant source predicates. + std::vector> newSourceVariables = declareNewVariables(relevantPredicatesAndVariables.first, newRelevantPredicates.first); + for (auto const& element : newSourceVariables) { + smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second])); + } + + // Insert the new variables into the record of relevant source variables. + relevantPredicatesAndVariables.first.insert(relevantPredicatesAndVariables.first.end(), newSourceVariables.begin(), newSourceVariables.end()); + std::sort(relevantPredicatesAndVariables.first.begin(), relevantPredicatesAndVariables.first.end(), [] (std::pair const& first, std::pair const& second) { return first.second < second.second; } ); + + // Do the same for every update. + for (uint_fast64_t index = 0; index < command.get().getNumberOfUpdates(); ++index) { + std::vector> newTargetVariables = declareNewVariables(relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]); + for (auto const& element : newSourceVariables) { + smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second].substitute(command.get().getUpdate(index).getAsVariableToExpressionMap()))); + } + + relevantPredicatesAndVariables.second[index].insert(relevantPredicatesAndVariables.second[index].end(), newTargetVariables.begin(), newTargetVariables.end()); + std::sort(relevantPredicatesAndVariables.second[index].begin(), relevantPredicatesAndVariables.second[index].end(), [] (std::pair const& first, std::pair const& second) { return first.second < second.second; } ); + } + } + + template + std::pair, uint_fast64_t> AbstractCommand::computeDd() { + // First, we check whether there is work to be done by recomputing the relevant predicates and checking + // whether they changed. + std::pair, std::vector>> newRelevantPredicates; + bool recomputeDd = this->relevantPredicatesChanged(newRelevantPredicates); + + if (recomputeDd) { + relevantPredicates = std::move(newRelevantPredicates); + + + + storm::dd::Add result; + + return result; + } else { + return cachedDd; + } + } + template class AbstractCommand; } } diff --git a/src/storage/prism/menu_games/AbstractCommand.h b/src/storage/prism/menu_games/AbstractCommand.h index 1b773f477..eedf28b03 100644 --- a/src/storage/prism/menu_games/AbstractCommand.h +++ b/src/storage/prism/menu_games/AbstractCommand.h @@ -37,9 +37,18 @@ namespace storm { */ AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + /*! + * Computes the abstraction of the command wrt. to the current set of predicates. + * + * @return The abstraction of the command in the form of an ADD together with the number of DD variables + * used to encode the choices of player 2. + */ + std::pair, uint_fast64_t> computeDd(); + private: /*! - * Determines the relevant predicates for source as well as target states. + * Determines the relevant predicates for source as well as target states wrt. to the given assignments + * (that, for example, form an update). * * @param assignments The assignments that are to be considered. * @return A pair whose first component represents the relevant source predicates and whose second @@ -47,6 +56,37 @@ namespace storm { */ std::pair, std::set> computeRelevantPredicates(std::vector const& assignments) const; + /*! + * Determines the relevant predicates for source as well as target states. + * + * @return A pair whose first component represents the relevant source predicates and whose second + * component represents the relevant target state predicates. + */ + std::pair, std::vector>> computeRelevantPredicates() const; + + /*! + * Checks whether the relevant predicates changed. + * + * @param newRelevantPredicates The new relevant predicates. + */ + bool relevantPredicatesChanged(std::pair, std::vector>> const& newRelevantPredicates) const; + + /*! + * Declares variables for the predicates that were added. + * + * @param oldRelevantPredicates The old relevant predicates (and the corresponding variables). + * @return Pairs of variable and predicate (indices) for the new relevant predicates. + */ + std::vector> declareNewVariables(std::vector> const& oldRelevantPredicates, std::set const& newRelevantPredicates); + + /*! + * Takes the new relevant predicates and creates the appropriate variables and assertions for the ones + * that are currently missing. + * + * @param newRelevantPredicates The new relevant predicates. + */ + void addMissingPredicates(std::pair, std::vector>> const& newRelevantPredicates); + // An SMT responsible for this abstract command. std::unique_ptr smtSolver; @@ -61,6 +101,13 @@ namespace storm { // The partition of variables and expressions. VariablePartition variablePartition; + + // The currently relevant source/target predicates and the corresponding variables. + std::pair>, std::vector>>> relevantPredicatesAndVariables; + + // The most recent result of a call to computeDd. If nothing has changed regarding the relevant + // predicates, this result may be reused. + std::pair, uint_fast64_t> cachedDd; }; } } diff --git a/src/storage/prism/menu_games/AbstractModule.cpp b/src/storage/prism/menu_games/AbstractModule.cpp index 860512da7..ae1ddedd6 100644 --- a/src/storage/prism/menu_games/AbstractModule.cpp +++ b/src/storage/prism/menu_games/AbstractModule.cpp @@ -3,6 +3,9 @@ #include "src/storage/prism/menu_games/AbstractionExpressionInformation.h" #include "src/storage/prism/menu_games/AbstractionDdInformation.h" +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddAdd.h" + #include "src/storage/prism/Module.h" namespace storm { @@ -10,7 +13,7 @@ namespace storm { namespace menu_games { template - AbstractModule::AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), commands(), module(module) { + AbstractModule::AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), ddInformation(ddInformation), commands(), module(module) { // For each concrete command, we create an abstract counterpart. for (auto const& command : module.getCommands()) { @@ -18,6 +21,23 @@ namespace storm { } } + template + storm::dd::Add AbstractModule::computeDd() { + // First, we retrieve the abstractions of all commands. + std::vector, uint_fast64_t>> commandDdsAndUsedOptionVariableCounts; + for (auto const& command : commands) { + commandDdsAndUsedOptionVariableCounts.push_back(command.computeDd()); + } + + // Then, we build the module ADD by adding the single command DDs. We need to make sure that all command + // DDs use the same amount DD variable encoding the choices of player 2. + storm::dd::Add result = ddInformation.ddManager->getAddZero(); + + // TODO + + return result; + } + template class AbstractModule; } } diff --git a/src/storage/prism/menu_games/AbstractModule.h b/src/storage/prism/menu_games/AbstractModule.h index fc1e002e8..6114267b7 100644 --- a/src/storage/prism/menu_games/AbstractModule.h +++ b/src/storage/prism/menu_games/AbstractModule.h @@ -33,12 +33,19 @@ namespace storm { */ AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + /*! + * Computes the abstraction of the module wrt. to the current set of predicates. + * + * @return The abstraction of the module in the form of an ADD. + */ + storm::dd::Add computeDd(); + private: // 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 DD-related information. + AbstractionDdInformation const& ddInformation; // The abstract commands of the abstract module. std::vector> commands; diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp index f45a9f8d1..42b09be50 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -5,6 +5,7 @@ #include "src/storage/prism/Program.h" #include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddAdd.h" #include "src/utility/macros.h" #include "src/utility/solver.h" @@ -15,15 +16,12 @@ namespace storm { namespace menu_games { template - AbstractProgram::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared>(new storm::dd::DdManager())), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables()), modules(), program(program) { + AbstractProgram::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector const& initialPredicates, std::unique_ptr&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program) { // 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()) { @@ -65,6 +63,12 @@ namespace storm { } } + template + storm::dd::Add AbstractProgram::computeDd() { + // As long as there is only one module, we build its game representation and return it. + return modules.front().computeDd(); + } + // Explicitly instantiate the class. template class AbstractProgram; diff --git a/src/storage/prism/menu_games/AbstractProgram.h b/src/storage/prism/menu_games/AbstractProgram.h index 1ed11dc16..1c59be4d3 100644 --- a/src/storage/prism/menu_games/AbstractProgram.h +++ b/src/storage/prism/menu_games/AbstractProgram.h @@ -36,8 +36,14 @@ 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: + /*! + * Uses the current set of predicates to derive the abstract menu game in the form of an ADD. + * + * @return The ADD representing the game. + */ + storm::dd::Add computeDd(); + private: // A factory that can be used to create new SMT solvers. std::unique_ptr smtSolverFactory; diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.cpp b/src/storage/prism/menu_games/AbstractionDdInformation.cpp index 105126772..ebb1790b5 100644 --- a/src/storage/prism/menu_games/AbstractionDdInformation.cpp +++ b/src/storage/prism/menu_games/AbstractionDdInformation.cpp @@ -10,6 +10,8 @@ namespace storm { AbstractionDdInformation::AbstractionDdInformation(std::shared_ptr> const& manager) : ddManager(manager) { // Intentionally left empty. } + + template class AbstractionDdInformation; } } diff --git a/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp b/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp index 9530bd96f..b3b927d70 100644 --- a/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp +++ b/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp @@ -7,7 +7,7 @@ namespace storm { namespace prism { namespace menu_games { - AbstractionExpressionInformation::AbstractionExpressionInformation(storm::expressions::ExpressionManager& expressionManager, std::vector const& predicates, std::set const& variables) : expressionManager(expressionManager), predicates(predicates), variables(variables) { + AbstractionExpressionInformation::AbstractionExpressionInformation(storm::expressions::ExpressionManager& expressionManager, std::vector const& predicates, std::set const& variables, std::vector const& rangeExpressions) : expressionManager(expressionManager), predicates(predicates), variables(variables), rangeExpressions(rangeExpressions) { // Intentionally left empty. } diff --git a/src/storage/prism/menu_games/AbstractionExpressionInformation.h b/src/storage/prism/menu_games/AbstractionExpressionInformation.h index d56c6c72d..0e03b4d72 100644 --- a/src/storage/prism/menu_games/AbstractionExpressionInformation.h +++ b/src/storage/prism/menu_games/AbstractionExpressionInformation.h @@ -21,7 +21,7 @@ namespace storm { * * @param expressionManager The expression manager to use. */ - AbstractionExpressionInformation(storm::expressions::ExpressionManager& expressionManager, std::vector const& predicates = std::vector(), std::set const& variables = std::set()); + AbstractionExpressionInformation(storm::expressions::ExpressionManager& expressionManager, std::vector const& predicates = std::vector(), std::set const& variables = std::set(), std::vector const& rangeExpressions = std::vector()); // The manager responsible for the expressions of the program and the SMT solvers. storm::expressions::ExpressionManager& expressionManager; @@ -31,6 +31,9 @@ namespace storm { // The set of all variables. std::set variables; + + // The expression characterizing the legal ranges of all variables. + std::vector rangeExpressions; }; } } diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp new file mode 100644 index 000000000..16027bf3f --- /dev/null +++ b/test/functional/abstraction/PrismMenuGameTest.cpp @@ -0,0 +1,29 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#ifdef STORM_HAVE_MSAT + +#include "src/parser/PrismParser.h" + +#include "src/storage/prism/menu_games/AbstractProgram.h" + +#include "src/storage/expressions/Expression.h" + +#include "src/storage/dd/CuddDd.h" +#include "src/storage/dd/CuddAdd.h" +#include "src/storage/dd/CuddBdd.h" + +#include "src/utility/solver.h" + +TEST(PrismMenuGame, CommandAbstractionTest) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + + std::vector initialPredicates; + storm::expressions::ExpressionManager& manager = program.getManager(); + + initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); + + storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); +} + +#endif \ No newline at end of file