From 1280c88b4f6c95ec3008479272245776f65f3568 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 10 Aug 2016 21:21:12 +0200 Subject: [PATCH] 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