diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index 42d4d6ef9..df26fa29b 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -300,12 +300,48 @@ namespace storm { } template - void AbstractProgram::exportToDot(std::string const& filename) const { + void AbstractProgram::exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStatesBdd, storm::dd::Bdd const& filter) const { std::ofstream out(filename); + + storm::dd::Add filteredTransitions = filter.template toAdd() * currentGame->getTransitionMatrix(); + storm::dd::Bdd filteredTransitionsBdd = filteredTransitions.toBdd().existsAbstract(currentGame->getNondeterminismVariables()); + storm::dd::Bdd filteredReachableStates = storm::utility::dd::computeReachableStates(currentGame->getInitialStates(), filteredTransitionsBdd, currentGame->getRowVariables(), currentGame->getColumnVariables()); + filteredTransitions *= filteredReachableStates.template toAdd(); + + // Determine all initial states so we can color them blue. + std::unordered_set initialStates; + storm::dd::Add initialStatesAsAdd = currentGame->getInitialStates().template toAdd(); + for (auto stateValue : initialStatesAsAdd) { + std::stringstream stateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + initialStates.insert(stateName.str()); + } + + // Determine all highlight states so we can color them red. + std::unordered_set highlightStates; + storm::dd::Add highlightStatesAdd = highlightStatesBdd.template toAdd(); + for (auto stateValue : highlightStatesAdd) { + std::stringstream stateName; + for (auto const& var : currentGame->getRowVariables()) { + if (stateValue.first.getBooleanValue(var)) { + stateName << "1"; + } else { + stateName << "0"; + } + } + highlightStates.insert(stateName.str()); + } + out << "digraph game {" << std::endl; // Create the player 1 nodes. - storm::dd::Add statesAsAdd = currentGame->getReachableStates().template toAdd(); + storm::dd::Add statesAsAdd = filteredReachableStates.template toAdd(); for (auto stateValue : statesAsAdd) { out << "\tpl1_"; std::stringstream stateName; @@ -316,18 +352,28 @@ namespace storm { stateName << "0"; } } - out << stateName.str(); + std::string stateNameAsString = stateName.str(); + out << stateNameAsString; out << " [ label=\""; if (stateValue.first.getBooleanValue(abstractionInformation.getBottomStateVariable(true))) { - out << "*\", margin=0, width=0, height=0, shape=\"none"; + out << "*\", margin=0, width=0, height=0, shape=\"none\""; } else { - out << stateName.str() << "\", margin=0, width=0, height=0, shape=\"oval"; + out << stateName.str() << "\", margin=0, width=0, height=0, shape=\"oval\""; + } + bool isInitial = initialStates.find(stateNameAsString) != initialStates.end(); + bool isHighlight = highlightStates.find(stateNameAsString) != highlightStates.end(); + if (isInitial && isHighlight) { + out << ", style=\"filled\", fillcolor=\"yellow\""; + } else if (isInitial) { + out << ", style=\"filled\", fillcolor=\"blue\""; + } else if (isHighlight) { + out << ", style=\"filled\", fillcolor=\"red\""; } - out << "\" ];" << std::endl; + out << " ];" << std::endl; } // Create the nodes of the second player. - storm::dd::Add player2States = currentGame->getTransitionMatrix().toBdd().existsAbstract(currentGame->getColumnVariables()).existsAbstract(currentGame->getPlayer2Variables()).template toAdd(); + storm::dd::Add player2States = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).existsAbstract(currentGame->getPlayer2Variables()).template toAdd(); for (auto stateValue : player2States) { out << "\tpl2_"; std::stringstream stateName; @@ -345,7 +391,7 @@ namespace storm { } // Create the nodes of the probabilistic player. - storm::dd::Add playerPStates = currentGame->getTransitionMatrix().toBdd().existsAbstract(currentGame->getColumnVariables()).template toAdd(); + storm::dd::Add playerPStates = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).template toAdd(); for (auto stateValue : playerPStates) { out << "\tplp_"; std::stringstream stateName; @@ -364,7 +410,7 @@ namespace storm { out << "\tpl2_" << stateName.str() << " -> " << "plp_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl; } - for (auto stateValue : currentGame->getTransitionMatrix()) { + for (auto stateValue : filteredTransitions) { std::stringstream sourceStateName; std::stringstream successorStateName; for (auto const& var : currentGame->getRowVariables()) { diff --git a/src/abstraction/prism/AbstractProgram.h b/src/abstraction/prism/AbstractProgram.h index 8ee848946..47c67ac8e 100644 --- a/src/abstraction/prism/AbstractProgram.h +++ b/src/abstraction/prism/AbstractProgram.h @@ -89,8 +89,10 @@ namespace storm { * Exports the current state of the abstraction in the dot format to the given file. * * @param filename The name of the file to which to write the dot output. + * @param highlightStates A BDD characterizing states that will be highlighted. + * @param filter A filter that is applied to select which part of the game to export. */ - void exportToDot(std::string const& filename) const; + void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const; private: /*! diff --git a/src/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/abstraction/prism/PrismMenuGameAbstractor.cpp index c1cc411e4..ad8c22e78 100644 --- a/src/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -30,12 +30,12 @@ namespace storm { } template - void PrismMenuGameAbstractor::exportToDot(std::string const& filename) const { - abstractProgram.exportToDot(filename); + void PrismMenuGameAbstractor::exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const { + abstractProgram.exportToDot(filename, highlightStates, filter); } template class PrismMenuGameAbstractor; template class PrismMenuGameAbstractor; } } -} \ No newline at end of file +} diff --git a/src/abstraction/prism/PrismMenuGameAbstractor.h b/src/abstraction/prism/PrismMenuGameAbstractor.h index d4ae2f7de..6aa450ff8 100644 --- a/src/abstraction/prism/PrismMenuGameAbstractor.h +++ b/src/abstraction/prism/PrismMenuGameAbstractor.h @@ -17,7 +17,7 @@ namespace storm { 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; + void exportToDot(std::string const& filename, storm::dd::Bdd const& highlightStates, storm::dd::Bdd const& filter) const; private: /// The abstract program that performs the actual abstraction. @@ -26,4 +26,4 @@ namespace storm { } } -} \ No newline at end of file +} diff --git a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 093c80d96..3e73ac35f 100644 --- a/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -319,6 +319,8 @@ namespace storm { // Then restrict the pivot states by requiring existing and different player 2 choices. pivotStates &= ((minPlayer1Strategy || maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()); + ((minPlayer1Strategy || maxPlayer1Strategy) && constraint).existsAbstract(game.getNondeterminismVariables()).template toAdd().exportToDot("a.dot"); + 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. @@ -337,7 +339,7 @@ namespace storm { // // minResult.exportToDot("minresult.dot"); // maxResult.exportToDot("maxresult.dot"); - pivotState.template toAdd().exportToDot("pivot.dot"); +// pivotState.template toAdd().exportToDot("pivot.dot"); // pivotStateLower.exportToDot("pivot_lower.dot"); // pivotStateUpper.exportToDot("pivot_upper.dot"); // pivotStateIsMinProb0.template toAdd().exportToDot("pivot_is_minprob0.dot"); @@ -459,7 +461,6 @@ namespace storm { storm::abstraction::prism::PrismMenuGameAbstractor abstractor(preprocessedProgram, initialPredicates, smtSolverFactory); for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) { STORM_LOG_TRACE("Starting iteration " << iterations << "."); - abstractor.exportToDot("game" + std::to_string(iterations) + ".dot"); // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression. storm::abstraction::MenuGame game = abstractor.abstract(); @@ -475,6 +476,9 @@ namespace storm { if (player1Direction == storm::OptimizationDirection::Minimize) { targetStates |= game.getBottomStates(); } + + abstractor.exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne()); + prob01.min = computeProb01States(player1Direction, storm::OptimizationDirection::Minimize, game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates); std::unique_ptr result = checkForResultAfterQualitativeCheck(checkTask, storm::OptimizationDirection::Minimize, game.getInitialStates(), prob01.min.first.getPlayer1States(), prob01.min.second.getPlayer1States()); if (result) { @@ -557,7 +561,6 @@ namespace storm { storm::dd::Bdd combinedMaxPlayer1QualitativeStrategies = (prob01.max.first.getPlayer1Strategy() || prob01.max.second.getPlayer1Strategy()); storm::dd::Bdd combinedMaxPlayer2QualitativeStrategies = (prob01.max.first.getPlayer2Strategy() || prob01.max.second.getPlayer2Strategy()); - // Likewise, the maximal value after qualitative checking can only be 1. If it was 0, we could have // given the result right awy. ValueType maxValue = storm::utility::one(); @@ -613,23 +616,6 @@ namespace storm { // Start by extending the quantitative strategies by the qualitative ones. //minMaybeStateResult.player1Strategy |= prob01.min.first.getPlayer1Strategy() || prob01.min.second.getPlayer1Strategy(); - - storm::dd::Bdd tmp = (prob01.min.first.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && prob01.min.second.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables())); - STORM_LOG_ASSERT(tmp.isZero(), "wth?"); - tmp = prob01.min.first.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && minMaybeStateResult.player2Strategy.existsAbstract(game.getPlayer2Variables()); - if (!tmp.isZero()) { - tmp = tmp && prob01.min.first.getPlayer2Strategy().exclusiveOr(minMaybeStateResult.player2Strategy).existsAbstract(game.getPlayer2Variables()); - (tmp && prob01.min.first.getPlayer2Strategy()).template toAdd().exportToDot("prob0_strat.dot"); - (tmp && minMaybeStateResult.player2Strategy).template toAdd().exportToDot("maybe_strat.dot"); - if (!tmp.isZero()) { - storm::dd::Add values = (tmp.template toAdd() * game.getTransitionMatrix() * minResult.swapVariables(game.getRowColumnMetaVariablePairs())).sumAbstract(game.getColumnVariables()); - tmp.template toAdd().exportToDot("illegal.dot"); - minResult.exportToDot("vals.dot"); - } - STORM_LOG_ASSERT(tmp.isZero(), "ddduuuudde?"); - } - STORM_LOG_ASSERT(tmp.isZero(), "wth2?"); - tmp = prob01.min.second.getPlayer2Strategy().existsAbstract(game.getPlayer2Variables()) && minMaybeStateResult.player2Strategy; //(minMaybeStateResult.player2Strategy && (prob01.min.first.getPlayer2Strategy() || prob01.min.second.getPlayer2Strategy())).template toAdd().exportToDot("strat_overlap.dot"); //minMaybeStateResult.player2Strategy |= prob01.min.first.getPlayer2Strategy() || prob01.min.second.getPlayer2Strategy(); @@ -642,6 +628,18 @@ namespace storm { STORM_LOG_ASSERT(minMaybeStateResult.player2Strategy.template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal."); STORM_LOG_ASSERT(maxMaybeStateResult.player2Strategy.template toAdd().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal."); + // Check whether the strategies coincide over the reachable parts. + storm::dd::Bdd tmp = game.getTransitionMatrix().toBdd() && (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && (minMaybeStateResult.player2Strategy || maxMaybeStateResult.player2Strategy); + storm::dd::Bdd commonReach = storm::utility::dd::computeReachableStates(game.getInitialStates(), tmp.existsAbstract(game.getNondeterminismVariables()), game.getRowVariables(), game.getColumnVariables()); + std::cout << "diff one? " << ((commonReach && minMaybeStateResult.player1Strategy) != (commonReach && maxMaybeStateResult.player1Strategy)) << std::endl; + std::cout << "diff one? " << ((commonReach && minMaybeStateResult.player2Strategy) != (commonReach && maxMaybeStateResult.player2Strategy)) << std::endl; + STORM_LOG_ASSERT((commonReach && minMaybeStateResult.player1Strategy) != (commonReach && maxMaybeStateResult.player1Strategy) || (commonReach && minMaybeStateResult.player2Strategy) != (commonReach && maxMaybeStateResult.player2Strategy), "The strategies fully coincide."); + + abstractor.exportToDot("lowerlower" + std::to_string(iterations) + ".dot", targetStates, minMaybeStateResult.player1Strategy && minMaybeStateResult.player2Strategy); + abstractor.exportToDot("upperupper" + std::to_string(iterations) + ".dot", targetStates, maxMaybeStateResult.player1Strategy && maxMaybeStateResult.player2Strategy); + abstractor.exportToDot("common" + std::to_string(iterations) + ".dot", targetStates, (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && minMaybeStateResult.player2Strategy && maxMaybeStateResult.player2Strategy); + abstractor.exportToDot("both" + std::to_string(iterations) + ".dot", targetStates, (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && (minMaybeStateResult.player2Strategy || maxMaybeStateResult.player2Strategy)); + refineAfterQuantitativeCheck(abstractor, game, minResult, maxResult, prob01, std::make_pair(minMaybeStateResult.player1Strategy, minMaybeStateResult.player2Strategy), std::make_pair(maxMaybeStateResult.player1Strategy, maxMaybeStateResult.player2Strategy), transitionMatrixBdd); } } @@ -688,4 +686,4 @@ namespace storm { template class GameBasedMdpModelChecker>; } -} \ No newline at end of file +}