extended partial bisimulation model checker by games as quotients

src/storm/abstraction/MenuGameRefiner.cpp

@@ -133,10 +133,10 @@ namespace storm {
                 maxPlayer1Strategy = qualitativeResult.get().prob1Max.getPlayer1Strategy();
                 maxPlayer2Strategy = qualitativeResult.get().prob1Max.getPlayer2Strategy();
             } else if (quantitativeResult) {
-                minPlayer1Strategy = quantitativeResult.get().min.player1Strategy;
-                minPlayer2Strategy = quantitativeResult.get().min.player2Strategy;
-                maxPlayer1Strategy = quantitativeResult.get().max.player1Strategy;
-                maxPlayer2Strategy = quantitativeResult.get().max.player2Strategy;
+                minPlayer1Strategy = quantitativeResult.get().min.getPlayer1Strategy();
+                minPlayer2Strategy = quantitativeResult.get().min.getPlayer2Strategy();
+                maxPlayer1Strategy = quantitativeResult.get().max.getPlayer1Strategy();
+                maxPlayer2Strategy = quantitativeResult.get().max.getPlayer2Strategy();
             } else {
                 STORM_LOG_ASSERT(false, "Either qualitative or quantitative result is required.");
             }
@@ -619,10 +619,10 @@ namespace storm {
         bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, QuantitativeGameResultMinMax<Type, ValueType> const& quantitativeResult) const {
             STORM_LOG_TRACE("Refining after quantitative check.");
             // Get all relevant strategies.
-            storm::dd::Bdd<Type> minPlayer1Strategy = quantitativeResult.min.player1Strategy;
-            storm::dd::Bdd<Type> minPlayer2Strategy = quantitativeResult.min.player2Strategy;
-            storm::dd::Bdd<Type> maxPlayer1Strategy = quantitativeResult.max.player1Strategy;
-            storm::dd::Bdd<Type> maxPlayer2Strategy = quantitativeResult.max.player2Strategy;
+            storm::dd::Bdd<Type> minPlayer1Strategy = quantitativeResult.min.getPlayer1Strategy();
+            storm::dd::Bdd<Type> minPlayer2Strategy = quantitativeResult.min.getPlayer2Strategy();
+            storm::dd::Bdd<Type> maxPlayer1Strategy = quantitativeResult.max.getPlayer1Strategy();
+            storm::dd::Bdd<Type> maxPlayer2Strategy = quantitativeResult.max.getPlayer2Strategy();
             
             // Compute all reached pivot states.
             PivotStateCandidatesResult<Type> pivotStateCandidatesResult = computePivotStates(game, transitionMatrixBdd, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);

src/storm/abstraction/QualitativeGameResult.h

@@ -1,12 +1,24 @@
 #pragma once
 
 #include "storm/utility/graph.h"
+#include "storm/abstraction/QualitativeResult.h"
 
 namespace storm {
     namespace abstraction {
         
         template <storm::dd::DdType Type>
-        using QualitativeGameResult = storm::utility::graph::GameProb01Result<Type>;
+        struct QualitativeGameResult : public storm::utility::graph::GameProb01Result<Type>, public QualitativeResult<Type> {
+            QualitativeGameResult() = default;
+            
+            QualitativeGameResult(storm::utility::graph::GameProb01Result<Type> const& prob01Result) : storm::utility::graph::GameProb01Result<Type>(prob01Result) {
+                // Intentionally left empty.
+            }
+            
+            virtual storm::dd::Bdd<Type> const& getStates() const override {
+                return this->getPlayer1States();
+            }
+            
+        };
         
     }
 }

src/storm/abstraction/QualitativeGameResultMinMax.h

@@ -2,20 +2,37 @@
 
 #include "storm/storage/dd/DdType.h"
 
-#include "storm/utility/graph.h"
+#include "storm/abstraction/QualitativeResultMinMax.h"
+#include "storm/abstraction/QualitativeGameResult.h"
 
 namespace storm {
     namespace abstraction {
 
         template<storm::dd::DdType Type>
-        struct QualitativeGameResultMinMax {
+        struct QualitativeGameResultMinMax : public QualitativeResultMinMax<Type> {
         public:
             QualitativeGameResultMinMax() = default;
             
-            storm::utility::graph::GameProb01Result<Type> prob0Min;
-            storm::utility::graph::GameProb01Result<Type> prob1Min;
-            storm::utility::graph::GameProb01Result<Type> prob0Max;
-            storm::utility::graph::GameProb01Result<Type> prob1Max;
+            virtual QualitativeResult<Type> const& getProb0(storm::OptimizationDirection const& dir) const override {
+                if (dir == storm::OptimizationDirection::Minimize) {
+                    return prob0Min;
+                } else {
+                    return prob0Max;
+                }
+            }
+            
+            virtual QualitativeResult<Type> const& getProb1(storm::OptimizationDirection const& dir) const override {
+                if (dir == storm::OptimizationDirection::Minimize) {
+                    return prob1Min;
+                } else {
+                    return prob1Max;
+                }
+            }
+            
+            QualitativeGameResult<Type> prob0Min;
+            QualitativeGameResult<Type> prob1Min;
+            QualitativeGameResult<Type> prob0Max;
+            QualitativeGameResult<Type> prob1Max;
         };
 
     }

src/storm/abstraction/QualitativeMdpResult.h

@@ -1,12 +1,24 @@
 #pragma once
 
-#include "storm/utility/graph.h"
+#include "storm/abstraction/QualitativeResult.h"
 
 namespace storm {
     namespace abstraction {
         
         template <storm::dd::DdType Type>
-        using QualitativeMdpResult = std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>>;
+        struct QualitativeMdpResult : public QualitativeResult<Type> {
+            QualitativeMdpResult() = default;
+            
+            QualitativeMdpResult(storm::dd::Bdd<Type> const& states) : states(states) {
+                // Intentionally left empty.
+            }
+            
+            virtual storm::dd::Bdd<Type> const& getStates() const override {
+                return states;
+            }
+            
+            storm::dd::Bdd<Type> states;
+        };
         
     }
 }

src/storm/abstraction/QualitativeMdpResultMinMax.h

@@ -2,18 +2,37 @@
 
 #include "storm/storage/dd/DdType.h"
 
+#include "storm/abstraction/QualitativeResultMinMax.h"
 #include "storm/abstraction/QualitativeMdpResult.h"
 
 namespace storm {
     namespace abstraction {
         
         template<storm::dd::DdType Type>
-        struct QualitativeMdpResultMinMax {
+        struct QualitativeMdpResultMinMax : public QualitativeResultMinMax<Type> {
         public:
             QualitativeMdpResultMinMax() = default;
             
-            QualitativeMdpResult<Type> min;
-            QualitativeMdpResult<Type> max;
+            virtual QualitativeResult<Type> const& getProb0(storm::OptimizationDirection const& dir) const override {
+                if (dir == storm::OptimizationDirection::Minimize) {
+                    return prob0Min;
+                } else {
+                    return prob0Max;
+                }
+            }
+            
+            virtual QualitativeResult<Type> const& getProb1(storm::OptimizationDirection const& dir) const override {
+                if (dir == storm::OptimizationDirection::Minimize) {
+                    return prob1Min;
+                } else {
+                    return prob1Max;
+                }
+            }
+            
+            QualitativeMdpResult<Type> prob0Min;
+            QualitativeMdpResult<Type> prob1Min;
+            QualitativeMdpResult<Type> prob0Max;
+            QualitativeMdpResult<Type> prob1Max;
         };
         
     }

src/storm/abstraction/QualitativeResult.cpp

@@ -0,0 +1,3 @@
+#include "storm/abstraction/QualitativeResult.h"
+
+

src/storm/abstraction/QualitativeResult.h

@@ -0,0 +1,21 @@
+#pragma once
+
+#include "storm/storage/dd/DdType.h"
+
+namespace storm {
+    namespace dd {
+        template <storm::dd::DdType Type>
+        class Bdd;
+    }
+    
+    namespace abstraction {
+        
+        template <storm::dd::DdType Type>
+        struct QualitativeResult {
+            virtual storm::dd::Bdd<Type> const& getStates() const = 0;
+        };
+        
+    }
+}
+
+

src/storm/abstraction/QualitativeResultMinMax.cpp

@@ -0,0 +1,32 @@
+#include "storm/abstraction/QualitativeResultMinMax.h"
+
+#include "storm/abstraction/QualitativeResult.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template<storm::dd::DdType Type>
+        QualitativeResult<Type> const& QualitativeResultMinMax<Type>::getProb0Min() const {
+            return getProb0(storm::OptimizationDirection::Minimize);
+        }
+        
+        template<storm::dd::DdType Type>
+        QualitativeResult<Type> const& QualitativeResultMinMax<Type>::getProb1Min() const {
+            return getProb1(storm::OptimizationDirection::Minimize);
+        }
+        
+        template<storm::dd::DdType Type>
+        QualitativeResult<Type> const& QualitativeResultMinMax<Type>::getProb0Max() const {
+            return getProb0(storm::OptimizationDirection::Maximize);
+        }
+        
+        template<storm::dd::DdType Type>
+        QualitativeResult<Type> const& QualitativeResultMinMax<Type>::getProb1Max() const {
+            return getProb1(storm::OptimizationDirection::Maximize);
+        }
+        
+        template struct QualitativeResultMinMax<storm::dd::DdType::CUDD>;
+        template struct QualitativeResultMinMax<storm::dd::DdType::Sylvan>;
+
+    }
+}

src/storm/abstraction/QualitativeResultMinMax.h

@@ -0,0 +1,31 @@
+#pragma once
+
+#include "storm/solver/OptimizationDirection.h"
+
+#include "storm/storage/dd/DdType.h"
+
+namespace storm {
+    namespace dd {
+        template<storm::dd::DdType Type>
+        class Bdd;
+    }
+    
+    namespace abstraction {
+        template<storm::dd::DdType Type>
+        struct QualitativeResult;
+        
+        template<storm::dd::DdType Type>
+        struct QualitativeResultMinMax {
+        public:
+            QualitativeResultMinMax() = default;
+
+            QualitativeResult<Type> const& getProb0Min() const;
+            QualitativeResult<Type> const& getProb1Min() const;
+            QualitativeResult<Type> const& getProb0Max() const;
+            QualitativeResult<Type> const& getProb1Max() const;
+            
+            virtual QualitativeResult<Type> const& getProb0(storm::OptimizationDirection const& dir) const = 0;
+            virtual QualitativeResult<Type> const& getProb1(storm::OptimizationDirection const& dir) const = 0;
+        };
+    }
+}

src/storm/abstraction/QuantitativeGameResult.h

@@ -10,15 +10,51 @@ namespace storm {
         template<storm::dd::DdType Type, typename ValueType>
         struct QuantitativeGameResult {
             QuantitativeGameResult() = default;
+
+            QuantitativeGameResult(storm::dd::Add<Type, ValueType> const& values) : values(values) {
+                // Intentionally left empty.
+            }
             
-            QuantitativeGameResult(std::pair<ValueType, ValueType> initialStatesRange, storm::dd::Add<Type, ValueType> const& values, storm::dd::Bdd<Type> const& player1Strategy, storm::dd::Bdd<Type> const& player2Strategy) : initialStatesRange(initialStatesRange), values(values), player1Strategy(player1Strategy), player2Strategy(player2Strategy) {
+            QuantitativeGameResult(boost::optional<std::pair<ValueType, ValueType>> const& initialStatesRange, storm::dd::Add<Type, ValueType> const& values, boost::optional<storm::dd::Bdd<Type>> const& player1Strategy, boost::optional<storm::dd::Bdd<Type>> const& player2Strategy) : initialStatesRange(initialStatesRange), values(values), player1Strategy(player1Strategy), player2Strategy(player2Strategy) {
                 // Intentionally left empty.
             }
             
-            std::pair<ValueType, ValueType> initialStatesRange;
+            bool hasPlayer1Strategy() const {
+                return static_cast<bool>(player1Strategy);
+            }
+
+            storm::dd::Bdd<Type> const& getPlayer1Strategy() const {
+                return player1Strategy.get();
+            }
+
+            storm::dd::Bdd<Type>& getPlayer1Strategy() {
+                return player1Strategy.get();
+            }
+
+            bool hasPlayer2Strategy() const {
+                return static_cast<bool>(player2Strategy);
+            }
+
+            storm::dd::Bdd<Type> const& getPlayer2Strategy() const {
+                return player2Strategy.get();
+            }
+
+            storm::dd::Bdd<Type>& getPlayer2Strategy() {
+                return player2Strategy.get();
+            }
+
+            bool hasInitialStatesRange() const {
+                return static_cast<bool>(initialStatesRange);
+            }
+            
+            std::pair<ValueType, ValueType> const& getInitialStatesRange() const {
+                return initialStatesRange.get();
+            }
+
+            boost::optional<std::pair<ValueType, ValueType>> initialStatesRange;
             storm::dd::Add<Type, ValueType> values;
-            storm::dd::Bdd<Type> player1Strategy;
-            storm::dd::Bdd<Type> player2Strategy;
+            boost::optional<storm::dd::Bdd<Type>> player1Strategy;
+            boost::optional<storm::dd::Bdd<Type>> player2Strategy;
         };
         
     }

src/storm/modelchecker/AbstractModelChecker.cpp

@@ -15,6 +15,7 @@
 #include "storm/models/symbolic/Dtmc.h"
 #include "storm/models/symbolic/Ctmc.h"
 #include "storm/models/symbolic/Mdp.h"
+#include "storm/models/symbolic/StochasticTwoPlayerGame.h"
 #include "storm/models/sparse/MarkovAutomaton.h"
 #include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/models/symbolic/StandardRewardModel.h"
@@ -330,5 +331,9 @@ namespace storm {
         template class AbstractModelChecker<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double>>;
         template class AbstractModelChecker<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalNumber>>;
         template class AbstractModelChecker<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
+        template class AbstractModelChecker<storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD, double>>;
+        template class AbstractModelChecker<storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, double>>;
+        template class AbstractModelChecker<storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, storm::RationalNumber>>;
+        template class AbstractModelChecker<storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
     }
 }

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -34,7 +34,6 @@
 #include "storm/settings/modules/CoreSettings.h"
 #include "storm/settings/modules/AbstractionSettings.h"
 
-#include "storm/utility/solver.h"
 #include "storm/utility/prism.h"
 #include "storm/utility/macros.h"
 
@@ -257,10 +256,10 @@ namespace storm {
             }
             
             // Create the solver and solve the equation system.
-            storm::utility::solver::SymbolicGameSolverFactory<Type, ValueType> solverFactory;
+            storm::solver::SymbolicGameSolverFactory<Type, ValueType> solverFactory;
             std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> solver = solverFactory.create(submatrix, maybeStates, game.getIllegalPlayer1Mask(), game.getIllegalPlayer2Mask(), game.getRowVariables(), game.getColumnVariables(), game.getRowColumnMetaVariablePairs(), game.getPlayer1Variables(), game.getPlayer2Variables());
             solver->setGeneratePlayersStrategies(true);
-            auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector, startInfo ? boost::make_optional(startInfo.get().player1Strategy) : boost::none, startInfo ? boost::make_optional(startInfo.get().player2Strategy) : boost::none);
+            auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector, startInfo ? boost::make_optional(startInfo.get().getPlayer1Strategy()) : boost::none, startInfo ? boost::make_optional(startInfo.get().getPlayer2Strategy()) : boost::none);
             return QuantitativeGameResult<Type, ValueType>(std::make_pair(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>()), values, solver->getPlayer1Strategy(), solver->getPlayer2Strategy());
         }
         
