From 1198951c3efa19db8a3098ddf086d0d80ca2b7e7 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 15 Sep 2015 14:10:23 +0200 Subject: [PATCH] more work on game abstraction of PRISM programs Former-commit-id: b5bec829e2a1fabb7dfc5f2fc78a6d54a0faeb57 --- src/storage/dd/CuddAdd.h | 14 +++ src/storage/dd/CuddBdd.h | 18 ++- .../prism/menu_games/AbstractCommand.cpp | 110 +++++++++++++++--- .../prism/menu_games/AbstractCommand.h | 37 ++++-- .../prism/menu_games/AbstractModule.cpp | 8 +- src/storage/prism/menu_games/AbstractModule.h | 4 +- .../prism/menu_games/AbstractProgram.cpp | 16 ++- .../menu_games/AbstractionDdInformation.cpp | 36 +++++- .../menu_games/AbstractionDdInformation.h | 34 +++++- 9 files changed, 231 insertions(+), 46 deletions(-) diff --git a/src/storage/dd/CuddAdd.h b/src/storage/dd/CuddAdd.h index acdc3d5e1..b7d9fbfcb 100644 --- a/src/storage/dd/CuddAdd.h +++ b/src/storage/dd/CuddAdd.h @@ -2,6 +2,7 @@ #define STORM_STORAGE_DD_CUDDADD_H_ #include +#include #include #include "src/storage/dd/Add.h" @@ -35,6 +36,8 @@ namespace storm { friend class Bdd; friend class Odd; + // Declare the hashing struct for DDs as a friend so it can access the internal DD pointer. + friend struct std::hash>; /*! * Creates an ADD from the given explicit vector. * @@ -825,4 +828,15 @@ namespace storm { } } +namespace std { + template <> struct hash> + { + size_t operator()(storm::dd::Add const& dd) const { + std::size_t seed = 0; + boost::hash_combine(seed, dd.getCuddAdd().getNode()); + return seed; + } + }; +} + #endif /* STORM_STORAGE_DD_CUDDADD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/CuddBdd.h b/src/storage/dd/CuddBdd.h index 3ce4f9d89..d9af17483 100644 --- a/src/storage/dd/CuddBdd.h +++ b/src/storage/dd/CuddBdd.h @@ -1,6 +1,8 @@ #ifndef STORM_STORAGE_DD_CUDDBDD_H_ #define STORM_STORAGE_DD_CUDDBDD_H_ +#include + #include "src/storage/dd/Bdd.h" #include "src/storage/dd/CuddDd.h" #include "src/utility/OsDetection.h" @@ -21,8 +23,6 @@ namespace storm { class BitVector; } - - namespace dd { // Forward-declare some classes. template class DdManager; @@ -51,6 +51,9 @@ namespace storm { friend class Add; friend class Odd; + // Declare the hashing struct for DDs as a friend so it can access the internal DD pointer. + friend struct std::hash>; + // Instantiate all copy/move constructors/assignments with the default implementation. Bdd() = default; Bdd(Bdd const& other) = default; @@ -357,4 +360,15 @@ namespace storm { } } +namespace std { + template <> struct hash> + { + size_t operator()(storm::dd::Bdd const& dd) const { + std::size_t seed = 0; + boost::hash_combine(seed, dd.getCuddBdd().getNode()); + return seed; + } + }; +} + #endif /* STORM_STORAGE_DD_CUDDBDD_H_ */ \ No newline at end of file diff --git a/src/storage/prism/menu_games/AbstractCommand.cpp b/src/storage/prism/menu_games/AbstractCommand.cpp index 7e6263067..6f01b1cae 100644 --- a/src/storage/prism/menu_games/AbstractCommand.cpp +++ b/src/storage/prism/menu_games/AbstractCommand.cpp @@ -1,5 +1,7 @@ #include "src/storage/prism/menu_games/AbstractCommand.h" +#include + #include "src/storage/prism/menu_games/AbstractionExpressionInformation.h" #include "src/storage/prism/menu_games/AbstractionDdInformation.h" @@ -13,7 +15,7 @@ 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), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), cachedDd(std::make_pair(ddInformation.ddManager->getAddZero(), 0)) { + 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.manager->getBddZero(), 0)), decisionVariables() { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates()); @@ -37,7 +39,7 @@ namespace storm { 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. + // Variables that are being assigned are relevant for the successor state. storm::expressions::Variable const& assignedVariable = assignment.getVariable(); auto const& leftHandSidePredicates = variablePartition.getExpressionsUsingVariable(assignedVariable); result.second.insert(leftHandSidePredicates.begin(), leftHandSidePredicates.end()); @@ -102,6 +104,7 @@ namespace storm { std::vector> newSourceVariables = declareNewVariables(relevantPredicatesAndVariables.first, newRelevantPredicates.first); for (auto const& element : newSourceVariables) { smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second])); + decisionVariables.push_back(element.first); } // Insert the new variables into the record of relevant source variables. @@ -110,34 +113,109 @@ namespace storm { // 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) { + std::vector> newSuccessorVariables = declareNewVariables(relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]); + for (auto const& element : newSuccessorVariables) { smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second].substitute(command.get().getUpdate(index).getAsVariableToExpressionMap()))); + decisionVariables.push_back(element.first); } - relevantPredicatesAndVariables.second[index].insert(relevantPredicatesAndVariables.second[index].end(), newTargetVariables.begin(), newTargetVariables.end()); + relevantPredicatesAndVariables.second[index].insert(relevantPredicatesAndVariables.second[index].end(), newSuccessorVariables.begin(), newSuccessorVariables.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); + storm::dd::Bdd AbstractCommand::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const { + storm::dd::Bdd result = ddInformation.manager->getBddOne(); + for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) { + if (model.getBooleanValue(variableIndexPair.first)) { + result &= ddInformation.predicateBdds[variableIndexPair.second].first; + } else { + result &= !ddInformation.predicateBdds[variableIndexPair.second].first; + } + } + return result; + } + + template + storm::dd::Bdd AbstractCommand::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const { + storm::dd::Bdd result = ddInformation.manager->getBddZero(); - if (recomputeDd) { - relevantPredicates = std::move(newRelevantPredicates); - + for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { + storm::dd::Bdd updateBdd = ddInformation.manager->getBddOne(); + + for (auto const& variableIndexPair : relevantPredicatesAndVariables.second[updateIndex]) { + if (model.getBooleanValue(variableIndexPair.first)) { + updateBdd &= ddInformation.predicateBdds[variableIndexPair.second].second; + } else { + updateBdd &= !ddInformation.predicateBdds[variableIndexPair.second].second; + } + updateBdd &= ddInformation.manager->getEncoding(ddInformation.updateDdVariable, updateIndex); + } + // Compute the identities that are missing for this update. + auto firstIt = relevantPredicatesAndVariables.first.begin(); + auto firstIte = relevantPredicatesAndVariables.first.end(); + auto secondIt = relevantPredicatesAndVariables.second[updateIndex].begin(); + auto secondIte = relevantPredicatesAndVariables.second[updateIndex].end(); - storm::dd::Add result; + for (; firstIt != firstIte; ++firstIt) { + if (secondIt == secondIte || firstIt->second != secondIt->second) { + result &= ddInformation.predicateIdentities[firstIt->second]; + } else if (secondIt != secondIte) { + ++secondIt; + } + } - return result; - } else { + result |= updateBdd; + } + + return result; + } + + 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 = this->computeRelevantPredicates(); + + // If the DD does not need recomputation, we can return the cached result. + bool recomputeDd = this->relevantPredicatesChanged(newRelevantPredicates); + if (!recomputeDd) { + // FIXME: multiply identity of new predicates return cachedDd; } + + // If the DD needs recomputation, it is because of new relevant predicates, so we need to assert the appropriate clauses in the solver. + addMissingPredicates(newRelevantPredicates); + + // Create a mapping from source state DDs to their distributions. + std::unordered_map, std::vector>> sourceToDistributionsMap; + smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this] (storm::solver::SmtSolver::ModelReference const& model) { sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model)); return true; } ); + + // Now we search for the maximal number of choices of player 2 to determine how many DD variables we + // need to encode the nondeterminism. + uint_fast64_t maximalNumberOfChoices = 0; + for (auto const& sourceDistributionsPair : sourceToDistributionsMap) { + maximalNumberOfChoices = std::max(maximalNumberOfChoices, static_cast(sourceDistributionsPair.second.size())); + } + + uint_fast64_t numberOfVariablesNeeded = static_cast(std::ceil(std::log2(maximalNumberOfChoices))); + + // Finally, build overall result. + storm::dd::Bdd resultBdd = ddInformation.manager->getBddZero(); + for (auto const& sourceDistributionsPair : sourceToDistributionsMap) { + uint_fast64_t distributionIndex = 0; + storm::dd::Bdd allDistributions = ddInformation.manager->getBddZero(); + for (auto const& distribution : sourceDistributionsPair.second) { + allDistributions |= distribution && ddInformation.encodeDistributionIndex(numberOfVariablesNeeded, distributionIndex); + } + resultBdd |= sourceDistributionsPair.first && allDistributions; + } + + // Cache the result before returning it. + cachedDd = std::make_pair(resultBdd, numberOfVariablesNeeded); + return cachedDd; } template class AbstractCommand; diff --git a/src/storage/prism/menu_games/AbstractCommand.h b/src/storage/prism/menu_games/AbstractCommand.h index eedf28b03..72a08ace6 100644 --- a/src/storage/prism/menu_games/AbstractCommand.h +++ b/src/storage/prism/menu_games/AbstractCommand.h @@ -2,7 +2,9 @@ #define STORM_STORAGE_PRISM_MENU_GAMES_ABSTRACTCOMMAND_H_ #include +#include #include +#include #include "src/storage/prism/menu_games/VariablePartition.h" @@ -40,27 +42,27 @@ namespace storm { /*! * 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 + * @return The abstraction of the command in the form of a BDD together with the number of DD variables * used to encode the choices of player 2. */ - std::pair, uint_fast64_t> computeDd(); + std::pair, uint_fast64_t> computeDd(); private: /*! - * Determines the relevant predicates for source as well as target states wrt. to the given assignments + * Determines the relevant predicates for source as well as successor 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 - * component represents the relevant target state predicates. + * component represents the relevant successor state predicates. */ std::pair, std::set> computeRelevantPredicates(std::vector const& assignments) const; /*! - * Determines the relevant predicates for source as well as target states. + * Determines the relevant predicates for source as well as successor states. * * @return A pair whose first component represents the relevant source predicates and whose second - * component represents the relevant target state predicates. + * component represents the relevant successor state predicates. */ std::pair, std::vector>> computeRelevantPredicates() const; @@ -87,6 +89,22 @@ namespace storm { */ void addMissingPredicates(std::pair, std::vector>> const& newRelevantPredicates); + /*! + * Translates the given model to a source state DD. + * + * @param model The model to translate. + * @return The source state encoded as a DD. + */ + storm::dd::Bdd getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const; + + /*! + * Translates the given model to a distribution over successor states. + * + * @param model The model to translate. + * @return The source state encoded as a DD. + */ + storm::dd::Bdd getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const; + // An SMT responsible for this abstract command. std::unique_ptr smtSolver; @@ -102,12 +120,15 @@ namespace storm { // The partition of variables and expressions. VariablePartition variablePartition; - // The currently relevant source/target predicates and the corresponding variables. + // The currently relevant source/successor 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; + std::pair, uint_fast64_t> cachedDd; + + // All relevant decision variables over which to perform AllSat. + std::vector decisionVariables; }; } } diff --git a/src/storage/prism/menu_games/AbstractModule.cpp b/src/storage/prism/menu_games/AbstractModule.cpp index ae1ddedd6..63afe243f 100644 --- a/src/storage/prism/menu_games/AbstractModule.cpp +++ b/src/storage/prism/menu_games/AbstractModule.cpp @@ -22,16 +22,16 @@ namespace storm { } template - storm::dd::Add AbstractModule::computeDd() { + storm::dd::Bdd AbstractModule::computeDd() { // First, we retrieve the abstractions of all commands. - std::vector, uint_fast64_t>> commandDdsAndUsedOptionVariableCounts; - for (auto const& command : commands) { + std::vector, uint_fast64_t>> commandDdsAndUsedOptionVariableCounts; + for (auto& 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(); + storm::dd::Bdd result = ddInformation.manager->getBddZero(); // TODO diff --git a/src/storage/prism/menu_games/AbstractModule.h b/src/storage/prism/menu_games/AbstractModule.h index 6114267b7..96ed4cbfd 100644 --- a/src/storage/prism/menu_games/AbstractModule.h +++ b/src/storage/prism/menu_games/AbstractModule.h @@ -36,9 +36,9 @@ namespace storm { /*! * 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. + * @return The abstraction of the module in the form of a BDD. */ - storm::dd::Add computeDd(); + storm::dd::Bdd computeDd(); private: // A factory that can be used to create new SMT solvers. diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp index 42b09be50..9e28539a8 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -1,7 +1,5 @@ #include "src/storage/prism/menu_games/AbstractProgram.h" -#include - #include "src/storage/prism/Program.h" #include "src/storage/dd/CuddDdManager.h" @@ -38,23 +36,22 @@ namespace storm { // Create DD variables for all predicates. for (auto const& predicate : expressionInformation.predicates) { - std::stringstream stream; - stream << predicate; - ddInformation.predicateDdVariables.push_back(ddInformation.ddManager->addMetaVariable(stream.str())); + ddInformation.addPredicate(predicate); } // Create DD variable for the command encoding. - ddInformation.commandDdVariable = ddInformation.ddManager->addMetaVariable("command", 0, totalNumberOfCommands - 1).first; + ddInformation.commandDdVariable = ddInformation.manager->addMetaVariable("command", 0, totalNumberOfCommands - 1).first; // Create DD variable for update encoding. - ddInformation.updateDdVariable = ddInformation.ddManager->addMetaVariable("update", 0, maximalUpdateCount - 1).first; + ddInformation.updateDdVariable = ddInformation.manager->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) { - ddInformation.optionDdVariables.push_back(ddInformation.ddManager->addMetaVariable("opt" + std::to_string(index)).first); + storm::expressions::Variable newOptionVar = ddInformation.manager->addMetaVariable("opt" + std::to_string(index)).first; + ddInformation.optionDdVariables.push_back(std::make_pair(newOptionVar, ddInformation.manager->getRange(newOptionVar))); } // For each module of the concrete program, we create an abstract counterpart. @@ -66,7 +63,8 @@ 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(); + // FIXME: multiply with probabilities for updates. + return modules.front().computeDd().toAdd(); } // Explicitly instantiate the class. diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.cpp b/src/storage/prism/menu_games/AbstractionDdInformation.cpp index ebb1790b5..f85831006 100644 --- a/src/storage/prism/menu_games/AbstractionDdInformation.cpp +++ b/src/storage/prism/menu_games/AbstractionDdInformation.cpp @@ -1,17 +1,47 @@ #include "src/storage/prism/menu_games/AbstractionDdInformation.h" -#include "src/storage/dd/DdManager.h" +#include + +#include "src/storage/expressions/Expression.h" + +#include "src/storage/dd/CuddDdManager.h" +#include "src/storage/dd/CuddBdd.h" +#include "src/storage/dd/CuddAdd.h" namespace storm { namespace prism { namespace menu_games { template - AbstractionDdInformation::AbstractionDdInformation(std::shared_ptr> const& manager) : ddManager(manager) { + AbstractionDdInformation::AbstractionDdInformation(std::shared_ptr> const& manager) : manager(manager) { // Intentionally left empty. } + + template + storm::dd::Bdd AbstractionDdInformation::encodeDistributionIndex(uint_fast64_t numberOfVariables, uint_fast64_t distributionIndex) const { + storm::dd::Bdd result = manager->getBddOne(); + for (uint_fast64_t bitIndex = 0; bitIndex < numberOfVariables; ++bitIndex) { + if ((distributionIndex & 1) != 0) { + result &= optionDdVariables[bitIndex].second; + } else { + result &= !optionDdVariables[bitIndex].second; + } + distributionIndex >>= 1; + } + return result; + } + + template + void AbstractionDdInformation::addPredicate(storm::expressions::Expression const& predicate) { + std::stringstream stream; + stream << predicate; + std::pair newMetaVariable = manager->addMetaVariable(stream.str()); + predicateDdVariables.push_back(newMetaVariable); + predicateBdds.emplace_back(manager->getRange(newMetaVariable.first), manager->getRange(newMetaVariable.second)); + predicateIdentities.push_back(manager->getIdentity(newMetaVariable.first).equals(manager->getIdentity(newMetaVariable.second)).toBdd()); + } - template class AbstractionDdInformation; + template struct AbstractionDdInformation; } } diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.h b/src/storage/prism/menu_games/AbstractionDdInformation.h index 9944c7e00..388a5bc8b 100644 --- a/src/storage/prism/menu_games/AbstractionDdInformation.h +++ b/src/storage/prism/menu_games/AbstractionDdInformation.h @@ -11,6 +11,13 @@ namespace storm { namespace dd { template class DdManager; + + template + class Bdd; + } + + namespace expressions { + class Expression; } namespace prism { @@ -26,11 +33,34 @@ namespace storm { */ AbstractionDdInformation(std::shared_ptr> const& manager); + /*! + * Encodes the given distribution index by using the given number of variables from the optionDdVariables + * vector. + * + * @param numberOfVariables The number of variables to use. + * @param distributionIndex The distribution index to encode. + * @return The encoded distribution index. + */ + storm::dd::Bdd encodeDistributionIndex(uint_fast64_t numberOfVariables, uint_fast64_t distributionIndex) const; + + /*! + * Adds the given predicate and creates all associated ressources. + * + * @param predicate The predicate to add. + */ + void addPredicate(storm::expressions::Expression const& predicate); + // The manager responsible for the DDs. - std::shared_ptr> ddManager; + std::shared_ptr> manager; // The DD variables corresponding to the predicates. std::vector> predicateDdVariables; + + // The BDDs corresponding to the predicates. + std::vector, storm::dd::Bdd>> predicateBdds; + + // The BDDs representing the predicate identities (i.e. source and successor variable have the same truth value). + std::vector> predicateIdentities; // The DD variable encoding the command (i.e., the nondeterministic choices of player 1). storm::expressions::Variable commandDdVariable; @@ -39,7 +69,7 @@ namespace storm { storm::expressions::Variable updateDdVariable; // The DD variables encoding the nondeterministic choices of player 2. - std::vector optionDdVariables; + std::vector>> optionDdVariables; }; }