started on refining menu games based on explicit results

src/storm/abstraction/ExplicitGameStrategy.cpp

@@ -0,0 +1,39 @@
+#include "storm/abstraction/ExplicitGameStrategy.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        const uint64_t ExplicitGameStrategy::UNDEFINED = std::numeric_limits<uint64_t>::max();
+        
+        ExplicitGameStrategy::ExplicitGameStrategy(uint64_t numberOfStates) : choices(numberOfStates, UNDEFINED) {
+            // Intentionally left empty.
+        }
+        
+        ExplicitGameStrategy::ExplicitGameStrategy(std::vector<uint64_t>&& choices) : choices(std::move(choices)) {
+            // Intentionally left empty.
+        }
+        
+        uint64_t ExplicitGameStrategy::getNumberOfStates() const {
+            return choices.size();
+        }
+        
+        uint64_t ExplicitGameStrategy::getChoice(uint64_t state) const {
+            return choices[state];
+        }
+        
+        void ExplicitGameStrategy::setChoice(uint64_t state, uint64_t choice) {
+            choices[state] = choice;
+        }
+        
+        bool ExplicitGameStrategy::hasDefinedChoice(uint64_t state) const {
+            return choices[state] != UNDEFINED;
+        }
+        
+        void ExplicitGameStrategy::undefineAll() {
+            for (auto& e : choices) {
+                e = UNDEFINED;
+            }
+        }
+        
+    }
+}

src/storm/abstraction/ExplicitGameStrategy.h

@@ -0,0 +1,27 @@
+#pragma once
+
+#include <cstdint>
+#include <vector>
+
+namespace storm {
+    namespace abstraction {
+        
+        class ExplicitGameStrategy {
+        public:
+            static const uint64_t UNDEFINED;
+            
+            ExplicitGameStrategy(uint64_t numberOfStates);
+            ExplicitGameStrategy(std::vector<uint64_t>&& choices);
+            
+            uint64_t getNumberOfStates() const;
+            uint64_t getChoice(uint64_t state) const;
+            void setChoice(uint64_t state, uint64_t choice);
+            bool hasDefinedChoice(uint64_t state) const;
+            void undefineAll();
+            
+        private:
+            std::vector<uint64_t> choices;
+        };
+        
+    }
+}

src/storm/abstraction/ExplicitGameStrategyPair.cpp

@@ -0,0 +1,31 @@
+#include "storm/abstraction/ExplicitGameStrategyPair.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        ExplicitGameStrategyPair::ExplicitGameStrategyPair(uint64_t numberOfPlayer1States, uint64_t numberOfPlayer2States) : player1Strategy(numberOfPlayer1States), player2Strategy(numberOfPlayer2States) {
+            // Intentionally left empty.
+        }
+        
+        ExplicitGameStrategyPair::ExplicitGameStrategyPair(ExplicitGameStrategy&& player1Strategy, ExplicitGameStrategy&& player2Strategy) : player1Strategy(std::move(player1Strategy)), player2Strategy(std::move(player2Strategy)) {
+            // Intentionally left empty.
+        }
+        
+        ExplicitGameStrategy& ExplicitGameStrategyPair::getPlayer1Strategy() {
+            return player1Strategy;
+        }
+        
+        ExplicitGameStrategy const& ExplicitGameStrategyPair::getPlayer1Strategy() const {
+            return player1Strategy;
+        }
+        
+        ExplicitGameStrategy& ExplicitGameStrategyPair::getPlayer2Strategy() {
+            return player2Strategy;
+        }
+        
+        ExplicitGameStrategy const& ExplicitGameStrategyPair::getPlayer2Strategy() const {
+            return player2Strategy;
+        }
+        
+    }
+}

src/storm/abstraction/ExplicitGameStrategyPair.h

@@ -0,0 +1,26 @@
+#pragma once
+
+#include <cstdint>
+
+#include "storm/abstraction/ExplicitGameStrategy.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        class ExplicitGameStrategyPair {
+        public:
+            ExplicitGameStrategyPair(uint64_t numberOfPlayer1States, uint64_t numberOfPlayer2States);
+            ExplicitGameStrategyPair(ExplicitGameStrategy&& player1Strategy, ExplicitGameStrategy&& player2Strategy);
+
+            ExplicitGameStrategy& getPlayer1Strategy();
+            ExplicitGameStrategy const& getPlayer1Strategy() const;
+            ExplicitGameStrategy& getPlayer2Strategy();
+            ExplicitGameStrategy const& getPlayer2Strategy() const;
+
+        private:
+            ExplicitGameStrategy player1Strategy;
+            ExplicitGameStrategy player2Strategy;
+        };
+        
+    }
+}

src/storm/abstraction/ExplicitQualitativeGameResultMinMax.cpp

@@ -19,6 +19,21 @@ namespace storm {
             }
         }
         
+        ExplicitQualitativeGameResult& ExplicitQualitativeGameResultMinMax::getProb0(storm::OptimizationDirection const& dir) {
+            if (dir == storm::OptimizationDirection::Minimize) {
+                return prob0Min;
+            } else {
+                return prob0Max;
+            }
+        }
+        
+        ExplicitQualitativeGameResult& ExplicitQualitativeGameResultMinMax::getProb1(storm::OptimizationDirection const& dir) {
+            if (dir == storm::OptimizationDirection::Minimize) {
+                return prob1Min;
+            } else {
+                return prob1Max;
+            }
+        }
     }
 }
 

src/storm/abstraction/ExplicitQualitativeGameResultMinMax.h

@@ -12,7 +12,9 @@ namespace storm {
             
             virtual ExplicitQualitativeGameResult const& getProb0(storm::OptimizationDirection const& dir) const override;
             virtual ExplicitQualitativeGameResult const& getProb1(storm::OptimizationDirection const& dir) const override;
-            
+            virtual ExplicitQualitativeGameResult& getProb0(storm::OptimizationDirection const& dir) override;
+            virtual ExplicitQualitativeGameResult& getProb1(storm::OptimizationDirection const& dir) override;
+
             ExplicitQualitativeGameResult prob0Min;
             ExplicitQualitativeGameResult prob1Min;
             ExplicitQualitativeGameResult prob0Max;

src/storm/abstraction/ExplicitQualitativeResult.cpp

@@ -0,0 +1,17 @@
+#include "storm/abstraction/ExplicitQualitativeResult.h"
+
+#include "storm/abstraction/ExplicitQualitativeGameResult.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        ExplicitQualitativeGameResult& ExplicitQualitativeResult::asExplicitQualitativeGameResult() {
+            return static_cast<ExplicitQualitativeGameResult&>(*this);
+        }
+        
+        ExplicitQualitativeGameResult const& ExplicitQualitativeResult::asExplicitQualitativeGameResult() const {
+            return static_cast<ExplicitQualitativeGameResult const&>(*this);
+        }
+        
+    }
+}

src/storm/abstraction/ExplicitQualitativeResult.h

@@ -10,11 +10,16 @@ namespace storm {
     }
     
     namespace abstraction {
+
+        class ExplicitQualitativeGameResult;
         
         class ExplicitQualitativeResult : public QualitativeResult {
         public:
             virtual ~ExplicitQualitativeResult() = default;
             
+            ExplicitQualitativeGameResult& asExplicitQualitativeGameResult();
+            ExplicitQualitativeGameResult const& asExplicitQualitativeGameResult() const;
+
             virtual storm::storage::BitVector const& getStates() const = 0;
         };
         

src/storm/abstraction/ExplicitQualitativeResultMinMax.cpp

@@ -25,5 +25,21 @@ namespace storm {
             return getProb1(storm::OptimizationDirection::Maximize);
         }
         
+        ExplicitQualitativeResult& ExplicitQualitativeResultMinMax::getProb0Min() {
+            return getProb0(storm::OptimizationDirection::Minimize);
+        }
+        
+        ExplicitQualitativeResult& ExplicitQualitativeResultMinMax::getProb1Min() {
+            return getProb1(storm::OptimizationDirection::Minimize);
+        }
+        
+        ExplicitQualitativeResult& ExplicitQualitativeResultMinMax::getProb0Max() {
+            return getProb0(storm::OptimizationDirection::Maximize);
+        }
+        
+        ExplicitQualitativeResult& ExplicitQualitativeResultMinMax::getProb1Max() {
+            return getProb1(storm::OptimizationDirection::Maximize);
+        }
+
     }
 }

src/storm/abstraction/ExplicitQualitativeResultMinMax.h

