From 1280c88b4f6c95ec3008479272245776f65f3568 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 10 Aug 2016 21:21:12 +0200 Subject: [PATCH 1/6] renamed prob branching variables to aux variables in preparation for proper bottom state creation in game abstraction Former-commit-id: e855b14b4661358fff048ef99b08377d54370e23 --- src/abstraction/AbstractionInformation.cpp | 47 +++++++++++----------- src/abstraction/AbstractionInformation.h | 41 ++++++++++--------- src/abstraction/prism/AbstractCommand.cpp | 6 +-- src/abstraction/prism/AbstractProgram.cpp | 6 +-- 4 files changed, 52 insertions(+), 48 deletions(-) diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp index f21dfbcc5..afa80f2a0 100644 --- a/src/abstraction/AbstractionInformation.cpp +++ b/src/abstraction/AbstractionInformation.cpp @@ -129,44 +129,44 @@ namespace storm { } template - void AbstractionInformation::createEncodingVariables(uint64_t player1VariableCount, uint64_t player2VariableCount, uint64_t probabilisticBranchingVariableCount) { - STORM_LOG_THROW(player1Variables.empty() && player2Variables.empty() && probabilisticBranchingVariables.empty(), storm::exceptions::InvalidOperationException, "Variables have already been created."); + void AbstractionInformation::createEncodingVariables(uint64_t player1VariableCount, uint64_t player2VariableCount, uint64_t auxVariableCount) { + STORM_LOG_THROW(player1Variables.empty() && player2Variables.empty() && auxVariables.empty(), storm::exceptions::InvalidOperationException, "Variables have already been created."); for (uint64_t index = 0; index < player1VariableCount; ++index) { - storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl1_" + std::to_string(index)).first; + storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl1." + std::to_string(index)).first; player1Variables.push_back(newVariable); player1VariableBdds.push_back(ddManager->getEncoding(newVariable, 1)); } STORM_LOG_DEBUG("Created " << player1VariableCount << " player 1 variables."); for (uint64_t index = 0; index < player2VariableCount; ++index) { - storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl2_" + std::to_string(index)).first; + storm::expressions::Variable newVariable = ddManager->addMetaVariable("pl2." + std::to_string(index)).first; player2Variables.push_back(newVariable); player2VariableBdds.push_back(ddManager->getEncoding(newVariable, 1)); } STORM_LOG_DEBUG("Created " << player2VariableCount << " player 2 variables."); - for (uint64_t index = 0; index < probabilisticBranchingVariableCount; ++index) { - storm::expressions::Variable newVariable = ddManager->addMetaVariable("pb_" + std::to_string(index)).first; - probabilisticBranchingVariables.push_back(newVariable); - probabilisticBranchingVariableBdds.push_back(ddManager->getEncoding(newVariable, 1)); + for (uint64_t index = 0; index < auxVariableCount; ++index) { + storm::expressions::Variable newVariable = ddManager->addMetaVariable("aux_" + std::to_string(index)).first; + auxVariables.push_back(newVariable); + auxVariableBdds.push_back(ddManager->getEncoding(newVariable, 1)); } - STORM_LOG_DEBUG("Created " << probabilisticBranchingVariableCount << " probabilistic branching variables."); + STORM_LOG_DEBUG("Created " << auxVariableCount << " auxiliary variables."); } template storm::dd::Bdd AbstractionInformation::encodePlayer1Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const { - return encodeChoice(index, numberOfVariables, player1VariableBdds); + return encodeChoice(index, 0, numberOfVariables, player1VariableBdds); } template storm::dd::Bdd AbstractionInformation::encodePlayer2Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const { - return encodeChoice(index, numberOfVariables, player2VariableBdds); + return encodeChoice(index, 0, numberOfVariables, player2VariableBdds); } template - storm::dd::Bdd AbstractionInformation::encodeProbabilisticChoice(uint_fast64_t index, uint_fast64_t numberOfVariables) const { - return encodeChoice(index, numberOfVariables, probabilisticBranchingVariableBdds); + storm::dd::Bdd AbstractionInformation::encodeAux(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables) const { + return encodeChoice(index, offset, numberOfVariables, auxVariableBdds); } template @@ -200,13 +200,13 @@ namespace storm { } template - std::vector const& AbstractionInformation::getProbabilisticBranchingVariables() const { - return probabilisticBranchingVariables; + std::vector const& AbstractionInformation::getAuxVariables() const { + return auxVariables; } template - std::set AbstractionInformation::getProbabilisticBranchingVariableSet(uint_fast64_t count) const { - return std::set(probabilisticBranchingVariables.begin(), probabilisticBranchingVariables.begin() + count); + std::set AbstractionInformation::getAuxVariableSet(uint_fast64_t offset, uint_fast64_t count) const { + return std::set(auxVariables.begin() + offset, auxVariables.begin() + offset + count); } template @@ -235,8 +235,8 @@ namespace storm { } template - std::size_t AbstractionInformation::getProbabilisticBranchingVariableCount() const { - return probabilisticBranchingVariables.size(); + std::size_t AbstractionInformation::getAuxVariableCount() const { + return auxVariables.size(); } template @@ -298,13 +298,14 @@ namespace storm { } template - storm::dd::Bdd AbstractionInformation::encodeChoice(uint_fast64_t index, uint_fast64_t numberOfVariables, std::vector> const& variables) const { + storm::dd::Bdd AbstractionInformation::encodeChoice(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables, std::vector> const& variables) const { storm::dd::Bdd result = ddManager->getBddOne(); - for (uint_fast64_t bitIndex = 0; bitIndex < numberOfVariables; ++bitIndex) { + numberOfVariables += offset; + for (uint_fast64_t bitIndex = numberOfVariables; bitIndex > offset; --bitIndex) { if ((index & 1) != 0) { - result &= variables[bitIndex]; + result &= variables[bitIndex - 1]; } else { - result &= !variables[bitIndex]; + result &= !variables[bitIndex - 1]; } index >>= 1; } diff --git a/src/abstraction/AbstractionInformation.h b/src/abstraction/AbstractionInformation.h index 76c721f77..2c076daae 100644 --- a/src/abstraction/AbstractionInformation.h +++ b/src/abstraction/AbstractionInformation.h @@ -162,13 +162,13 @@ namespace storm { std::set const& getVariables() const; /*! - * Creates the given number of variables used to encode the choices of player 1/2 and probabilistic branching. + * Creates the given number of variables used to encode the choices of player 1/2 and auxiliary information. * * @param player1VariableCount The number of variables to use for encoding player 1 choices. * @param player2VariableCount The number of variables to use for encoding player 2 choices. - * @param probabilisticBranchingVariableCount The number of variables to use for encoding probabilistic branching. + * @param auxVariableCount The number of variables to use for encoding auxiliary information. */ - void createEncodingVariables(uint64_t player1VariableCount, uint64_t player2VariableCount, uint64_t probabilisticBranchingVariableCount); + void createEncodingVariables(uint64_t player1VariableCount, uint64_t player2VariableCount, uint64_t auxVariableCount); /*! * Encodes the given index using the indicated player 1 variables. @@ -192,10 +192,11 @@ namespace storm { * Encodes the given index using the indicated probabilistic branching variables. * * @param index The index to encode. + * @param offset The offset within the auxiliary variables at which to start encoding. * @param numberOfVariables The number of variables to use for encoding the index. * @return The index encoded as a BDD. */ - storm::dd::Bdd encodeProbabilisticChoice(uint_fast64_t index, uint_fast64_t numberOfVariables) const; + storm::dd::Bdd encodeAux(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables) const; /*! * Retrieves the cube of player 2 variables in the given range [offset, numberOfVariables). @@ -252,26 +253,27 @@ namespace storm { std::set getPlayer2VariableSet(uint_fast64_t count) const; /*! - * Retrieves the meta variables associated with the probabilistic branching. + * Retrieves the meta variables associated with auxiliary information. * - * @return The meta variables associated with the probabilistic branching. + * @return The meta variables associated with auxiliary information. */ - std::vector const& getProbabilisticBranchingVariables() const; + std::vector const& getAuxVariables() const; /*! - * Retrieves the set of probabilistic branching variables. + * Retrieves the requested set of auxiliary variables. * - * @param count The number of probabilistic branching variables to include. - * @return The set of probabilistic branching variables. + * @param offset The offset at which to start gatherin the auxiliary variables. + * @param count The number of auxiliary variables to include. + * @return The set of auxiliary variables. */ - std::set getProbabilisticBranchingVariableSet(uint_fast64_t count) const; + std::set getAuxVariableSet(uint_fast64_t offset, uint_fast64_t count) const; /*! - * Retrieves the number of probabilistic branching variables. + * Retrieves the number of auxiliary variables. * - * @return The number of probabilistic branching variables. + * @return The number of auxiliary variables. */ - std::size_t getProbabilisticBranchingVariableCount() const; + std::size_t getAuxVariableCount() const; /*! * Retrieves the set of source meta variables. @@ -354,10 +356,11 @@ namespace storm { * Encodes the given index with the given number of variables from the given variables. * * @param index The index to encode. + * @param offset The offset at which to start encoding. * @param numberOfVariables The total number of variables to use. * @param variables The BDDs of the variables to use to encode the index. */ - storm::dd::Bdd encodeChoice(uint_fast64_t index, uint_fast64_t numberOfVariables, std::vector> const& variables) const; + storm::dd::Bdd encodeChoice(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables, std::vector> const& variables) const; // The expression related data. @@ -415,11 +418,11 @@ namespace storm { /// The BDDs associated with the meta variables of player 2. std::vector> player2VariableBdds; - /// Variables that can be used to encode the probabilistic branching. - std::vector probabilisticBranchingVariables; + /// Variables that can be used to encode auxiliary information. + std::vector auxVariables; - /// The BDDs associated with the meta variables encoding the probabilistic branching. - std::vector> probabilisticBranchingVariableBdds; + /// The BDDs associated with the meta variables encoding auxiliary information. + std::vector> auxVariableBdds; }; } diff --git a/src/abstraction/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp index ea39a5922..d8b39cb5e 100644 --- a/src/abstraction/prism/AbstractCommand.cpp +++ b/src/abstraction/prism/AbstractCommand.cpp @@ -226,7 +226,7 @@ namespace storm { } else { updateBdd &= !this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second); } - updateBdd &= this->getAbstractionInformation().encodeProbabilisticChoice(updateIndex, this->getAbstractionInformation().getProbabilisticBranchingVariableCount()); + updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); } result |= updateBdd; @@ -265,7 +265,7 @@ namespace storm { } } - result |= updateIdentity && this->getAbstractionInformation().encodeProbabilisticChoice(updateIndex, this->getAbstractionInformation().getProbabilisticBranchingVariableCount()); + result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); } return result; } @@ -295,7 +295,7 @@ namespace storm { storm::dd::Add AbstractCommand::getCommandUpdateProbabilitiesAdd() const { storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { - result += this->getAbstractionInformation().encodeProbabilisticChoice(updateIndex, this->getAbstractionInformation().getProbabilisticBranchingVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression())); + result += this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression())); } result *= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd(); return result; diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index 441dd07b6..8c0321d9c 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -132,7 +132,7 @@ namespace storm { std::set variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount())); auto player2Variables = abstractionInformation.getPlayer2VariableSet(gameBdd.second); variablesToAbstract.insert(player2Variables.begin(), player2Variables.end()); - auto probBranchingVariables = abstractionInformation.getProbabilisticBranchingVariableSet(abstractionInformation.getProbabilisticBranchingVariableCount()); + auto probBranchingVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount()); variablesToAbstract.insert(probBranchingVariables.begin(), probBranchingVariables.end()); // Do a reachability analysis on the raw transition relation. @@ -156,7 +156,7 @@ namespace storm { // 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.encodeProbabilisticChoice(0, abstractionInformation.getProbabilisticBranchingVariableCount())).template toAdd(); + deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, gameBdd.second) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd(); } // Construct the transition matrix by cutting away the transitions of unreachable states. @@ -167,7 +167,7 @@ namespace storm { std::set allNondeterminismVariables = usedPlayer2Variables; allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()); - return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStates, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables(), abstractionInformation.getSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, std::set(abstractionInformation.getProbabilisticBranchingVariables().begin(), abstractionInformation.getProbabilisticBranchingVariables().end()), abstractionInformation.getPredicateToBddMap()); + return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStates, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables(), abstractionInformation.getSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, std::set(abstractionInformation.getAuxVariables().begin(), abstractionInformation.getAuxVariables().end()), abstractionInformation.getPredicateToBddMap()); } template From 4f54759f3827b1abb58148d3020951166f2176cb Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 11 Aug 2016 12:09:14 +0200 Subject: [PATCH 2/6] 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 From 3bc0b4eacc38f3d4878d02d17e654e8b6d528add Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 12 Aug 2016 20:57:31 +0200 Subject: [PATCH 3/6] more work on proper bottom state computation Former-commit-id: 38718e1c5c8dadcfce2b7d0b2bc6cf5a476e5b4e --- src/abstraction/AbstractionInformation.cpp | 25 +++++++------- src/abstraction/AbstractionInformation.h | 26 +++++++------- src/abstraction/BottomStateResult.cpp | 14 ++++++++ src/abstraction/BottomStateResult.h | 19 ++++++++++ src/abstraction/MenuGame.cpp | 1 + src/abstraction/StateSetAbstractor.cpp | 2 ++ src/abstraction/prism/AbstractCommand.cpp | 40 ++++++++++++++++++---- src/abstraction/prism/AbstractCommand.h | 18 +++++++++- src/abstraction/prism/AbstractModule.cpp | 9 +++-- src/abstraction/prism/AbstractModule.h | 8 +++-- src/abstraction/prism/AbstractProgram.cpp | 40 ++++++++++------------ src/abstraction/prism/GameBddResult.cpp | 4 ++- 12 files changed, 143 insertions(+), 63 deletions(-) create mode 100644 src/abstraction/BottomStateResult.cpp create mode 100644 src/abstraction/BottomStateResult.h diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp index afa80f2a0..a5500092b 100644 --- a/src/abstraction/AbstractionInformation.cpp +++ b/src/abstraction/AbstractionInformation.cpp @@ -155,24 +155,24 @@ namespace storm { } template - storm::dd::Bdd AbstractionInformation::encodePlayer1Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const { - return encodeChoice(index, 0, numberOfVariables, player1VariableBdds); + storm::dd::Bdd AbstractionInformation::encodePlayer1Choice(uint_fast64_t index, uint_fast64_t end) const { + return encodeChoice(index, 0, end, player1VariableBdds); } template - storm::dd::Bdd AbstractionInformation::encodePlayer2Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const { - return encodeChoice(index, 0, numberOfVariables, player2VariableBdds); + storm::dd::Bdd AbstractionInformation::encodePlayer2Choice(uint_fast64_t index, uint_fast64_t end) const { + return encodeChoice(index, 0, end, player2VariableBdds); } template - storm::dd::Bdd AbstractionInformation::encodeAux(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables) const { - return encodeChoice(index, offset, numberOfVariables, auxVariableBdds); + storm::dd::Bdd AbstractionInformation::encodeAux(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end) const { + return encodeChoice(index, start, end, auxVariableBdds); } template - storm::dd::Bdd AbstractionInformation::getPlayer2ZeroCube(uint_fast64_t numberOfVariables, uint_fast64_t offset) const { + storm::dd::Bdd AbstractionInformation::getPlayer2ZeroCube(uint_fast64_t start, uint_fast64_t end) const { storm::dd::Bdd result = ddManager->getBddOne(); - for (uint_fast64_t index = offset; index < numberOfVariables; ++index) { + for (uint_fast64_t index = start; index < end; ++index) { result &= player2VariableBdds[index]; } STORM_LOG_ASSERT(!result.isZero(), "Zero cube must not be zero."); @@ -205,8 +205,8 @@ namespace storm { } template - std::set AbstractionInformation::getAuxVariableSet(uint_fast64_t offset, uint_fast64_t count) const { - return std::set(auxVariables.begin() + offset, auxVariables.begin() + offset + count); + std::set AbstractionInformation::getAuxVariableSet(uint_fast64_t start, uint_fast64_t end) const { + return std::set(auxVariables.begin() + start, auxVariables.begin() + end); } template @@ -298,10 +298,9 @@ namespace storm { } template - storm::dd::Bdd AbstractionInformation::encodeChoice(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables, std::vector> const& variables) const { + storm::dd::Bdd AbstractionInformation::encodeChoice(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end, std::vector> const& variables) const { storm::dd::Bdd result = ddManager->getBddOne(); - numberOfVariables += offset; - for (uint_fast64_t bitIndex = numberOfVariables; bitIndex > offset; --bitIndex) { + for (uint_fast64_t bitIndex = end; bitIndex > start; --bitIndex) { if ((index & 1) != 0) { result &= variables[bitIndex - 1]; } else { diff --git a/src/abstraction/AbstractionInformation.h b/src/abstraction/AbstractionInformation.h index 2c076daae..fab9c1526 100644 --- a/src/abstraction/AbstractionInformation.h +++ b/src/abstraction/AbstractionInformation.h @@ -174,29 +174,29 @@ namespace storm { * Encodes the given index using the indicated player 1 variables. * * @param index The index to encode. - * @param numberOfVariables The number of variables to use for encoding the index. + * @param end The index of the variable past the end of the range that is used to encode the index. * @return The index encoded as a BDD. */ - storm::dd::Bdd encodePlayer1Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const; + storm::dd::Bdd encodePlayer1Choice(uint_fast64_t index, uint_fast64_t end) const; /*! * Encodes the given index using the indicated player 2 variables. * * @param index The index to encode. - * @param numberOfVariables The number of variables to use for encoding the index. + * @param end The index of the variable past the end of the range that is used to encode the index. * @return The index encoded as a BDD. */ - storm::dd::Bdd encodePlayer2Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const; + storm::dd::Bdd encodePlayer2Choice(uint_fast64_t index, uint_fast64_t end) const; /*! * Encodes the given index using the indicated probabilistic branching variables. * * @param index The index to encode. - * @param offset The offset within the auxiliary variables at which to start encoding. - * @param numberOfVariables The number of variables to use for encoding the index. + * @param start The index of the first variable of the range that is used to encode the index. + * @param end The index of the variable past the end of the range that is used to encode the index. * @return The index encoded as a BDD. */ - storm::dd::Bdd encodeAux(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables) const; + storm::dd::Bdd encodeAux(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end) const; /*! * Retrieves the cube of player 2 variables in the given range [offset, numberOfVariables). @@ -262,11 +262,11 @@ namespace storm { /*! * Retrieves the requested set of auxiliary variables. * - * @param offset The offset at which to start gatherin the auxiliary variables. - * @param count The number of auxiliary variables to include. + * @param start The index of the first auxiliary variable to include. + * @param end The index of the auxiliary variable past the end of the range to include. * @return The set of auxiliary variables. */ - std::set getAuxVariableSet(uint_fast64_t offset, uint_fast64_t count) const; + std::set getAuxVariableSet(uint_fast64_t start, uint_fast64_t end) const; /*! * Retrieves the number of auxiliary variables. @@ -356,11 +356,11 @@ namespace storm { * Encodes the given index with the given number of variables from the given variables. * * @param index The index to encode. - * @param offset The offset at which to start encoding. - * @param numberOfVariables The total number of variables to use. + * @param start The index of the first variable to use for the encoding. + * @param end The index of the variable past the end of the range to use for the encoding. * @param variables The BDDs of the variables to use to encode the index. */ - storm::dd::Bdd encodeChoice(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables, std::vector> const& variables) const; + storm::dd::Bdd encodeChoice(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end, std::vector> const& variables) const; // The expression related data. diff --git a/src/abstraction/BottomStateResult.cpp b/src/abstraction/BottomStateResult.cpp new file mode 100644 index 000000000..32b1417b7 --- /dev/null +++ b/src/abstraction/BottomStateResult.cpp @@ -0,0 +1,14 @@ +#include "src/abstraction/BottomStateResult.h" + +namespace storm { + namespace abstraction { + + template + BottomStateResult::BottomStateResult(storm::dd::Bdd const& states, storm::dd::Bdd const& transitions) : states(states), transitions(transitions) { + // Intentionally left empty. + } + + template class BottomStateResult; + template class BottomStateResult; + } +} \ No newline at end of file diff --git a/src/abstraction/BottomStateResult.h b/src/abstraction/BottomStateResult.h new file mode 100644 index 000000000..c3f2f69d4 --- /dev/null +++ b/src/abstraction/BottomStateResult.h @@ -0,0 +1,19 @@ +#pragma once + +#include "src/storage/dd/DdType.h" +#include "src/storage/dd/Bdd.h" + +namespace storm { + namespace abstraction { + + template + struct BottomStateResult { + public: + BottomStateResult(storm::dd::Bdd const& states, storm::dd::Bdd const& transitions); + + storm::dd::Bdd states; + storm::dd::Bdd transitions; + }; + + } +} \ No newline at end of file diff --git a/src/abstraction/MenuGame.cpp b/src/abstraction/MenuGame.cpp index 4ada7add8..10b8c2fe4 100644 --- a/src/abstraction/MenuGame.cpp +++ b/src/abstraction/MenuGame.cpp @@ -28,6 +28,7 @@ namespace storm { std::set const& probabilisticBranchingVariables, std::map> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame(manager, reachableStates, initialStates, deadlockStates, transitionMatrix.sumAbstract(probabilisticBranchingVariables), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), probabilisticBranchingVariables(probabilisticBranchingVariables), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) { // Intentionally left empty. + this->getTransitionMatrix().exportToDot("trans.dot"); } template diff --git a/src/abstraction/StateSetAbstractor.cpp b/src/abstraction/StateSetAbstractor.cpp index 97874d080..35bedcd73 100644 --- a/src/abstraction/StateSetAbstractor.cpp +++ b/src/abstraction/StateSetAbstractor.cpp @@ -125,6 +125,8 @@ namespace storm { // Create a new backtracking point before adding the constraint. smtSolver->push(); + constraint.template toAdd().exportToDot("constraint.dot"); + // Create the constraint. std::pair, std::unordered_map> result = constraint.toExpression(this->getAbstractionInformation().getExpressionManager()); diff --git a/src/abstraction/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp index ade2e85b7..723d67b41 100644 --- a/src/abstraction/prism/AbstractCommand.cpp +++ b/src/abstraction/prism/AbstractCommand.cpp @@ -3,6 +3,7 @@ #include #include "src/abstraction/AbstractionInformation.h" +#include "src/abstraction/BottomStateResult.h" #include "src/storage/dd/DdManager.h" #include "src/storage/dd/Add.h" @@ -17,7 +18,7 @@ namespace storm { namespace abstraction { namespace prism { template - 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) { + 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, 0), decisionVariables(), guardIsPredicate(guardIsPredicate), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, abstractionInformation.getExpressionVariables(), {!command.getGuardExpression()}, smtSolverFactory) { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates()); @@ -37,9 +38,6 @@ namespace storm { allPredicateIndices[index] = index; } this->refine(allPredicateIndices); - - // Refine the bottom state abstractor. - bottomStateAbstractor.refine(allPredicateIndices); } template @@ -97,8 +95,15 @@ namespace storm { // Finally, build overall result. storm::dd::Bdd resultBdd = this->getAbstractionInformation().getDdManager().getBddZero(); + if (!guardIsPredicate) { + abstractGuard = this->getAbstractionInformation().getDdManager().getBddZero(); + } uint_fast64_t sourceStateIndex = 0; for (auto const& sourceDistributionsPair : sourceToDistributionsMap) { + if (!guardIsPredicate) { + abstractGuard |= sourceDistributionsPair.first; + } + STORM_LOG_ASSERT(!sourceDistributionsPair.first.isZero(), "The source BDD must not be empty."); STORM_LOG_ASSERT(!sourceDistributionsPair.second.empty(), "The distributions must not be empty."); storm::dd::Bdd allDistributions = this->getAbstractionInformation().getDdManager().getBddZero(); @@ -236,7 +241,7 @@ namespace storm { } else { updateBdd &= !this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second); } - updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); + updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount()); } result |= updateBdd; @@ -275,7 +280,7 @@ namespace storm { } } - result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); + result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount()); } return result; } @@ -301,11 +306,32 @@ namespace storm { return cachedDd; } + template + BottomStateResult AbstractCommand::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { + BottomStateResult result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero()); + + // Use the state abstractor to compute the set of abstract states that has this command enabled but + // still has a transition to a bottom state. + bottomStateAbstractor.constrain(reachableStates && abstractGuard); + result.states = bottomStateAbstractor.getAbstractStates(); + + // Now equip all these states with an actual transition to a bottom state. + result.transitions = result.states && this->getAbstractionInformation().getAllPredicateIdentities(); + + // Add the command encoding and the next free player 2 encoding. + result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(cachedDd.nextFreePlayer2Index, cachedDd.numberOfPlayer2Variables); + + result.states.template toAdd().exportToDot("bottom_" + std::to_string(command.get().getGlobalIndex()) + ".dot"); + result.transitions.template toAdd().exportToDot("bottom_trans_" + std::to_string(command.get().getGlobalIndex()) + ".dot"); + + return result; + } + template storm::dd::Add AbstractCommand::getCommandUpdateProbabilitiesAdd() const { storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { - result += this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression())); + result += this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression())); } result *= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd(); return result; diff --git a/src/abstraction/prism/AbstractCommand.h b/src/abstraction/prism/AbstractCommand.h index 3000d6474..f972873e8 100644 --- a/src/abstraction/prism/AbstractCommand.h +++ b/src/abstraction/prism/AbstractCommand.h @@ -40,7 +40,10 @@ namespace storm { namespace abstraction { template class AbstractionInformation; - + + template + class BottomStateResult; + namespace prism { template struct GameBddResult; @@ -73,6 +76,15 @@ namespace storm { */ GameBddResult getAbstractBdd(); + /*! + * Retrieves the transitions to bottom states of this command. + * + * @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. + */ + BottomStateResult getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables); + /*! * Retrieves an ADD that maps the encoding of the command and its updates to their probabilities. * @@ -201,6 +213,10 @@ namespace storm { // is no need to compute bottom states. bool guardIsPredicate; + // The abstract guard of the command. This is only used if the guard is not a predicate, because it can + // then be used to constrain the bottom state abstractor. + storm::dd::Bdd abstractGuard; + // 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 46fc41da5..ee76febf4 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/BottomStateResult.h" #include "src/abstraction/prism/GameBddResult.h" #include "src/storage/dd/DdManager.h" @@ -50,11 +51,13 @@ namespace storm { } template - storm::dd::Bdd AbstractModule::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { - storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); + BottomStateResult AbstractModule::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { + BottomStateResult result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero()); for (auto& command : commands) { - result |= command.getBottomStateTransitions(reachableStates, numberOfPlayer2Variables); + BottomStateResult commandBottomStateResult = command.getBottomStateTransitions(reachableStates, numberOfPlayer2Variables); + result.states |= commandBottomStateResult.states; + result.transitions |= commandBottomStateResult.transitions; } return result; diff --git a/src/abstraction/prism/AbstractModule.h b/src/abstraction/prism/AbstractModule.h index 57f78aaf1..f8016ec61 100644 --- a/src/abstraction/prism/AbstractModule.h +++ b/src/abstraction/prism/AbstractModule.h @@ -17,12 +17,14 @@ namespace storm { namespace abstraction { template class AbstractionInformation; + + template + struct BottomStateResult; namespace prism { template struct GameBddResult; - template class AbstractModule { public: @@ -60,9 +62,9 @@ namespace storm { * * @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. + * @return The bottom states and the necessary transitions. */ - storm::dd::Bdd getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables); + BottomStateResult 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. diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index 9ca9dd9c5..c0fd0459b 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -1,5 +1,7 @@ #include "src/abstraction/prism/AbstractProgram.h" +#include "src/abstraction/BottomStateResult.h" + #include "src/storage/prism/Program.h" #include "src/storage/dd/DdManager.h" @@ -54,7 +56,7 @@ namespace storm { // NOTE: currently we assume that 100 player 2 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. - abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount)))); + abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount))) + 1); // Now that we have created all other DD variables, we create the DD variables for the predicates. std::vector allPredicateIndices; @@ -127,31 +129,18 @@ namespace storm { std::set variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount())); 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()); + auto auxVariables = abstractionInformation.getAuxVariableSet(1, abstractionInformation.getAuxVariableCount()); + variablesToAbstract.insert(auxVariables.begin(), auxVariables.end()); + std::cout << "vars" << std::endl; + for (auto const& var : auxVariables) { + std::cout << var.getName() << std::endl; + } // Do a reachability analysis on the raw transition relation. 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. - if (addedAllGuards) { - bottomStates = abstractionInformation.getDdManager().getBddZero(); - } else { - bottomStateAbstractor.constrain(reachableStates); - bottomStates = bottomStateAbstractor.getAbstractStates(); - } - // 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()); @@ -163,15 +152,22 @@ namespace storm { deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, game.numberOfPlayer2Variables) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd(); } + // Compute bottom states and the appropriate transitions if necessary. + BottomStateResult bottomStateResult(abstractionInformation.getDdManager().getBddZero(), abstractionInformation.getDdManager().getBddZero()); + if (!addedAllGuards) { + bottomStateResult = modules.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables); + } + // Construct the transition matrix by cutting away the transitions of unreachable states. - storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; + storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions;// + bottomStateResult.transitions.template toAdd(); + transitionMatrix.exportToDot("trans_upd.dot"); std::set usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + game.numberOfPlayer2Variables); std::set allNondeterminismVariables = usedPlayer2Variables; allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()); - return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStates, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables(), abstractionInformation.getSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, std::set(abstractionInformation.getAuxVariables().begin(), abstractionInformation.getAuxVariables().end()), abstractionInformation.getPredicateToBddMap()); + return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables(), abstractionInformation.getSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap()); } template diff --git a/src/abstraction/prism/GameBddResult.cpp b/src/abstraction/prism/GameBddResult.cpp index 01780ebcd..df22713d7 100644 --- a/src/abstraction/prism/GameBddResult.cpp +++ b/src/abstraction/prism/GameBddResult.cpp @@ -13,7 +13,9 @@ namespace storm { GameBddResult::GameBddResult(storm::dd::Bdd const& gameBdd, uint_fast64_t numberOfPlayer2Variables, uint_fast64_t nextFreePlayer2Index) : bdd(gameBdd), numberOfPlayer2Variables(numberOfPlayer2Variables), nextFreePlayer2Index(nextFreePlayer2Index) { // Intentionally left empty. } - + + template class GameBddResult; + template class GameBddResult; } } } \ No newline at end of file From e2ba3f3725c4e824fb097ebacd231a27f030442c Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 12 Aug 2016 23:12:16 +0200 Subject: [PATCH 4/6] bottom states appear to be working, tests not yet adapted Former-commit-id: 801d99c1281375891d782b0b2ae0c820e72d3440 --- src/abstraction/AbstractionInformation.cpp | 40 +++++++++++++++++++++ src/abstraction/AbstractionInformation.h | 41 ++++++++++++++++++++++ src/abstraction/prism/AbstractCommand.cpp | 18 +++++----- src/abstraction/prism/AbstractModule.cpp | 2 +- src/abstraction/prism/AbstractProgram.cpp | 32 ++++++++++++----- 5 files changed, 114 insertions(+), 19 deletions(-) diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp index a5500092b..d033be86b 100644 --- a/src/abstraction/AbstractionInformation.cpp +++ b/src/abstraction/AbstractionInformation.cpp @@ -152,6 +152,10 @@ namespace storm { auxVariableBdds.push_back(ddManager->getEncoding(newVariable, 1)); } STORM_LOG_DEBUG("Created " << auxVariableCount << " auxiliary variables."); + + bottomStateVariables = ddManager->addMetaVariable("bot"); + bottomStateBdds = std::make_pair(ddManager->getEncoding(bottomStateVariables.first, 1), ddManager->getEncoding(bottomStateVariables.second, 1)); + extendedPredicateDdVariables.push_back(bottomStateVariables); } template @@ -204,6 +208,11 @@ namespace storm { return auxVariables; } + template + storm::expressions::Variable const& AbstractionInformation::getAuxVariable(uint_fast64_t index) const { + return auxVariables[index]; + } + template std::set AbstractionInformation::getAuxVariableSet(uint_fast64_t start, uint_fast64_t end) const { return std::set(auxVariables.begin() + start, auxVariables.begin() + end); @@ -255,6 +264,37 @@ namespace storm { return predicateDdVariables; } + template + std::vector> const& AbstractionInformation::getExtendedSourceSuccessorVariablePairs() const { + return extendedPredicateDdVariables; + } + + template + storm::expressions::Variable const& AbstractionInformation::getBottomStateVariable(bool source) const { + if (source) { + return bottomStateVariables.first; + } else { + return bottomStateVariables.second; + } + } + + template + storm::dd::Bdd AbstractionInformation::getBottomStateBdd(bool source, bool negated) const { + if (source) { + if (negated) { + return !bottomStateBdds.first; + } else { + return bottomStateBdds.first; + } + } else { + if (negated) { + return !bottomStateBdds.second; + } else { + return bottomStateBdds.second; + } + } + } + template storm::dd::Bdd const& AbstractionInformation::encodePredicateAsSource(uint_fast64_t predicateIndex) const { return predicateBdds[predicateIndex].first; diff --git a/src/abstraction/AbstractionInformation.h b/src/abstraction/AbstractionInformation.h index fab9c1526..4be327e4e 100644 --- a/src/abstraction/AbstractionInformation.h +++ b/src/abstraction/AbstractionInformation.h @@ -258,6 +258,14 @@ namespace storm { * @return The meta variables associated with auxiliary information. */ std::vector const& getAuxVariables() const; + + /*! + * Retrieves the auxiliary variable with the given index. + * + * @param index The index of the auxiliary variable to retrieve. + * @return The auxiliary variable with the given index. + */ + storm::expressions::Variable const& getAuxVariable(uint_fast64_t index) const; /*! * Retrieves the requested set of auxiliary variables. @@ -309,6 +317,30 @@ namespace storm { * @return The meta variable pairs for all predicates. */ std::vector> const& getSourceSuccessorVariablePairs() const; + + /*! + * Retrieves the meta variables pairs for all predicates together with the meta variables marking the bottom states. + * + * @return The meta variable pairs for all predicates and bottom states. + */ + std::vector> const& getExtendedSourceSuccessorVariablePairs() const; + + /*! + * Retrieves the meta variable marking the bottom states. + * + * @param source A flag indicating whether the source or successor meta variable is to be returned. + * @return The meta variable marking the bottom states. + */ + storm::expressions::Variable const& getBottomStateVariable(bool source) const; + + /*! + * Retrieves the BDD that can be used to mark the bottom states. + * + * @param source A flag indicating whether the source or successor BDD is to be returned. + * @param negated A flag indicating whether the BDD should encode the bottom states or the non-bottom states. + * @return The BDD that can be used to mark bottom states. + */ + storm::dd::Bdd getBottomStateBdd(bool source, bool negated) const; /*! * Retrieves the BDD for the predicate with the given index over the source variables. @@ -388,6 +420,9 @@ namespace storm { /// The DD variables corresponding to the predicates. std::vector> predicateDdVariables; + /// The DD variables corresponding to the predicates together with the DD variables marking the bottom states. + std::vector> extendedPredicateDdVariables; + /// The set of all source variables. std::set sourceVariables; @@ -403,6 +438,12 @@ namespace storm { /// A BDD that represents the identity of all predicate variables. storm::dd::Bdd allPredicateIdentities; + /// A meta variable pair that marks bottom states. + std::pair bottomStateVariables; + + /// The BDDs associated with the bottom state variable pair. + std::pair, storm::dd::Bdd> bottomStateBdds; + /// A mapping from DD variable indices to the predicate index they represent. std::unordered_map ddVariableIndexToPredicateIndexMap; diff --git a/src/abstraction/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp index 723d67b41..071a3a9c0 100644 --- a/src/abstraction/prism/AbstractCommand.cpp +++ b/src/abstraction/prism/AbstractCommand.cpp @@ -90,7 +90,7 @@ namespace storm { } // We now compute how many variables we need to encode the choices. We add one to the maximal number of - // choices to + // choices to account for a possible transition to a bottom state. uint_fast64_t numberOfVariablesNeeded = static_cast(std::ceil(std::log2(maximalNumberOfChoices + 1))); // Finally, build overall result. @@ -241,7 +241,7 @@ namespace storm { } else { updateBdd &= !this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second); } - updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount()); + updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); } result |= updateBdd; @@ -280,7 +280,7 @@ namespace storm { } } - result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount()); + result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); } return result; } @@ -316,13 +316,13 @@ namespace storm { result.states = bottomStateAbstractor.getAbstractStates(); // Now equip all these states with an actual transition to a bottom state. - result.transitions = result.states && this->getAbstractionInformation().getAllPredicateIdentities(); + result.transitions = result.states && this->getAbstractionInformation().getAllPredicateIdentities() && this->getAbstractionInformation().getBottomStateBdd(false, false); - // Add the command encoding and the next free player 2 encoding. - result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(cachedDd.nextFreePlayer2Index, cachedDd.numberOfPlayer2Variables); + // Mark the states as bottom states. + result.states &= this->getAbstractionInformation().getBottomStateBdd(true, false); - result.states.template toAdd().exportToDot("bottom_" + std::to_string(command.get().getGlobalIndex()) + ".dot"); - result.transitions.template toAdd().exportToDot("bottom_trans_" + std::to_string(command.get().getGlobalIndex()) + ".dot"); + // Add the command encoding and the next free player 2 encoding. + result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(cachedDd.nextFreePlayer2Index, cachedDd.numberOfPlayer2Variables) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount()); return result; } @@ -331,7 +331,7 @@ namespace storm { storm::dd::Add AbstractCommand::getCommandUpdateProbabilitiesAdd() const { storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { - result += this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression())); + result += this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression())); } result *= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd(); return result; diff --git a/src/abstraction/prism/AbstractModule.cpp b/src/abstraction/prism/AbstractModule.cpp index ee76febf4..30a60928e 100644 --- a/src/abstraction/prism/AbstractModule.cpp +++ b/src/abstraction/prism/AbstractModule.cpp @@ -45,7 +45,7 @@ namespace storm { // 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.bdd && this->getAbstractionInformation().getPlayer2ZeroCube(maximalNumberOfUsedOptionVariables, commandDd.numberOfPlayer2Variables); + result |= commandDd.bdd && this->getAbstractionInformation().getPlayer2ZeroCube(commandDd.numberOfPlayer2Variables, maximalNumberOfUsedOptionVariables); } return GameBddResult(result, maximalNumberOfUsedOptionVariables, nextFreePlayer2Index); } diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index c0fd0459b..07b3078c8 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -56,7 +56,7 @@ namespace storm { // NOTE: currently we assume that 100 player 2 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. - abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount))) + 1); + abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount)))); // Now that we have created all other DD variables, we create the DD variables for the predicates. std::vector allPredicateIndices; @@ -129,12 +129,8 @@ namespace storm { std::set variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount())); auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables); variablesToAbstract.insert(player2Variables.begin(), player2Variables.end()); - auto auxVariables = abstractionInformation.getAuxVariableSet(1, abstractionInformation.getAuxVariableCount()); + auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount()); variablesToAbstract.insert(auxVariables.begin(), auxVariables.end()); - std::cout << "vars" << std::endl; - for (auto const& var : auxVariables) { - std::cout << var.getName() << std::endl; - } // Do a reachability analysis on the raw transition relation. storm::dd::Bdd transitionRelation = game.bdd.existsAbstract(variablesToAbstract); @@ -154,20 +150,38 @@ namespace storm { // Compute bottom states and the appropriate transitions if necessary. BottomStateResult bottomStateResult(abstractionInformation.getDdManager().getBddZero(), abstractionInformation.getDdManager().getBddZero()); + bool hasBottomStates = false; if (!addedAllGuards) { bottomStateResult = modules.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables); + hasBottomStates = !bottomStateResult.states.isZero(); } // Construct the transition matrix by cutting away the transitions of unreachable states. - storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions;// + bottomStateResult.transitions.template toAdd(); - transitionMatrix.exportToDot("trans_upd.dot"); + storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; + + // If there are bottom states, we need to mark all other states as non-bottom now. + if (hasBottomStates) { + transitionMatrix *= (abstractionInformation.getBottomStateBdd(true, true) && abstractionInformation.getBottomStateBdd(false, true)).template toAdd(); + transitionMatrix += bottomStateResult.transitions.template toAdd(); + reachableStates &= abstractionInformation.getBottomStateBdd(true, true); + reachableStates |= bottomStateResult.states; + } std::set usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + game.numberOfPlayer2Variables); std::set allNondeterminismVariables = usedPlayer2Variables; allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()); - return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables(), abstractionInformation.getSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap()); + std::set allSourceVariables(abstractionInformation.getSourceVariables()); + if (hasBottomStates) { + allSourceVariables.insert(abstractionInformation.getBottomStateVariable(true)); + } + std::set allSuccessorVariables(abstractionInformation.getSuccessorVariables()); + if (hasBottomStates) { + allSuccessorVariables.insert(abstractionInformation.getBottomStateVariable(false)); + } + + return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, hasBottomStates ? abstractionInformation.getExtendedSourceSuccessorVariablePairs() : abstractionInformation.getSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap()); } template From 9e64e998f37d95c488b499dbda11c2aaf05decbd Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 14 Aug 2016 20:21:40 +0200 Subject: [PATCH 5/6] fixed tests wrt. proper bottom state computation Former-commit-id: 223795c955ffbe53f45ed077a79982d3cb9851e1 --- src/abstraction/MenuGame.cpp | 1 - src/abstraction/StateSetAbstractor.cpp | 2 - .../abstraction/PrismMenuGameTest.cpp | 100 +++++++++--------- 3 files changed, 50 insertions(+), 53 deletions(-) diff --git a/src/abstraction/MenuGame.cpp b/src/abstraction/MenuGame.cpp index 10b8c2fe4..4ada7add8 100644 --- a/src/abstraction/MenuGame.cpp +++ b/src/abstraction/MenuGame.cpp @@ -28,7 +28,6 @@ namespace storm { std::set const& probabilisticBranchingVariables, std::map> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame(manager, reachableStates, initialStates, deadlockStates, transitionMatrix.sumAbstract(probabilisticBranchingVariables), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), probabilisticBranchingVariables(probabilisticBranchingVariables), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) { // Intentionally left empty. - this->getTransitionMatrix().exportToDot("trans.dot"); } template diff --git a/src/abstraction/StateSetAbstractor.cpp b/src/abstraction/StateSetAbstractor.cpp index 35bedcd73..97874d080 100644 --- a/src/abstraction/StateSetAbstractor.cpp +++ b/src/abstraction/StateSetAbstractor.cpp @@ -125,8 +125,6 @@ namespace storm { // Create a new backtracking point before adding the constraint. smtSolver->push(); - constraint.template toAdd().exportToDot("constraint.dot"); - // Create the constraint. std::pair, std::unordered_map> result = constraint.toExpression(this->getAbstractionInformation().getExpressionManager()); diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp index b3e26ce8f..35af85399 100644 --- a/test/functional/abstraction/PrismMenuGameTest.cpp +++ b/test/functional/abstraction/PrismMenuGameTest.cpp @@ -28,9 +28,9 @@ TEST(PrismMenuGame, DieAbstractionTest_Cudd) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(10, game.getNumberOfTransitions()); - EXPECT_EQ(2, game.getNumberOfStates()); - EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(26, game.getNumberOfTransitions()); + EXPECT_EQ(4, game.getNumberOfStates()); + EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, DieAbstractionTest_Sylvan) { @@ -45,9 +45,9 @@ TEST(PrismMenuGame, DieAbstractionTest_Sylvan) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(10, game.getNumberOfTransitions()); - EXPECT_EQ(2, game.getNumberOfStates()); - EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(26, game.getNumberOfTransitions()); + EXPECT_EQ(4, game.getNumberOfStates()); + EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) { @@ -64,9 +64,9 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(10, game.getNumberOfTransitions()); - EXPECT_EQ(3, game.getNumberOfStates()); - EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(24, game.getNumberOfTransitions()); + EXPECT_EQ(5, game.getNumberOfStates()); + EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) { @@ -83,9 +83,9 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(10, game.getNumberOfTransitions()); - EXPECT_EQ(3, game.getNumberOfStates()); - EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(24, game.getNumberOfTransitions()); + EXPECT_EQ(5, game.getNumberOfStates()); + EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) { @@ -165,9 +165,9 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(11, game.getNumberOfTransitions()); - EXPECT_EQ(2, game.getNumberOfStates()); - EXPECT_EQ(1, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(31, game.getNumberOfTransitions()); + EXPECT_EQ(4, game.getNumberOfStates()); + EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) { @@ -183,9 +183,9 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(11, game.getNumberOfTransitions()); - EXPECT_EQ(2, game.getNumberOfStates()); - EXPECT_EQ(1, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(31, game.getNumberOfTransitions()); + EXPECT_EQ(4, game.getNumberOfStates()); + EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) { @@ -203,9 +203,9 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(28, game.getNumberOfTransitions()); - EXPECT_EQ(4, game.getNumberOfStates()); - EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(84, game.getNumberOfTransitions()); + EXPECT_EQ(8, game.getNumberOfStates()); + EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) { @@ -223,9 +223,9 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(28, game.getNumberOfTransitions()); - EXPECT_EQ(4, game.getNumberOfStates()); - EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(84, game.getNumberOfTransitions()); + EXPECT_EQ(8, game.getNumberOfStates()); + EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) { @@ -297,7 +297,7 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) { EXPECT_EQ(15113, game.getNumberOfTransitions()); EXPECT_EQ(8607, game.getNumberOfStates()); - EXPECT_EQ(1260, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) { @@ -369,7 +369,7 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) { EXPECT_EQ(15113, game.getNumberOfTransitions()); EXPECT_EQ(8607, game.getNumberOfStates()); - EXPECT_EQ(1260, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) { @@ -387,9 +387,9 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(34, game.getNumberOfTransitions()); - EXPECT_EQ(4, game.getNumberOfStates()); - EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(90, game.getNumberOfTransitions()); + EXPECT_EQ(8, game.getNumberOfStates()); + EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) { @@ -407,9 +407,9 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(34, game.getNumberOfTransitions()); - EXPECT_EQ(4, game.getNumberOfStates()); - EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(90, game.getNumberOfTransitions()); + EXPECT_EQ(8, game.getNumberOfStates()); + EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) { @@ -429,9 +429,9 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(164, game.getNumberOfTransitions()); - EXPECT_EQ(8, game.getNumberOfStates()); - EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(324, game.getNumberOfTransitions()); + EXPECT_EQ(16, game.getNumberOfStates()); + EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) { @@ -451,9 +451,9 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(164, game.getNumberOfTransitions()); - EXPECT_EQ(8, game.getNumberOfStates()); - EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(324, game.getNumberOfTransitions()); + EXPECT_EQ(16, game.getNumberOfStates()); + EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) { @@ -574,9 +574,9 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(275, game.getNumberOfTransitions()); - EXPECT_EQ(4, game.getNumberOfStates()); - EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(2323, game.getNumberOfTransitions()); + EXPECT_EQ(12, game.getNumberOfStates()); + EXPECT_EQ(8, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) { @@ -595,9 +595,9 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(275, game.getNumberOfTransitions()); - EXPECT_EQ(4, game.getNumberOfStates()); - EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(2323, game.getNumberOfTransitions()); + EXPECT_EQ(12, game.getNumberOfStates()); + EXPECT_EQ(8, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) { @@ -618,9 +618,9 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(552, game.getNumberOfTransitions()); - EXPECT_EQ(8, game.getNumberOfStates()); - EXPECT_EQ(8, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(4600, game.getNumberOfTransitions()); + EXPECT_EQ(24, game.getNumberOfStates()); + EXPECT_EQ(16, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) { @@ -641,9 +641,9 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) { storm::abstraction::MenuGame game = abstractProgram.getAbstractGame(); - EXPECT_EQ(552, game.getNumberOfTransitions()); - EXPECT_EQ(8, game.getNumberOfStates()); - EXPECT_EQ(8, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(4600, game.getNumberOfTransitions()); + EXPECT_EQ(24, game.getNumberOfStates()); + EXPECT_EQ(16, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) { From f7f14f13fce2f12d83c694668a388512218bf2cb Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 14 Aug 2016 22:17:51 +0200 Subject: [PATCH 6/6] minor fix before bedtime Former-commit-id: c558c23122a0cd42a98b4626fdc7f7c8efba8ec7 --- .../abstraction/GameBasedMdpModelChecker.cpp | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 388ffcfa5..9b079d111 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -98,13 +98,18 @@ namespace storm { game.getTransitionMatrix().exportToDot("trans.dot"); bottomStatesBdd.template toAdd().exportToDot("bottom.dot"); - // Start by computing the states with probability 0/1 for the case in which player 2 minimizes. - storm::utility::graph::GameProb01Result prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), game.getStates(targetStateExpression), player1Direction, storm::OptimizationDirection::Minimize, true); - storm::utility::graph::GameProb01Result prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), game.getStates(targetStateExpression), player1Direction, storm::OptimizationDirection::Minimize, true); + storm::dd::Bdd targetStates = game.getStates(targetStateExpression); + if (player1Direction == storm::OptimizationDirection::Minimize) { + targetStates |= game.getBottomStates(); + } + + // Start by computing the states with probability 0/1 when player 2 minimizes. + storm::utility::graph::GameProb01Result prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, true); + storm::utility::graph::GameProb01Result prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, true); - // Now compute the states with probability 0/1 for the case in which player 2 maximizes. - storm::utility::graph::GameProb01Result prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), game.getStates(targetStateExpression), player1Direction, storm::OptimizationDirection::Maximize, true); - storm::utility::graph::GameProb01Result prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), game.getStates(targetStateExpression), player1Direction, storm::OptimizationDirection::Maximize, true); + // Now compute the states with probability 0/1 when player 2 maximizes. + storm::utility::graph::GameProb01Result prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true); + storm::utility::graph::GameProb01Result prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true); STORM_LOG_DEBUG("Min: " << prob0Min.states.getNonZeroCount() << " no states, " << prob1Min.states.getNonZeroCount() << " yes states."); STORM_LOG_DEBUG("Max: " << prob0Max.states.getNonZeroCount() << " no states, " << prob1Max.states.getNonZeroCount() << " yes states.");