diff --git a/src/storage/prism/menu_games/AbstractCommand.cpp b/src/storage/prism/menu_games/AbstractCommand.cpp index 6f01b1cae..ef5011b6c 100644 --- a/src/storage/prism/menu_games/AbstractCommand.cpp +++ b/src/storage/prism/menu_games/AbstractCommand.cpp @@ -11,6 +11,8 @@ #include "src/storage/prism/Command.h" #include "src/storage/prism/Update.h" +#include "src/utility/macros.h" + namespace storm { namespace prism { namespace menu_games { @@ -24,6 +26,80 @@ namespace storm { for (auto const& rangeExpression : expressionInformation.rangeExpressions) { smtSolver->add(rangeExpression); } + + // Assert the guard of the command. + smtSolver->add(command.getGuardExpression()); + + // Refine the command based on all initial predicates. + std::vector allPredicateIndices(expressionInformation.predicates.size()); + for (auto index = 0; index < expressionInformation.predicates.size(); ++index) { + allPredicateIndices[index] = index; + } + this->refine(allPredicateIndices); + } + + template + void AbstractCommand::refine(std::vector const& predicates) { + // Add all predicates to the variable partition. + for (auto predicateIndex : predicates) { + variablePartition.addExpression(expressionInformation.predicates[predicateIndex]); + } + + STORM_LOG_TRACE("Current variable partition is: " << variablePartition); + + // Next, 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) { + // If the new predicates are unrelated to the BDD of this command, we need to multiply their identities. + for (auto predicateIndex : predicates) { + cachedDd.first &= ddInformation.predicateIdentities[predicateIndex]; + } + } else { + // 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); + + // Finally recompute the cached BDD. + this->recomputeCachedBdd(); + } + } + + template + void AbstractCommand::recomputeCachedBdd() { + STORM_LOG_TRACE("Recomputing BDD for command " << command.get()); + + // 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; + } + + resultBdd &= computeMissingSourceStateIdentities(); + resultBdd &= ddInformation.manager->getEncoding(ddInformation.commandDdVariable, command.get().getGlobalIndex()); + + // Cache the result before returning it. + cachedDd = std::make_pair(resultBdd, numberOfVariablesNeeded); } template @@ -126,6 +202,7 @@ namespace storm { template storm::dd::Bdd AbstractCommand::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const { + STORM_LOG_TRACE("Building source state BDD."); storm::dd::Bdd result = ddInformation.manager->getBddOne(); for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) { if (model.getBooleanValue(variableIndexPair.first)) { @@ -139,11 +216,13 @@ namespace storm { template storm::dd::Bdd AbstractCommand::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const { + STORM_LOG_TRACE("Building distribution BDD."); storm::dd::Bdd result = ddInformation.manager->getBddZero(); for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { storm::dd::Bdd updateBdd = ddInformation.manager->getBddOne(); + // Translate block variables for this update into a successor block. for (auto const& variableIndexPair : relevantPredicatesAndVariables.second[updateIndex]) { if (model.getBooleanValue(variableIndexPair.first)) { updateBdd &= ddInformation.predicateBdds[variableIndexPair.second].second; @@ -159,9 +238,12 @@ namespace storm { auto secondIt = relevantPredicatesAndVariables.second[updateIndex].begin(); auto secondIte = relevantPredicatesAndVariables.second[updateIndex].end(); + // Go through all relevant source predicates. This is guaranteed to be a superset of the set of + // relevant successor predicates for any update. for (; firstIt != firstIte; ++firstIt) { + // If the predicates do not match, there is a predicate missing, so we need to add its identity. if (secondIt == secondIte || firstIt->second != secondIt->second) { - result &= ddInformation.predicateIdentities[firstIt->second]; + updateBdd &= ddInformation.predicateIdentities[firstIt->second]; } else if (secondIt != secondIte) { ++secondIt; } @@ -172,49 +254,23 @@ namespace storm { 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))); + storm::dd::Bdd AbstractCommand::computeMissingSourceStateIdentities() const { + auto relevantIt = relevantPredicatesAndVariables.first.begin(); + auto relevantIte = relevantPredicatesAndVariables.first.end(); - // 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); + storm::dd::Bdd result = ddInformation.manager->getBddOne(); + for (uint_fast64_t predicateIndex = 0; predicateIndex < expressionInformation.predicates.size(); ++predicateIndex) { + if (relevantIt == relevantIte || relevantIt->second != predicateIndex) { + result &= ddInformation.predicateIdentities[predicateIndex]; } - resultBdd |= sourceDistributionsPair.first && allDistributions; } - - // Cache the result before returning it. - cachedDd = std::make_pair(resultBdd, numberOfVariablesNeeded); + return result; + } + + template + std::pair, uint_fast64_t> AbstractCommand::getAbstractBdd() { return cachedDd; } diff --git a/src/storage/prism/menu_games/AbstractCommand.h b/src/storage/prism/menu_games/AbstractCommand.h index 72a08ace6..4402bb4bf 100644 --- a/src/storage/prism/menu_games/AbstractCommand.h +++ b/src/storage/prism/menu_games/AbstractCommand.h @@ -39,13 +39,20 @@ namespace storm { */ AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + /*! + * Refines the abstract command with the given predicates. + * + * @param predicates The new predicates. + */ + void refine(std::vector const& predicates); + /*! * Computes the abstraction of the command wrt. to the current set of predicates. * * @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> getAbstractBdd(); private: /*! @@ -105,6 +112,19 @@ namespace storm { */ storm::dd::Bdd getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const; + /*! + * Recomputes the cached BDD. This needs to be triggered if any relevant predicates change. + */ + void recomputeCachedBdd(); + + /*! + * Computes the missing source state identities. + * + * @return A BDD that represents the source state identities for predicates that are irrelevant for the + * source states. + */ + storm::dd::Bdd computeMissingSourceStateIdentities() const; + // An SMT responsible for this abstract command. std::unique_ptr smtSolver; diff --git a/src/storage/prism/menu_games/AbstractModule.cpp b/src/storage/prism/menu_games/AbstractModule.cpp index 63afe243f..5da411997 100644 --- a/src/storage/prism/menu_games/AbstractModule.cpp +++ b/src/storage/prism/menu_games/AbstractModule.cpp @@ -22,19 +22,28 @@ namespace storm { } template - storm::dd::Bdd AbstractModule::computeDd() { + void AbstractModule::refine(std::vector const& predicates) { + for (auto& command : commands) { + command.refine(predicates); + } + } + + template + storm::dd::Bdd AbstractModule::getAbstractBdd() { // First, we retrieve the abstractions of all commands. std::vector, uint_fast64_t>> commandDdsAndUsedOptionVariableCounts; + uint_fast64_t maximalNumberOfUsedOptionVariables = 0; for (auto& command : commands) { - commandDdsAndUsedOptionVariableCounts.push_back(command.computeDd()); + commandDdsAndUsedOptionVariableCounts.push_back(command.getAbstractBdd()); + maximalNumberOfUsedOptionVariables = std::max(maximalNumberOfUsedOptionVariables, commandDdsAndUsedOptionVariableCounts.back().second); } - // Then, we build the module ADD by adding the single command DDs. We need to make sure that all command + // Then, we build the module BDD 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::Bdd result = ddInformation.manager->getBddZero(); - - // TODO - + for (auto const& commandDd : commandDdsAndUsedOptionVariableCounts) { + result |= commandDd.first && ddInformation.getMissingOptionVariableCube(commandDd.second, maximalNumberOfUsedOptionVariables); + } return result; } diff --git a/src/storage/prism/menu_games/AbstractModule.h b/src/storage/prism/menu_games/AbstractModule.h index 96ed4cbfd..77101e3d7 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); + /*! + * Refines the abstract module with the given predicates. + * + * @param predicates The new predicate indices. + */ + void refine(std::vector const& predicates); + /*! * Computes the abstraction of the module wrt. to the current set of predicates. * * @return The abstraction of the module in the form of a BDD. */ - storm::dd::Bdd computeDd(); + storm::dd::Bdd getAbstractBdd(); 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 9e28539a8..d978ef9b6 100644 --- a/src/storage/prism/menu_games/AbstractProgram.cpp +++ b/src/storage/prism/menu_games/AbstractProgram.cpp @@ -56,15 +56,17 @@ namespace storm { // For each module of the concrete program, we create an abstract counterpart. for (auto const& module : program.getModules()) { - modules.emplace_back(module, expressionInformation, ddInformation, *smtSolverFactory); + modules.emplace_back(module, expressionInformation, ddInformation, *this->smtSolverFactory); } } template - storm::dd::Add AbstractProgram::computeDd() { + storm::dd::Add AbstractProgram::getAbstractAdd() { // As long as there is only one module, we build its game representation and return it. + + // FIXME: multiply with probabilities for updates. - return modules.front().computeDd().toAdd(); + return modules.front().getAbstractBdd().toAdd(); } // Explicitly instantiate the class. diff --git a/src/storage/prism/menu_games/AbstractProgram.h b/src/storage/prism/menu_games/AbstractProgram.h index 1c59be4d3..0da48b672 100644 --- a/src/storage/prism/menu_games/AbstractProgram.h +++ b/src/storage/prism/menu_games/AbstractProgram.h @@ -41,7 +41,7 @@ namespace storm { * * @return The ADD representing the game. */ - storm::dd::Add computeDd(); + storm::dd::Add getAbstractAdd(); private: // A factory that can be used to create new SMT solvers. diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.cpp b/src/storage/prism/menu_games/AbstractionDdInformation.cpp index f85831006..7946115fb 100644 --- a/src/storage/prism/menu_games/AbstractionDdInformation.cpp +++ b/src/storage/prism/menu_games/AbstractionDdInformation.cpp @@ -37,10 +37,21 @@ namespace storm { stream << predicate; std::pair newMetaVariable = manager->addMetaVariable(stream.str()); predicateDdVariables.push_back(newMetaVariable); - predicateBdds.emplace_back(manager->getRange(newMetaVariable.first), manager->getRange(newMetaVariable.second)); + 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()); } + template + storm::dd::Bdd AbstractionDdInformation::getMissingOptionVariableCube(uint_fast64_t lastUsed, uint_fast64_t lastToBe) const { + storm::dd::Bdd result = manager->getBddOne(); + + for (uint_fast64_t index = lastUsed + 1; index <= lastToBe; ++index) { + result &= optionDdVariables[index].second; + } + + return result; + } + template struct AbstractionDdInformation; } diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.h b/src/storage/prism/menu_games/AbstractionDdInformation.h index 388a5bc8b..b0b239107 100644 --- a/src/storage/prism/menu_games/AbstractionDdInformation.h +++ b/src/storage/prism/menu_games/AbstractionDdInformation.h @@ -50,6 +50,15 @@ namespace storm { */ void addPredicate(storm::expressions::Expression const& predicate); + /*! + * Retrieves the cube of option variables in the range (lastUsed, lastToBe] the given indices. + * + * @param lastUsed The last variable before the range to return. + * @param lastToBe The last variable of the range to return. + * @return The cube of variables in the given range. + */ + storm::dd::Bdd getMissingOptionVariableCube(uint_fast64_t lastUsed, uint_fast64_t lastToBe) const; + // The manager responsible for the DDs. std::shared_ptr> manager; diff --git a/src/storage/prism/menu_games/VariablePartition.cpp b/src/storage/prism/menu_games/VariablePartition.cpp index 92738dfb8..a8705e599 100644 --- a/src/storage/prism/menu_games/VariablePartition.cpp +++ b/src/storage/prism/menu_games/VariablePartition.cpp @@ -7,7 +7,15 @@ namespace storm { namespace prism { namespace menu_games { - VariablePartition::VariablePartition(std::set const& relevantVariables, std::vector const& expressions) : relevantVariables(relevantVariables), expressionBlocks(expressions.size()) { + VariablePartition::VariablePartition(std::set const& relevantVariables, std::vector const& expressions) : relevantVariables(relevantVariables), expressionBlocks(relevantVariables.size()) { + // Assign each variable to a new block. + uint_fast64_t currentBlock = 0; + for (auto const& variable : relevantVariables) { + this->variableToBlockMapping[variable] = currentBlock; + this->variableToExpressionsMapping[variable] = std::set(); + } + + // Add all expressions, which might relate some variables. for (auto const& expression : expressions) { this->addExpression(expression); } diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp index 16027bf3f..76321e237 100644 --- a/test/functional/abstraction/PrismMenuGameTest.cpp +++ b/test/functional/abstraction/PrismMenuGameTest.cpp @@ -24,6 +24,9 @@ TEST(PrismMenuGame, CommandAbstractionTest) { initialPredicates.push_back(manager.getVariableExpression("s") < manager.integer(3)); storm::prism::menu_games::AbstractProgram abstractProgram(program.getManager(), program, initialPredicates, std::make_unique(), false); + + storm::dd::Add abstraction = abstractProgram.getAbstractAdd(); + abstraction.exportToDot("abstr.dot"); } #endif \ No newline at end of file