@@ -7,6 +7,7 @@
 namespace storm {
     namespace abstraction {
         class ExplicitQualitativeResult;
+        class ExplicitQualitativeGameResultMinMax;
 
         class ExplicitQualitativeResultMinMax : public QualitativeResultMinMax {
         public:
@@ -18,9 +19,15 @@ namespace storm {
             ExplicitQualitativeResult const& getProb1Min() const;
             ExplicitQualitativeResult const& getProb0Max() const;
             ExplicitQualitativeResult const& getProb1Max() const;
-            
+            ExplicitQualitativeResult& getProb0Min();
+            ExplicitQualitativeResult& getProb1Min();
+            ExplicitQualitativeResult& getProb0Max();
+            ExplicitQualitativeResult& getProb1Max();
+
             virtual ExplicitQualitativeResult const& getProb0(storm::OptimizationDirection const& dir) const = 0;
             virtual ExplicitQualitativeResult const& getProb1(storm::OptimizationDirection const& dir) const = 0;
+            virtual ExplicitQualitativeResult& getProb0(storm::OptimizationDirection const& dir) = 0;
+            virtual ExplicitQualitativeResult& getProb1(storm::OptimizationDirection const& dir) = 0;
         };
         
     }

src/storm/abstraction/MenuGameRefiner.cpp

@@ -4,8 +4,11 @@
 #include "storm/abstraction/MenuGameAbstractor.h"
 
 #include "storm/storage/BitVector.h"
+#include "storm/abstraction/ExplicitQualitativeGameResultMinMax.h"
+#include "storm/abstraction/ExplicitGameStrategyPair.h"
 
 #include "storm/storage/dd/DdManager.h"
+#include "storm/storage/dd/Odd.h"
 #include "storm/utility/dd.h"
 #include "storm/utility/solver.h"
 
@@ -42,7 +45,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        MostProbablePathsResult<Type, ValueType>::MostProbablePathsResult(storm::dd::Add<Type, ValueType> const& maxProbabilities, storm::dd::Bdd<Type> const& spanningTree) : maxProbabilities(maxProbabilities), spanningTree(spanningTree) {
+        SymbolicMostProbablePathsResult<Type, ValueType>::SymbolicMostProbablePathsResult(storm::dd::Add<Type, ValueType> const& maxProbabilities, storm::dd::Bdd<Type> const& spanningTree) : maxProbabilities(maxProbabilities), spanningTree(spanningTree) {
             // Intentionally left empty.
         }
         
@@ -54,7 +57,7 @@ namespace storm {
         };
         
         template<storm::dd::DdType Type, typename ValueType>
-        PivotStateResult<Type, ValueType>::PivotStateResult(storm::dd::Bdd<Type> const& pivotState, storm::OptimizationDirection fromDirection, boost::optional<MostProbablePathsResult<Type, ValueType>> const& mostProbablePathsResult) : pivotState(pivotState), fromDirection(fromDirection), mostProbablePathsResult(mostProbablePathsResult) {
+        SymbolicPivotStateResult<Type, ValueType>::SymbolicPivotStateResult(storm::dd::Bdd<Type> const& pivotState, storm::OptimizationDirection fromDirection, boost::optional<SymbolicMostProbablePathsResult<Type, ValueType>> const& symbolicMostProbablePathsResult) : pivotState(pivotState), fromDirection(fromDirection), symbolicMostProbablePathsResult(symbolicMostProbablePathsResult) {
             // Intentionally left empty.
         }
         
@@ -89,7 +92,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        MostProbablePathsResult<Type, ValueType> getMostProbablePathSpanningTree(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionFilter) {
+        SymbolicMostProbablePathsResult<Type, ValueType> getMostProbablePathSpanningTree(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionFilter) {
             storm::dd::Add<Type, ValueType> maxProbabilities = game.getInitialStates().template toAdd<ValueType>();
             
             storm::dd::Bdd<Type> border = game.getInitialStates();
@@ -120,11 +123,11 @@ namespace storm {
                 border = updateStates;
             }
             
-            return MostProbablePathsResult<Type, ValueType>(maxProbabilities, spanningTree);
+            return SymbolicMostProbablePathsResult<Type, ValueType>(maxProbabilities, spanningTree);
         }
                 
         template<storm::dd::DdType Type, typename ValueType>
-        PivotStateResult<Type, ValueType> pickPivotState(AbstractionSettings::PivotSelectionHeuristic const& heuristic, storm::abstraction::MenuGame<Type, ValueType> const& game, PivotStateCandidatesResult<Type> const& pivotStateCandidateResult, boost::optional<SymbolicQualitativeGameResultMinMax<Type>> const& qualitativeResult, boost::optional<SymbolicQuantitativeGameResultMinMax<Type, ValueType>> const& quantitativeResult) {
+        SymbolicPivotStateResult<Type, ValueType> pickPivotState(AbstractionSettings::PivotSelectionHeuristic const& heuristic, storm::abstraction::MenuGame<Type, ValueType> const& game, PivotStateCandidatesResult<Type> const& pivotStateCandidateResult, boost::optional<SymbolicQualitativeGameResultMinMax<Type>> const& qualitativeResult, boost::optional<SymbolicQuantitativeGameResultMinMax<Type, ValueType>> const& quantitativeResult) {
             
             // Get easy access to strategies.
             storm::dd::Bdd<Type> minPlayer1Strategy;
@@ -163,7 +166,7 @@ namespace storm {
                 bool foundPivotState = !frontierPivotStates.isZero();
                 if (foundPivotState) {
                     STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total.");
-                    return PivotStateResult<Type, ValueType>(frontierPivotStates.existsAbstractRepresentative(rowVariables), storm::OptimizationDirection::Minimize);
+                    return SymbolicPivotStateResult<Type, ValueType>(frontierPivotStates.existsAbstractRepresentative(rowVariables), storm::OptimizationDirection::Minimize);
                 } else {
                     // Otherwise, we perform a simulatenous BFS in the sense that we make one step in both the min and max
                     // transitions and check for pivot states we encounter.
@@ -195,7 +198,7 @@ namespace storm {
                                 }
                                 
                                 STORM_LOG_TRACE("Picked pivot state with difference " << diffValue << " from " << numberOfPivotStateCandidatesOnLevel << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total.");
-                                return PivotStateResult<Type, ValueType>(direction == storm::OptimizationDirection::Minimize ? diffMin.maxAbstractRepresentative(rowVariables) : diffMax.maxAbstractRepresentative(rowVariables), direction);
+                                return SymbolicPivotStateResult<Type, ValueType>(direction == storm::OptimizationDirection::Minimize ? diffMin.maxAbstractRepresentative(rowVariables) : diffMax.maxAbstractRepresentative(rowVariables), direction);
                             } else {
                                 STORM_LOG_TRACE("Picked pivot state from " << numberOfPivotStateCandidatesOnLevel << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total.");
                                 
@@ -206,18 +209,18 @@ namespace storm {
                                     direction = storm::OptimizationDirection::Maximize;
                                 }
                                 
-                                return PivotStateResult<Type, ValueType>(direction == storm::OptimizationDirection::Minimize ? frontierMinPivotStates.existsAbstractRepresentative(rowVariables) : frontierMaxPivotStates.existsAbstractRepresentative(rowVariables), direction);
+                                return SymbolicPivotStateResult<Type, ValueType>(direction == storm::OptimizationDirection::Minimize ? frontierMinPivotStates.existsAbstractRepresentative(rowVariables) : frontierMaxPivotStates.existsAbstractRepresentative(rowVariables), direction);
                             }
                         }
                     }
                 }
             } else {
                 // Compute the most probable paths to the reachable states and the corresponding spanning trees.
-                MostProbablePathsResult<Type, ValueType> minMostProbablePathsResult = getMostProbablePathSpanningTree(game, minPlayer1Strategy && minPlayer2Strategy);
-                MostProbablePathsResult<Type, ValueType> maxMostProbablePathsResult = getMostProbablePathSpanningTree(game, maxPlayer1Strategy && maxPlayer2Strategy);
+                SymbolicMostProbablePathsResult<Type, ValueType> minSymbolicMostProbablePathsResult = getMostProbablePathSpanningTree(game, minPlayer1Strategy && minPlayer2Strategy);
+                SymbolicMostProbablePathsResult<Type, ValueType> maxSymbolicMostProbablePathsResult = getMostProbablePathSpanningTree(game, maxPlayer1Strategy && maxPlayer2Strategy);
                 storm::dd::Bdd<Type> selectedPivotState;
                 
-                storm::dd::Add<Type, ValueType> score = pivotStates.template toAdd<ValueType>() * minMostProbablePathsResult.maxProbabilities.maximum(maxMostProbablePathsResult.maxProbabilities);
+                storm::dd::Add<Type, ValueType> score = pivotStates.template toAdd<ValueType>() * minSymbolicMostProbablePathsResult.maxProbabilities.maximum(maxSymbolicMostProbablePathsResult.maxProbabilities);
                 
                 if (heuristic == AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation && quantitativeResult) {
                     score = score * (quantitativeResult.get().max.values - quantitativeResult.get().min.values);
@@ -227,15 +230,15 @@ namespace storm {
 
                 storm::OptimizationDirection fromDirection = storm::OptimizationDirection::Minimize;
                 storm::dd::Add<Type, ValueType> selectedPivotStateAsAdd = selectedPivotState.template toAdd<ValueType>();
-                if ((selectedPivotStateAsAdd * maxMostProbablePathsResult.maxProbabilities).getMax() > (selectedPivotStateAsAdd * minMostProbablePathsResult.maxProbabilities).getMax()) {
+                if ((selectedPivotStateAsAdd * maxSymbolicMostProbablePathsResult.maxProbabilities).getMax() > (selectedPivotStateAsAdd * minSymbolicMostProbablePathsResult.maxProbabilities).getMax()) {
                     fromDirection = storm::OptimizationDirection::Maximize;
                 }
                 
-                return PivotStateResult<Type, ValueType>(selectedPivotState, fromDirection, fromDirection == storm::OptimizationDirection::Minimize ? minMostProbablePathsResult : maxMostProbablePathsResult);
+                return SymbolicPivotStateResult<Type, ValueType>(selectedPivotState, fromDirection, fromDirection == storm::OptimizationDirection::Minimize ? minSymbolicMostProbablePathsResult : maxSymbolicMostProbablePathsResult);
             }
             
             STORM_LOG_ASSERT(false, "This point must not be reached, because then no pivot state could be found.");
-            return PivotStateResult<Type, ValueType>(storm::dd::Bdd<Type>(), storm::OptimizationDirection::Minimize);
+            return SymbolicPivotStateResult<Type, ValueType>(storm::dd::Bdd<Type>(), storm::OptimizationDirection::Minimize);
         }
         
         template <storm::dd::DdType Type, typename ValueType>
@@ -522,23 +525,23 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        boost::optional<RefinementPredicates> MenuGameRefiner<Type, ValueType>::derivePredicatesFromInterpolation(storm::abstraction::MenuGame<Type, ValueType> const& game, PivotStateResult<Type, ValueType> const& pivotStateResult, storm::dd::Bdd<Type> const& minPlayer1Strategy, storm::dd::Bdd<Type> const& minPlayer2Strategy, storm::dd::Bdd<Type> const& maxPlayer1Strategy, storm::dd::Bdd<Type> const& maxPlayer2Strategy) const {
+        boost::optional<RefinementPredicates> MenuGameRefiner<Type, ValueType>::derivePredicatesFromInterpolation(storm::abstraction::MenuGame<Type, ValueType> const& game, SymbolicPivotStateResult<Type, ValueType> const& symbolicPivotStateResult, storm::dd::Bdd<Type> const& minPlayer1Strategy, storm::dd::Bdd<Type> const& minPlayer2Strategy, storm::dd::Bdd<Type> const& maxPlayer1Strategy, storm::dd::Bdd<Type> const& maxPlayer2Strategy) const {
             
             AbstractionInformation<Type> const& abstractionInformation = abstractor.get().getAbstractionInformation();
             
             // Compute the most probable path from any initial state to the pivot state.
-            MostProbablePathsResult<Type, ValueType> mostProbablePathsResult;
-            if (!pivotStateResult.mostProbablePathsResult) {
-                mostProbablePathsResult = getMostProbablePathSpanningTree(game, pivotStateResult.fromDirection == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy);
+            SymbolicMostProbablePathsResult<Type, ValueType> symbolicMostProbablePathsResult;
+            if (!symbolicPivotStateResult.symbolicMostProbablePathsResult) {
+                symbolicMostProbablePathsResult = getMostProbablePathSpanningTree(game, symbolicPivotStateResult.fromDirection == storm::OptimizationDirection::Minimize ? minPlayer1Strategy && minPlayer2Strategy : maxPlayer1Strategy && maxPlayer2Strategy);
             } else {
-                mostProbablePathsResult = pivotStateResult.mostProbablePathsResult.get();
+                symbolicMostProbablePathsResult = symbolicPivotStateResult.symbolicMostProbablePathsResult.get();
             }
             
             // Create a new expression manager that we can use for the interpolation.
             std::shared_ptr<storm::expressions::ExpressionManager> interpolationManager = abstractionInformation.getExpressionManager().clone();
             
             // Build the trace of the most probable path in terms of which predicates hold in each step.
-            std::pair<std::vector<std::vector<storm::expressions::Expression>>, std::map<storm::expressions::Variable, storm::expressions::Expression>> traceAndVariableSubstitution = buildTrace(*interpolationManager, game, mostProbablePathsResult.spanningTree, pivotStateResult.pivotState);
+            std::pair<std::vector<std::vector<storm::expressions::Expression>>, std::map<storm::expressions::Variable, storm::expressions::Expression>> traceAndVariableSubstitution = buildTrace(*interpolationManager, game, symbolicMostProbablePathsResult.spanningTree, symbolicPivotStateResult.pivotState);
             auto const& trace = traceAndVariableSubstitution.first;
             auto const& variableSubstitution = traceAndVariableSubstitution.second;
 
@@ -615,11 +618,11 @@ namespace storm {
             STORM_LOG_ASSERT(!pivotStateCandidatesResult.pivotStates.isZero(), "Unable to proceed without pivot state candidates.");
             
             // Now that we have the pivot state candidates, we need to pick one.
-            PivotStateResult<Type, ValueType> pivotStateResult = pickPivotState<Type, ValueType>(pivotSelectionHeuristic, game, pivotStateCandidatesResult, qualitativeResult, boost::none);
+            SymbolicPivotStateResult<Type, ValueType> SymbolicPivotStateResult = pickPivotState<Type, ValueType>(pivotSelectionHeuristic, game, pivotStateCandidatesResult, qualitativeResult, boost::none);
 
 //            // SANITY CHECK TO MAKE SURE OUR STRATEGIES ARE NOT BROKEN.
 //            // FIXME.
-//            auto min1ChoiceInPivot = pivotStateResult.pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy;
+//            auto min1ChoiceInPivot = SymbolicPivotStateResult.pivotState && game.getExtendedTransitionMatrix().toBdd() && minPlayer1Strategy;
 //            STORM_LOG_ASSERT(!min1ChoiceInPivot.isZero(), "wth?");
 //            bool min1ChoiceInPivotIsProb0Min = !(min1ChoiceInPivot && qualitativeResult.prob0Min.getPlayer2States()).isZero();
 //            bool min1ChoiceInPivotIsProb0Max = !(min1ChoiceInPivot && qualitativeResult.prob0Max.getPlayer2States()).isZero();
@@ -643,7 +646,7 @@ namespace storm {
 //            std::cout << "max/min choice there? " << min1MinPlayer2Choice << std::endl;
 //            std::cout << "max/max choice there? " << min1MaxPlayer2Choice << std::endl;
 //
-//            auto max1ChoiceInPivot = pivotStateResult.pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy;
+//            auto max1ChoiceInPivot = SymbolicPivotStateResult.pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy;
 //            STORM_LOG_ASSERT(!max1ChoiceInPivot.isZero(), "wth?");
 //            bool max1ChoiceInPivotIsProb0Min = !(max1ChoiceInPivot && qualitativeResult.prob0Min.getPlayer2States()).isZero();
 //            bool max1ChoiceInPivotIsProb0Max = !(max1ChoiceInPivot && qualitativeResult.prob0Max.getPlayer2States()).isZero();
@@ -661,12 +664,12 @@ namespace storm {
 
             boost::optional<RefinementPredicates> predicates;
             if (useInterpolation) {
-                predicates = derivePredicatesFromInterpolation(game, pivotStateResult, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
+                predicates = derivePredicatesFromInterpolation(game, SymbolicPivotStateResult, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
             }
             if (predicates) {
                 STORM_LOG_TRACE("Obtained predicates by interpolation.");
             } else {
-                predicates = derivePredicatesFromPivotState(game, pivotStateResult.pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
+                predicates = derivePredicatesFromPivotState(game, SymbolicPivotStateResult.pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
             }
             STORM_LOG_THROW(static_cast<bool>(predicates), storm::exceptions::InvalidStateException, "Predicates needed to continue.");
             
@@ -676,6 +679,130 @@ namespace storm {
             return true;
         }
         
+        template<typename ValueType>
+        ExplicitMostProbablePathsResult<ValueType>::ExplicitMostProbablePathsResult(ValueType const& maxProbability, std::vector<std::pair<uint64_t, uint64_t>>&& predecessors) : maxProbability(maxProbability), predecessors(std::move(predecessors)) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        ExplicitPivotStateResult<ValueType>::ExplicitPivotStateResult(uint64_t pivotState, storm::OptimizationDirection fromDirection, boost::optional<ExplicitMostProbablePathsResult<ValueType>>&& explicitMostProbablePathsResult) : pivotState(pivotState), fromDirection(fromDirection), explicitMostProbablePathsResult(std::move(explicitMostProbablePathsResult)) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        ExplicitPivotStateResult<ValueType> pickPivotState(AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& relevantStates, storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) {
+            
+            // Perform Dijkstra search that stays within the relevant states and searches for a state in which the
+            // strategies for the (commonly chosen) player 1 action leads to a player 2 state in which the choices differ.
+            ExplicitPivotStateResult<ValueType> explicitPivotStateResult;
+            explicitPivotStateResult.explicitMostProbablePathsResult = ExplicitMostProbablePathsResult<ValueType>();
+            auto& explicitMostProbablePathsResult = explicitPivotStateResult.explicitMostProbablePathsResult.get();
+            
+            bool probabilityDistances = pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MostProbablePath;
+            uint64_t numberOfStates = initialStates.size();
+            ValueType inftyDistance = probabilityDistances ? storm::utility::zero<ValueType>() : storm::utility::infinity<ValueType>();
+            ValueType zeroDistance = probabilityDistances ? storm::utility::one<ValueType>() : storm::utility::zero<ValueType>();
+            std::vector<ValueType> distances(numberOfStates, inftyDistance);
+            explicitMostProbablePathsResult.predecessors.resize(numberOfStates, std::make_pair(0, 0));
+
+            // Use set as priority queue with unique membership; default comparison on pair works fine if distance is
+            // the first entry.
+            std::set<std::pair<ValueType, uint64_t>, std::greater<std::pair<ValueType, uint64_t>>> dijkstraQueue;
+
+            for (auto initialState : initialStates) {
+                if (!relevantStates.get(initialState)) {
+                    continue;
+                }
+                
+                distances[initialState] = zeroDistance;
+                dijkstraQueue.emplace(zeroDistance, initialState);
+            }
+
+            while (!dijkstraQueue.empty()) {
+                uint64_t currentState = (*dijkstraQueue.begin()).second;
+                dijkstraQueue.erase(dijkstraQueue.begin());
+                
+                // Determine whether the current state is a pivot state.
+                bool isPivotState = false;
+                if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) {
+                    uint64_t player2Successor = minStrategyPair.getPlayer1Strategy().getChoice(currentState);
+                    if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor)) {
+                        isPivotState = true;
+                    }
+                } else if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) {
+                    uint64_t player2Successor = maxStrategyPair.getPlayer1Strategy().getChoice(currentState);
+                    if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor) && maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2Successor)) {
+                        isPivotState = true;
+                    }
+                }
+                
+                // If it is indeed a pivot state, we can abort the search here.
+                if (isPivotState) {
+                    explicitPivotStateResult.pivotState = currentState;
+                    return explicitPivotStateResult;
+                }
+                
+                // Otherwise, we explore all its relevant successors.
+                if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) {
+                    uint64_t minPlayer2Successor = minStrategyPair.getPlayer1Strategy().getChoice(currentState);
+                    uint64_t minPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(minPlayer2Successor);
+                    
+                    for (auto const& entry : transitionMatrix.getRow(minPlayer2Choice)) {
+                        uint64_t player1Successor = entry.getColumn();
+                        if (!relevantStates.get(player1Successor)) {
+                            continue;
+                        }
+                        
+                        ValueType alternateDistance = probabilityDistances ? distances[currentState] * entry.getValue() : distances[currentState] + storm::utility::one<ValueType>();
+                        if ((probabilityDistances && alternateDistance > distances[player1Successor]) || (!probabilityDistances && alternateDistance < distances[player1Successor])) {
+                            distances[player1Successor] = alternateDistance;
+                            explicitMostProbablePathsResult.predecessors[player1Successor] = std::make_pair(currentState, minPlayer2Successor);
+                            dijkstraQueue.emplace(alternateDistance, player1Successor);
+                        }
+                    }
+                }
+                if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(currentState)) {
+                    uint64_t maxPlayer2Successor = maxStrategyPair.getPlayer1Strategy().getChoice(currentState);
+                    uint64_t maxPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(maxPlayer2Successor);
+                    
+                    for (auto const& entry : transitionMatrix.getRow(maxPlayer2Choice)) {
+                        uint64_t player1Successor = entry.getColumn();
+                        if (!relevantStates.get(player1Successor)) {
+                            continue;
+                        }
+                        
+                        ValueType alternateDistance = probabilityDistances ? distances[currentState] * entry.getValue() : distances[currentState] + storm::utility::one<ValueType>();
+                        if ((probabilityDistances && alternateDistance > distances[player1Successor]) || (!probabilityDistances && alternateDistance < distances[player1Successor])) {
+                            distances[player1Successor] = alternateDistance;
+                            explicitMostProbablePathsResult.predecessors[player1Successor] = std::make_pair(currentState, maxPlayer2Successor);
+                            dijkstraQueue.emplace(alternateDistance, player1Successor);
+                        }
+                    }
+                }
+            }
+            
+            // If we arrived at this point, we have explored all relevant states, but none of them was a pivot state,
+            // which can happen when trying to refine using the qualitative result only.
+            return explicitPivotStateResult;
+        }
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Odd const& odd, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping, std::vector<uint64_t> const& player1Labeling, std::vector<uint64_t> const& player2Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) const {
+            
+            // Compute the set of states whose result we have for the min and max case.
+            storm::storage::BitVector relevantStates = (qualitativeResult.getProb0Min().getStates() | qualitativeResult.getProb1Min().getStates()) & (qualitativeResult.getProb0Max().getStates() | qualitativeResult.getProb1Max().getStates());
+            
+            ExplicitPivotStateResult<ValueType> pivotStateResult = pickPivotState(pivotSelectionHeuristic, transitionMatrix, player1Grouping, initialStates, relevantStates, targetStates, qualitativeResult, minStrategyPair, maxStrategyPair);
+            
+            // If there was no pivot state, continue the search.
+            if (!pivotStateResult.pivotState) {
+                return false;
+            }
+            
+            // Otherwise, we can refine.
+            storm::dd::Bdd<Type> pivotState = storm::dd::Bdd<Type>::getEncoding(game.getManager(), pivotStateResult.pivotState.get(), odd, game.getRowVariables());
+        }
+        
         template<storm::dd::DdType Type, typename ValueType>
         bool MenuGameRefiner<Type, ValueType>::refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, SymbolicQuantitativeGameResultMinMax<Type, ValueType> const& quantitativeResult) const {
             STORM_LOG_TRACE("Refining after quantitative check.");
@@ -691,16 +818,16 @@ namespace storm {
             STORM_LOG_ASSERT(!pivotStateCandidatesResult.pivotStates.isZero(), "Unable to refine without pivot state candidates.");
             
             // Now that we have the pivot state candidates, we need to pick one.
-            PivotStateResult<Type, ValueType> pivotStateResult = pickPivotState<Type, ValueType>(pivotSelectionHeuristic, game, pivotStateCandidatesResult, boost::none, quantitativeResult);
+            SymbolicPivotStateResult<Type, ValueType> SymbolicPivotStateResult = pickPivotState<Type, ValueType>(pivotSelectionHeuristic, game, pivotStateCandidatesResult, boost::none, quantitativeResult);
 
             boost::optional<RefinementPredicates> predicates;
             if (useInterpolation) {
-                predicates = derivePredicatesFromInterpolation(game, pivotStateResult, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
+                predicates = derivePredicatesFromInterpolation(game, SymbolicPivotStateResult, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
             }
             if (predicates) {
                 STORM_LOG_TRACE("Obtained predicates by interpolation.");
             } else {
-                predicates = derivePredicatesFromPivotState(game, pivotStateResult.pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
+                predicates = derivePredicatesFromPivotState(game, SymbolicPivotStateResult.pivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
             }
             STORM_LOG_THROW(static_cast<bool>(predicates), storm::exceptions::InvalidStateException, "Predicates needed to continue.");
             

src/storm/abstraction/MenuGameRefiner.h

@@ -21,6 +21,14 @@
 #include "storm/utility/solver.h"
 
 namespace storm {
+    namespace dd {
+        class Odd;
+    }
+    
+    namespace storage {
+        class BitVector;
+    }
+    
     namespace abstraction {
 
         template <storm::dd::DdType Type, typename ValueType>
@@ -48,23 +56,48 @@ namespace storm {
         };
 
         template<storm::dd::DdType Type, typename ValueType>
-        struct MostProbablePathsResult {
-            MostProbablePathsResult() = default;
-            MostProbablePathsResult(storm::dd::Add<Type, ValueType> const& maxProbabilities, storm::dd::Bdd<Type> const& spanningTree);
+        struct SymbolicMostProbablePathsResult {
+            SymbolicMostProbablePathsResult() = default;
+            SymbolicMostProbablePathsResult(storm::dd::Add<Type, ValueType> const& maxProbabilities, storm::dd::Bdd<Type> const& spanningTree);
             
             storm::dd::Add<Type, ValueType> maxProbabilities;
             storm::dd::Bdd<Type> spanningTree;
         };
         
         template<storm::dd::DdType Type, typename ValueType>
-        struct PivotStateResult {
-            PivotStateResult(storm::dd::Bdd<Type> const& pivotState, storm::OptimizationDirection fromDirection, boost::optional<MostProbablePathsResult<Type, ValueType>> const& mostProbablePathsResult = boost::none);
+        struct SymbolicPivotStateResult {
+            SymbolicPivotStateResult(storm::dd::Bdd<Type> const& pivotState, storm::OptimizationDirection fromDirection, boost::optional<SymbolicMostProbablePathsResult<Type, ValueType>> const& symbolicMostProbablePathsResult = boost::none);
             
             storm::dd::Bdd<Type> pivotState;
             storm::OptimizationDirection fromDirection;
-            boost::optional<MostProbablePathsResult<Type, ValueType>> mostProbablePathsResult;
+            boost::optional<SymbolicMostProbablePathsResult<Type, ValueType>> symbolicMostProbablePathsResult;
+        };
+        
+        template<typename ValueType>
+        struct ExplicitMostProbablePathsResult {
+            ExplicitMostProbablePathsResult() = default;
+            ExplicitMostProbablePathsResult(ValueType const& maxProbability, std::vector<std::pair<uint64_t, uint64_t>>&& predecessors);
+
+            /// The maximal probability with which the state in question is reached.
+            ValueType maxProbability;
+            
+            /// The predecessors for the states to obtain this probability.
+            std::vector<std::pair<uint64_t, uint64_t>> predecessors;
+        };
+        
+        template<typename ValueType>
+        struct ExplicitPivotStateResult {
+            ExplicitPivotStateResult() = default;
+            ExplicitPivotStateResult(uint64_t pivotState, storm::OptimizationDirection fromDirection, boost::optional<ExplicitMostProbablePathsResult<ValueType>>&& explicitMostProbablePathsResult = boost::none);
+            
+            boost::optional<uint64_t> pivotState;
+            storm::OptimizationDirection fromDirection;
+            boost::optional<ExplicitMostProbablePathsResult<ValueType>> explicitMostProbablePathsResult;
         };
         
+        class ExplicitQualitativeGameResultMinMax;
+        class ExplicitGameStrategyPair;
+        
         template<storm::dd::DdType Type, typename ValueType>
         class MenuGameRefiner {
         public:
@@ -86,7 +119,14 @@ namespace storm {
              * @param True if predicates for refinement could be derived, false otherwise.
              */
             bool refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, SymbolicQualitativeGameResultMinMax<Type> const& qualitativeResult) const;
-            
+
+            /*!
+             * Refines the abstractor based on the qualitative result by trying to derive suitable predicates.
+             *
+             * @param True if predicates for refinement could be derived, false otherwise.
+             */
+            bool refine(storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Odd const& odd, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping, std::vector<uint64_t> const& player1Labeling, std::vector<uint64_t> const& player2Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) const;
+
             /*!
              * Refines the abstractor based on the quantitative result by trying to derive suitable predicates.
              *
@@ -113,7 +153,7 @@ namespace storm {
              */
             std::vector<RefinementCommand> createGlobalRefinement(std::vector<storm::expressions::Expression> const& predicates) const;
             
-            boost::optional<RefinementPredicates> derivePredicatesFromInterpolation(storm::abstraction::MenuGame<Type, ValueType> const& game, PivotStateResult<Type, ValueType> const& pivotStateResult, storm::dd::Bdd<Type> const& minPlayer1Strategy, storm::dd::Bdd<Type> const& minPlayer2Strategy, storm::dd::Bdd<Type> const& maxPlayer1Strategy, storm::dd::Bdd<Type> const& maxPlayer2Strategy) const;
+            boost::optional<RefinementPredicates> derivePredicatesFromInterpolation(storm::abstraction::MenuGame<Type, ValueType> const& game, SymbolicPivotStateResult<Type, ValueType> const& symbolicPivotStateResult, storm::dd::Bdd<Type> const& minPlayer1Strategy, storm::dd::Bdd<Type> const& minPlayer2Strategy, storm::dd::Bdd<Type> const& maxPlayer1Strategy, storm::dd::Bdd<Type> const& maxPlayer2Strategy) const;
             std::pair<std::vector<std::vector<storm::expressions::Expression>>, std::map<storm::expressions::Variable, storm::expressions::Expression>> buildTrace(storm::expressions::ExpressionManager& expressionManager, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& spanningTree, storm::dd::Bdd<Type> const& pivotState) const;
             
             void performRefinement(std::vector<RefinementCommand> const& refinementCommands) const;

src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp

@@ -61,10 +61,10 @@ namespace storm {
                     totalNumberOfCommands += automaton.getNumberOfEdges();
                 }
                 
-                // NOTE: currently we assume that 100 player 2 variables suffice, which corresponds to 2^100 possible
+                // NOTE: currently we assume that 64 player 2 variables suffice, which corresponds to 2^64 possible
                 // choices. If for some reason this should not be enough, we could grow this vector dynamically, but
                 // odds are that it's impossible to treat such models in any event.
-                abstractionInformation.createEncodingVariables(static_cast<uint_fast64_t>(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast<uint_fast64_t>(std::ceil(std::log2(maximalUpdateCount))));
+                abstractionInformation.createEncodingVariables(static_cast<uint_fast64_t>(std::ceil(std::log2(totalNumberOfCommands))), 64, static_cast<uint_fast64_t>(std::ceil(std::log2(maximalUpdateCount))));
                 
                 // For each module of the concrete program, we create an abstract counterpart.
                 bool useDecomposition = storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isUseDecompositionSet();

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -58,10 +58,10 @@ namespace storm {
                     totalNumberOfCommands += module.getNumberOfCommands();
                 }
                 
-                // NOTE: currently we assume that 100 player 2 variables suffice, which corresponds to 2^100 possible
+                // NOTE: currently we assume that 64 player 2 variables suffice, which corresponds to 2^64 possible
                 // choices. If for some reason this should not be enough, we could grow this vector dynamically, but
                 // odds are that it's impossible to treat such models in any event.
-                abstractionInformation.createEncodingVariables(static_cast<uint_fast64_t>(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast<uint_fast64_t>(std::ceil(std::log2(maximalUpdateCount))));
+                abstractionInformation.createEncodingVariables(static_cast<uint_fast64_t>(std::ceil(std::log2(totalNumberOfCommands))), 64, static_cast<uint_fast64_t>(std::ceil(std::log2(maximalUpdateCount))));
                 
                 // For each module of the concrete program, we create an abstract counterpart.
                 bool useDecomposition = storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isUseDecompositionSet();

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -24,6 +24,7 @@
 #include "storm/abstraction/prism/PrismMenuGameAbstractor.h"
 #include "storm/abstraction/jani/JaniMenuGameAbstractor.h"
 #include "storm/abstraction/MenuGameRefiner.h"
+#include "storm/abstraction/ExplicitGameStrategyPair.h"
 
 #include "storm/abstraction/ExplicitQualitativeGameResultMinMax.h"
 
@@ -174,6 +175,53 @@ namespace storm {
             }
             return result;
         }
+        
+        template <typename ValueType>
+        std::unique_ptr<CheckResult> checkForResultAfterQualitativeCheck(CheckTask<storm::logic::Formula> const& checkTask, storm::OptimizationDirection player2Direction, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& prob0, storm::storage::BitVector const& prob1) {
+            std::unique_ptr<CheckResult> result;
+            
+            if (checkTask.isBoundSet()) {
+                // Despite having a bound, we create a quantitative result so that the next layer can perform the comparison.
+                
+                if (player2Direction == storm::OptimizationDirection::Minimize) {
+                    if (storm::logic::isLowerBound(checkTask.getBoundComparisonType())) {
+                        if (initialStates.isSubsetOf(prob1)) {
+                            result = std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), storm::utility::one<ValueType>());
+                        }
+                    } else {
+                        if (!initialStates.isDisjointFrom(prob1)) {
+                            result = std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), storm::utility::one<ValueType>());
+                        }
+                    }
+                } else if (player2Direction == storm::OptimizationDirection::Maximize) {
+                    if (!storm::logic::isLowerBound(checkTask.getBoundComparisonType())) {
+                        if (initialStates.isSubsetOf(prob0)) {
+                            result = std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), storm::utility::zero<ValueType>());
+                        }
+                    } else {
+                        if (!initialStates.isDisjointFrom(prob0)) {
+                            result = std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), storm::utility::zero<ValueType>());
+                        }
+                    }
+                }
+            }
+            
+            return result;
+        }
+        
+        template <typename ValueType>
+        std::unique_ptr<CheckResult> checkForResultAfterQualitativeCheck(CheckTask<storm::logic::Formula> const& checkTask, storm::storage::BitVector const& initialStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult) {
+            // Check whether we can already give the answer based on the current information.
+            std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, initialStates, qualitativeResult.prob0Min.getPlayer1States(), qualitativeResult.prob1Min.getPlayer1States());
+            if (result) {
+                return result;
+            }
+            result = checkForResultAfterQualitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, initialStates, qualitativeResult.prob0Max.getPlayer1States(), qualitativeResult.prob1Max.getPlayer1States());
+            if (result) {
+                return result;
+            }
+            return result;
+        }
 
         template<typename ValueType>
         std::unique_ptr<CheckResult> checkForResultAfterQuantitativeCheck(CheckTask<storm::logic::Formula> const& checkTask, storm::OptimizationDirection const& player2Direction, std::pair<ValueType, ValueType> const& initialValueRange) {
@@ -506,7 +554,7 @@ namespace storm {
             // Return null to indicate no result has been found yet.
             return nullptr;
         }
-
+        
         template<storm::dd::DdType Type, typename ModelType>
         std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ModelType>::performExplicitAbstractionSolutionStep(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& initialStatesBdd, storm::dd::Bdd<Type> const& constraintStatesBdd, storm::dd::Bdd<Type> const& targetStatesBdd, storm::abstraction::MenuGameRefiner<Type, ValueType> const& refiner, boost::optional<ExplicitQualitativeGameResultMinMax>& previousQualitativeResult) {
             STORM_LOG_TRACE("Using sparse solving.");
@@ -514,22 +562,24 @@ namespace storm {
             // (0) Start by transforming the necessary symbolic elements to explicit ones.
             storm::dd::Odd odd = game.getReachableStates().createOdd();
             
-            std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<uint64_t>> transitionMatrixAndLabeling = game.getTransitionMatrix().toLabeledMatrix(game.getRowVariables(), game.getColumnVariables(), game.getNondeterminismVariables(), game.getPlayer1Variables(), odd, odd, true);
-            auto& transitionMatrix = transitionMatrixAndLabeling.first;
-            auto& labeling = transitionMatrixAndLabeling.second;
-            
+            std::vector<std::set<storm::expressions::Variable>> labelingVariableSets = {game.getPlayer1Variables(), game.getPlayer2Variables()};
+            typename storm::dd::Add<Type, ValueType>::MatrixAndLabeling matrixAndLabeling = game.getTransitionMatrix().toLabeledMatrix(game.getRowVariables(), game.getColumnVariables(), game.getNondeterminismVariables(), odd, odd, labelingVariableSets);
+            auto& transitionMatrix = matrixAndLabeling.matrix;
+            auto& player1Labeling = matrixAndLabeling.labelings.front();
+            auto& player2Labeling = matrixAndLabeling.labelings.back();
+
             // Create the player 2 row grouping from the labeling.
             std::vector<uint64_t> tmpPlayer2RowGrouping;
             for (uint64_t player1State = 0; player1State < transitionMatrix.getRowGroupCount(); ++player1State) {
                 uint64_t lastLabel = std::numeric_limits<uint64_t>::max();
                 for (uint64_t row = transitionMatrix.getRowGroupIndices()[player1State]; row < transitionMatrix.getRowGroupIndices()[player1State + 1]; ++row) {
-                    if (labeling[row] != lastLabel) {
+                    if (player1Labeling[row] != lastLabel) {
                         tmpPlayer2RowGrouping.emplace_back(row);
-                        lastLabel = labeling[row];
+                        lastLabel = player1Labeling[row];
                     }
                 }
             }
-            tmpPlayer2RowGrouping.emplace_back(labeling.size());
+            tmpPlayer2RowGrouping.emplace_back(player1Labeling.size());
             
             std::vector<uint64_t> player1RowGrouping = transitionMatrix.swapRowGroupIndices(std::move(tmpPlayer2RowGrouping));
             auto const& player2RowGrouping = transitionMatrix.getRowGroupIndices();
@@ -548,17 +598,22 @@ namespace storm {
                 player1Groups[player1State + 1] = player2State;
             }
             
+            // Create explicit representations of important state sets.
             storm::storage::BitVector initialStates = initialStatesBdd.toVector(odd);
             storm::storage::BitVector constraintStates = constraintStatesBdd.toVector(odd);
             storm::storage::BitVector targetStates = targetStatesBdd.toVector(odd);
 
+            // Prepare the two strategies.
+            abstraction::ExplicitGameStrategyPair minStrategyPair(initialStates.size(), transitionMatrix.getRowGroupCount());
+            abstraction::ExplicitGameStrategyPair maxStrategyPair(initialStates.size(), transitionMatrix.getRowGroupCount());
+            
             // (1) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max).
             auto qualitativeStart = std::chrono::high_resolution_clock::now();
-            ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, player1Direction, transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates);
-//            std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, initialStates, qualitativeResult);
-//            if (result) {
-//                return result;
-//            }
+            ExplicitQualitativeGameResultMinMax qualitativeResult = computeProb01States(previousQualitativeResult, player1Direction, transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, minStrategyPair, maxStrategyPair);
+            std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<ValueType>(checkTask, initialStates, qualitativeResult);
+            if (result) {
+                return result;
+            }
             auto qualitativeEnd = std::chrono::high_resolution_clock::now();
             STORM_LOG_DEBUG("Qualitative computation completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(qualitativeEnd - qualitativeStart).count() << "ms.");
 
@@ -568,6 +623,31 @@ namespace storm {
 //            std::cout << constraintStates << std::endl;
 //            std::cout << targetStates << std::endl;
             
+            // (2) compute the states for which we have to determine quantitative information.
+            storm::storage::BitVector maybeMin = ~(qualitativeResult.getProb0Min().getStates() | qualitativeResult.getProb1Min().getStates());
+            storm::storage::BitVector maybeMax = ~(qualitativeResult.getProb0Max().getStates() | qualitativeResult.getProb1Max().getStates());
+            
+            // (3) if the initial states are not maybe states, then we can refine at this point.
+            storm::storage::BitVector initialMaybeStates = initialStates & (maybeMin | maybeMax);
+            bool qualitativeRefinement = false;
+            if (initialMaybeStates.empty()) {
+                // In this case, we know the result for the initial states for both player 2 minimizing and maximizing.
+                STORM_LOG_TRACE("No initial state is a 'maybe' state.");
+                
+                STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states. Refining abstraction based on qualitative check.");
+                
+                // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1)
+                // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine.
+                auto qualitativeRefinementStart = std::chrono::high_resolution_clock::now();
+                qualitativeRefinement = refiner.refine(game, odd, transitionMatrix, player1Groups, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, qualitativeResult, minStrategyPair, maxStrategyPair);
+                auto qualitativeRefinementEnd = std::chrono::high_resolution_clock::now();
+                STORM_LOG_DEBUG("Qualitative refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(qualitativeRefinementEnd - qualitativeRefinementStart).count() << "ms.");
+            } else if (initialStates.isSubsetOf(initialMaybeStates) && checkTask.isQualitativeSet()) {
+                // If all initial states are 'maybe' states and the property we needed to check is a qualitative one,
+                // we can return the result here.
+                return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), ValueType(0.5));
+            }
+            
             return nullptr;
         }
         
@@ -630,7 +710,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ModelType>
-        ExplicitQualitativeGameResultMinMax GameBasedMdpModelChecker<Type, ModelType>::computeProb01States(boost::optional<ExplicitQualitativeGameResultMinMax> const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates) {
+        ExplicitQualitativeGameResultMinMax GameBasedMdpModelChecker<Type, ModelType>::computeProb01States(boost::optional<ExplicitQualitativeGameResultMinMax> const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair) {
             
             ExplicitQualitativeGameResultMinMax result;
             
@@ -679,10 +759,10 @@ namespace storm {
 //                    result.prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true, boost::make_optional(prob1MaxMaxMdp));
 //                }
 //            } else {
-                result.prob0Min = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true);
-                result.prob1Min = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true);
-                result.prob0Max = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true);
-                result.prob1Max = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true);
+                result.prob0Min = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, &minStrategyPair.getPlayer1Strategy(), &minStrategyPair.getPlayer2Strategy());
+                result.prob1Min = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Minimize, &minStrategyPair.getPlayer1Strategy(), &minStrategyPair.getPlayer2Strategy());
+                result.prob0Max = storm::utility::graph::performProb0(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, &maxStrategyPair.getPlayer1Strategy(), &maxStrategyPair.getPlayer2Strategy());
+                result.prob1Max = storm::utility::graph::performProb1(transitionMatrix, player1Groups, player1BackwardTransitions, player2BackwardTransitions, constraintStates, targetStates, player1Direction, storm::OptimizationDirection::Maximize, &maxStrategyPair.getPlayer1Strategy(), &maxStrategyPair.getPlayer2Strategy());
 //            }
             
             STORM_LOG_TRACE("Qualitative precomputation completed.");

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h

@@ -39,6 +39,8 @@ namespace storm {
         
         class ExplicitQualitativeGameResult;
         class ExplicitQualitativeGameResultMinMax;
+        class ExplicitGameStrategy;
+        class ExplicitGameStrategyPair;
     }
     
     namespace modelchecker {
@@ -92,7 +94,7 @@ namespace storm {
              */
             SymbolicQualitativeGameResultMinMax<Type> computeProb01States(boost::optional<SymbolicQualitativeGameResultMinMax<Type>> const& previousQualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates);
             
-            ExplicitQualitativeGameResultMinMax computeProb01States(boost::optional<ExplicitQualitativeGameResultMinMax> const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates);
+            ExplicitQualitativeGameResultMinMax computeProb01States(boost::optional<ExplicitQualitativeGameResultMinMax> const& previousQualitativeResult, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair);
             
             void printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game) const;
             

src/storm/storage/dd/Add.cpp

@@ -704,16 +704,18 @@ namespace storm {
             }
             
             // Create the canonical row group sizes and build the matrix.
-            return toLabeledMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, groupMetaVariables, rowOdd, columnOdd).first;
+            return toLabeledMatrix(rowMetaVariables, columnMetaVariables, groupMetaVariables, rowOdd, columnOdd).matrix;
         }
 
         template<DdType LibraryType, typename ValueType>
-        std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<uint64_t>> Add<LibraryType, ValueType>::toLabeledMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, std::set<storm::expressions::Variable> const& labelMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, bool buildLabeling) const {
+        typename Add<LibraryType, ValueType>::MatrixAndLabeling Add<LibraryType, ValueType>::toLabeledMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, std::vector<std::set<storm::expressions::Variable>> const& labelMetaVariables) const {
             std::vector<uint_fast64_t> ddRowVariableIndices;
             std::vector<uint_fast64_t> ddColumnVariableIndices;
             std::vector<uint_fast64_t> ddGroupVariableIndices;
-            storm::storage::BitVector ddLabelVariableIndices;
+            std::vector<storm::storage::BitVector> ddLabelVariableIndicesVector;
             std::set<storm::expressions::Variable> rowAndColumnMetaVariables;
+            bool buildLabeling = !labelMetaVariables.empty();
+            MatrixAndLabeling result;
             
             for (auto const& variable : rowMetaVariables) {
                 DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager().getMetaVariable(variable);
@@ -739,21 +741,23 @@ namespace storm {
             }
             std::sort(ddGroupVariableIndices.begin(), ddGroupVariableIndices.end());
             if (buildLabeling) {
-                std::set<uint64_t> ddLabelVariableIndicesSet;
-                for (auto const& variable : labelMetaVariables) {
-                    DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager().getMetaVariable(variable);
-                    for (auto const& ddVariable : metaVariable.getDdVariables()) {
-                        ddLabelVariableIndicesSet.insert(ddVariable.getIndex());
+                for (auto const& labelMetaVariableSet : labelMetaVariables) {
+                    std::set<uint64_t> ddLabelVariableIndicesSet;
+                    for (auto const& variable : labelMetaVariableSet) {
+                        DdMetaVariable<LibraryType> const& metaVariable = this->getDdManager().getMetaVariable(variable);
+                        for (auto const& ddVariable : metaVariable.getDdVariables()) {
+                            ddLabelVariableIndicesSet.insert(ddVariable.getIndex());
+                        }
                     }
-                }
-                
-                ddLabelVariableIndices = storm::storage::BitVector(ddGroupVariableIndices.size());
-                uint64_t position = 0;
-                for (auto const& index : ddGroupVariableIndices) {
-                    if (ddLabelVariableIndicesSet.find(index) != ddLabelVariableIndicesSet.end()) {
-                        ddLabelVariableIndices.set(position);
+                    
+                    ddLabelVariableIndicesVector.emplace_back(ddGroupVariableIndices.size());
+                    uint64_t position = 0;
+                    for (auto const& index : ddGroupVariableIndices) {
+                        if (ddLabelVariableIndicesSet.find(index) != ddLabelVariableIndicesSet.end()) {
+                            ddLabelVariableIndicesVector.back().set(position);
+                        }
+                        ++position;
                     }
-                    ++position;
                 }
             }
 
@@ -781,10 +785,12 @@ namespace storm {
             }
             
             // Create the group labelings if requested.
-            std::vector<uint64_t> groupLabels;
+            std::vector<std::vector<uint64_t>> groupLabelings;
             if (buildLabeling) {
-                groupLabels = internalAdd.decodeGroupLabels(ddGroupVariableIndices, ddLabelVariableIndices);
-                STORM_LOG_ASSERT(groupLabels.size() == groups.size(), "Mismatching label sizes.");
+                for (auto const& ddLabelVariableIndices : ddLabelVariableIndicesVector) {
+                    groupLabelings.emplace_back(internalAdd.decodeGroupLabels(ddGroupVariableIndices, ddLabelVariableIndices));
+                    STORM_LOG_ASSERT(groupLabelings.back().size() == groups.size(), "Mismatching label sizes.");
+                }
             }
             
             // Create the actual storage for the non-zero entries.
@@ -793,9 +799,10 @@ namespace storm {
             // Now compute the indices at which the individual rows start.
             std::vector<uint_fast64_t> rowIndications(rowGroupIndices.back() + 1);
             
-            std::vector<uint64_t> labeling;
             if (buildLabeling) {
-                labeling.resize(rowGroupIndices.back());
+                for (uint64_t i = 0; i < labelMetaVariables.size(); ++i) {
+                    result.labelings.emplace_back(rowGroupIndices.back());
+                }
             }
             
             std::vector<InternalAdd<LibraryType, uint_fast64_t>> statesWithGroupEnabled(groups.size());
@@ -811,8 +818,10 @@ namespace storm {
                 
                 statesWithGroupEnabled[i] = groupNotZero.existsAbstract(columnMetaVariables).template toAdd<uint_fast64_t>();
                 if (buildLabeling) {
-                    uint64_t currentLabel = groupLabels[i];
-                    statesWithGroupEnabled[i].forEach(rowOdd, ddRowVariableIndices, [currentLabel, &rowGroupIndices, &labeling] (uint64_t const& offset, uint_fast64_t const& value) { labeling[rowGroupIndices[offset]] = currentLabel; });
+                    for (uint64_t j = 0; j < labelMetaVariables.size(); ++j) {
+                        uint64_t currentLabel = groupLabelings[j][i];
+                        statesWithGroupEnabled[i].forEach(rowOdd, ddRowVariableIndices, [currentLabel, &rowGroupIndices, &result, j] (uint64_t const& offset, uint_fast64_t const& value) { result.labelings[j][rowGroupIndices[offset]] = currentLabel; });
+                    }
                 }
                 statesWithGroupEnabled[i].composeWithExplicitVector(rowOdd, ddRowVariableIndices, rowGroupIndices, std::plus<uint_fast64_t>());
             }
@@ -847,8 +856,10 @@ namespace storm {
                 rowIndications[i] = rowIndications[i - 1];
             }
             rowIndications[0] = 0;
-            
-            return std::make_pair(storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices)), labeling);
+
+            // Move-construct matrix and return.
+            result.matrix = storm::storage::SparseMatrix<ValueType>(columnOdd.getTotalOffset(), std::move(rowIndications), std::move(columnsAndValues), std::move(rowGroupIndices));
+            return result;
         }
         
         template<DdType LibraryType, typename ValueType>

src/storm/storage/dd/Add.h

@@ -655,7 +655,22 @@ namespace storm {
              * @return The matrix that is represented by this ADD and a vector corresponding to row labeling
              * (if requested).
              */
-            std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<uint64_t>> toLabeledMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, std::set<storm::expressions::Variable> const& labelMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, bool buildLabeling = false) const;
+            struct MatrixAndLabeling {
+                MatrixAndLabeling() = default;
+                
+                MatrixAndLabeling(storm::storage::SparseMatrix<ValueType> const& matrix) : matrix(matrix) {
+                    // Intentionally left empty.
+                }
+
+                MatrixAndLabeling(storm::storage::SparseMatrix<ValueType>&& matrix) : matrix(std::move(matrix)) {
+                    // Intentionally left empty.
+                }
+
+                storm::storage::SparseMatrix<ValueType> matrix;
+                std::vector<std::vector<uint64_t>> labelings;
+            };
+            
+            MatrixAndLabeling toLabeledMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd const& rowOdd, storm::dd::Odd const& columnOdd, std::vector<std::set<storm::expressions::Variable>> const& labelMetaVariables = std::vector<std::set<storm::expressions::Variable>>()) const;
             
             /*!
              * Converts the ADD to a row-grouped (sparse) matrix and the given vector to a row-grouped vector.

src/storm/storage/dd/Bdd.cpp

@@ -63,6 +63,11 @@ namespace storm {
             return Bdd<LibraryType>(ddManager, InternalBdd<LibraryType>::fromVector(&ddManager.getInternalDdManager(), odd, ddManager.getSortedVariableIndices(metaVariables), [&truthValues] (uint64_t offset) { return truthValues[offset]; } ), metaVariables);
         }
         
+        template<DdType LibraryType>
+        Bdd<LibraryType> Bdd<LibraryType>::getEncoding(DdManager<LibraryType> const& ddManager, uint64_t targetOffset, storm::dd::Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables) {
+            return Bdd<LibraryType>(ddManager, InternalBdd<LibraryType>::fromVector(&ddManager.getInternalDdManager(), odd, ddManager.getSortedVariableIndices(metaVariables), [targetOffset] (uint64_t offset) { return offset == targetOffset; }), metaVariables);
+        }
+        
         template<DdType LibraryType>
         bool Bdd<LibraryType>::operator==(Bdd<LibraryType> const& other) const {
             return internalBdd == other.internalBdd;

src/storm/storage/dd/Bdd.h

@@ -45,6 +45,16 @@ namespace storm {
             Bdd(Bdd<LibraryType>&& other) = default;
             Bdd& operator=(Bdd<LibraryType>&& other) = default;
 
+            /*!
+             * Constructs the BDD representation of the encoding with the given offset.
+             *
+             * @param ddManager The DD manager responsible for the resulting BDD.
+             * @param targetOffset The offset to encode (interpreted within the ODD).
+             * @param odd The ODD used for the translation from the explicit representation to a symbolic one.
+             * @param metaVariables The meta variables to use for the symbolic encoding.
+             */
+            static Bdd<LibraryType> getEncoding(DdManager<LibraryType> const& ddManager, uint64_t targetOffset, storm::dd::Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables);
+            
             /*!
              * Constructs a BDD representation of all encodings whose value is true in the given list of truth values.
              *

src/storm/utility/graph.cpp

@@ -9,6 +9,7 @@
 #include "storm/storage/dd/Add.h"
 #include "storm/storage/dd/DdManager.h"
 
+#include "storm/abstraction/ExplicitGameStrategy.h"
 #include "storm/storage/StronglyConnectedComponentDecomposition.h"
 
 #include "storm/models/symbolic/DeterministicModel.h"
@@ -1084,7 +1085,7 @@ namespace storm {
             }
 
             template <typename ValueType>
-            ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) {
+            ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy, storm::abstraction::ExplicitGameStrategy* player2Strategy) {
              
                 ExplicitGameProb01Result result(psiStates, storm::storage::BitVector(transitionMatrix.getRowGroupCount()));
                 
@@ -1102,7 +1103,7 @@ namespace storm {
                         uint64_t player2Predecessor = player2PredecessorEntry.getColumn();
                         if (!result.player2States.get(player2Predecessor)) {
                             bool addPlayer2State = false;
-                            if (player2Strategy == OptimizationDirection::Minimize) {
+                            if (player2Direction == OptimizationDirection::Minimize) {
                                 bool allChoicesHavePlayer1State = true;
                                 for (uint64_t row = transitionMatrix.getRowGroupIndices()[player2Predecessor]; row < transitionMatrix.getRowGroupIndices()[player2Predecessor + 1]; ++row) {
                                     bool choiceHasPlayer1State = false;
@@ -1132,7 +1133,7 @@ namespace storm {
                                 
                                 if (!result.player1States.get(player1Predecessor)) {
                                     bool addPlayer1State = false;
-                                    if (player1Strategy == OptimizationDirection::Minimize) {
+                                    if (player1Direction == OptimizationDirection::Minimize) {
                                         bool allPlayer2Successors = true;
                                         for (uint64_t player2State = player1Groups[player1Predecessor]; player2State < player1Groups[player1Predecessor + 1]; ++player2State) {
                                             if (!result.player2States.get(player2State)) {
@@ -1162,36 +1163,31 @@ namespace storm {
                 result.player2States.complement();
                 
                 // Generate player 1 strategy if required.
-                if (producePlayer1Strategy) {
-                    result.player1Strategy = std::vector<uint64_t>(result.player1States.size());
-                    
+                if (player1Strategy) {
                     for (auto player1State : result.player1States) {
-                        if (player1Strategy == storm::OptimizationDirection::Minimize) {
+                        if (player1Direction == storm::OptimizationDirection::Minimize) {
                             // At least one player 2 successor is a state with probability 0, find it.
                             bool foundProb0Successor = false;
                             uint64_t player2State;
                             for (player2State = player1Groups[player1State]; player2State < player1Groups[player1State + 1]; ++player2State) {
                                 if (result.player2States.get(player2State)) {
-                                    result.player1Strategy.get()[player1State] = player2State;
                                     foundProb0Successor = true;
                                     break;
                                 }
                             }
                             STORM_LOG_ASSERT(foundProb0Successor, "Expected at least one state 2 successor with probability 0.");
-                            result.player1Strategy.get()[player1State] = player2State;
+                            player1Strategy->setChoice(player1State, player2State);
                         } else {
                             // Since all player 2 successors are states with probability 0, just pick any.
-                            result.player1Strategy.get()[player1State] = player1Groups[player1State];
+                            player1Strategy->setChoice(player1State, player1Groups[player1State]);
                         }
                     }
                 }
 
                 // Generate player 2 strategy if required.
-                if (producePlayer2Strategy) {
-                    result.player2Strategy = std::vector<uint64_t>(result.player2States.size());
-                    
+                if (player2Strategy) {
                     for (auto player2State : result.player2States) {
-                        if (player2Strategy == storm::OptimizationDirection::Minimize) {
+                        if (player2Direction == storm::OptimizationDirection::Minimize) {
                             // At least one distribution only has successors with probability 0, find it.
                             bool foundProb0SuccessorDistribution = false;
                             
@@ -1211,10 +1207,10 @@ namespace storm {
                             }
                             
                             STORM_LOG_ASSERT(foundProb0SuccessorDistribution, "Expected at least one distribution with only successors with probability 0.");
-                            result.player2Strategy.get()[player2State] = row;
+                            player2Strategy->setChoice(player2State, row);
                         } else {
                             // Since all player 1 successors are states with probability 0, just pick any.
-                            result.player2Strategy.get()[player2State] = transitionMatrix.getRowGroupIndices()[player2State];
+                            player2Strategy->setChoice(player2State, transitionMatrix.getRowGroupIndices()[player2State]);
                         }
                     }
                 }
@@ -1290,7 +1286,7 @@ namespace storm {
             }
             
             template <typename ValueType>
-            ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional<storm::storage::BitVector> const& player1Candidates) {
+            ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy, storm::abstraction::ExplicitGameStrategy* player2Strategy, boost::optional<storm::storage::BitVector> const& player1Candidates) {
                 
                 // During the execution, the two state sets in the result hold the potential player 1/2 states.
                 ExplicitGameProb01Result result;
@@ -1314,16 +1310,6 @@ namespace storm {
                     stack.clear();
                     stack.insert(stack.end(), psiStates.begin(), psiStates.end());
                     
-                    // If we are to produce strategies in this iteration, we prepare some storage.
-                    if (produceStrategiesInIteration) {
-                        if (producePlayer1Strategy) {
-                            result.player1Strategy = std::vector<uint64_t>(result.player1States.size());
-                        }
-                        if (producePlayer2Strategy) {
-                            result.player2Strategy = std::vector<uint64_t>(result.player2States.size());
-                        }
-                    }
-                    
                     // Perform the actual DFS.
                     uint_fast64_t currentState;
                     while (!stack.empty()) {
@@ -1333,7 +1319,7 @@ namespace storm {
                         for (auto player2PredecessorEntry : player1BackwardTransitions.getRow(currentState)) {
                             uint64_t player2Predecessor = player2PredecessorEntry.getColumn();
                             if (!player2Solution.get(player2PredecessorEntry.getColumn())) {
-                                bool addPlayer2State = player2Strategy == storm::OptimizationDirection::Minimize ? true : false;
+                                bool addPlayer2State = player2Direction == storm::OptimizationDirection::Minimize ? true : false;
                                 
                                 uint64_t validChoice = transitionMatrix.getRowGroupIndices()[player2Predecessor];
                                 for (uint64_t row = validChoice; row < transitionMatrix.getRowGroupIndices()[player2Predecessor + 1]; ++row) {
@@ -1350,12 +1336,12 @@ namespace storm {
                                     }
                                     
                                     if (choiceHasSolutionSuccessor && choiceStaysInMaybeStates) {
-                                        if (player2Strategy == storm::OptimizationDirection::Maximize) {
+                                        if (player2Direction == storm::OptimizationDirection::Maximize) {
                                             validChoice = row;
                                             addPlayer2State = true;
                                             break;
                                         }
-                                    } else if (player2Strategy == storm::OptimizationDirection::Minimize) {
+                                    } else if (player2Direction == storm::OptimizationDirection::Minimize) {
                                         addPlayer2State = false;
                                         break;
                                     }
@@ -1363,8 +1349,8 @@ namespace storm {
                                 
                                 if (addPlayer2State) {
                                     player2Solution.set(player2Predecessor);
-                                    if (produceStrategiesInIteration && producePlayer2Strategy) {
-                                        result.player2Strategy.get()[player2Predecessor] = validChoice;
+                                    if (produceStrategiesInIteration && player2Strategy) {
+                                        player2Strategy->setChoice(player2Predecessor, validChoice);
                                     }
                                     
                                     // Check whether the addition of the player 2 state changes the state of the (single)
@@ -1372,17 +1358,17 @@ namespace storm {
                                     uint64_t player1Predecessor = player2BackwardTransitions[player2Predecessor];
                                     
                                     if (!player1Solution.get(player1Predecessor)) {
-                                        bool addPlayer1State = player1Strategy == storm::OptimizationDirection::Minimize ? true : false;
+                                        bool addPlayer1State = player1Direction == storm::OptimizationDirection::Minimize ? true : false;
                                         
                                         validChoice = player1Groups[player1Predecessor];
                                         for (uint64_t player2Successor = validChoice; player2Successor < player1Groups[player1Predecessor + 1]; ++player2Successor) {
                                             if (player2Solution.get(player2Successor)) {
-                                                if (player1Strategy == storm::OptimizationDirection::Maximize) {
+                                                if (player1Direction == storm::OptimizationDirection::Maximize) {
                                                     validChoice = player2Successor;
                                                     addPlayer1State = true;
                                                     break;
                                                 }
-                                            } else if (player1Strategy == storm::OptimizationDirection::Minimize) {
+                                            } else if (player1Direction == storm::OptimizationDirection::Minimize) {
                                                 addPlayer1State = false;
                                                 break;
                                             }
@@ -1391,8 +1377,8 @@ namespace storm {
                                         if (addPlayer1State) {
                                             player1Solution.set(player1Predecessor);
                                             
-                                            if (produceStrategiesInIteration && producePlayer1Strategy) {
-                                                result.player1Strategy.get()[player1Predecessor] = validChoice;
+                                            if (produceStrategiesInIteration && player1Strategy) {
+                                                player1Strategy->setChoice(player1Predecessor, validChoice);
                                             }
                                             
                                             stack.emplace_back(player1Predecessor);
@@ -1690,9 +1676,9 @@ namespace storm {
 			template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
 #endif
             
-            template ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<double> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy);
+            template ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<double> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy, storm::abstraction::ExplicitGameStrategy* player2Strategy);
             
-            template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<double> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy, boost::optional<storm::storage::BitVector> const& player1Candidates);
+            template ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<double> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy, storm::abstraction::ExplicitGameStrategy* player2Strategy, boost::optional<storm::storage::BitVector> const& player1Candidates);
             
             template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<double> const& matrix) ;
             

src/storm/utility/graph.h

@@ -49,6 +49,9 @@ namespace storm {
         
     }
     
+    namespace abstraction {
+        class ExplicitGameStrategy;
+    }
     
     namespace utility {
         namespace graph {
@@ -621,34 +624,10 @@ namespace storm {
                     // Intentionally left empty.
                 }
                 
-                ExplicitGameProb01Result(storm::storage::BitVector const& player1States, storm::storage::BitVector const& player2States, boost::optional<std::vector<uint64_t>> const& player1Strategy = boost::none, boost::optional<std::vector<uint64_t>> const& player2Strategy = boost::none) : player1States(player1States), player2States(player2States), player1Strategy(player1Strategy), player2Strategy(player2Strategy) {
+                ExplicitGameProb01Result(storm::storage::BitVector const& player1States, storm::storage::BitVector const& player2States) : player1States(player1States), player2States(player2States) {
                     // Intentionally left empty.
                 }
                 
-                bool hasPlayer1Strategy() const {
-                    return static_cast<bool>(player1Strategy);
-                }
-                
-                std::vector<uint64_t> const& getPlayer1Strategy() const {
-                    return player1Strategy.get();
-                }
-                
-                boost::optional<std::vector<uint64_t>> const& getOptionalPlayer1Strategy() {
-                    return player1Strategy;
-                }
-                
-                bool hasPlayer2Strategy() const {
-                    return static_cast<bool>(player2Strategy);
-                }
-                
-                std::vector<uint64_t> const& getPlayer2Strategy() const {
-                    return player2Strategy.get();
-                }
-                
-                boost::optional<std::vector<uint64_t>> const& getOptionalPlayer2Strategy() {
-                    return player2Strategy;
-                }
-                
                 storm::storage::BitVector const& getPlayer1States() const {
                     return player1States;
                 }
@@ -659,8 +638,6 @@ namespace storm {
                 
                 storm::storage::BitVector player1States;
                 storm::storage::BitVector player2States;
-                boost::optional<std::vector<uint64_t>> player1Strategy;
-                boost::optional<std::vector<uint64_t>> player2Strategy;
             };
             
             /*!
@@ -672,11 +649,15 @@ namespace storm {
              * @param player2BackwardTransitions The backward transitions (player 2 to player 1).
              * @param phiStates The phi states of the model.
              * @param psiStates The psi states of the model.
-             * @param producePlayer1Strategy A flag indicating whether the strategy of player 1 shall be produced.
-             * @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced.
+             * @param player1Direction The optimization direction of player 1.
+             * @param player2Direction The optimization direction of player 2.
+             * @param player1Strategy If not null, a player 1 strategy is synthesized and the corresponding choices
+             * are written to this strategy.
+             * @param player2Strategy If not null, a player 2 strategy is synthesized and the corresponding choices
+             * are written to this strategy.
              */
             template <typename ValueType>
-            ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false);
+            ExplicitGameProb01Result performProb0(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy = nullptr, storm::abstraction::ExplicitGameStrategy* player2Strategy = nullptr);
             
             /*!
              * Computes the set of states that have probability 1 given the strategies of the two players.
@@ -687,12 +668,16 @@ namespace storm {
              * @param player2BackwardTransitions The backward transitions (player 2 to player 1).
              * @param phiStates The phi states of the model.
              * @param psiStates The psi states of the model.
-             * @param producePlayer1Strategy A flag indicating whether the strategy of player 1 shall be produced.
-             * @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced.
+             * @param player1Direction The optimization direction of player 1.
+             * @param player2Direction The optimization direction of player 2.
+             * @param player1Strategy If not null, a player 1 strategy is synthesized and the corresponding choices
+             * are written to this strategy.
+             * @param player2Strategy If not null, a player 2 strategy is synthesized and the corresponding choices
+             * are written to this strategy.
              * @param player1Candidates If given, this set constrains the candidates of player 1 states that are considered.
              */
             template <typename ValueType>
-            ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false, boost::optional<storm::storage::BitVector> const& player1Candidates = boost::none);
+            ExplicitGameProb01Result performProb1(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::ExplicitGameStrategy* player1Strategy = nullptr, storm::abstraction::ExplicitGameStrategy* player2Strategy = nullptr, boost::optional<storm::storage::BitVector> const& player1Candidates = boost::none);
             
             /*!
              * Performs a topological sort of the states of the system according to the given transitions.