@@ -294,8 +293,8 @@ namespace storm {
                 result = solveMaybeStates(player1Direction, player2Direction, game, maybeStates, min ? qualitativeResult.prob1Min.getPlayer1States() : qualitativeResult.prob1Max.getPlayer1States(), startInfo);
                 
                 // Cut the obtained strategies to the reachable states of the game.
-                result.player1Strategy &= game.getReachableStates();
-                result.player2Strategy &= game.getReachableStates();
+                result.getPlayer1Strategy() &= game.getReachableStates();
+                result.getPlayer2Strategy() &= game.getReachableStates();
                 
                 // Extend the values of the maybe states by the qualitative values.
                 result.values += min ? qualitativeResult.prob1Min.getPlayer1States().template toAdd<ValueType>() : qualitativeResult.prob1Max.getPlayer1States().template toAdd<ValueType>();
@@ -315,11 +314,11 @@ namespace storm {
             
             result.initialStatesRange = std::make_pair(minValueOverInitialStates, maxValueOverInitialStates);
             
-            result.player1Strategy = combinedPlayer1QualitativeStrategies.existsAbstract(game.getPlayer1Variables()).ite(combinedPlayer1QualitativeStrategies, result.player1Strategy);
-            result.player2Strategy = combinedPlayer2QualitativeStrategies.existsAbstract(game.getPlayer2Variables()).ite(combinedPlayer2QualitativeStrategies, result.player2Strategy);
+            result.player1Strategy = combinedPlayer1QualitativeStrategies.existsAbstract(game.getPlayer1Variables()).ite(combinedPlayer1QualitativeStrategies, result.getPlayer1Strategy());
+            result.player2Strategy = combinedPlayer2QualitativeStrategies.existsAbstract(game.getPlayer2Variables()).ite(combinedPlayer2QualitativeStrategies, result.getPlayer2Strategy());
             
             auto end = std::chrono::high_resolution_clock::now();
-            STORM_LOG_TRACE("Obtained quantitative " << (min ? "lower" : "upper") << " bound " << (min ? result.initialStatesRange.first : result.initialStatesRange.second) << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+            STORM_LOG_TRACE("Obtained quantitative " << (min ? "lower" : "upper") << " bound " << (min ? result.getInitialStatesRange().first : result.getInitialStatesRange().second) << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
             
             return result;
         }
@@ -431,7 +430,7 @@ namespace storm {
                     // (7) Solve the min values and check whether we can give the answer already.
                     quantitativeResult.min = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none);
                     previousMinQuantitativeResult = quantitativeResult.min;
-                    result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.initialStatesRange);
+                    result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.getInitialStatesRange());
                     if (result) {
                         printStatistics(*abstractor, game);
                         return result;
@@ -439,27 +438,27 @@ namespace storm {
                     
                     // (8) Solve the max values and check whether we can give the answer already.
                     quantitativeResult.max = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min));
-                    result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.initialStatesRange);
+                    result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.getInitialStatesRange());
                     if (result) {
                         printStatistics(*abstractor, game);
                         return result;
                     }
 
                     auto quantitativeEnd = std::chrono::high_resolution_clock::now();
