diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp index 6af114592..7efb46245 100644 --- a/src/abstraction/AbstractionInformation.cpp +++ b/src/abstraction/AbstractionInformation.cpp @@ -132,50 +132,54 @@ 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."); + + bottomStateVariables = ddManager->addMetaVariable("bot"); + bottomStateBdds = std::make_pair(ddManager->getEncoding(bottomStateVariables.first, 1), ddManager->getEncoding(bottomStateVariables.second, 1)); + extendedPredicateDdVariables.push_back(bottomStateVariables); } template - storm::dd::Bdd AbstractionInformation::encodePlayer1Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const { - return encodeChoice(index, 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, 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::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 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."); @@ -203,13 +207,18 @@ 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); + 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); } template @@ -238,8 +247,8 @@ namespace storm { } template - std::size_t AbstractionInformation::getProbabilisticBranchingVariableCount() const { - return probabilisticBranchingVariables.size(); + std::size_t AbstractionInformation::getAuxVariableCount() const { + return auxVariables.size(); } template @@ -258,6 +267,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; @@ -301,13 +341,13 @@ 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 start, uint_fast64_t end, std::vector> const& variables) const { storm::dd::Bdd result = ddManager->getBddOne(); - for (uint_fast64_t bitIndex = 0; bitIndex < numberOfVariables; ++bitIndex) { + for (uint_fast64_t bitIndex = end; bitIndex > start; --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 ebad0817a..ea3a7e0dc 100644 --- a/src/abstraction/AbstractionInformation.h +++ b/src/abstraction/AbstractionInformation.h @@ -163,40 +163,41 @@ 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. * * @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 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 encodeProbabilisticChoice(uint_fast64_t index, 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). @@ -253,26 +254,35 @@ 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 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 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 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 getProbabilisticBranchingVariableSet(uint_fast64_t count) const; + std::set getAuxVariableSet(uint_fast64_t start, uint_fast64_t end) 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. @@ -308,6 +318,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. @@ -355,10 +389,11 @@ namespace storm { * Encodes the given index with the given number of variables from the given variables. * * @param index The index to encode. - * @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 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. @@ -386,6 +421,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; @@ -401,6 +439,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; @@ -416,11 +460,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/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/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp index a394b83cc..7d6387b6f 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" @@ -20,7 +21,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, 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()); @@ -28,6 +29,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. @@ -40,7 +42,7 @@ namespace storm { } this->refine(allPredicateIndices); } - + template void AbstractCommand::refine(std::vector const& predicates) { // Add all predicates to the variable partition. @@ -58,7 +60,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); @@ -66,6 +68,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 @@ -86,12 +92,21 @@ 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 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. 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(); @@ -111,7 +126,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 @@ -229,7 +244,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; @@ -268,7 +283,7 @@ namespace storm { } } - result |= updateIdentity && this->getAbstractionInformation().encodeProbabilisticChoice(updateIndex, this->getAbstractionInformation().getProbabilisticBranchingVariableCount()); + result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); } return result; } @@ -290,15 +305,36 @@ namespace storm { } template - std::pair, uint_fast64_t> AbstractCommand::getAbstractBdd() { + GameBddResult AbstractCommand::getAbstractBdd() { 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() && this->getAbstractionInformation().getBottomStateBdd(false, false); + + // Mark the states as bottom states. + result.states &= this->getAbstractionInformation().getBottomStateBdd(true, 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) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount()); + + 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().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/AbstractCommand.h b/src/abstraction/prism/AbstractCommand.h index 97f4d464c..f972873e8 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" @@ -38,8 +40,14 @@ namespace storm { namespace abstraction { template class AbstractionInformation; - + + template + class BottomStateResult; + namespace prism { + template + struct GameBddResult; + template class AbstractCommand { public: @@ -49,8 +57,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,8 +74,17 @@ 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 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. * @@ -186,10 +204,21 @@ 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; + + // 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 7bd8e0f97..655ffb6e5 100644 --- a/src/abstraction/prism/AbstractModule.cpp +++ b/src/abstraction/prism/AbstractModule.cpp @@ -1,6 +1,8 @@ #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" #include "src/storage/dd/Add.h" @@ -15,11 +17,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); } } @@ -31,22 +33,37 @@ 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(commandDd.numberOfPlayer2Variables, maximalNumberOfUsedOptionVariables); } - return std::make_pair(result, maximalNumberOfUsedOptionVariables); + return GameBddResult(result, maximalNumberOfUsedOptionVariables, nextFreePlayer2Index); + } + + template + 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) { + BottomStateResult commandBottomStateResult = command.getBottomStateTransitions(reachableStates, numberOfPlayer2Variables); + result.states |= commandBottomStateResult.states; + result.transitions |= commandBottomStateResult.transitions; + } + + return result; } template diff --git a/src/abstraction/prism/AbstractModule.h b/src/abstraction/prism/AbstractModule.h index 28428e2f1..f8016ec61 100644 --- a/src/abstraction/prism/AbstractModule.h +++ b/src/abstraction/prism/AbstractModule.h @@ -17,8 +17,14 @@ namespace storm { namespace abstraction { template class AbstractionInformation; + + template + struct BottomStateResult; namespace prism { + template + struct GameBddResult; + template class AbstractModule { public: @@ -28,8 +34,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 +55,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 states and the necessary transitions. + */ + 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. @@ -66,7 +82,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 97695f133..61dadc76f 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" @@ -24,7 +26,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. @@ -37,7 +39,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; @@ -73,12 +74,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(); @@ -106,10 +106,7 @@ namespace storm { // Refine initial state abstractor. initialStateAbstractor.refine(newPredicateIndices); - - // Refine bottom state abstractor. - bottomStateAbstractor.refine(newPredicateIndices); - + // Finally, we rebuild the game. currentGame = buildGame(); } @@ -129,48 +126,65 @@ 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.getProbabilisticBranchingVariableSet(abstractionInformation.getProbabilisticBranchingVariableCount()); - variablesToAbstract.insert(probBranchingVariables.begin(), probBranchingVariables.end()); + auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount()); + variablesToAbstract.insert(auxVariables.begin(), auxVariables.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); - // Determine the bottom states. - storm::dd::Bdd bottomStates; - if (addedAllGuards) { - bottomStates = abstractionInformation.getDdManager().getBddZero(); - } else { - bottomStateAbstractor.constrain(reachableStates); - 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.encodeProbabilisticChoice(0, abstractionInformation.getProbabilisticBranchingVariableCount())).template toAdd(); + 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()); + 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 = (gameBdd.first && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; + 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() + 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()); - 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()); + 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 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..df22713d7 --- /dev/null +++ b/src/abstraction/prism/GameBddResult.cpp @@ -0,0 +1,21 @@ +#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. + } + + template class GameBddResult; + template class GameBddResult; + } + } +} \ 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 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."); diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp index 246d8a167..397213e68 100644 --- a/test/functional/abstraction/PrismMenuGameTest.cpp +++ b/test/functional/abstraction/PrismMenuGameTest.cpp @@ -30,9 +30,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) { @@ -47,9 +47,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()); } #ifdef STORM_HAVE_CARL @@ -85,9 +85,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) { @@ -104,9 +104,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) { @@ -186,9 +186,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) { @@ -204,9 +204,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) { @@ -224,9 +224,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) { @@ -244,9 +244,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) { @@ -318,7 +318,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) { @@ -390,7 +390,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) { @@ -408,9 +408,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) { @@ -428,9 +428,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) { @@ -450,9 +450,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) { @@ -472,9 +472,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) { @@ -595,9 +595,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) { @@ -616,9 +616,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) { @@ -639,9 +639,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) { @@ -662,9 +662,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) {