diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c index b9f6a7db9..9643cbfaa 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c +++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c @@ -542,15 +542,12 @@ cuddBddExistAbstractRepresentativeRecur( if (cube == one) { // printf("return in preprocessing...\n"); return one; - } else { -// printf("return in preprocessing...\n"); - return cube; } } else if (cube == one) { // printf("return in preprocessing...\n"); return f; } - /* From now on, f and cube are non-constant. */ + /* From now on, cube is non-constant, but f might be constant. */ // printf("F perm %i and cube perm %i\n", manager->perm[F->index], manager->perm[cube->index]); @@ -591,27 +588,10 @@ cuddBddExistAbstractRepresentativeRecur( /* If the two indices are the same, so are their levels. */ if (F->index == cube->index) { -// if (E == one) { -// cuddRef(zero); -// cuddRef(cuddT(cube)); -// res1 = cuddUniqueInter(manager, (int) F->index, zero, cuddT(cube)); -// cuddDeref(zero); -// cuddDeref(cuddT(cube)); -// return res1; -// } else if (T == one) { -// cuddRef(zero); -// cuddRef(cuddT(cube)); -// res1 = cuddUniqueInter(manager, (int) F->index, cuddT(cube), zero); -// cuddDeref(zero); -// cuddDeref(cuddT(cube)); -// return res1; -// } - res1 = cuddBddExistAbstractRepresentativeRecur(manager, E, cuddT(cube)); if (res1 == NULL) { return(NULL); } - // FIXME if (res1 == one) { if (F->ref != 1) { cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, Cudd_Not(cube)); diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp index 97f3d46f4..8e0d44def 100644 --- a/src/abstraction/AbstractionInformation.cpp +++ b/src/abstraction/AbstractionInformation.cpp @@ -57,6 +57,7 @@ namespace storm { allPredicateIdentities &= predicateIdentities.back(); sourceVariables.insert(newMetaVariable.first); successorVariables.insert(newMetaVariable.second); + orderedSuccessorVariables.push_back(newMetaVariable.second); ddVariableIndexToPredicateIndexMap[predicateIdentities.back().getIndex()] = predicateIndex; return predicateIndex; } @@ -122,6 +123,11 @@ namespace storm { return predicateBdds[indexIt->second].first; } + template + bool AbstractionInformation::hasPredicate(storm::expressions::Expression const& predicate) const { + return predicateToIndexMap.find(predicate) != predicateToIndexMap.end(); + } + template std::size_t AbstractionInformation::getNumberOfPredicates() const { return predicates.size(); @@ -167,16 +173,31 @@ namespace storm { return encodeChoice(index, 0, end, player1VariableBdds); } + template + uint_fast64_t AbstractionInformation::decodePlayer1Choice(storm::expressions::Valuation const& valuation, uint_fast64_t end) const { + return decodeChoice(valuation, 0, end, player1Variables); + } + template storm::dd::Bdd AbstractionInformation::encodePlayer2Choice(uint_fast64_t index, uint_fast64_t end) const { return encodeChoice(index, 0, end, player2VariableBdds); } - + + template + uint_fast64_t AbstractionInformation::decodePlayer2Choice(storm::expressions::Valuation const& valuation, uint_fast64_t end) const { + return decodeChoice(valuation, 0, end, player2Variables); + } + template 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 + uint_fast64_t AbstractionInformation::decodeAux(storm::expressions::Valuation const& valuation, uint_fast64_t start, uint_fast64_t end) const { + return decodeChoice(valuation, start, end, auxVariables); + } + template storm::dd::Bdd AbstractionInformation::getPlayer2ZeroCube(uint_fast64_t start, uint_fast64_t end) const { storm::dd::Bdd result = ddManager->getBddOne(); @@ -232,6 +253,11 @@ namespace storm { return successorVariables; } + template + std::vector const& AbstractionInformation::getOrderedSuccessorVariables() const { + return orderedSuccessorVariables; + } + template storm::dd::Bdd const& AbstractionInformation::getAllPredicateIdentities() const { return allPredicateIdentities; @@ -356,6 +382,18 @@ namespace storm { return result; } + template + uint_fast64_t AbstractionInformation::decodeChoice(storm::expressions::Valuation const& valuation, uint_fast64_t start, uint_fast64_t end, std::vector const& variables) const { + uint_fast64_t result = 0; + for (uint_fast64_t variableIndex = start; variableIndex < end; ++variableIndex) { + result <<= 1; + if (valuation.getBooleanValue(variables[variableIndex])) { + result |= 1; + } + } + return result; + } + template class AbstractionInformation; template class AbstractionInformation; } diff --git a/src/abstraction/AbstractionInformation.h b/src/abstraction/AbstractionInformation.h index ea3a7e0dc..dcd35f52c 100644 --- a/src/abstraction/AbstractionInformation.h +++ b/src/abstraction/AbstractionInformation.h @@ -148,6 +148,13 @@ namespace storm { */ storm::dd::Bdd getPredicateSourceVariable(storm::expressions::Expression const& predicate) const; + /*! + * Determines whether the given predicate is in the set of known predicates. + * + * @param predicate The predicate for which to query membership. + */ + bool hasPredicate(storm::expressions::Expression const& predicate) const; + /*! * Retrieves the number of predicates. * @@ -180,6 +187,15 @@ namespace storm { */ storm::dd::Bdd encodePlayer1Choice(uint_fast64_t index, uint_fast64_t end) const; + /*! + * Decodes the player 1 choice in the given valuation. + * + * @param valuation The valuation to decode. + * @param end The index of the variable past the end of the range that is used to encode the index. + * @return The decoded player 1 choice. + */ + uint_fast64_t decodePlayer1Choice(storm::expressions::Valuation const& valuation, uint_fast64_t end) const; + /*! * Encodes the given index using the indicated player 2 variables. * @@ -190,7 +206,16 @@ namespace storm { storm::dd::Bdd encodePlayer2Choice(uint_fast64_t index, uint_fast64_t end) const; /*! - * Encodes the given index using the indicated probabilistic branching variables. + * Decodes the player 2 choice in the given valuation. + * + * @param valuation The valuation to decode. + * @param end The index of the variable past the end of the range that is used to encode the index. + * @return The decoded player 2 choice. + */ + uint_fast64_t decodePlayer2Choice(storm::expressions::Valuation const& valuation, uint_fast64_t end) const; + + /*! + * Encodes the given index using the indicated auxiliary variables. * * @param index The index to encode. * @param start The index of the first variable of the range that is used to encode the index. @@ -199,6 +224,16 @@ namespace storm { */ storm::dd::Bdd encodeAux(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end) const; + /*! + * Decodes the auxiliary index in the given valuation. + * + * @param valuation The valuation to decode. + * @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 decoded auxiliary index. + */ + uint_fast64_t decodeAux(storm::expressions::Valuation const& valuation, uint_fast64_t start, uint_fast64_t end) const; + /*! * Retrieves the cube of player 2 variables in the given range [offset, numberOfVariables). * @@ -298,6 +333,13 @@ namespace storm { */ std::set const& getSuccessorVariables() const; + /*! + * Retrieves the ordered collection of successor meta variables. + * + * @return All successor meta variables. + */ + std::vector const& getOrderedSuccessorVariables() const; + /*! * Retrieves a BDD representing the identities of all predicates. * @@ -392,16 +434,27 @@ namespace storm { * @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. + * @return The BDD encoding the index. */ storm::dd::Bdd encodeChoice(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end, std::vector> const& variables) const; - + + /*! + * Decodes the index encoded in the valuation using the given variables. + * + * @param valuation The valuation to decode. + * @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 variables used to encode the index. + * @return The encoded index. + */ + uint_fast64_t decodeChoice(storm::expressions::Valuation const& valuation, uint_fast64_t start, uint_fast64_t end, std::vector const& variables) const; + // The expression related data. /// The manager responsible for the expressions of the program and the SMT solvers. std::reference_wrapper expressionManager; /// A mapping from predicates to their indices in the predicate list. - // FIXME: Does this properly store the expressions? What about equality checking? std::unordered_map predicateToIndexMap; /// The current set of predicates used in the abstraction. @@ -427,9 +480,12 @@ namespace storm { /// The set of all source variables. std::set sourceVariables; - /// The set of all source variables. + /// The set of all successor variables. std::set successorVariables; + /// An ordered collection of the successor variables. + std::vector orderedSuccessorVariables; + /// The BDDs corresponding to the predicates. std::vector, storm::dd::Bdd>> predicateBdds; diff --git a/src/abstraction/MenuGame.cpp b/src/abstraction/MenuGame.cpp index be65510fd..82ad3ebfe 100644 --- a/src/abstraction/MenuGame.cpp +++ b/src/abstraction/MenuGame.cpp @@ -29,7 +29,7 @@ namespace storm { std::set const& player2Variables, std::set const& allNondeterminismVariables, 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) { + std::map> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame(manager, reachableStates, initialStates, deadlockStates, transitionMatrix.sumAbstract(probabilisticBranchingVariables), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), extendedTransitionMatrix(transitionMatrix), probabilisticBranchingVariables(probabilisticBranchingVariables), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) { // Intentionally left empty. } @@ -64,6 +64,16 @@ namespace storm { return bottomStates; } + template + storm::dd::Add const& MenuGame::getExtendedTransitionMatrix() const { + return extendedTransitionMatrix; + } + + template + std::set const& MenuGame::getProbabilisticBranchingVariables() const { + return probabilisticBranchingVariables; + } + template bool MenuGame::hasLabel(std::string const& label) const { return false; diff --git a/src/abstraction/MenuGame.h b/src/abstraction/MenuGame.h index 3b192881b..e559632b1 100644 --- a/src/abstraction/MenuGame.h +++ b/src/abstraction/MenuGame.h @@ -84,9 +84,28 @@ namespace storm { */ storm::dd::Bdd getBottomStates() const; + /*! + * Retrieves the transition matrix extended by variables that encode additional information for the + * probabilistic branching. + * + * @reutrn Th extended transition matrix. + */ + storm::dd::Add const& getExtendedTransitionMatrix() const; + + /*! + * Retrieves the variables used to encode additional information for the probabilistic branching in the + * extended transition matrix. + * + * @return The probabilistic branching variables. + */ + std::set const& getProbabilisticBranchingVariables() const; + virtual bool hasLabel(std::string const& label) const override; private: + // The transition relation extended byt the probabilistic branching variables. + storm::dd::Add extendedTransitionMatrix; + // The meta variables used to probabilistic branching. std::set probabilisticBranchingVariables; diff --git a/src/abstraction/MenuGameAbstractor.h b/src/abstraction/MenuGameAbstractor.h index 98ba1fb9c..f144ce82b 100644 --- a/src/abstraction/MenuGameAbstractor.h +++ b/src/abstraction/MenuGameAbstractor.h @@ -12,6 +12,7 @@ namespace storm { public: virtual storm::abstraction::MenuGame abstract() = 0; virtual void refine(std::vector const& predicates) = 0; + virtual void refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) = 0; }; } diff --git a/src/abstraction/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp index 7d6387b6f..a600f1792 100644 --- a/src/abstraction/prism/AbstractCommand.cpp +++ b/src/abstraction/prism/AbstractCommand.cpp @@ -340,6 +340,16 @@ namespace storm { return result; } + template + storm::prism::Command const& AbstractCommand::getConcreteCommand() const { + return command.get(); + } + + template + void AbstractCommand::notifyGuardIsPredicate() { + guardIsPredicate = true; + } + template AbstractionInformation const& AbstractCommand::getAbstractionInformation() const { return abstractionInformation.get(); diff --git a/src/abstraction/prism/AbstractCommand.h b/src/abstraction/prism/AbstractCommand.h index f972873e8..d8b1434d2 100644 --- a/src/abstraction/prism/AbstractCommand.h +++ b/src/abstraction/prism/AbstractCommand.h @@ -92,6 +92,19 @@ namespace storm { */ storm::dd::Add getCommandUpdateProbabilitiesAdd() const; + /*! + * Retrieves the concrete command that is abstracted by this abstract command. + * + * @return The concrete command. + */ + storm::prism::Command const& getConcreteCommand() const; + + /*! + * Notifies this abstract command that its guard is now a predicate. This affects the computation of the + * bottom states. + */ + void notifyGuardIsPredicate(); + private: /*! * Determines the relevant predicates for source as well as successor states wrt. to the given assignments diff --git a/src/abstraction/prism/AbstractModule.cpp b/src/abstraction/prism/AbstractModule.cpp index 655ffb6e5..bd2d42d32 100644 --- a/src/abstraction/prism/AbstractModule.cpp +++ b/src/abstraction/prism/AbstractModule.cpp @@ -75,6 +75,16 @@ namespace storm { return result; } + template + std::vector> const& AbstractModule::getCommands() const { + return commands; + } + + template + std::vector>& AbstractModule::getCommands() { + return commands; + } + template AbstractionInformation const& AbstractModule::getAbstractionInformation() const { return abstractionInformation.get(); diff --git a/src/abstraction/prism/AbstractModule.h b/src/abstraction/prism/AbstractModule.h index f8016ec61..bc885194c 100644 --- a/src/abstraction/prism/AbstractModule.h +++ b/src/abstraction/prism/AbstractModule.h @@ -73,6 +73,20 @@ namespace storm { */ storm::dd::Add getCommandUpdateProbabilitiesAdd() const; + /*! + * Retrieves the abstract commands of this abstract module. + * + * @return The abstract commands. + */ + std::vector> const& getCommands() const; + + /*! + * Retrieves the abstract commands of this abstract module. + * + * @return The abstract commands. + */ + std::vector>& getCommands(); + private: /*! * Retrieves the abstraction information. diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index b760dbcdc..c68269870 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -2,6 +2,8 @@ #include "src/abstraction/BottomStateResult.h" +#include "src/storage/BitVector.h" + #include "src/storage/prism/Program.h" #include "src/storage/dd/DdManager.h" @@ -9,6 +11,7 @@ #include "src/models/symbolic/StandardRewardModel.h" +#include "src/utility/dd.h" #include "src/utility/macros.h" #include "src/utility/solver.h" #include "src/exceptions/WrongFormatException.h" @@ -111,6 +114,83 @@ namespace storm { currentGame = buildGame(); } + template + std::map AbstractProgram::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const { + std::map result; + + storm::dd::Add lowerChoiceAsAdd = choice.template toAdd(); + for (auto const& successorValuePair : lowerChoiceAsAdd) { + uint_fast64_t updateIndex = abstractionInformation.decodeAux(successorValuePair.first, 0, currentGame->getProbabilisticBranchingVariables().size()); + + storm::storage::BitVector successor(abstractionInformation.getNumberOfPredicates()); + for (uint_fast64_t index = 0; index < abstractionInformation.getOrderedSuccessorVariables().size(); ++index) { + auto const& successorVariable = abstractionInformation.getOrderedSuccessorVariables()[index]; + if (successorValuePair.first.getBooleanValue(successorVariable)) { + successor.set(index); + } + } + + result[updateIndex] = successor; + } + return result; + } + + template + void AbstractProgram::refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) { + // Decode the index of the command chosen by player 1. + storm::dd::Add player1ChoiceAsAdd = player1Choice.template toAdd(); + auto pl1It = player1ChoiceAsAdd.begin(); + uint_fast64_t commandIndex = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount()); + storm::abstraction::prism::AbstractCommand& abstractCommand = modules.front().getCommands()[commandIndex]; + storm::prism::Command const& concreteCommand = abstractCommand.getConcreteCommand(); + + // Check whether there are bottom states in the game and whether one of the choices actually picks the + // bottom state as the successor. + bool buttomStateSuccessor = false; + if (!currentGame->getBottomStates().isZero()) { + buttomStateSuccessor = !((abstractionInformation.getBottomStateBdd(false, false) && lowerChoice) || (abstractionInformation.getBottomStateBdd(false, false) && upperChoice)).isZero(); + } + + // If one of the choices picks the bottom state, the new predicate is based on the guard of the appropriate + // command (that is the player 1 choice). + if (buttomStateSuccessor) { + STORM_LOG_DEBUG("One of the successors is a bottom state, taking a guard as a new predicate."); + abstractCommand.notifyGuardIsPredicate(); + storm::expressions::Expression newPredicate = concreteCommand.getGuardExpression(); + STORM_LOG_DEBUG("Derived new predicate: " << newPredicate); + this->refine({newPredicate}); + } else { + STORM_LOG_DEBUG("No bottom state successor. Deriving a new predicate using weakest precondition."); + + // Decode both choices to explicit mappings. + std::map lowerChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(lowerChoice); + std::map upperChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(upperChoice); + STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode."); + + // Now go through the mappings and find points of deviation. Currently, we take the first deviation. + storm::expressions::Expression newPredicate; + auto lowerIt = lowerChoiceUpdateToSuccessorMapping.begin(); + auto lowerIte = lowerChoiceUpdateToSuccessorMapping.end(); + auto upperIt = upperChoiceUpdateToSuccessorMapping.begin(); + for (; lowerIt != lowerIte; ++lowerIt, ++upperIt) { + STORM_LOG_ASSERT(lowerIt->first == upperIt->first, "Update indices mismatch."); + uint_fast64_t updateIndex = lowerIt->first; + bool deviates = lowerIt->second != upperIt->second; + if (deviates) { + for (uint_fast64_t predicateIndex = 0; predicateIndex < lowerIt->second.size(); ++predicateIndex) { + if (lowerIt->second.get(predicateIndex) != upperIt->second.get(predicateIndex)) { + // Now we know the point of the deviation (command, update, predicate). + newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap()); + break; + } + } + } + } + + this->refine({newPredicate}); + } + } + template MenuGame AbstractProgram::getAbstractGame() { STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); @@ -138,7 +218,7 @@ namespace storm { // 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 reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); // 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. @@ -167,6 +247,7 @@ namespace storm { transitionMatrix *= (abstractionInformation.getBottomStateBdd(true, true) && abstractionInformation.getBottomStateBdd(false, true)).template toAdd(); transitionMatrix += bottomStateResult.transitions.template toAdd(); reachableStates &= abstractionInformation.getBottomStateBdd(true, true); + initialStates &= abstractionInformation.getBottomStateBdd(true, true); reachableStates |= bottomStateResult.states; } @@ -186,25 +267,7 @@ namespace storm { 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 - storm::dd::Bdd AbstractProgram::getReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitionRelation) { - storm::dd::Bdd frontier = initialStates; - - storm::dd::Bdd reachableStates = initialStates; - uint_fast64_t reachabilityIteration = 0; - while (!frontier.isZero()) { - ++reachabilityIteration; - frontier = frontier.andExists(transitionRelation, abstractionInformation.getSourceVariables()); - frontier = frontier.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs()); - frontier &= !reachableStates; - reachableStates |= frontier; - STORM_LOG_TRACE("Iteration " << reachabilityIteration << " of reachability analysis."); - } - - return reachableStates; - } - + template void AbstractProgram::exportToDot(std::string const& filename) const { std::ofstream out(filename); @@ -244,13 +307,7 @@ namespace storm { stateName << "0"; } } - uint_fast64_t index = 0; - for (uint_fast64_t player1VariableIndex = 0; player1VariableIndex < abstractionInformation.getPlayer1VariableCount(); ++player1VariableIndex) { - index <<= 1; - if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer1Variables()[player1VariableIndex])) { - index |= 1; - } - } + uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); out << stateName.str() << "_" << index; out << " [ shape=\"square\", width=0, height=0, margin=0, label=\"" << index << "\" ];" << std::endl; out << "\tpl1_" << stateName.str() << " -> " << "pl2_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; @@ -268,21 +325,9 @@ namespace storm { stateName << "0"; } } - uint_fast64_t index = 0; - for (uint_fast64_t player1VariableIndex = 0; player1VariableIndex < abstractionInformation.getPlayer1VariableCount(); ++player1VariableIndex) { - index <<= 1; - if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer1Variables()[player1VariableIndex])) { - index |= 1; - } - } + uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); stateName << "_" << index; - index = 0; - for (uint_fast64_t player2VariableIndex = 0; player2VariableIndex < currentGame->getPlayer2Variables().size(); ++player2VariableIndex) { - index <<= 1; - if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer2Variables()[player2VariableIndex])) { - index |= 1; - } - } + index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size()); out << stateName.str() << "_" << index; out << " [ shape=\"point\", label=\"\" ];" << std::endl; out << "\tpl2_" << stateName.str() << " -> " << "plp_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; @@ -305,20 +350,8 @@ namespace storm { successorStateName << "0"; } } - uint_fast64_t pl1Index = 0; - for (uint_fast64_t player1VariableIndex = 0; player1VariableIndex < abstractionInformation.getPlayer1VariableCount(); ++player1VariableIndex) { - pl1Index <<= 1; - if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer1Variables()[player1VariableIndex])) { - pl1Index |= 1; - } - } - uint_fast64_t pl2Index = 0; - for (uint_fast64_t player2VariableIndex = 0; player2VariableIndex < currentGame->getPlayer2Variables().size(); ++player2VariableIndex) { - pl2Index <<= 1; - if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer2Variables()[player2VariableIndex])) { - pl2Index |= 1; - } - } + uint_fast64_t pl1Index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); + uint_fast64_t pl2Index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size()); out << "\tplp_" << sourceStateName.str() << "_" << pl1Index << "_" << pl2Index << " -> pl1_" << successorStateName.str() << " [ label=\"" << stateValue.second << "\"];" << std::endl; } diff --git a/src/abstraction/prism/AbstractProgram.h b/src/abstraction/prism/AbstractProgram.h index ec33b3135..8ee848946 100644 --- a/src/abstraction/prism/AbstractProgram.h +++ b/src/abstraction/prism/AbstractProgram.h @@ -75,23 +75,24 @@ namespace storm { void refine(std::vector const& predicates); /*! - * Exports the current state of the abstraction in the dot format to the given file. + * Refines the abstract program using the pivot state, and player 1 choice. The refinement guarantees that + * the two provided choices are not possible from the same pivot state using the given player 1 choice. * - * @param filename The name of the file to which to write the dot output. + * @param pivotState The pivot state on which to base the refinement. + * @param player1Choice The player 1 choice that needs to be refined. + * @param lowerChoice The first of the two choices on which to base the refinement. + * @param upperChoice The first of the two choices on which to base the refinement. */ - void exportToDot(std::string const& filename) const; + void refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice); - private: /*! - * Computes the reachable states of the transition relation. + * Exports the current state of the abstraction in the dot format to the given file. * - * @param initialStates The BDD representing the initial states of the model. - * @param transitionRelation The BDD representing the transition relation that does only contain state - * and successor variables. - * @return The BDD representing the reachable states. + * @param filename The name of the file to which to write the dot output. */ - storm::dd::Bdd getReachableStates(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitionRelation); + void exportToDot(std::string const& filename) const; + private: /*! * Builds the stochastic game representing the abstraction of the program. * @@ -99,6 +100,14 @@ namespace storm { */ std::unique_ptr> buildGame(); + /*! + * Decodes the given choice over the auxiliary and successor variables to a mapping from update indices + * to bit vectors representing the successors under these updates. + * + * @param choice The choice to decode. + */ + std::map decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd const& choice) const; + // The concrete program this abstract program refers to. std::reference_wrapper program; diff --git a/src/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/abstraction/prism/PrismMenuGameAbstractor.cpp index 16421829a..c1cc411e4 100644 --- a/src/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -24,6 +24,11 @@ namespace storm { abstractProgram.refine(predicates); } + template + void PrismMenuGameAbstractor::refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) { + abstractProgram.refine(pivotState, player1Choice, lowerChoice, upperChoice); + } + template void PrismMenuGameAbstractor::exportToDot(std::string const& filename) const { abstractProgram.exportToDot(filename); diff --git a/src/abstraction/prism/PrismMenuGameAbstractor.h b/src/abstraction/prism/PrismMenuGameAbstractor.h index b46a4f497..d4ae2f7de 100644 --- a/src/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/abstraction/prism/PrismMenuGameAbstractor.h @@ -15,6 +15,7 @@ namespace storm { virtual storm::abstraction::MenuGame abstract() override; virtual void refine(std::vector const& predicates) override; + virtual void refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) override; void exportToDot(std::string const& filename) const; diff --git a/src/exceptions/InvalidModelException.h b/src/exceptions/InvalidModelException.h new file mode 100644 index 000000000..3d8b8b7c4 --- /dev/null +++ b/src/exceptions/InvalidModelException.h @@ -0,0 +1,13 @@ +#pragma once + +#include "src/exceptions/BaseException.h" +#include "src/exceptions/ExceptionMacros.h" + +namespace storm { + namespace exceptions { + + STORM_NEW_EXCEPTION(InvalidModelException) + + } // namespace exceptions +} // namespace storm + diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 5859a8d58..250742025 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -1,7 +1,7 @@ #include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h" -#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" -#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/models/symbolic/StandardRewardModel.h" @@ -13,10 +13,12 @@ #include "src/logic/FragmentSpecification.h" +#include "src/utility/dd.h" #include "src/utility/macros.h" #include "src/exceptions/NotSupportedException.h" #include "src/exceptions/InvalidPropertyException.h" +#include "src/exceptions/InvalidModelException.h" #include "src/modelchecker/results/CheckResult.h" @@ -56,7 +58,7 @@ namespace storm { template std::unique_ptr GameBasedMdpModelChecker::computeUntilProbabilities(CheckTask const& checkTask) { storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); - return performGameBasedAbstractionRefinement(CheckTask(pathFormula), getExpression(pathFormula.getLeftSubformula()), getExpression(pathFormula.getRightSubformula())); + return performGameBasedAbstractionRefinement(checkTask.substituteFormula(pathFormula), getExpression(pathFormula.getLeftSubformula()), getExpression(pathFormula.getRightSubformula())); } template @@ -84,11 +86,70 @@ namespace storm { template std::unique_ptr getResultAfterQualitativeCheck(CheckTask const& checkTask, storm::dd::DdManager const& ddManager, storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& initialStates, bool prob0) { - if (checkTask.isBoundSet()) { - bool result = getResultConsideringBound(prob0 ? storm::utility::zero() : storm::utility::one(), checkTask.getBound()); - return std::make_unique>(reachableStates, initialStates, result ? initialStates : ddManager.getBddZero()); + return std::make_unique>(storm::storage::sparse::state_type(0), prob0 ? storm::utility::zero() : storm::utility::one()); + } + + template + storm::dd::Bdd pickPivotState(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowVariables, std::set const& columnVariables, storm::dd::Bdd const& pivotStates) { + // Perform a BFS and pick the first pivot state we encounter. + storm::dd::Bdd pivotState; + storm::dd::Bdd frontier = initialStates; + storm::dd::Bdd frontierPivotStates = frontier && pivotStates; + + bool foundPivotState = !frontierPivotStates.isZero(); + if (foundPivotState) { + pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables); } else { - return std::make_unique>(reachableStates, initialStates, prob0 ? ddManager.template getAddZero() : initialStates.template toAdd()); + while (!foundPivotState) { + frontier = frontier.relationalProduct(transitions, rowVariables, columnVariables); + frontierPivotStates = frontier && pivotStates; + + if (!frontierPivotStates.isZero()) { + pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables); + foundPivotState = true; + } + } + } + + return pivotState; + } + + template + void refineAfterQualitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor& abstractor, storm::abstraction::MenuGame const& game, detail::GameProb01Result const& prob01, storm::dd::Bdd const& transitionMatrixBdd) { + storm::dd::Bdd transitionsInIntersection = transitionMatrixBdd && prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy() && prob01.max.second.getPlayer1Strategy() && prob01.max.second.getPlayer2Strategy(); + + // First, we have to find the pivot state candidates. Start by constructing the reachable fragment of the + // state space *under both* strategy pairs. + storm::dd::Bdd pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), transitionsInIntersection.existsAbstract(game.getNondeterminismVariables()), game.getRowVariables(), game.getColumnVariables()); + + // Then constrain this set by requiring that the two stratey pairs resolve the nondeterminism differently. + pivotStates &= (prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy()).exclusiveOr(prob01.max.second.getPlayer1Strategy() && prob01.max.second.getPlayer2Strategy()).existsAbstract(game.getNondeterminismVariables()); + STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates."); + + // Now that we have the pivot state candidates, we need to pick one. + storm::dd::Bdd pivotState = pickPivotState(game.getInitialStates(), transitionsInIntersection, game.getRowVariables(), game.getColumnVariables(), pivotStates); + + // Compute the lower and the upper choice for the pivot state. + std::set variablesToAbstract = game.getNondeterminismVariables(); + variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end()); + storm::dd::Bdd lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && prob01.min.first.getPlayer1Strategy(); + storm::dd::Bdd lowerChoice1 = (lowerChoice && prob01.min.first.getPlayer2Strategy()).existsAbstract(variablesToAbstract); + storm::dd::Bdd lowerChoice2 = (lowerChoice && prob01.max.second.getPlayer2Strategy()).existsAbstract(variablesToAbstract); + + bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); + if (lowerChoicesDifferent) { + abstractor.refine(pivotState, (pivotState && prob01.min.first.getPlayer1Strategy()).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2); + } else { + storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && prob01.max.second.getPlayer1Strategy(); + storm::dd::Bdd upperChoice1 = (upperChoice && prob01.min.first.getPlayer2Strategy()).existsAbstract(variablesToAbstract); + storm::dd::Bdd upperChoice2 = (upperChoice && prob01.max.second.getPlayer2Strategy()).existsAbstract(variablesToAbstract); + + bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero(); + if (upperChoicesDifferent) { + abstractor.refine(pivotState, (pivotState && prob01.max.second.getPlayer1Strategy()).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); + } else { + STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates."); + } } } @@ -106,60 +167,73 @@ namespace storm { } // Derive the optimization direction for player 1 (assuming menu-game abstraction). - storm::OptimizationDirection player1Direction = checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize; + storm::OptimizationDirection player1Direction; + if (checkTask.isOptimizationDirectionSet()) { + player1Direction = checkTask.getOptimizationDirection(); + } else if (checkTask.isBoundSet() && !originalProgram.isDeterministicModel()) { + player1Direction = storm::logic::isLowerBound(checkTask.getBoundComparisonType()) ? storm::OptimizationDirection::Minimize : storm::OptimizationDirection::Maximize; + } else { + STORM_LOG_THROW(originalProgram.isDeterministicModel(), storm::exceptions::InvalidPropertyException, "Requiring either min or max annotation in property for nondeterministic models."); + player1Direction = storm::OptimizationDirection::Maximize; + } storm::abstraction::prism::PrismMenuGameAbstractor abstractor(preprocessedProgram, initialPredicates, smtSolverFactory); - // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression. - storm::abstraction::MenuGame game = abstractor.abstract(); - STORM_LOG_DEBUG("Initial abstraction has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions."); + for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) { + STORM_LOG_TRACE("Starting iteration " << iterations); + abstractor.exportToDot("game" + std::to_string(iterations) + ".dot"); - // 2. compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). - detail::GameProb01Result prob01 = computeProb01States(player1Direction, game, constraintExpression, targetStateExpression); - - // 3. compute the states for which we know the result/for which we know there is more work to be done. - storm::dd::Bdd maybeMin = !(prob01.min.first.states || prob01.min.second.states) && game.getReachableStates(); - storm::dd::Bdd maybeMax = !(prob01.max.first.states || prob01.max.second.states) && game.getReachableStates(); - - // 4. if the initial states are not maybe states, then we can refine at this point. - storm::dd::Bdd initialMaybeStates = game.getInitialStates() && (maybeMin || maybeMax); - if (initialMaybeStates.isZero()) { - // In this case, we know the result for the initial states for both player 2 minimizing and maximizing. - - // If the result is 0 independent of the player 2 strategy, then we know the final result and can return it. - storm::dd::Bdd tmp = game.getInitialStates() && prob01.min.first.states && prob01.max.first.states; - if (tmp == game.getInitialStates()) { - getResultAfterQualitativeCheck(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), true); - } + // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression. + storm::abstraction::MenuGame game = abstractor.abstract(); + STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions."); + STORM_LOG_THROW(game.getInitialStates().getNonZeroCount(), storm::exceptions::InvalidModelException, "Cannot treat models with more than one (abstract) initial state."); - // If the result is 1 independent of the player 2 strategy, then we know the final result and can return it. - tmp = game.getInitialStates() && prob01.min.second.states && prob01.max.second.states; - if (tmp == game.getInitialStates()) { - getResultAfterQualitativeCheck(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), false); - } + // 1.5 build a BDD from the transition matrix for various later uses. + storm::dd::Bdd transitionMatrixBdd = game.getTransitionMatrix().toBdd(); - // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) - // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine. + // 2. compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max). + detail::GameProb01Result prob01 = computeProb01States(player1Direction, game, transitionMatrixBdd, constraintExpression, targetStateExpression); + // 3. compute the states for which we know the result/for which we know there is more work to be done. + storm::dd::Bdd maybeMin = !(prob01.min.first.states || prob01.min.second.states) && game.getReachableStates(); + storm::dd::Bdd maybeMax = !(prob01.max.first.states || prob01.max.second.states) && game.getReachableStates(); + // 4. if the initial states are not maybe states, then we can refine at this point. + storm::dd::Bdd initialMaybeStates = (game.getInitialStates() && maybeMin) || (game.getInitialStates() && maybeMax); + if (initialMaybeStates.isZero()) { + // In this case, we know the result for the initial states for both player 2 minimizing and maximizing. + STORM_LOG_TRACE("No initial state is a 'maybe' state. Refining abstraction based on qualitative check."); + + // If the result is 0 independent of the player 2 strategy, then we know the final result and can return it. + storm::dd::Bdd tmp = game.getInitialStates() && prob01.min.first.states && prob01.max.first.states; + if (tmp == game.getInitialStates()) { + return getResultAfterQualitativeCheck(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), true); + } + + // If the result is 1 independent of the player 2 strategy, then we know the final result and can return it. + tmp = game.getInitialStates() && prob01.min.second.states && prob01.max.second.states; + if (tmp == game.getInitialStates()) { + return getResultAfterQualitativeCheck(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), false); + } + + // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1) + // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine. + refineAfterQualitativeCheck(abstractor, game, prob01, transitionMatrixBdd); + } else { + + // If we can already answer the question, do not solve the game numerically. + + + STORM_LOG_ASSERT(false, "Quantiative refinement not yet there. :)"); + } } - - - -// std::unique_ptr> gameSolverFactory = std::make_unique>(); -// gameSolverFactory->create(game.getTransitionMatrix(), game.getReachableStates()); -// storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs, std::set const& player1Variables, std::set const& player2Variables - - // 3. if the bounds suffice to complete checkTask, return result now. - - // 4. if the bounds do not suffice - + + STORM_LOG_ASSERT(false, "This point must not be reached."); return nullptr; } template - detail::GameProb01Result GameBasedMdpModelChecker::computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame const& game, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { - storm::dd::Bdd transitionMatrixBdd = game.getTransitionMatrix().toBdd(); + detail::GameProb01Result GameBasedMdpModelChecker::computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) { storm::dd::Bdd bottomStatesBdd = game.getBottomStates(); storm::dd::Bdd targetStates = game.getStates(targetStateExpression); @@ -168,27 +242,35 @@ namespace storm { } // 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, false); + storm::utility::graph::GameProb01Result prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true); + storm::utility::graph::GameProb01Result prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, false, false); // 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, false); - storm::utility::graph::GameProb01Result prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true); + storm::utility::graph::GameProb01Result prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, false, false); + storm::utility::graph::GameProb01Result prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true); + prob1Max.getPlayer1Strategy().template toAdd().exportToDot("prob1maxstrat.dot"); - 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."); + STORM_LOG_ASSERT(prob0Min.hasPlayer1Strategy(), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(prob0Min.hasPlayer2Strategy(), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(prob1Max.hasPlayer1Strategy(), "Unable to proceed without strategy."); + STORM_LOG_ASSERT(prob1Max.hasPlayer2Strategy(), "Unable to proceed without strategy."); + + STORM_LOG_TRACE("Min: " << prob0Min.states.getNonZeroCount() << " no states, " << prob1Min.states.getNonZeroCount() << " yes states."); + STORM_LOG_TRACE("Max: " << prob0Max.states.getNonZeroCount() << " no states, " << prob1Max.states.getNonZeroCount() << " yes states."); return detail::GameProb01Result(prob0Min, prob1Min, prob0Max, prob1Max); } template storm::expressions::Expression GameBasedMdpModelChecker::getExpression(storm::logic::Formula const& formula) { - STORM_LOG_THROW(formula.isAtomicExpressionFormula() || formula.isAtomicLabelFormula(), storm::exceptions::InvalidPropertyException, "The target states have to be given as label or an expression."); + STORM_LOG_THROW(formula.isBooleanLiteralFormula() || formula.isAtomicExpressionFormula() || formula.isAtomicLabelFormula(), storm::exceptions::InvalidPropertyException, "The target states have to be given as label or an expression."); storm::expressions::Expression result; if (formula.isAtomicLabelFormula()) { result = preprocessedProgram.getLabelExpression(formula.asAtomicLabelFormula().getLabel()); - } else { + } else if (formula.isAtomicExpressionFormula()) { result = formula.asAtomicExpressionFormula().getExpression(); + } else { + result = formula.asBooleanLiteralFormula().isTrueFormula() ? originalProgram.getManager().boolean(true) : originalProgram.getManager().boolean(false); } return result; } diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.h b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h index a7a9ae485..2e480e9fa 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.h +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.h @@ -50,7 +50,7 @@ namespace storm { private: std::unique_ptr performGameBasedAbstractionRefinement(CheckTask const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); - detail::GameProb01Result computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame const& game, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); + detail::GameProb01Result computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame const& game, storm::dd::Bdd const& transitionMatrixBdd, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression); storm::expressions::Expression getExpression(storm::logic::Formula const& formula); diff --git a/src/utility/dd.cpp b/src/utility/dd.cpp index b50bc0031..290a38071 100644 --- a/src/utility/dd.cpp +++ b/src/utility/dd.cpp @@ -27,7 +27,6 @@ namespace storm { changed = true; } - reachableStates |= newReachableStates; ++iteration; diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp index 55cb72cda..f357256be 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -924,7 +924,7 @@ namespace storm { } template - GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies) { + GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) { // The solution set. storm::dd::Bdd solution = psiStates; @@ -966,13 +966,13 @@ namespace storm { storm::dd::Bdd onlyProb0Successors = (transitionsBetweenProb0States || model.getIllegalSuccessorMask()).universalAbstract(model.getColumnVariables()); boost::optional> player2StrategyBdd; - if (produceStrategies && player2Strategy == OptimizationDirection::Minimize) { + if (producePlayer2Strategy) { // Pick a distribution that has only prob0 successors. player2StrategyBdd = onlyProb0Successors.existsAbstractRepresentative(model.getPlayer2Variables()); } boost::optional> player1StrategyBdd; - if (produceStrategies && player1Strategy == OptimizationDirection::Minimize) { + if (producePlayer1Strategy) { // Move from player 2 choices with only prob0 successors to player 1 choices with only prob 0 successors. onlyProb0Successors = onlyProb0Successors.existsAbstract(model.getPlayer2Variables()); @@ -984,12 +984,11 @@ namespace storm { } template - GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies) { + GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) { // Create two sets of states. Those states for which we definitely know that their probability is 1 and // those states that potentially have a probability of 1. storm::dd::Bdd maybeStates = model.getReachableStates(); - storm::dd::Bdd solution = psiStates; // A flag that governs whether strategies are produced in the current iteration. bool produceStrategiesInIteration = false; @@ -1012,6 +1011,7 @@ namespace storm { consideredPlayer2States = model.getManager().getBddZero(); } + storm::dd::Bdd solution = psiStates; while (!solutionStatesDone) { // Start by computing the transitions that have only maybe states as successors. Note that at // this point, there may be illegal transitions. @@ -1024,7 +1024,7 @@ namespace storm { // The valid distributions are then those that emanate from phi states, stay completely in the // maybe states and have at least one successor with probability 1. storm::dd::Bdd valid = phiStates && distributionsStayingInMaybe && distributionsWithProb1Successor; - + // Depending on the strategy of player 2, we need to check whether all choices are valid or // there exists a valid choice. if (player2Strategy == OptimizationDirection::Minimize) { @@ -1079,7 +1079,7 @@ namespace storm { // If we were asked to produce strategies, we propagate that by triggering another iteration. // We only do this if at least one strategy will be produced. - produceStrategiesInIteration = !produceStrategiesInIteration && produceStrategies && (player1Strategy == OptimizationDirection::Maximize || player2Strategy == OptimizationDirection::Maximize); + produceStrategiesInIteration = !produceStrategiesInIteration && ((producePlayer1Strategy && player1Strategy == OptimizationDirection::Maximize) || (producePlayer2Strategy && player2Strategy == OptimizationDirection::Maximize)); } else { // Otherwise, we use the current hypothesis for the states with probability 1 as the new maybe // state set. @@ -1088,7 +1088,23 @@ namespace storm { ++maybeStateIterations; } - return GameProb01Result(solution, player1StrategyBdd, player2StrategyBdd); + // From now on, the solution is stored in maybeStates (as it coincides with the previous solution). + + // If we were asked to produce strategies that do not need to pick a certain successor but are + // 'arbitrary', do so now. + bool strategiesToCompute = (producePlayer1Strategy && !player1StrategyBdd) || (producePlayer2Strategy && !player2StrategyBdd); + if (strategiesToCompute) { + storm::dd::Bdd relevantStates = (transitionMatrix && maybeStates).existsAbstract(model.getColumnVariables()); + if (producePlayer2Strategy && !player2StrategyBdd) { + player2StrategyBdd = relevantStates.existsAbstractRepresentative(model.getPlayer2Variables()); + } + if (producePlayer1Strategy && !player1StrategyBdd) { + relevantStates = relevantStates.existsAbstract(model.getPlayer2Variables()); + player1StrategyBdd = relevantStates.existsAbstractRepresentative(model.getPlayer1Variables()); + } + } + + return GameProb01Result(maybeStates, player1StrategyBdd, player2StrategyBdd); } template @@ -1488,9 +1504,9 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies); + template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); - template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies); + template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); // Instantiations for Sylvan. @@ -1520,9 +1536,9 @@ namespace storm { template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); - template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies); + template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); - template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies); + template GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy); } // namespace graph } // namespace utility diff --git a/src/utility/graph.h b/src/utility/graph.h index cd03b42dd..07b0aafa8 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -568,11 +568,11 @@ namespace storm { * @param transitionMatrix The transition matrix of the model as a BDD. * @param phiStates The BDD containing all phi states of the model. * @param psiStates The BDD containing all psi states of the model. - * @param produceStrategies A flag indicating whether strategies should be produced. Note that the strategies - * are only produced in case the choices of the player are not irrelevant. + * @param producePlayer1Strategy A flag indicating whether the strategy of player 1 shall be produced. + * @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced. */ template - GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies = false); + GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false); /*! * Computes the set of states that have probability 1 given the strategies of the two players. @@ -581,11 +581,11 @@ namespace storm { * @param transitionMatrix The transition matrix of the model as a BDD. * @param phiStates The BDD containing all phi states of the model. * @param psiStates The BDD containing all psi states of the model. - * @param produceStrategies A flag indicating whether strategies should be produced. Note that the strategies - * are only produced in case the choices of the player are not irrelevant. + * @param producePlayer1Strategy A flag indicating whether the strategy of player 1 shall be produced. + * @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced. */ template - GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategybool, bool produceStrategies = false); + GameProb01Result performProb1(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false); /*! * Performs a topological sort of the states of the system according to the given transitions. diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 534f33df5..7b431e67e 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -214,33 +214,33 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { // The target states are those states where !(s < 3). storm::dd::Bdd targetStates = game.getStates(initialPredicates[0], true); - storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); EXPECT_EQ(2, result.states.getNonZeroCount()); - EXPECT_TRUE(static_cast(result.player1Strategy)); - EXPECT_TRUE(static_cast(result.player2Strategy)); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); EXPECT_EQ(2, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); EXPECT_EQ(2, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); EXPECT_EQ(2, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); EXPECT_EQ(2, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); EXPECT_EQ(2, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); EXPECT_EQ(1, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); EXPECT_EQ(3, result.states.getNonZeroCount()); - EXPECT_TRUE(static_cast(result.player1Strategy)); - EXPECT_TRUE(static_cast(result.player2Strategy)); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); abstractProgram.refine({manager.getVariableExpression("s") < manager.integer(2)}); game = abstractProgram.getAbstractGame(); @@ -248,10 +248,10 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { // We need to create a new BDD for the target states since the reachable states might have changed. targetStates = game.getStates(initialPredicates[0], true); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); EXPECT_EQ(2, result.states.getNonZeroCount()); - EXPECT_TRUE(static_cast(result.player1Strategy)); - EXPECT_TRUE(static_cast(result.player2Strategy)); + ASSERT_TRUE(result.hasPlayer1Strategy()); + ASSERT_TRUE(result.hasPlayer2Strategy()); // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy. storm::dd::Bdd nonProb0StatesWithStrategy = !result.states && result.player1Strategy.get(); @@ -265,28 +265,28 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); EXPECT_EQ(1, stateDistributionCount.getMax()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); EXPECT_EQ(3, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); EXPECT_EQ(1, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); EXPECT_EQ(4, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); EXPECT_EQ(2, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); EXPECT_EQ(3, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); EXPECT_EQ(1, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); EXPECT_EQ(4, result.states.getNonZeroCount()); - EXPECT_TRUE(static_cast(result.player1Strategy)); - EXPECT_TRUE(static_cast(result.player2Strategy)); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy. storm::dd::Bdd nonProb1StatesWithStrategy = !result.states && result.player1Strategy.get(); @@ -350,10 +350,10 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { // The target states are those states where s1 == 7 & s2 == 7 & d1 + d2 == 1. storm::dd::Bdd targetStates = game.getStates(initialPredicates[7], false) && game.getStates(initialPredicates[22], false) && game.getStates(initialPredicates[9], false) && game.getStates(initialPredicates[24], false); - storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); EXPECT_EQ(153, result.states.getNonZeroCount()); - EXPECT_TRUE(static_cast(result.player1Strategy)); - EXPECT_TRUE(static_cast(result.player2Strategy)); + ASSERT_TRUE(result.hasPlayer1Strategy()); + ASSERT_TRUE(result.hasPlayer2Strategy()); // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy. storm::dd::Bdd nonProb0StatesWithStrategy = !result.states && result.player1Strategy.get(); @@ -366,28 +366,28 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); EXPECT_EQ(1, stateDistributionCount.getMax()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); EXPECT_EQ(1, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); EXPECT_EQ(153, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); EXPECT_EQ(1, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); EXPECT_EQ(153, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); EXPECT_EQ(1, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); EXPECT_EQ(153, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); EXPECT_EQ(1, result.states.getNonZeroCount()); - EXPECT_TRUE(static_cast(result.player1Strategy)); - EXPECT_TRUE(static_cast(result.player2Strategy)); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy. storm::dd::Bdd nonProb1StatesWithStrategy = !result.states && result.player1Strategy.get(); @@ -519,10 +519,10 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) { // The target states are those states where col == 2. storm::dd::Bdd targetStates = game.getStates(initialPredicates[2], false); - storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); EXPECT_EQ(2831, result.states.getNonZeroCount()); - ASSERT_TRUE(static_cast(result.player1Strategy)); - ASSERT_TRUE(static_cast(result.player2Strategy)); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy. storm::dd::Bdd nonProb0StatesWithStrategy = !result.states && result.player1Strategy.get(); @@ -536,28 +536,28 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) { storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); EXPECT_EQ(1, stateDistributionCount.getMax()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); EXPECT_EQ(2692, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); EXPECT_EQ(2831, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); EXPECT_EQ(2692, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); EXPECT_EQ(2064, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); EXPECT_EQ(2884, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); EXPECT_EQ(2064, result.states.getNonZeroCount()); - result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true); + result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); EXPECT_EQ(2884, result.states.getNonZeroCount()); - EXPECT_TRUE(static_cast(result.player1Strategy)); - EXPECT_TRUE(static_cast(result.player2Strategy)); + EXPECT_TRUE(result.hasPlayer1Strategy()); + EXPECT_TRUE(result.hasPlayer2Strategy()); // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy. storm::dd::Bdd nonProb1StatesWithStrategy = !result.states && result.player1Strategy.get();