Merge branch 'menu_games' of https://sselab.de/lab9/private/git/storm into menu_games

Former-commit-id: 96a0e32e2f

src/abstraction/prism/AbstractProgram.cpp

@@ -300,12 +300,48 @@ namespace storm {
             }
                         
             template <storm::dd::DdType DdType, typename ValueType>
-            void AbstractProgram<DdType, ValueType>::exportToDot(std::string const& filename) const {
+            void AbstractProgram<DdType, ValueType>::exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const {
                 std::ofstream out(filename);
+                
+                storm::dd::Add<DdType, ValueType> filteredTransitions = filter.template toAdd<ValueType>() * currentGame->getTransitionMatrix();
+                storm::dd::Bdd<DdType> filteredTransitionsBdd = filteredTransitions.toBdd().existsAbstract(currentGame->getNondeterminismVariables());
+                storm::dd::Bdd<DdType> filteredReachableStates = storm::utility::dd::computeReachableStates(currentGame->getInitialStates(), filteredTransitionsBdd, currentGame->getRowVariables(), currentGame->getColumnVariables());
+                filteredTransitions *= filteredReachableStates.template toAdd<ValueType>();
+                
+                // Determine all initial states so we can color them blue.
+                std::unordered_set<std::string> initialStates;
+                storm::dd::Add<DdType, ValueType> initialStatesAsAdd = currentGame->getInitialStates().template toAdd<ValueType>();
+                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<std::string> highlightStates;
+                storm::dd::Add<DdType, ValueType> highlightStatesAdd = highlightStatesBdd.template toAdd<ValueType>();
+                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<DdType, ValueType> statesAsAdd = currentGame->getReachableStates().template toAdd<ValueType>();
+                storm::dd::Add<DdType, ValueType> statesAsAdd = filteredReachableStates.template toAdd<ValueType>();
                 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<DdType, ValueType> player2States = currentGame->getTransitionMatrix().toBdd().existsAbstract(currentGame->getColumnVariables()).existsAbstract(currentGame->getPlayer2Variables()).template toAdd<ValueType>();
+                storm::dd::Add<DdType, ValueType> player2States = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).existsAbstract(currentGame->getPlayer2Variables()).template toAdd<ValueType>();
                 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<DdType, ValueType> playerPStates = currentGame->getTransitionMatrix().toBdd().existsAbstract(currentGame->getColumnVariables()).template toAdd<ValueType>();
+                storm::dd::Add<DdType, ValueType> playerPStates = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).template toAdd<ValueType>();
                 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()) {

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<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const;
                 
             private:                
                 /*!

src/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -30,8 +30,8 @@ namespace storm {
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            void PrismMenuGameAbstractor<DdType, ValueType>::exportToDot(std::string const& filename) const {
-                abstractProgram.exportToDot(filename);
+            void PrismMenuGameAbstractor<DdType, ValueType>::exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const {
+                abstractProgram.exportToDot(filename, highlightStates, filter);
             }
          
             template class PrismMenuGameAbstractor<storm::dd::DdType::CUDD, double>;

src/abstraction/prism/PrismMenuGameAbstractor.h

@@ -17,7 +17,7 @@ namespace storm {
                 virtual void refine(std::vector<storm::expressions::Expression> const& predicates) override;
                 virtual void refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice) override;
 
-                void exportToDot(std::string const& filename) const;
+                void exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const;
                 
             private:
                 /// The abstract program that performs the actual abstraction.

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<ValueType>().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<ValueType>().exportToDot("pivot.dot");
+//            pivotState.template toAdd<ValueType>().exportToDot("pivot.dot");
 //            pivotStateLower.exportToDot("pivot_lower.dot");
 //            pivotStateUpper.exportToDot("pivot_upper.dot");
 //            pivotStateIsMinProb0.template toAdd<ValueType>().exportToDot("pivot_is_minprob0.dot");
@@ -459,7 +461,6 @@ namespace storm {
             storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType> 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<Type, ValueType> 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<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(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<Type> combinedMaxPlayer1QualitativeStrategies = (prob01.max.first.getPlayer1Strategy() || prob01.max.second.getPlayer1Strategy());
 					storm::dd::Bdd<Type> 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<ValueType>();
@@ -614,23 +617,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<Type> 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<ValueType>().exportToDot("prob0_strat.dot");
-                        (tmp && minMaybeStateResult.player2Strategy).template toAdd<ValueType>().exportToDot("maybe_strat.dot");
-                        if (!tmp.isZero()) {
-                            storm::dd::Add<Type, ValueType> values = (tmp.template toAdd<ValueType>() * game.getTransitionMatrix() * minResult.swapVariables(game.getRowColumnMetaVariablePairs())).sumAbstract(game.getColumnVariables());
-                            tmp.template toAdd<ValueType>().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<ValueType>().exportToDot("strat_overlap.dot");
                     //minMaybeStateResult.player2Strategy |= prob01.min.first.getPlayer2Strategy() || prob01.min.second.getPlayer2Strategy();
                     //maxMaybeStateResult.player1Strategy |= prob01.max.first.getPlayer1Strategy() || prob01.max.second.getPlayer1Strategy();
@@ -642,6 +628,18 @@ namespace storm {
                     STORM_LOG_ASSERT(minMaybeStateResult.player2Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal.");
                     STORM_LOG_ASSERT(maxMaybeStateResult.player2Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal.");
                     
+                    // Check whether the strategies coincide over the reachable parts.
+                    storm::dd::Bdd<Type> tmp = game.getTransitionMatrix().toBdd() && (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && (minMaybeStateResult.player2Strategy || maxMaybeStateResult.player2Strategy);
+                    storm::dd::Bdd<Type> 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);
                 }
             }