From 4f54759f3827b1abb58148d3020951166f2176cb Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 11 Aug 2016 12:09:14 +0200 Subject: [PATCH] intermediate commit [fixing bottom states/transitions] Former-commit-id: d457ce2fb44bb294081616d28858ad8f7245c2b3 --- src/abstraction/prism/AbstractCommand.cpp | 22 +++++++++---- src/abstraction/prism/AbstractCommand.h | 19 ++++++++++-- src/abstraction/prism/AbstractModule.cpp | 28 ++++++++++++----- src/abstraction/prism/AbstractModule.h | 20 ++++++++++-- src/abstraction/prism/AbstractProgram.cpp | 38 +++++++++++++---------- src/abstraction/prism/AbstractProgram.h | 4 --- src/abstraction/prism/GameBddResult.cpp | 19 ++++++++++++ src/abstraction/prism/GameBddResult.h | 21 +++++++++++++ 8 files changed, 131 insertions(+), 40 deletions(-) create mode 100644 src/abstraction/prism/GameBddResult.cpp create mode 100644 src/abstraction/prism/GameBddResult.h diff --git a/src/abstraction/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp index d8b39cb5e..ade2e85b7 100644 --- a/src/abstraction/prism/AbstractCommand.cpp +++ b/src/abstraction/prism/AbstractCommand.cpp @@ -17,7 +17,7 @@ namespace storm { namespace abstraction { namespace prism { template - AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(std::make_pair(abstractionInformation.getDdManager().getBddZero(), 0)), decisionVariables() { + AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool guardIsPredicate) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), guardIsPredicate(guardIsPredicate), bottomStateAbstractor(abstractionInformation, abstractionInformation.getExpressionVariables(), {!command.getGuardExpression()}, smtSolverFactory) { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates()); @@ -25,6 +25,7 @@ namespace storm { // Assert all constraints to enforce legal variable values. for (auto const& constraint : abstractionInformation.getConstraints()) { smtSolver->add(constraint); + bottomStateAbstractor.constrain(constraint); } // Assert the guard of the command. @@ -36,8 +37,11 @@ namespace storm { allPredicateIndices[index] = index; } this->refine(allPredicateIndices); + + // Refine the bottom state abstractor. + bottomStateAbstractor.refine(allPredicateIndices); } - + template void AbstractCommand::refine(std::vector const& predicates) { // Add all predicates to the variable partition. @@ -55,7 +59,7 @@ namespace storm { 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. - cachedDd.first &= computeMissingGlobalIdentities(); + cachedDd.bdd &= computeMissingGlobalIdentities(); } 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); @@ -63,6 +67,10 @@ namespace storm { // Finally recompute the cached BDD. this->recomputeCachedBdd(); } + + // Refine bottom state abstractor. + // FIXME: Should this only be done if the other BDD needs recomputation? + bottomStateAbstractor.refine(predicates); } template @@ -83,7 +91,9 @@ namespace storm { maximalNumberOfChoices = std::max(maximalNumberOfChoices, static_cast(sourceDistributionsPair.second.size())); } - uint_fast64_t numberOfVariablesNeeded = static_cast(std::ceil(std::log2(maximalNumberOfChoices))); + // We now compute how many variables we need to encode the choices. We add one to the maximal number of + // choices to + uint_fast64_t numberOfVariablesNeeded = static_cast(std::ceil(std::log2(maximalNumberOfChoices + 1))); // Finally, build overall result. storm::dd::Bdd resultBdd = this->getAbstractionInformation().getDdManager().getBddZero(); @@ -108,7 +118,7 @@ namespace storm { STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions."); // Cache the result. - cachedDd = std::make_pair(resultBdd, numberOfVariablesNeeded); + cachedDd = GameBddResult(resultBdd, numberOfVariablesNeeded, maximalNumberOfChoices); } template @@ -287,7 +297,7 @@ namespace storm { } template - std::pair, uint_fast64_t> AbstractCommand::getAbstractBdd() { + GameBddResult AbstractCommand::getAbstractBdd() { return cachedDd; } diff --git a/src/abstraction/prism/AbstractCommand.h b/src/abstraction/prism/AbstractCommand.h index 97f4d464c..3000d6474 100644 --- a/src/abstraction/prism/AbstractCommand.h +++ b/src/abstraction/prism/AbstractCommand.h @@ -6,6 +6,8 @@ #include #include "src/abstraction/LocalExpressionInformation.h" +#include "src/abstraction/StateSetAbstractor.h" +#include "src/abstraction/prism/GameBddResult.h" #include "src/storage/expressions/ExpressionEvaluator.h" @@ -40,6 +42,9 @@ namespace storm { class AbstractionInformation; namespace prism { + template + struct GameBddResult; + template class AbstractCommand { public: @@ -49,8 +54,9 @@ namespace storm { * @param command The concrete command for which to build the abstraction. * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs. * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. + * @param guardIsPredicate A flag indicating whether the guard of the command was added as a predicate. */ - AbstractCommand(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + AbstractCommand(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool guardIsPredicate = false); /*! * Refines the abstract command with the given predicates. @@ -65,7 +71,7 @@ namespace storm { * @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> getAbstractBdd(); + GameBddResult getAbstractBdd(); /*! * Retrieves an ADD that maps the encoding of the command and its updates to their probabilities. @@ -186,10 +192,17 @@ namespace storm { // 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; + GameBddResult cachedDd; // All relevant decision variables over which to perform AllSat. std::vector decisionVariables; + + // A flag indicating whether the guard of the command was added as a predicate. If this is true, there + // is no need to compute bottom states. + bool guardIsPredicate; + + // A state-set abstractor used to determine the bottom states if not all guards were added. + StateSetAbstractor bottomStateAbstractor; }; } } diff --git a/src/abstraction/prism/AbstractModule.cpp b/src/abstraction/prism/AbstractModule.cpp index 3adcc9860..46fc41da5 100644 --- a/src/abstraction/prism/AbstractModule.cpp +++ b/src/abstraction/prism/AbstractModule.cpp @@ -1,6 +1,7 @@ #include "src/abstraction/prism/AbstractModule.h" #include "src/abstraction/AbstractionInformation.h" +#include "src/abstraction/prism/GameBddResult.h" #include "src/storage/dd/DdManager.h" #include "src/storage/dd/Add.h" @@ -12,11 +13,11 @@ namespace storm { namespace prism { template - AbstractModule::AbstractModule(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) { + AbstractModule::AbstractModule(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool allGuardsAdded) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), commands(), module(module) { // For each concrete command, we create an abstract counterpart. for (auto const& command : module.getCommands()) { - commands.emplace_back(command, abstractionInformation, smtSolverFactory); + commands.emplace_back(command, abstractionInformation, smtSolverFactory, allGuardsAdded); } } @@ -28,22 +29,35 @@ namespace storm { } template - std::pair, uint_fast64_t> AbstractModule::getAbstractBdd() { + GameBddResult AbstractModule::getAbstractBdd() { // First, we retrieve the abstractions of all commands. - std::vector, uint_fast64_t>> commandDdsAndUsedOptionVariableCounts; + std::vector> commandDdsAndUsedOptionVariableCounts; uint_fast64_t maximalNumberOfUsedOptionVariables = 0; + uint_fast64_t nextFreePlayer2Index = 0; for (auto& command : commands) { commandDdsAndUsedOptionVariableCounts.push_back(command.getAbstractBdd()); - maximalNumberOfUsedOptionVariables = std::max(maximalNumberOfUsedOptionVariables, commandDdsAndUsedOptionVariableCounts.back().second); + maximalNumberOfUsedOptionVariables = std::max(maximalNumberOfUsedOptionVariables, commandDdsAndUsedOptionVariableCounts.back().numberOfPlayer2Variables); + nextFreePlayer2Index = std::max(nextFreePlayer2Index, commandDdsAndUsedOptionVariableCounts.back().nextFreePlayer2Index); } // 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 = this->getAbstractionInformation().getDdManager().getBddZero(); for (auto const& commandDd : commandDdsAndUsedOptionVariableCounts) { - result |= commandDd.first && this->getAbstractionInformation().getPlayer2ZeroCube(maximalNumberOfUsedOptionVariables, commandDd.second); + result |= commandDd.bdd && this->getAbstractionInformation().getPlayer2ZeroCube(maximalNumberOfUsedOptionVariables, commandDd.numberOfPlayer2Variables); } - return std::make_pair(result, maximalNumberOfUsedOptionVariables); + return GameBddResult(result, maximalNumberOfUsedOptionVariables, nextFreePlayer2Index); + } + + template + storm::dd::Bdd AbstractModule::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { + storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); + + for (auto& command : commands) { + result |= command.getBottomStateTransitions(reachableStates, numberOfPlayer2Variables); + } + + return result; } template diff --git a/src/abstraction/prism/AbstractModule.h b/src/abstraction/prism/AbstractModule.h index 28428e2f1..57f78aaf1 100644 --- a/src/abstraction/prism/AbstractModule.h +++ b/src/abstraction/prism/AbstractModule.h @@ -19,6 +19,10 @@ namespace storm { class AbstractionInformation; namespace prism { + template + struct GameBddResult; + + template class AbstractModule { public: @@ -28,8 +32,9 @@ namespace storm { * @param module The concrete module for which to build the abstraction. * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs. * @param smtSolverFactory A factory that is to be used for creating new SMT solvers. + * @param allGuardsAdded A flag indicating whether all guards of the program were added. */ - AbstractModule(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory); + AbstractModule(storm::prism::Module const& module, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory = std::make_shared(), bool allGuardsAdded = false); AbstractModule(AbstractModule const&) = default; AbstractModule& operator=(AbstractModule const&) = default; @@ -48,7 +53,16 @@ namespace storm { * * @return The abstraction of the module in the form of a BDD together with how many option variables were used. */ - std::pair, uint_fast64_t> getAbstractBdd(); + GameBddResult getAbstractBdd(); + + /*! + * Retrieves the transitions to bottom states of this module. + * + * @param reachableStates A BDD representing the reachable states. + * @param numberOfPlayer2Variables The number of variables used to encode the choices of player 2. + * @return The bottom state transitions in the form of a BDD. + */ + storm::dd::Bdd getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables); /*! * Retrieves an ADD that maps the encodings of commands and their updates to their probabilities. @@ -66,7 +80,7 @@ namespace storm { AbstractionInformation const& getAbstractionInformation() const; // A factory that can be used to create new SMT solvers. - storm::utility::solver::SmtSolverFactory const& smtSolverFactory; + std::shared_ptr smtSolverFactory; // The DD-related information. std::reference_wrapper const> abstractionInformation; diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index 8c0321d9c..9ca9dd9c5 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -21,7 +21,7 @@ namespace storm { std::vector const& initialPredicates, std::shared_ptr const& smtSolverFactory, bool addAllGuards) - : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialConstruct().getInitialStatesExpression()}, this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), program.getAllGuards(true), this->smtSolverFactory), currentGame(nullptr) { + : program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialConstruct().getInitialStatesExpression()}, this->smtSolverFactory), addedAllGuards(addAllGuards), currentGame(nullptr) { // 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. @@ -34,7 +34,6 @@ namespace storm { for (auto const& range : this->program.get().getAllRangeExpressions()) { abstractionInformation.addConstraint(range); initialStateAbstractor.constrain(range); - bottomStateAbstractor.constrain(range); } uint_fast64_t totalNumberOfCommands = 0; @@ -70,12 +69,11 @@ namespace storm { // For each module of the concrete program, we create an abstract counterpart. for (auto const& module : program.getModules()) { - this->modules.emplace_back(module, abstractionInformation, *this->smtSolverFactory); + this->modules.emplace_back(module, abstractionInformation, this->smtSolverFactory, addAllGuards); } - // Refine the state abstractors using the initial predicates. + // Refine the initial state abstractors using the initial predicates. initialStateAbstractor.refine(allPredicateIndices); - bottomStateAbstractor.refine(allPredicateIndices); // Retrieve the command-update probability ADD, so we can multiply it with the abstraction BDD later. commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd(); @@ -103,10 +101,7 @@ namespace storm { // Refine initial state abstractor. initialStateAbstractor.refine(newPredicateIndices); - - // Refine bottom state abstractor. - bottomStateAbstractor.refine(newPredicateIndices); - + // Finally, we rebuild the game. currentGame = buildGame(); } @@ -126,22 +121,30 @@ namespace storm { template std::unique_ptr> AbstractProgram::buildGame() { // As long as there is only one module, we only build its game representation. - std::pair, uint_fast64_t> gameBdd = modules.front().getAbstractBdd(); + GameBddResult game = modules.front().getAbstractBdd(); // Construct a set of all unnecessary variables, so we can abstract from it. std::set variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount())); - auto player2Variables = abstractionInformation.getPlayer2VariableSet(gameBdd.second); + auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables); variablesToAbstract.insert(player2Variables.begin(), player2Variables.end()); auto probBranchingVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount()); variablesToAbstract.insert(probBranchingVariables.begin(), probBranchingVariables.end()); // Do a reachability analysis on the raw transition relation. - storm::dd::Bdd transitionRelation = gameBdd.first.existsAbstract(variablesToAbstract); + storm::dd::Bdd transitionRelation = game.bdd.existsAbstract(variablesToAbstract); storm::dd::Bdd initialStates = initialStateAbstractor.getAbstractStates(); storm::dd::Bdd reachableStates = this->getReachableStates(initialStates, transitionRelation); + storm::dd::Bdd bottomStateTransitions = abstractionInformation.getDdManager().getBddZero(); + storm::dd::Bdd bottomStates = bottomStateTransitions; + if (addedAllGuards) { + bottomStateTransitions = modules.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables); + + // If there are transitions to the bottom states, add them and register the new states as well. + transitionRelation |= bottomStateTransitions; + } + // Determine the bottom states. - storm::dd::Bdd bottomStates; if (addedAllGuards) { bottomStates = abstractionInformation.getDdManager().getBddZero(); } else { @@ -149,20 +152,21 @@ namespace storm { bottomStates = bottomStateAbstractor.getAbstractStates(); } - // Find the deadlock states in the model. + // Find the deadlock states in the model. Note that this does not find the 'deadlocks' in bottom states, + // as the bottom states are not contained in the reachable states. storm::dd::Bdd deadlockStates = transitionRelation.existsAbstract(abstractionInformation.getSuccessorVariables()); deadlockStates = reachableStates && !deadlockStates; // If there are deadlock states, we fix them now. storm::dd::Add deadlockTransitions = abstractionInformation.getDdManager().template getAddZero(); if (!deadlockStates.isZero()) { - deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, gameBdd.second) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd(); + deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, game.numberOfPlayer2Variables) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd(); } // Construct the transition matrix by cutting away the transitions of unreachable states. - storm::dd::Add transitionMatrix = (gameBdd.first && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; + storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; - std::set usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + gameBdd.second); + std::set usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + game.numberOfPlayer2Variables); std::set allNondeterminismVariables = usedPlayer2Variables; allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()); diff --git a/src/abstraction/prism/AbstractProgram.h b/src/abstraction/prism/AbstractProgram.h index 39c5e0e78..77eb91c07 100644 --- a/src/abstraction/prism/AbstractProgram.h +++ b/src/abstraction/prism/AbstractProgram.h @@ -3,7 +3,6 @@ #include "src/storage/dd/DdType.h" #include "src/abstraction/AbstractionInformation.h" -#include "src/abstraction/StateSetAbstractor.h" #include "src/abstraction/MenuGame.h" #include "src/abstraction/prism/AbstractModule.h" @@ -110,9 +109,6 @@ namespace storm { // A flag that stores whether all guards were added (which is relevant for determining the bottom states). bool addedAllGuards; - - // A state-set abstractor used to determine the bottom states if not all guards were added. - StateSetAbstractor bottomStateAbstractor; // An ADD characterizing the probabilities of commands and their updates. storm::dd::Add commandUpdateProbabilitiesAdd; diff --git a/src/abstraction/prism/GameBddResult.cpp b/src/abstraction/prism/GameBddResult.cpp new file mode 100644 index 000000000..01780ebcd --- /dev/null +++ b/src/abstraction/prism/GameBddResult.cpp @@ -0,0 +1,19 @@ +#include "src/abstraction/prism/GameBddResult.h" + +namespace storm { + namespace abstraction { + namespace prism { + + template + GameBddResult::GameBddResult() : bdd(), numberOfPlayer2Variables(0), nextFreePlayer2Index(0) { + // Intentionally left empty. + } + + template + GameBddResult::GameBddResult(storm::dd::Bdd const& gameBdd, uint_fast64_t numberOfPlayer2Variables, uint_fast64_t nextFreePlayer2Index) : bdd(gameBdd), numberOfPlayer2Variables(numberOfPlayer2Variables), nextFreePlayer2Index(nextFreePlayer2Index) { + // Intentionally left empty. + } + + } + } +} \ No newline at end of file diff --git a/src/abstraction/prism/GameBddResult.h b/src/abstraction/prism/GameBddResult.h new file mode 100644 index 000000000..c04309e98 --- /dev/null +++ b/src/abstraction/prism/GameBddResult.h @@ -0,0 +1,21 @@ +#pragma once + +#include "src/storage/dd/Bdd.h" + +namespace storm { + namespace abstraction { + namespace prism { + + template + struct GameBddResult { + GameBddResult(); + GameBddResult(storm::dd::Bdd const& gameBdd, uint_fast64_t numberOfPlayer2Variables, uint_fast64_t nextFreePlayer2Index); + + storm::dd::Bdd bdd; + uint_fast64_t numberOfPlayer2Variables; + uint_fast64_t nextFreePlayer2Index; + }; + + } + } +} \ No newline at end of file