-                    STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.min.initialStatesRange.first << ", " << quantitativeResult.max.initialStatesRange.second << "] on the actual value for the initial states in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeEnd - quantitativeStart).count() << "ms.");
+                    STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.min.getInitialStatesRange().first << ", " << quantitativeResult.max.getInitialStatesRange().second << "] on the actual value for the initial states in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeEnd - quantitativeStart).count() << "ms.");
                     
                     // (9) Check whether the lower and upper bounds are close enough to terminate with an answer.
-                    result = checkForResultAfterQuantitativeCheck<ValueType>(quantitativeResult.min.initialStatesRange.first, quantitativeResult.max.initialStatesRange.second, comparator);
+                    result = checkForResultAfterQuantitativeCheck<ValueType>(quantitativeResult.min.getInitialStatesRange().first, quantitativeResult.max.getInitialStatesRange().second, comparator);
                     if (result) {
                         printStatistics(*abstractor, game);
                         return result;
                     }
 
                     // Make sure that all strategies are still valid strategies.
-                    STORM_LOG_ASSERT(quantitativeResult.min.player1Strategy.isZero() || quantitativeResult.min.player1Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal.");
-                    STORM_LOG_ASSERT(quantitativeResult.max.player1Strategy.isZero() || quantitativeResult.max.player1Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal.");
-                    STORM_LOG_ASSERT(quantitativeResult.min.player2Strategy.isZero() || quantitativeResult.min.player2Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal.");
-                    STORM_LOG_ASSERT(quantitativeResult.max.player2Strategy.isZero() || quantitativeResult.max.player2Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal.");
+                    STORM_LOG_ASSERT(quantitativeResult.min.getPlayer1Strategy().isZero() || quantitativeResult.min.getPlayer1Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal.");
+                    STORM_LOG_ASSERT(quantitativeResult.max.getPlayer1Strategy().isZero() || quantitativeResult.max.getPlayer1Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal.");
+                    STORM_LOG_ASSERT(quantitativeResult.min.getPlayer2Strategy().isZero() || quantitativeResult.min.getPlayer2Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal.");
+                    STORM_LOG_ASSERT(quantitativeResult.max.getPlayer2Strategy().isZero() || quantitativeResult.max.getPlayer2Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal.");
 
                     auto quantitativeRefinementStart = std::chrono::high_resolution_clock::now();
                     // (10) If we arrived at this point, it means that we have all qualitative and quantitative

src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.cpp

@@ -18,10 +18,14 @@
 #include "storm/storage/dd/BisimulationDecomposition.h"
 
 #include "storm/abstraction/QualitativeMdpResultMinMax.h"
+#include "storm/abstraction/QualitativeGameResultMinMax.h"
+#include "storm/abstraction/QuantitativeGameResult.h"
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/AbstractionSettings.h"
 
+#include "storm/solver/SymbolicGameSolver.h"
+
 #include "storm/utility/macros.h"
 #include "storm/exceptions/NotSupportedException.h"
 #include "storm/exceptions/InvalidPropertyException.h"
@@ -119,7 +123,7 @@ namespace storm {
                         
                     if (!converged) {
                         STORM_LOG_TRACE("Performing bisimulation step.");
-                        bisimulation.compute(10);
+                        bisimulation.compute(1);
                     }
                 }
                 
@@ -184,7 +188,10 @@ namespace storm {
         }
         
         template<typename ModelType>
-        bool PartialBisimulationMdpModelChecker<ModelType>::boundsSufficient(storm::models::Model<ValueType> const& quotient, bool lowerBounds, QuantitativeCheckResult<ValueType> const& result, storm::logic::ComparisonType comparisonType, ValueType const& threshold) {
+        bool PartialBisimulationMdpModelChecker<ModelType>::checkForResult(storm::models::Model<ValueType> const& quotient, bool lowerBounds, QuantitativeCheckResult<ValueType> const& result, CheckTask<storm::logic::Formula> const& checkTask) {
+            storm::logic::ComparisonType comparisonType = checkTask.getBoundComparisonType();
+            ValueType threshold = checkTask.getBoundThreshold();
+            
             if (lowerBounds) {
                 if (storm::logic::isLowerBound(comparisonType)) {
                     ValueType minimalLowerBound = getExtremalBound(storm::OptimizationDirection::Minimize, result);
@@ -222,10 +229,11 @@ namespace storm {
         }
         
         template<typename ModelType>
-        std::pair<storm::dd::Bdd<PartialBisimulationMdpModelChecker<ModelType>::DdType>, storm::dd::Bdd<PartialBisimulationMdpModelChecker<ModelType>::DdType>> PartialBisimulationMdpModelChecker<ModelType>::getConstraintAndTargetStates(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
+        template<typename QuotientModelType>
+        std::pair<storm::dd::Bdd<PartialBisimulationMdpModelChecker<ModelType>::DdType>, storm::dd::Bdd<PartialBisimulationMdpModelChecker<ModelType>::DdType>> PartialBisimulationMdpModelChecker<ModelType>::getConstraintAndTargetStates(QuotientModelType const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
             std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> result;
             
-            SymbolicPropositionalModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>> checker(quotient);
+            SymbolicPropositionalModelChecker<QuotientModelType> checker(quotient);
             if (checkTask.getFormula().isUntilFormula()) {
                 std::unique_ptr<CheckResult> subresult = checker.check(checkTask.getFormula().asUntilFormula().getLeftSubformula());
                 result.first = subresult->asSymbolicQualitativeCheckResult<DdType>().getTruthValuesVector();
@@ -246,18 +254,24 @@ namespace storm {
         template<typename ModelType>
         storm::abstraction::QualitativeMdpResultMinMax<PartialBisimulationMdpModelChecker<ModelType>::DdType> PartialBisimulationMdpModelChecker<ModelType>::computeQualitativeResult(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask, storm::dd::Bdd<DdType> const& constraintStates, storm::dd::Bdd<DdType> const& targetStates) {
 
-            STORM_LOG_DEBUG("Computing qualitative solution.");
+            STORM_LOG_DEBUG("Computing qualitative solution for quotient MDP.");
             storm::abstraction::QualitativeMdpResultMinMax<DdType> result;
             
             auto start = std::chrono::high_resolution_clock::now();
             bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
             storm::dd::Bdd<DdType> transitionMatrixBdd = quotient.getTransitionMatrix().notZero();
             if (isRewardFormula) {
-                result.min.second = storm::utility::graph::performProb1E(quotient, transitionMatrixBdd, constraintStates, targetStates, storm::utility::graph::performProbGreater0E(quotient, transitionMatrixBdd, constraintStates, targetStates));
-                result.max.second = storm::utility::graph::performProb1A(quotient, transitionMatrixBdd, targetStates, storm::utility::graph::performProbGreater0A(quotient, transitionMatrixBdd, constraintStates, targetStates));
+                auto prob1 = storm::utility::graph::performProb1E(quotient, transitionMatrixBdd, constraintStates, targetStates, storm::utility::graph::performProbGreater0E(quotient, transitionMatrixBdd, constraintStates, targetStates));
+                result.prob1Min = storm::abstraction::QualitativeMdpResult<DdType>(prob1);
+                prob1 = storm::utility::graph::performProb1A(quotient, transitionMatrixBdd, targetStates, storm::utility::graph::performProbGreater0A(quotient, transitionMatrixBdd, constraintStates, targetStates));
+                result.prob1Max = storm::abstraction::QualitativeMdpResult<DdType>(prob1);
             } else {
-                result.min = storm::utility::graph::performProb01Min(quotient, transitionMatrixBdd, constraintStates, targetStates);
-                result.max = storm::utility::graph::performProb01Max(quotient, transitionMatrixBdd, constraintStates, targetStates);
+                auto prob01 = storm::utility::graph::performProb01Min(quotient, transitionMatrixBdd, constraintStates, targetStates);
+                result.prob0Min = storm::abstraction::QualitativeMdpResult<DdType>(prob01.first);
+                result.prob1Min = storm::abstraction::QualitativeMdpResult<DdType>(prob01.second);
+                prob01 = storm::utility::graph::performProb01Max(quotient, transitionMatrixBdd, constraintStates, targetStates);
+                result.prob0Max = storm::abstraction::QualitativeMdpResult<DdType>(prob01.first);
+                result.prob1Max = storm::abstraction::QualitativeMdpResult<DdType>(prob01.second);
             }
             auto end = std::chrono::high_resolution_clock::now();
 
@@ -266,25 +280,57 @@ namespace storm {
 
             return result;
         }
-        
+
         template<typename ModelType>
-        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::checkForResult(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, storm::abstraction::QualitativeMdpResultMinMax<DdType> const& qualitativeResults, CheckTask<storm::logic::Formula> const& checkTask) {
+        storm::abstraction::QualitativeGameResultMinMax<PartialBisimulationMdpModelChecker<ModelType>::DdType> PartialBisimulationMdpModelChecker<ModelType>::computeQualitativeResult(storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask, storm::dd::Bdd<DdType> const& constraintStates, storm::dd::Bdd<DdType> const& targetStates, storm::OptimizationDirection optimizationDirectionInModel) {
+            
+            STORM_LOG_DEBUG("Computing qualitative solution for quotient game.");
+            storm::abstraction::QualitativeGameResultMinMax<DdType> result;
+            
+            auto start = std::chrono::high_resolution_clock::now();
+            bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
+            storm::dd::Bdd<DdType> transitionMatrixBdd = quotient.getTransitionMatrix().notZero();
+            if (isRewardFormula) {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rewards are currently not supported for quotient stochastic games.");
+            } else {
+                result.prob0Min = storm::utility::graph::performProb0(quotient, quotient.getQualitativeTransitionMatrix(), constraintStates, targetStates, storm::OptimizationDirection::Minimize, optimizationDirectionInModel);
+                result.prob1Min = storm::utility::graph::performProb1(quotient, quotient.getQualitativeTransitionMatrix(), constraintStates, targetStates, storm::OptimizationDirection::Minimize, optimizationDirectionInModel);
+                result.prob0Max = storm::utility::graph::performProb0(quotient, quotient.getQualitativeTransitionMatrix(), constraintStates, targetStates, storm::OptimizationDirection::Maximize, optimizationDirectionInModel);
+                result.prob1Max = storm::utility::graph::performProb1(quotient, quotient.getQualitativeTransitionMatrix(), constraintStates, targetStates, storm::OptimizationDirection::Maximize, optimizationDirectionInModel);
+            }
+            auto end = std::chrono::high_resolution_clock::now();
+            
+            auto timeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count();
+            STORM_LOG_DEBUG("Computed qualitative solution in " << timeInMilliseconds << "ms.");
+            
+            return result;
+        }
+
+        template<typename ModelType>
+        std::unique_ptr<CheckResult> PartialBisimulationMdpModelChecker<ModelType>::checkForResult(storm::models::symbolic::Model<DdType, ValueType> const& quotient, storm::abstraction::QualitativeResultMinMax<DdType> const& qualitativeResults, CheckTask<storm::logic::Formula> const& checkTask) {
             std::unique_ptr<CheckResult> result;
             
             bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
             if (isRewardFormula) {
                 // In the reachability reward case, we can give an answer if all initial states of the system are infinity
                 // states in the min result.
-                if ((quotient.getInitialStates() && !qualitativeResults.min.second) == quotient.getInitialStates()) {
+                if ((quotient.getInitialStates() && !qualitativeResults.getProb1Min().getStates()) == quotient.getInitialStates()) {
                     result = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(quotient.getReachableStates(), quotient.getInitialStates(), quotient.getInitialStates().ite(quotient.getManager().getConstant(storm::utility::infinity<ValueType>()), quotient.getManager().template getAddZero<ValueType>()));
                 }
             } else {
                 // In the reachability probability case, we can give the answer if all initial states are prob1 states
                 // in the min result or if all initial states are prob0 in the max case.
-                if ((quotient.getInitialStates() && qualitativeResults.min.second) == quotient.getInitialStates()) {
+                // Furthermore, we can give the answer if there are initial states with probability > 0 in the min case
+                // and the probability bound was 0 or if there are initial states with probability < 1 in the max case
+                // and the probability bound was 1.
+                if ((quotient.getInitialStates() && qualitativeResults.getProb1Min().getStates()) == quotient.getInitialStates()) {
                     result = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(quotient.getReachableStates(), quotient.getInitialStates(), quotient.getManager().template getAddOne<ValueType>());
-                } else if ((quotient.getInitialStates() && qualitativeResults.max.first) == quotient.getInitialStates()) {
+                } else if ((quotient.getInitialStates() && qualitativeResults.getProb0Max().getStates()) == quotient.getInitialStates()) {
                     result = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(quotient.getReachableStates(), quotient.getInitialStates(), quotient.getManager().template getAddZero<ValueType>());
+                } else if (checkTask.isBoundSet() && checkTask.getBoundThreshold() == storm::utility::zero<ValueType>() && (quotient.getInitialStates() && qualitativeResults.getProb0Min().getStates()) != quotient.getInitialStates()) {
+                    result = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(quotient.getReachableStates(), quotient.getInitialStates(), (quotient.getInitialStates() && qualitativeResults.getProb0Min().getStates()).ite(quotient.getManager().template getConstant<ValueType>(0.5), quotient.getManager().template getAddZero<ValueType>()));
+                } else if (checkTask.isBoundSet() && checkTask.getBoundThreshold() == storm::utility::one<ValueType>() && (quotient.getInitialStates() && qualitativeResults.getProb1Max().getStates()) != quotient.getInitialStates()) {
+                    result = std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>>(quotient.getReachableStates(), quotient.getInitialStates(), (quotient.getInitialStates() && qualitativeResults.getProb1Max().getStates()).ite(quotient.getManager().template getConstant<ValueType>(0.5), quotient.getManager().template getAddZero<ValueType>()) + qualitativeResults.getProb1Max().getStates().template toAdd<ValueType>());
                 }
             }
             
@@ -292,17 +338,17 @@ namespace storm {
         }
         
         template<typename ModelType>
-        bool PartialBisimulationMdpModelChecker<ModelType>::skipQuantitativeSolution(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, storm::abstraction::QualitativeMdpResultMinMax<DdType> const& qualitativeResults, CheckTask<storm::logic::Formula> const& checkTask) {
+        bool PartialBisimulationMdpModelChecker<ModelType>::skipQuantitativeSolution(storm::models::symbolic::Model<DdType, ValueType> const& quotient, storm::abstraction::QualitativeResultMinMax<DdType> const& qualitativeResults, CheckTask<storm::logic::Formula> const& checkTask) {
             
             bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
             if (isRewardFormula) {
-                if ((quotient.getInitialStates() && qualitativeResults.min.second) != (quotient.getInitialStates() && qualitativeResults.max.second)) {
+                if ((quotient.getInitialStates() && qualitativeResults.getProb1Min().getStates()) != (quotient.getInitialStates() && qualitativeResults.getProb1Max().getStates())) {
                     return true;
                 }
             } else {
-                if ((quotient.getInitialStates() && qualitativeResults.min.first) != (quotient.getInitialStates() && qualitativeResults.max.first)) {
+                if ((quotient.getInitialStates() && qualitativeResults.getProb0Min().getStates()) != (quotient.getInitialStates() && qualitativeResults.getProb0Max().getStates())) {
                     return true;
-                } else if ((quotient.getInitialStates() && qualitativeResults.min.second) != (quotient.getInitialStates() && qualitativeResults.max.second)) {
+                } else if ((quotient.getInitialStates() && qualitativeResults.getProb1Min().getStates()) != (quotient.getInitialStates() && qualitativeResults.getProb1Max().getStates())) {
                     return true;
                 }
             }
@@ -310,31 +356,75 @@ namespace storm {
         }
         
         template<typename ModelType>
-        std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeQuantitativeResult(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask, storm::dd::Bdd<DdType> const& constraintStates, storm::dd::Bdd<DdType> const& targetStates, storm::abstraction::QualitativeMdpResultMinMax<DdType> const& qualitativeResults) {
+        std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeQuantitativeResult(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask, storm::dd::Bdd<DdType> const& constraintStates, storm::dd::Bdd<DdType> const& targetStates, storm::abstraction::QualitativeResultMinMax<DdType> const& qualitativeResults) {
 
             std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> result;
             
             bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
             if (isRewardFormula) {
-                storm::dd::Bdd<DdType> maybeMin = qualitativeResults.min.second && quotient.getReachableStates();
-                result.first = storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(storm::OptimizationDirection::Minimize, quotient, quotient.getTransitionMatrix(), quotient.getTransitionMatrix().notZero(), checkTask.isRewardModelSet() ? quotient.getRewardModel(checkTask.getRewardModel()) : quotient.getRewardModel(""), maybeMin, targetStates, !qualitativeResults.min.second && quotient.getReachableStates(), storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType>(), quotient.getManager().template getAddZero<ValueType>());
+                storm::dd::Bdd<DdType> maybeMin = qualitativeResults.getProb1Min().getStates() && quotient.getReachableStates();
+                result.first = storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(storm::OptimizationDirection::Minimize, quotient, quotient.getTransitionMatrix(), quotient.getTransitionMatrix().notZero(), checkTask.isRewardModelSet() ? quotient.getRewardModel(checkTask.getRewardModel()) : quotient.getRewardModel(""), maybeMin, targetStates, !qualitativeResults.getProb1Min().getStates() && quotient.getReachableStates(), storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType>(), quotient.getManager().template getAddZero<ValueType>());
                 
-                storm::dd::Bdd<DdType> maybeMax = qualitativeResults.max.second && quotient.getReachableStates();
-                result.second = storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(storm::OptimizationDirection::Maximize, quotient, quotient.getTransitionMatrix(), quotient.getTransitionMatrix().notZero(), checkTask.isRewardModelSet() ? quotient.getRewardModel(checkTask.getRewardModel()) : quotient.getRewardModel(""), maybeMin, targetStates, !qualitativeResults.min.second && quotient.getReachableStates(), storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType>(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector(), quotient.getManager().template getAddZero<ValueType>()));
+                storm::dd::Bdd<DdType> maybeMax = qualitativeResults.getProb1Max().getStates() && quotient.getReachableStates();
+                result.second = storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeReachabilityRewards(storm::OptimizationDirection::Maximize, quotient, quotient.getTransitionMatrix(), quotient.getTransitionMatrix().notZero(), checkTask.isRewardModelSet() ? quotient.getRewardModel(checkTask.getRewardModel()) : quotient.getRewardModel(""), maybeMin, targetStates, !qualitativeResults.getProb1Max().getStates() && quotient.getReachableStates(), storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType>(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector(), quotient.getManager().template getAddZero<ValueType>()));
             } else {
-                storm::dd::Bdd<DdType> maybeMin = !(qualitativeResults.min.first || qualitativeResults.min.second) && quotient.getReachableStates();
-                result.first = storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeUntilProbabilities(storm::OptimizationDirection::Minimize, quotient, quotient.getTransitionMatrix(), maybeMin, qualitativeResults.min.second, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType>(), quotient.getManager().template getAddZero<ValueType>());
+                storm::dd::Bdd<DdType> maybeMin = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && quotient.getReachableStates();
+                result.first = storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeUntilProbabilities(storm::OptimizationDirection::Minimize, quotient, quotient.getTransitionMatrix(), maybeMin, qualitativeResults.getProb1Min().getStates(), storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType>(), quotient.getManager().template getAddZero<ValueType>());
                 
-                storm::dd::Bdd<DdType> maybeMax = !(qualitativeResults.max.first || qualitativeResults.max.second) && quotient.getReachableStates();
-                result.second = storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeUntilProbabilities(storm::OptimizationDirection::Maximize, quotient, quotient.getTransitionMatrix(), maybeMax, qualitativeResults.max.second, storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType>(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector(), quotient.getManager().template getAddZero<ValueType>()));
+                storm::dd::Bdd<DdType> maybeMax = !(qualitativeResults.getProb0Max().getStates() || qualitativeResults.getProb1Max().getStates()) && quotient.getReachableStates();
+                result.second = storm::modelchecker::helper::SymbolicMdpPrctlHelper<DdType, ValueType>::computeUntilProbabilities(storm::OptimizationDirection::Maximize, quotient, quotient.getTransitionMatrix(), maybeMax, qualitativeResults.getProb1Max().getStates(), storm::solver::SymbolicGeneralMinMaxLinearEquationSolverFactory<DdType, ValueType>(), maybeMax.ite(result.first->asSymbolicQuantitativeCheckResult<DdType, ValueType>().getValueVector(), quotient.getManager().template getAddZero<ValueType>()));
             }
             
             return result;
         }
+
+        template<storm::dd::DdType Type, typename ValueType>
+        std::unique_ptr<CheckResult> computeReachabilityProbabilitiesHelper(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& quotient, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction,  storm::dd::Bdd<Type> const& maybeStates, storm::dd::Bdd<Type> const& prob1States) {
+            
+            STORM_LOG_TRACE("Performing quantative solution step. Player 1: " << player1Direction << ", player 2: " << player2Direction << ".");
+            
+            // Compute the ingredients of the equation system.
+            storm::dd::Add<Type, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
+            storm::dd::Add<Type, ValueType> submatrix = maybeStatesAdd * quotient.getTransitionMatrix();
+            storm::dd::Add<Type, ValueType> prob1StatesAsColumn = prob1States.template toAdd<ValueType>().swapVariables(quotient.getRowColumnMetaVariablePairs());
+            storm::dd::Add<Type, ValueType> subvector = submatrix * prob1StatesAsColumn;
+            subvector = subvector.sumAbstract(quotient.getColumnVariables());
+            
+            // Cut away all columns targeting non-maybe states.
+            submatrix *= maybeStatesAdd.swapVariables(quotient.getRowColumnMetaVariablePairs());
+            
+            // Cut the starting vector to the maybe states of this query.
+            storm::dd::Add<Type, ValueType> startVector = quotient.getManager().template getAddZero<ValueType>();
+            
+            // Create the solver and solve the equation system.
+            storm::solver::SymbolicGameSolverFactory<Type, ValueType> solverFactory;
+            std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> solver = solverFactory.create(submatrix, maybeStates, quotient.getIllegalPlayer1Mask(), quotient.getIllegalPlayer2Mask(), quotient.getRowVariables(), quotient.getColumnVariables(), quotient.getRowColumnMetaVariablePairs(), quotient.getPlayer1Variables(), quotient.getPlayer2Variables());
+            auto values = solver->solveGame(player1Direction, player2Direction, startVector, subvector);
+            
+            return std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<Type, ValueType>>(quotient.getReachableStates(), prob1States.template toAdd<ValueType>() + values);
+        }
         
         template<typename ModelType>
-        std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
+        std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeQuantitativeResult(storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask, storm::dd::Bdd<DdType> const& constraintStates, storm::dd::Bdd<DdType> const& targetStates, storm::abstraction::QualitativeResultMinMax<DdType> const& qualitativeResults) {
+            
+            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> result;
+            
+            bool isRewardFormula = checkTask.getFormula().isEventuallyFormula() && checkTask.getFormula().asEventuallyFormula().getContext() == storm::logic::FormulaContext::Reward;
+            if (isRewardFormula) {
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Computing rewards for stochastic games is currently unsupported.");
+            } else {
+                storm::dd::Bdd<DdType> maybeMin = !(qualitativeResults.getProb0Min().getStates() || qualitativeResults.getProb1Min().getStates()) && quotient.getReachableStates();
+                result.first = computeReachabilityProbabilitiesHelper(quotient, storm::OptimizationDirection::Minimize, checkTask.getOptimizationDirection(), maybeMin, qualitativeResults.getProb1Min().getStates());
+                
+                storm::dd::Bdd<DdType> maybeMax = !(qualitativeResults.getProb0Max().getStates() || qualitativeResults.getProb1Max().getStates()) && quotient.getReachableStates();
+                result.second = computeReachabilityProbabilitiesHelper(quotient, storm::OptimizationDirection::Maximize, checkTask.getOptimizationDirection(), maybeMin, qualitativeResults.getProb1Max().getStates());
+            }
+            
+            return result;
+        }
 
+        template<typename ModelType>
+        std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
             std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> result;
 
             // We go through two phases. In phase (1) we are solving the qualitative part and in phase (2) the quantitative part.
@@ -364,13 +454,58 @@ namespace storm {
                 result.first->filter(initialStateFilter);
                 result.second->filter(initialStateFilter);
                 printBoundsInformation(result);
+                
+                // Check whether the answer can be given after the quantitative solution.
+                if (checkForResult(quotient, true, result.first->asQuantitativeCheckResult<ValueType>(), checkTask)) {
+                    result.second = nullptr;
+                }
+                if (checkForResult(quotient, false, result.second->asQuantitativeCheckResult<ValueType>(), checkTask)) {
+                    result.first = nullptr;
+                }
             }
             return result;
         }
 
         template<typename ModelType>
         std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> PartialBisimulationMdpModelChecker<ModelType>::computeBoundsPartialQuotient(storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask) {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Currently not implemented.");
+            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> result;
+            
+            // We go through two phases. In phase (1) we are solving the qualitative part and in phase (2) the quantitative part.
+            
+            // Preparation: determine the constraint states and the target states of the reachability objective.
+            std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> constraintTargetStates = getConstraintAndTargetStates(quotient, checkTask);
+            
+            // Phase (1): solve qualitatively.
+            storm::abstraction::QualitativeGameResultMinMax<DdType> qualitativeResults = computeQualitativeResult(quotient, checkTask, constraintTargetStates.first, constraintTargetStates.second, checkTask.getOptimizationDirection());
+            
+            // Check whether the answer can be given after the qualitative solution.
+            result.first = checkForResult(quotient, qualitativeResults, checkTask);
+            if (result.first) {
+                return result;
+            }
+
+            // Check whether we should skip the quantitative solution (for example if there are initial states for which
+            // the value is already known to be different at this point.
+            bool doSkipQuantitativeSolution = skipQuantitativeSolution(quotient, qualitativeResults, checkTask);
+            STORM_LOG_TRACE("" << (doSkipQuantitativeSolution ? "Skipping" : "Not skipping") << " quantitative solution.");
+
+            // Phase (2): solve quantitatively.
+            if (!doSkipQuantitativeSolution) {
+                result = computeQuantitativeResult(quotient, checkTask, constraintTargetStates.first, constraintTargetStates.second, qualitativeResults);
+
+                storm::modelchecker::SymbolicQualitativeCheckResult<DdType> initialStateFilter(quotient.getReachableStates(), quotient.getInitialStates());
+                result.first->filter(initialStateFilter);
+                result.second->filter(initialStateFilter);
+                printBoundsInformation(result);
+                
+                // Check whether the answer can be given after the quantitative solution.
+                if (checkForResult(quotient, true, result.first->asQuantitativeCheckResult<ValueType>(), checkTask)) {
+                    result.second = nullptr;
+                } else if (checkForResult(quotient, false, result.second->asQuantitativeCheckResult<ValueType>(), checkTask)) {
+                    result.first = nullptr;
+                }
+            }
+            return result;
         }
 
         template<typename ModelType>

src/storm/modelchecker/abstraction/PartialBisimulationMdpModelChecker.h

@@ -17,6 +17,9 @@ namespace storm {
         class Model;
 
         namespace symbolic {
+            template <storm::dd::DdType DdType, typename ValueType>
+            class Model;
+            
             template <storm::dd::DdType DdType, typename ValueType>
             class Dtmc;
             
@@ -29,8 +32,14 @@ namespace storm {
     }
     
     namespace abstraction {
+        template <storm::dd::DdType DdType>
+        struct QualitativeResultMinMax;
+        
         template <storm::dd::DdType DdType>
         struct QualitativeMdpResultMinMax;
+        
+        template <storm::dd::DdType DdType>
+        struct QualitativeGameResultMinMax;
     }
     
     namespace modelchecker {
@@ -67,21 +76,23 @@ namespace storm {
 
             // Methods related to the qualitative solution.
             storm::abstraction::QualitativeMdpResultMinMax<DdType> computeQualitativeResult(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask, storm::dd::Bdd<DdType> const& constraintStates, storm::dd::Bdd<DdType> const& targetStates);
-            std::unique_ptr<CheckResult> checkForResult(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, storm::abstraction::QualitativeMdpResultMinMax<DdType> const& qualitativeResults, CheckTask<storm::logic::Formula> const& checkTask);
-            bool skipQuantitativeSolution(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, storm::abstraction::QualitativeMdpResultMinMax<DdType> const& qualitativeResults, CheckTask<storm::logic::Formula> const& checkTask);
+            storm::abstraction::QualitativeGameResultMinMax<DdType> computeQualitativeResult(storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask, storm::dd::Bdd<DdType> const& constraintStates, storm::dd::Bdd<DdType> const& targetStates, storm::OptimizationDirection optimizationDirectionInModel);
+            std::unique_ptr<CheckResult> checkForResult(storm::models::symbolic::Model<DdType, ValueType> const& quotient, storm::abstraction::QualitativeResultMinMax<DdType> const& qualitativeResults, CheckTask<storm::logic::Formula> const& checkTask);
+            bool skipQuantitativeSolution(storm::models::symbolic::Model<DdType, ValueType> const& quotient, storm::abstraction::QualitativeResultMinMax<DdType> const& qualitativeResults, CheckTask<storm::logic::Formula> const& checkTask);
 
             // Methods related to the quantitative solution.
-            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeQuantitativeResult(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask, storm::dd::Bdd<DdType> const& constraintStates, storm::dd::Bdd<DdType> const& targetStates, storm::abstraction::QualitativeMdpResultMinMax<DdType> const& qualitativeResults);
-            
+            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeQuantitativeResult(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask, storm::dd::Bdd<DdType> const& constraintStates, storm::dd::Bdd<DdType> const& targetStates, storm::abstraction::QualitativeResultMinMax<DdType> const& qualitativeResults);
+            std::pair<std::unique_ptr<CheckResult>, std::unique_ptr<CheckResult>> computeQuantitativeResult(storm::models::symbolic::StochasticTwoPlayerGame<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask, storm::dd::Bdd<DdType> const& constraintStates, storm::dd::Bdd<DdType> const& targetStates, storm::abstraction::QualitativeResultMinMax<DdType> const& qualitativeResults);
+
             // Retrieves the constraint and target states of the quotient wrt. to the formula in the check task.
-            std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> getConstraintAndTargetStates(storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, CheckTask<storm::logic::Formula> const& checkTask);
+            template<typename QuotientModelType>
+            std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>> getConstraintAndTargetStates(QuotientModelType const& quotient, CheckTask<storm::logic::Formula> const& checkTask);
             
             // Retrieves the extremal bound (wrt. to the optimization direction) of the quantitative check result.
             ValueType getExtremalBound(storm::OptimizationDirection dir, QuantitativeCheckResult<ValueType> const& result);
             
-            // Retrieves whether the quantitative bounds are sufficient to answer the the query given by the bound (comparison
-            // type and threshold).
-            bool boundsSufficient(storm::models::Model<ValueType> const& quotient, bool lowerBounds, QuantitativeCheckResult<ValueType> const& result, storm::logic::ComparisonType comparisonType, ValueType const& threshold);
+            // Checks whether the quantitative result is sufficient for answering the query.
+            bool checkForResult(storm::models::Model<ValueType> const& quotient, bool lowerBounds, QuantitativeCheckResult<ValueType> const& result, CheckTask<storm::logic::Formula> const& checkTask);
             
             // Methods to compute bounds on the partial quotient.
             std::unique_ptr<CheckResult> computeBoundsPartialQuotient(SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<DdType, ValueType>>& checker, storm::models::symbolic::Mdp<DdType, ValueType> const& quotient, storm::OptimizationDirection const& dir, CheckTask<storm::logic::Formula>& checkTask);

src/storm/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp

@@ -6,6 +6,7 @@
 #include "storm/models/symbolic/Dtmc.h"
 #include "storm/models/symbolic/Ctmc.h"
 #include "storm/models/symbolic/Mdp.h"
+#include "storm/models/symbolic/StochasticTwoPlayerGame.h"
 #include "storm/models/symbolic/StandardRewardModel.h"
 
 #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
@@ -61,18 +62,22 @@ namespace storm {
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>;
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double>>;
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>;
+        template class SymbolicPropositionalModelChecker<storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD, double>>;
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double>>;
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>;
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double>>;
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>;
+        template class SymbolicPropositionalModelChecker<storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, double>>;
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalNumber>>;
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalNumber>>;
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalNumber>>;
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, storm::RationalNumber>>;
+        template class SymbolicPropositionalModelChecker<storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, storm::RationalNumber>>;
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
         template class SymbolicPropositionalModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
+        template class SymbolicPropositionalModelChecker<storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
 
     }
 }

src/storm/solver/SymbolicGameSolver.cpp

@@ -150,9 +150,16 @@ namespace storm {
             return player2Strategy.get();
         }
 
+        template<storm::dd::DdType Type, typename ValueType>
+        std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> SymbolicGameSolverFactory<Type, ValueType>::create(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables) const {
+            return std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>>(new storm::solver::SymbolicGameSolver<Type, ValueType>(A, allRows, illegalPlayer1Mask, illegalPlayer2Mask, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables));
+        }
         
         template class SymbolicGameSolver<storm::dd::DdType::CUDD, double>;
         template class SymbolicGameSolver<storm::dd::DdType::Sylvan, double>;
         
+        template class SymbolicGameSolverFactory<storm::dd::DdType::CUDD, double>;
+        template class SymbolicGameSolverFactory<storm::dd::DdType::Sylvan, double>;
+        
     }
 }

src/storm/solver/SymbolicGameSolver.h

@@ -130,6 +130,12 @@ namespace storm {
             bool relative;
         };
         
+        template<storm::dd::DdType Type, typename ValueType>
+        class SymbolicGameSolverFactory {
+        public:
+            virtual std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> create(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables) const;
+        };
+        
     } // namespace solver
 } // namespace storm
 

src/storm/storage/dd/bisimulation/SignatureRefiner.cpp

@@ -183,8 +183,6 @@ namespace storm {
                         bool skipped = true;
                         DdNode* partitionThen;
                         DdNode* partitionElse;
-                        DdNode* signatureThen;
-                        DdNode* signatureElse;
                         short offset;
                         bool isNondeterminismVariable = false;
                         while (skipped && !Cudd_IsConstant(nonBlockVariablesNode)) {

src/storm/utility/solver.cpp

@@ -21,12 +21,7 @@
 namespace storm {
     namespace utility {
         namespace solver {
-            
-            template<storm::dd::DdType Type, typename ValueType>
-            std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> SymbolicGameSolverFactory<Type, ValueType>::create(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables) const {
-                return std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>>(new storm::solver::SymbolicGameSolver<Type, ValueType>(A, allRows, illegalPlayer1Mask, illegalPlayer2Mask, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables));
-            }
-            
+                        
             template<typename ValueType>
             std::unique_ptr<storm::solver::LpSolver<ValueType>> LpSolverFactory<ValueType>::create(std::string const& name, storm::solver::LpSolverTypeSelection solvT) const {
                 storm::solver::LpSolverType t;
@@ -111,8 +106,6 @@ namespace storm {
                 return factory->create(manager);
             }
             
-            template class SymbolicGameSolverFactory<storm::dd::DdType::CUDD, double>;
-            template class SymbolicGameSolverFactory<storm::dd::DdType::Sylvan, double>;
             template class LpSolverFactory<double>;
             template class LpSolverFactory<storm::RationalNumber>;
             template class GlpkLpSolverFactory<double>;

src/storm/utility/solver.h

@@ -56,12 +56,6 @@ namespace storm {
     namespace utility {
         namespace solver {
             
-            template<storm::dd::DdType Type, typename ValueType>
-            class SymbolicGameSolverFactory {
-            public:
-                virtual std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> create(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables) const;
-            };
-
             template<typename ValueType>
             class LpSolverFactory {
             public: