diff --git a/src/storage/prism/menu_games/AbstractCommand.cpp b/src/storage/prism/menu_games/AbstractCommand.cpp index ef5011b6c..4e8c2abc2 100644 --- a/src/storage/prism/menu_games/AbstractCommand.cpp +++ b/src/storage/prism/menu_games/AbstractCommand.cpp @@ -274,6 +274,16 @@ namespace storm { return cachedDd; } + template + storm::dd::Add AbstractCommand::getCommandUpdateProbabilitiesAdd() const { + storm::dd::Add result = ddInformation.manager->getAddZero(); + for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { + result += ddInformation.manager->getEncoding(ddInformation.updateDdVariable, updateIndex).toAdd() * ddInformation.manager->getConstant(command.get().getUpdate(updateIndex).getLikelihoodExpression().evaluateAsDouble()); + } + result *= ddInformation.manager->getEncoding(ddInformation.commandDdVariable, command.get().getGlobalIndex()).toAdd(); + return result; + } + template class AbstractCommand; } } diff --git a/src/storage/prism/menu_games/AbstractCommand.h b/src/storage/prism/menu_games/AbstractCommand.h index 4402bb4bf..5d8765053 100644 --- a/src/storage/prism/menu_games/AbstractCommand.h +++ b/src/storage/prism/menu_games/AbstractCommand.h @@ -54,6 +54,13 @@ namespace storm { */ std::pair, uint_fast64_t> getAbstractBdd(); + /*! + * Retrieves an ADD that maps the encoding of the command and its updates to their probabilities. + * + * @return The command-update probability ADD. + */ + storm::dd::Add getCommandUpdateProbabilitiesAdd() const; + private: /*! * Determines the relevant predicates for source as well as successor states wrt. to the given assignments diff --git a/src/storage/prism/menu_games/AbstractModule.cpp b/src/storage/prism/menu_games/AbstractModule.cpp index 5da411997..2a6fde0b2 100644 --- a/src/storage/prism/menu_games/AbstractModule.cpp +++ b/src/storage/prism/menu_games/AbstractModule.cpp @@ -47,6 +47,15 @@ namespace storm { return result; } + template + storm::dd::Add AbstractModule::getCommandUpdateProbabilitiesAdd() const { + storm::dd::Add result = ddInformation.manager->getAddZero(); + for (auto const& command : commands) { + result += command.getCommandUpdateProbabilitiesAdd(); + } + return result; + } + template class AbstractModule; } } diff --git a/src/storage/prism/menu_games/AbstractModule.h b/src/storage/prism/menu_games/AbstractModule.h index 77101e3d7..b345613bf 100644 --- a/src/storage/prism/menu_games/AbstractModule.h +++ b/src/storage/prism/menu_games/AbstractModule.h @@ -47,6 +47,13 @@ namespace storm { */ storm::dd::Bdd getAbstractBdd(); + /*! + * Retrieves an ADD that maps the encodings of commands and their updates to their probabilities. + * + * @return The command-update probability ADD. + */ + storm::dd::Add getCommandUpdateProbabilitiesAdd() const; + private: // 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 d978ef9b6..2fe2e593b 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -58,15 +58,28 @@ namespace storm { for (auto const& module : program.getModules()) { modules.emplace_back(module, expressionInformation, ddInformation, *this->smtSolverFactory); } + + // Finally, retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later. + commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd(); } template storm::dd::Add AbstractProgram::getAbstractAdd() { // As long as there is only one module, we build its game representation and return it. + return modules.front().getAbstractBdd().toAdd() * commandUpdateProbabilitiesAdd; + } + + template + storm::dd::Bdd AbstractProgram::getReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitionRelation) { + storm::dd::Bdd frontier = initialStates; + + storm::dd::Bdd reachableStates = initialStates; + while (!frontier.isZero()) { + frontier = frontier.andExists(transitionRelation, ddInformation.successorVariables); + reachableStates |= frontier; + } - - // FIXME: multiply with probabilities for updates. - return modules.front().getAbstractBdd().toAdd(); + return reachableStates; } // Explicitly instantiate the class. diff --git a/src/storage/prism/menu_games/AbstractProgram.h b/src/storage/prism/menu_games/AbstractProgram.h index 0da48b672..801acab62 100644 --- a/src/storage/prism/menu_games/AbstractProgram.h +++ b/src/storage/prism/menu_games/AbstractProgram.h @@ -44,6 +44,16 @@ namespace storm { storm::dd::Add getAbstractAdd(); private: + /*! + * Computes the reachable states of the transition relation. + * + * @param initialStates The BDD representing the initial states of the model. + * @param transitionRelation The BDD representing the transition relation that does only contain state + * and successor variables. + * @return The BDD representing the reachable states. + */ + storm::dd::Bdd getReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitionRelation); + // A factory that can be used to create new SMT solvers. std::unique_ptr smtSolverFactory; @@ -58,6 +68,9 @@ namespace storm { // The concrete program this abstract program refers to. std::reference_wrapper program; + + // An ADD characterizing the probabilities of commands and their updates. + storm::dd::Add commandUpdateProbabilitiesAdd; }; } } diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.cpp b/src/storage/prism/menu_games/AbstractionDdInformation.cpp index 7946115fb..01a673d96 100644 --- a/src/storage/prism/menu_games/AbstractionDdInformation.cpp +++ b/src/storage/prism/menu_games/AbstractionDdInformation.cpp @@ -39,6 +39,8 @@ namespace storm { predicateDdVariables.push_back(newMetaVariable); predicateBdds.emplace_back(manager->getEncoding(newMetaVariable.first, 1), manager->getEncoding(newMetaVariable.second, 1)); predicateIdentities.push_back(manager->getIdentity(newMetaVariable.first).equals(manager->getIdentity(newMetaVariable.second)).toBdd()); + sourceVariables.insert(newMetaVariable.first); + successorVariables.insert(newMetaVariable.second); } template diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.h b/src/storage/prism/menu_games/AbstractionDdInformation.h index b0b239107..b013589a8 100644 --- a/src/storage/prism/menu_games/AbstractionDdInformation.h +++ b/src/storage/prism/menu_games/AbstractionDdInformation.h @@ -3,6 +3,7 @@ #include #include +#include #include "src/storage/dd/DdType.h" #include "src/storage/expressions/Variable.h" @@ -64,6 +65,12 @@ namespace storm { // The DD variables corresponding to the predicates. std::vector> predicateDdVariables; + + // The set of all source variables. + std::set sourceVariables; + + // The set of all source variables. + std::set successorVariables; // The BDDs corresponding to the predicates. std::vector, storm::dd::Bdd>> predicateBdds;