diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp index 0ce9201ef..041b50d1b 100644 --- a/src/abstraction/AbstractionInformation.cpp +++ b/src/abstraction/AbstractionInformation.cpp @@ -119,6 +119,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(); @@ -164,16 +169,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(); @@ -353,6 +373,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 4be327e4e..55ba8af6a 100644 --- a/src/abstraction/AbstractionInformation.h +++ b/src/abstraction/AbstractionInformation.h @@ -147,6 +147,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. * @@ -179,6 +186,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. * @@ -189,7 +205,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. @@ -198,6 +223,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). * @@ -391,16 +426,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. diff --git a/src/abstraction/MenuGame.cpp b/src/abstraction/MenuGame.cpp index 4ada7add8..ba47698e2 100644 --- a/src/abstraction/MenuGame.cpp +++ b/src/abstraction/MenuGame.cpp @@ -26,7 +26,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. } @@ -61,6 +61,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 071a3a9c0..91f305d9b 100644 --- a/src/abstraction/prism/AbstractCommand.cpp +++ b/src/abstraction/prism/AbstractCommand.cpp @@ -337,6 +337,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 30a60928e..72e354584 100644 --- a/src/abstraction/prism/AbstractModule.cpp +++ b/src/abstraction/prism/AbstractModule.cpp @@ -72,6 +72,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 f5a1d0763..84ea2ad19 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -9,6 +9,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" @@ -108,6 +109,33 @@ namespace storm { currentGame = buildGame(); } + template + void AbstractProgram::refine(storm::dd::Bdd const& pivotState, storm::dd::Bdd const& player1Choice, storm::dd::Bdd const& lowerChoice, storm::dd::Bdd const& upperChoice) { +// std::cout << "refining in program!" << std::endl; +// lowerChoice.template toAdd().exportToDot("lchoice.dot"); +// upperChoice.template toAdd().exportToDot("uchoice.dot"); +// player1Choice.template toAdd().exportToDot("pl1_choice.dot"); +// pivotState.template toAdd().exportToDot("pivotstate.dot"); + + // 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()); + + bool bottomSuccessor = !((abstractionInformation.getBottomStateBdd(false, false) && lowerChoice) || (abstractionInformation.getBottomStateBdd(false, false) && upperChoice)).isZero(); + if (bottomSuccessor) { + storm::abstraction::prism::AbstractCommand& abstractCommand = modules.front().getCommands()[commandIndex]; + abstractCommand.notifyGuardIsPredicate(); + storm::expressions::Expression newPredicate = abstractCommand.getConcreteCommand().getGuardExpression(); + STORM_LOG_DEBUG("Derived new predicate: " << newPredicate); + this->refine({newPredicate}); + } else { + exit(-1); + } + + storm::dd::Add lowerChoiceAsAdd = lowerChoice.template toAdd(); + } + template MenuGame AbstractProgram::getAbstractGame() { STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created."); @@ -135,7 +163,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. @@ -164,6 +192,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; } @@ -183,25 +212,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); @@ -241,13 +252,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; @@ -265,21 +270,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; @@ -302,20 +295,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..e3f04f8b9 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. * 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/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 98e4737b2..19cf3052b 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -13,6 +13,7 @@ #include "src/logic/FragmentSpecification.h" +#include "src/utility/dd.h" #include "src/utility/macros.h" #include "src/exceptions/NotSupportedException.h" @@ -92,16 +93,68 @@ namespace storm { } } + 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 { + 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::MenuGame const& game, detail::GameProb01Result const& prob01, storm::dd::Bdd const& transitionMatrixBdd) { + 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 pivotStateCandidates = transitionMatrixBdd.existsAbstract(game.getColumnVariables()); - pivotStateCandidates &= prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy() && prob01.max.first.getPlayer1Strategy() && prob01.max.first.getPlayer2Strategy(); - pivotStateCandidates = pivotStateCandidates.existsAbstract(game.getNondeterminismVariables()); + 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); - std::cout << "found pivot state candidates" << std::endl; + // 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); + } + + 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); + upperChoice1.template toAdd().exportToDot("uchoice1.dot"); + upperChoice2.template toAdd().exportToDot("uchoice2.dot"); + + bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero(); + if (upperChoicesDifferent) { + abstractor.refine(pivotState, (pivotState && prob01.max.second.getPlayer1Strategy()).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2); + } } template @@ -155,7 +208,7 @@ namespace storm { // 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(game, prob01, transitionMatrixBdd); + refineAfterQualitativeCheck(abstractor, game, prob01, transitionMatrixBdd); } @@ -187,6 +240,7 @@ namespace storm { // 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, 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_ASSERT(prob0Min.hasPlayer1Strategy(), "Unable to proceed without strategy."); STORM_LOG_ASSERT(prob0Min.hasPlayer2Strategy(), "Unable to proceed without strategy."); 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 da42fad1b..f357256be 100644 --- a/src/utility/graph.cpp +++ b/src/utility/graph.cpp @@ -989,7 +989,6 @@ namespace storm { // 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) { @@ -1088,11 +1088,13 @@ namespace storm { ++maybeStateIterations; } + // 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 && solution).existsAbstract(model.getColumnVariables()); + storm::dd::Bdd relevantStates = (transitionMatrix && maybeStates).existsAbstract(model.getColumnVariables()); if (producePlayer2Strategy && !player2StrategyBdd) { player2StrategyBdd = relevantStates.existsAbstractRepresentative(model.getPlayer2Variables()); } @@ -1102,7 +1104,7 @@ namespace storm { } } - return GameProb01Result(solution, player1StrategyBdd, player2StrategyBdd); + return GameProb01Result(maybeStates, player1StrategyBdd, player2StrategyBdd); } template