explicit interpolation and started on explicit quantitative solution

src/storm/abstraction/AbstractionInformation.cpp

@@ -138,6 +138,22 @@ namespace storm {
             return result;
         }
         
+        template<storm::dd::DdType DdType>
+        std::vector<storm::expressions::Expression> AbstractionInformation<DdType>::getPredicatesExcludingBottom(storm::storage::BitVector const& predicateValuation) const {
+            STORM_LOG_ASSERT(predicateValuation.size() == this->getNumberOfPredicates() + 1, "Size of predicate valuation does not match number of predicates.");
+            
+            std::vector<storm::expressions::Expression> result;
+            for (uint64_t index = 0; index < this->getNumberOfPredicates(); ++index) {
+                if (predicateValuation[index + 1]) {
+                    result.push_back(this->getPredicateByIndex(index));
+                } else {
+                    result.push_back(!this->getPredicateByIndex(index));
+                }
+            }
+            
+            return result;
+        }
+        
         template<storm::dd::DdType DdType>
         storm::expressions::Expression const& AbstractionInformation<DdType>::getPredicateByIndex(uint_fast64_t index) const {
             return predicates[index];

src/storm/abstraction/AbstractionInformation.h

@@ -139,7 +139,13 @@ namespace storm {
              * Retrieves a list of expression that corresponds to the given predicate valuation.
              */
             std::vector<storm::expressions::Expression> getPredicates(storm::storage::BitVector const& predicateValuation) const;
-            
+
+            /*!
+             * Retrieves a list of expression that corresponds to the given predicate valuation that mentions all of the
+             * predicates' truth values *and* the value of the bottom variable (at the first index).
+             */
+            std::vector<storm::expressions::Expression> getPredicatesExcludingBottom(storm::storage::BitVector const& predicateValuation) const;
+
             /*!
              * Retrieves the predicate with the given index.
              *

src/storm/abstraction/ExplicitQuantiativeResultMinMax.cpp

@@ -0,0 +1,48 @@
+#include "storm/abstraction/ExplicitQuantitativeResultMinMax.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template<typename ValueType>
+        ExplicitQuantitativeResultMinMax<ValueType>::ExplicitQuantitativeResultMinMax(uint64_t numberOfStates) = default;
+        
+        template<typename ValueType>
+        ExplicitQuantitativeResult<ValueType> const& ExplicitQuantitativeResultMinMax<ValueType>::getMin() const {
+            return min;
+        }
+        
+        template<typename ValueType>
+        ExplicitQuantitativeResult<ValueType>& ExplicitQuantitativeResultMinMax<ValueType>::getMin() {
+            return min;
+        }
+        
+        template<typename ValueType>
+        ExplicitQuantitativeResult<ValueType> const& ExplicitQuantitativeResultMinMax<ValueType>::getMax() const {
+            return max;
+        }
+        
+        template<typename ValueType>
+        ExplicitQuantitativeResult<ValueType>& ExplicitQuantitativeResultMinMax<ValueType>::getMax() {
+            return max;
+        }
+        
+        template<typename ValueType>
+        ExplicitQuantitativeResult<ValueType> const& ExplicitQuantitativeResultMinMax<ValueType>::get(storm::OptimizationDirection const& dir) const {
+            if (dir == storm::OptimizationDirection::Minimize) {
+                return this->getMin();
+            } else {
+                return this->getMax();
+            }
+        }
+        
+        template<typename ValueType>
+        ExplicitQuantitativeResult<ValueType>& ExplicitQuantitativeResultMinMax<ValueType>::get(storm::OptimizationDirection const& dir) {
+            if (dir == storm::OptimizationDirection::Minimize) {
+                return this->getMin();
+            } else {
+                return this->getMax();
+            }
+        }
+
+    }
+}

src/storm/abstraction/ExplicitQuantitativeResult.cpp

@@ -0,0 +1,54 @@
+#include "storm/abstraction/ExplicitQuantitativeResult.h"
+
+#include "storm/storage/BitVector.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template<typename ValueType>
+        ExplicitQuantitativeResult<ValueType>::ExplicitQuantitativeResult(uint64_t numberOfStates) : values(numberOfStates) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        std::vector<ValueType> const& ExplicitQuantitativeResult<ValueType>::getValues() const {
+            return values;
+        }
+        
+        template<typename ValueType>
+        std::vector<ValueType>& ExplicitQuantitativeResult<ValueType>::getValues() {
+            return values;
+        }
+        
+        template<typename ValueType>
+        void ExplicitQuantitativeResult<ValueType>::setValue(uint64_t state, ValueType const& value) {
+            values[state] = value;
+        }
+        
+        template<typename ValueType>
+        std::pair<ValueType, ValueType> ExplicitQuantitativeResult<ValueType>::getRange(storm::storage::BitVector const& states) const {
+            STORM_LOG_THROW(!states.empty(), storm::exceptions::InvalidArgumentException, "Expected non-empty set of states.");
+            
+            auto stateIt = states.begin();
+            std::pair<ValueType, ValueType> result = std::make_pair(values[*stateIt], values[*stateIt]);
+            ++stateIt;
+            
+            while (stateIt != states.end()) {
+                if (values[*stateIt] < result.first) {
+                    result.first = values[*stateIt];
+                } else if (values[*stateIt] < result.first) {
+                    result.second = values[*stateIt];
+                }
+                
+                ++stateIt;
+            }
+            
+            return result;
+        }
+        
+        template class ExplicitQuantitativeResult<double>;
+    }
+}

src/storm/abstraction/ExplicitQuantitativeResult.h

@@ -0,0 +1,31 @@
+#pragma once
+
+#include <cstdint>
+#include <vector>
+
+namespace storm {
+    namespace storage {
+        class BitVector;
+    }
+    
+    namespace abstraction {
+        
+        template<typename ValueType>
+        class ExplicitQuantitativeResult {
+        public:
+            ExplicitQuantitativeResult() = default;
+            ExplicitQuantitativeResult(uint64_t numberOfStates);
+            
+            std::vector<ValueType> const& getValues() const;
+            std::vector<ValueType>& getValues();
+            void setValue(uint64_t state, ValueType const& value);
+            
+            std::pair<ValueType, ValueType> getRange(storm::storage::BitVector const& states) const;
+            
+        private:
+            std::vector<ValueType> values;
+        };
+        
+    }
+}
+

src/storm/abstraction/ExplicitQuantitativeResultMinMax.cpp

@@ -0,0 +1,61 @@
+#include "storm/abstraction/ExplicitQuantitativeResultMinMax.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template<typename ValueType>
+        ExplicitQuantitativeResultMinMax<ValueType>::ExplicitQuantitativeResultMinMax(uint64_t numberOfStates) : min(numberOfStates), max(numberOfStates) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        ExplicitQuantitativeResult<ValueType> const& ExplicitQuantitativeResultMinMax<ValueType>::getMin() const {
+            return min;
+        }
+        
+        template<typename ValueType>
+        ExplicitQuantitativeResult<ValueType>& ExplicitQuantitativeResultMinMax<ValueType>::getMin() {
+            return min;
+        }
+        
+        template<typename ValueType>
+        ExplicitQuantitativeResult<ValueType> const& ExplicitQuantitativeResultMinMax<ValueType>::getMax() const {
+            return max;
+        }
+        
+        template<typename ValueType>
+        ExplicitQuantitativeResult<ValueType>& ExplicitQuantitativeResultMinMax<ValueType>::getMax() {
+            return max;
+        }
+        
+        template<typename ValueType>
+        void ExplicitQuantitativeResultMinMax<ValueType>::setMin(ExplicitQuantitativeResult<ValueType>&& newMin) {
+            min = std::move(newMin);
+        }
+        
+        template<typename ValueType>
+        void ExplicitQuantitativeResultMinMax<ValueType>::setMax(ExplicitQuantitativeResult<ValueType>&& newMax) {
+            max = std::move(newMax);
+        }
+        
+        template<typename ValueType>
+        ExplicitQuantitativeResult<ValueType> const& ExplicitQuantitativeResultMinMax<ValueType>::get(storm::OptimizationDirection const& dir) const {
+            if (dir == storm::OptimizationDirection::Minimize) {
+                return this->getMin();
+            } else {
+                return this->getMax();
+            }
+        }
+        
+        template<typename ValueType>
+        ExplicitQuantitativeResult<ValueType>& ExplicitQuantitativeResultMinMax<ValueType>::get(storm::OptimizationDirection const& dir) {
+            if (dir == storm::OptimizationDirection::Minimize) {
+                return this->getMin();
+            } else {
+                return this->getMax();
+            }
+        }
+
+        template class ExplicitQuantitativeResultMinMax<double>;
+    }
+}

src/storm/abstraction/ExplicitQuantitativeResultMinMax.h

@@ -0,0 +1,32 @@
+#pragma once
+
+#include "storm/abstraction/ExplicitQuantitativeResult.h"
+
+#include "storm/solver/OptimizationDirection.h"
+
+namespace storm {
+    namespace abstraction {
+        
+        template<typename ValueType>
+        class ExplicitQuantitativeResultMinMax {
+        public:
+            ExplicitQuantitativeResultMinMax() = default;
+            ExplicitQuantitativeResultMinMax(uint64_t numberOfStates);
+
+            ExplicitQuantitativeResult<ValueType> const& getMin() const;
+            ExplicitQuantitativeResult<ValueType>& getMin();
+            ExplicitQuantitativeResult<ValueType> const& getMax() const;
+            ExplicitQuantitativeResult<ValueType>& getMax();
+            ExplicitQuantitativeResult<ValueType> const& get(storm::OptimizationDirection const& dir) const;
+            ExplicitQuantitativeResult<ValueType>& get(storm::OptimizationDirection const& dir);
+
+            void setMin(ExplicitQuantitativeResult<ValueType>&& newMin);
+            void setMax(ExplicitQuantitativeResult<ValueType>&& newMax);
+
+        private:
+            ExplicitQuantitativeResult<ValueType> min;
+            ExplicitQuantitativeResult<ValueType> max;
+        };
+        
+    }
+}

src/storm/abstraction/MenuGameAbstractor.cpp

@@ -23,6 +23,15 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        template <storm::dd::DdType DdType, typename ValueType>
+        std::vector<std::map<storm::expressions::Variable, storm::expressions::Expression>> MenuGameAbstractor<DdType, ValueType>::getVariableUpdates(uint64_t player1Choice) const {
+            std::vector<std::map<storm::expressions::Variable, storm::expressions::Expression>> result(this->getNumberOfUpdates(player1Choice));
+            for (uint64_t i = 0; i < result.size(); ++i) {
+                result[i] = this->getVariableUpdates(player1Choice, i);
+            }
+            return result;
+        }
+        
         template <typename ValueType>
         std::string getStateName(std::pair<storm::expressions::SimpleValuation, ValueType> const& stateValue, std::set<storm::expressions::Variable> const& locationVariables, std::set<storm::expressions::Variable> const& predicateVariables, storm::expressions::Variable const& bottomVariable) {
             std::stringstream stateName;

src/storm/abstraction/MenuGameAbstractor.h

@@ -34,6 +34,8 @@ namespace storm {
             virtual AbstractionInformation<DdType> const& getAbstractionInformation() const = 0;
             virtual storm::expressions::Expression const& getGuard(uint64_t player1Choice) const = 0;
             virtual std::pair<uint64_t, uint64_t> getPlayer1ChoiceRange() const = 0;
+            virtual uint64_t getNumberOfUpdates(uint64_t player1Choice) const = 0;
+            std::vector<std::map<storm::expressions::Variable, storm::expressions::Expression>> getVariableUpdates(uint64_t player1Choice) const;
             virtual std::map<storm::expressions::Variable, storm::expressions::Expression> getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const = 0;
             virtual storm::expressions::Expression getInitialExpression() const = 0;
             

src/storm/abstraction/MenuGameRefiner.cpp

@@ -526,6 +526,112 @@ namespace storm {
             predicates.back().push_back(initialExpression.changeManager(expressionManager).substitute(lastSubstitution));
             return std::make_pair(predicates, stepVariableToCopiedVariableMap);
         }
+        
+        template<typename ValueType>
+        const uint64_t ExplicitPivotStateResult<ValueType>::NO_PREDECESSOR = std::numeric_limits<uint64_t>::max();
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        std::pair<std::vector<std::vector<storm::expressions::Expression>>, std::map<storm::expressions::Variable, storm::expressions::Expression>> MenuGameRefiner<Type, ValueType>::buildTrace(storm::expressions::ExpressionManager& expressionManager, storm::abstraction::MenuGame<Type, ValueType> const& game, ExplicitPivotStateResult<ValueType> const& pivotStateResult, storm::dd::Odd const& odd) const {
+            
+            std::vector<std::vector<storm::expressions::Expression>> predicates;
+
+            AbstractionInformation<Type> const& abstractionInformation = abstractor.get().getAbstractionInformation();
+            storm::expressions::Expression initialExpression = abstractor.get().getInitialExpression();
+
+            std::set<storm::expressions::Variable> oldVariables = initialExpression.getVariables();
+            for (auto const& predicate : abstractionInformation.getPredicates()) {
+                std::set<storm::expressions::Variable> usedVariables = predicate.getVariables();
+                oldVariables.insert(usedVariables.begin(), usedVariables.end());
+            }
+            
+            std::map<storm::expressions::Variable, storm::expressions::Variable> oldToNewVariables;
+            for (auto const& variable : oldVariables) {
+                oldToNewVariables[variable] = expressionManager.getVariable(variable.getName());
+            }
+            std::map<storm::expressions::Variable, storm::expressions::Expression> lastSubstitution;
+            for (auto const& variable : oldToNewVariables) {
+                lastSubstitution[variable.second] = variable.second;
+            }
+            std::map<storm::expressions::Variable, storm::expressions::Expression> stepVariableToCopiedVariableMap;
+            
+            // The state valuation also includes the bottom state, so we need to reserve one more than the number of
+            // predicates here.
+            storm::storage::BitVector extendedPredicateValuation = odd.getEncoding(pivotStateResult.pivotState, abstractionInformation.getNumberOfPredicates() + 1);
+            
+            // Decode pivot state.
+            predicates.emplace_back(abstractionInformation.getPredicatesExcludingBottom(extendedPredicateValuation));
+            for (auto& predicate : predicates.back()) {
+                predicate = predicate.changeManager(expressionManager);
+            }
+            
+            // Perform a backward traversal from the pivot state along the chosen predecessors until there is no more
+            // predecessors.
+            uint64_t currentState = pivotStateResult.predecessors[pivotStateResult.pivotState].first;
+            uint64_t currentAction = pivotStateResult.predecessors[pivotStateResult.pivotState].second;
+            while (currentState != ExplicitPivotStateResult<ValueType>::NO_PREDECESSOR) {
+                // Create a new copy of each variable to use for this step.
+                std::map<storm::expressions::Variable, storm::expressions::Expression> substitution;
+                for (auto const& variablePair : oldToNewVariables) {
+                    storm::expressions::Variable variableCopy = expressionManager.declareVariableCopy(variablePair.second);
+                    substitution[variablePair.second] = variableCopy;
+                    stepVariableToCopiedVariableMap[variableCopy] = variablePair.second;
+                }
+                
+                // Retrieve the variable updates that the predecessor needs to perform to get to the current state.
+                auto variableUpdateVector = abstractor.get().getVariableUpdates(currentAction);
+                storm::expressions::Expression allVariableUpdateExpression;
+                for (auto const& variableUpdates : variableUpdateVector) {
+                    storm::expressions::Expression variableUpdateExpression;
+                    for (auto const& oldNewVariablePair : oldToNewVariables) {
+                        storm::expressions::Variable const& newVariable = oldNewVariablePair.second;
+                        
+                        // If the variable was set, use its update expression.
+                        auto updateIt = variableUpdates.find(oldNewVariablePair.first);
+                        if (updateIt != variableUpdates.end()) {
+                            auto const& update = *updateIt;
+                            
+                            if (update.second.hasBooleanType()) {
+                                variableUpdateExpression = variableUpdateExpression && storm::expressions::iff(lastSubstitution.at(newVariable), update.second.changeManager(expressionManager).substitute(substitution));
+                            } else {
+                                variableUpdateExpression = variableUpdateExpression && lastSubstitution.at(newVariable) == update.second.changeManager(expressionManager).substitute(substitution);
+                            }
+                        } else {
+                            // Otherwise, make sure that the new variable maintains the old value.
+                            if (newVariable.hasBooleanType()) {
+                                variableUpdateExpression = variableUpdateExpression && storm::expressions::iff(lastSubstitution.at(newVariable), substitution.at(newVariable));
+                            } else {
+                                variableUpdateExpression = variableUpdateExpression && lastSubstitution.at(newVariable) == substitution.at(newVariable);
+                            }
+                        }
+                    }
+                    
+                    allVariableUpdateExpression = allVariableUpdateExpression || variableUpdateExpression;
+                }
+                
+                // Add variable update expression.
+                predicates.back().emplace_back(allVariableUpdateExpression);
+                
+                // Add the guard of the choice.
+                predicates.back().emplace_back(abstractor.get().getGuard(currentAction).changeManager(expressionManager).substitute(substitution));
+                
+                // Retrieve the predicate valuation in the predecessor.
+                extendedPredicateValuation = odd.getEncoding(currentState, abstractionInformation.getNumberOfPredicates() + 1);
+                predicates.emplace_back(abstractionInformation.getPredicatesExcludingBottom(extendedPredicateValuation));
+                for (auto& predicate : predicates.back()) {
+                    predicate = predicate.changeManager(expressionManager).substitute(substitution);
+                }
+                
+                // Move backwards one step.
+                lastSubstitution = std::move(substitution);
+
+                std::pair<uint64_t, uint64_t> predecessorPair = pivotStateResult.predecessors[currentState];
+                currentState = predecessorPair.first;
+                currentAction = predecessorPair.second;
+            }
+            
+            predicates.back().push_back(initialExpression.changeManager(expressionManager).substitute(lastSubstitution));
+            return std::make_pair(predicates, stepVariableToCopiedVariableMap);
+        }
 
         template<storm::dd::DdType Type>
         boost::optional<RefinementPredicates> derivePredicatesFromInterpolation(storm::expressions::ExpressionManager& interpolationManager, AbstractionInformation<Type> const& abstractionInformation, std::vector<std::vector<storm::expressions::Expression>> const& trace, std::map<storm::expressions::Variable, storm::expressions::Expression> const& variableSubstitution) {
@@ -579,8 +685,6 @@ namespace storm {
         template<storm::dd::DdType Type, typename ValueType>
         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.
             SymbolicMostProbablePathsResult<Type, ValueType> symbolicMostProbablePathsResult;
             if (!symbolicPivotStateResult.symbolicMostProbablePathsResult) {
@@ -590,6 +694,7 @@ namespace storm {
             }
             
             // Create a new expression manager that we can use for the interpolation.
+            AbstractionInformation<Type> const& abstractionInformation = abstractor.get().getAbstractionInformation();
             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.
@@ -600,7 +705,15 @@ namespace storm {
         
         template<storm::dd::DdType Type, typename ValueType>
         boost::optional<RefinementPredicates> MenuGameRefiner<Type, ValueType>::derivePredicatesFromInterpolation(storm::abstraction::MenuGame<Type, ValueType> const& game, ExplicitPivotStateResult<ValueType> const& pivotStateResult, storm::dd::Odd const& odd) const {
-            // TODO.
+
+            // Create a new expression manager that we can use for the interpolation.
+            AbstractionInformation<Type> const& abstractionInformation = abstractor.get().getAbstractionInformation();
+            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, pivotStateResult, odd);
+            
+            return storm::abstraction::derivePredicatesFromInterpolation(*interpolationManager, abstractionInformation, traceAndVariableSubstitution.first, traceAndVariableSubstitution.second);
         }
         
         template<storm::dd::DdType Type, typename ValueType>
@@ -631,7 +744,7 @@ 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.
-            SymbolicPivotStateResult<Type, ValueType> SymbolicPivotStateResult = 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.
@@ -677,12 +790,12 @@ namespace storm {
 
             boost::optional<RefinementPredicates> predicates;
             if (useInterpolation) {
-                predicates = derivePredicatesFromInterpolation(game, SymbolicPivotStateResult, 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, SymbolicPivotStateResult.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.");
             
@@ -693,8 +806,11 @@ namespace storm {
         }
         
         template<typename ValueType>
-        boost::optional<ExplicitPivotStateResult<ValueType>> pickPivotState(bool generatePredecessors, 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) {
+        boost::optional<ExplicitPivotStateResult<ValueType>> pickPivotState(bool generatePredecessors, AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Grouping, std::vector<uint64_t> const& player1Labeling, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& relevantStates, storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair, std::vector<ValueType> const* lowerValues = nullptr, std::vector<ValueType> const* upperValues = nullptr) {
             
+            STORM_LOG_ASSERT(!lowerValues || upperValues, "Expected none or both value results.");
+            STORM_LOG_ASSERT(!upperValues || lowerValues, "Expected none or both value results.");
+
             // 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> result;
@@ -705,7 +821,7 @@ namespace storm {
             ValueType zeroDistance = probabilityDistances ? storm::utility::one<ValueType>() : storm::utility::zero<ValueType>();
             std::vector<ValueType> distances(numberOfStates, inftyDistance);
             if (generatePredecessors) {
-                result.predecessors.resize(numberOfStates, std::make_pair(0, 0));
+                result.predecessors.resize(numberOfStates, std::make_pair(ExplicitPivotStateResult<ValueType>::NO_PREDECESSOR, ExplicitPivotStateResult<ValueType>::NO_PREDECESSOR));
             }
 
             // Use set as priority queue with unique membership; default comparison on pair works fine if distance is
@@ -722,8 +838,9 @@ namespace storm {
             }
 
             // For some heuristics, we need to potentially find more than just one pivot.
+            bool considerDeviation = (pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::NearestMaximalDeviation || pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation) && lowerValues && upperValues;
             bool foundPivotState = false;
-            ValueType maximalDeviation = storm::utility::zero<ValueType>();
+            ValueType pivotStateDeviation = storm::utility::zero<ValueType>();
             
             while (!dijkstraQueue.empty()) {
                 auto distanceStatePair = *dijkstraQueue.begin();
@@ -731,8 +848,17 @@ namespace storm {
                 ValueType currentDistance = distanceStatePair.first;
                 dijkstraQueue.erase(dijkstraQueue.begin());
                 
-                if (foundPivotState && currentDistance > result.distance) {
-                    return result;
+                if (foundPivotState && (probabilityDistances ? currentDistance < result.distance : currentDistance > result.distance)) {
+                    if (pivotSelectionHeuristic != storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation) {
+                        // For the nearest maximal deviation and most probable path heuristics, future pivot states are
+                        // not important any more, because their distance will be strictly larger, so we can return the
+                        // current pivot state.
+                        return result;
+                    } else if (pivotStateDeviation >= currentDistance) {
+                        // If the heuristic is maximal weighted deviation and the weighted deviation for any future pivot
+                        // state is necessarily at most as high as the current one, we can abort the search.
+                        return result;
+                    }
                 }
                 
                 // Determine whether the current state is a pivot state.
@@ -751,14 +877,26 @@ namespace storm {
                 
                 // If it is indeed a pivot state, we can abort the search here.
                 if (isPivotState) {
-                    if (foundPivotState && haveQuantitativeResults && deviationOfCurrentState > currentPivotState) {
-                        result.pivotState = currentState;
-                        maximalDeviation = deviationForCurrentState;
+                    if (considerDeviation && foundPivotState) {
+                        ValueType deviationOfCurrentState = (*upperValues)[currentState] - (*lowerValues)[currentState];
+                        if (deviationOfCurrentState > pivotStateDeviation) {
+                            result.pivotState = currentState;
+                            pivotStateDeviation = deviationOfCurrentState;
+                            if (pivotSelectionHeuristic == storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation) {
+                                // Scale the deviation with the distance (probability) for this heuristic.
+                                pivotStateDeviation *= currentDistance;
+                            }
+                        }
                     } else if (!foundPivotState) {
                         result.pivotState = currentState;
                         result.distance = distances[currentState];
                         foundPivotState = true;
                     }
+                    
+                    // If there is no need to look at other deviations, stop here.
+                    if (!considerDeviation) {
+                        return result;
+                    }
                 }
                 
                 // Otherwise, we explore all its relevant successors.
@@ -776,7 +914,7 @@ namespace storm {
                         if ((probabilityDistances && alternateDistance > distances[player1Successor]) || (!probabilityDistances && alternateDistance < distances[player1Successor])) {
                             distances[player1Successor] = alternateDistance;
                             if (generatePredecessors) {
-                                result.predecessors[player1Successor] = std::make_pair(currentState, minPlayer2Successor);
+                                result.predecessors[player1Successor] = std::make_pair(currentState, player1Labeling[minPlayer2Successor]);
                             }
                             dijkstraQueue.emplace(alternateDistance, player1Successor);
                         }
@@ -812,12 +950,10 @@ namespace storm {
         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 {
             
-            STORM_LOG_THROW(heuristic != AbstractionSettings::PivotSelectionHeuristic::MaxWeightedDeviation, storm::exceptions::NotImplementedException, "The pivot selection heuristic 'maximal weighted deviation' is not supported by the sparse solution strategy.");
-            
             // 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());
 
-            boost::optional<ExplicitPivotStateResult<ValueType>> optionalPivotStateResult = pickPivotState(useInterpolation, pivotSelectionHeuristic, transitionMatrix, player1Grouping, initialStates, relevantStates, targetStates, qualitativeResult, minStrategyPair, maxStrategyPair);
+            boost::optional<ExplicitPivotStateResult<ValueType>> optionalPivotStateResult = pickPivotState(useInterpolation, pivotSelectionHeuristic, transitionMatrix, player1Grouping, player1Labeling, initialStates, relevantStates, targetStates, qualitativeResult, minStrategyPair, maxStrategyPair);
             
             // If there was no pivot state, continue the search.
             if (!optionalPivotStateResult) {
@@ -866,7 +1002,6 @@ namespace storm {
             boost::optional<RefinementPredicates> predicates;
             if (useInterpolation) {
                 predicates = derivePredicatesFromInterpolation(game, pivotStateResult, odd);
-
             }
             if (!predicates) {
                 predicates = derivePredicatesFromPivotState(game, symbolicPivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
@@ -972,7 +1107,9 @@ namespace storm {
                 for (auto const& predicate : command.getPredicates()) {
                     STORM_LOG_TRACE(predicate);
                 }
-                abstractor.get().refine(command);
+                if (!command.getPredicates().empty()) {
+                    abstractor.get().refine(command);
+                }
             }
             
             STORM_LOG_TRACE("Current set of predicates:");

src/storm/abstraction/MenuGameRefiner.h

@@ -82,6 +82,9 @@ namespace storm {
             /// The distance with which the state in question is reached.
             ValueType distance;
             
+            /// The value filled in for states without predecessors in the search.
+            static const uint64_t NO_PREDECESSOR;
+            
             /// The predecessors for the states to obtain the given distance.
             std::vector<std::pair<uint64_t, uint64_t>> predecessors;
         };
@@ -146,6 +149,8 @@ namespace storm {
             
             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;
+            
+            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, ExplicitPivotStateResult<ValueType> const& pivotStateResult, storm::dd::Odd const& odd) const;
             boost::optional<RefinementPredicates> derivePredicatesFromInterpolation(storm::abstraction::MenuGame<Type, ValueType> const& game, ExplicitPivotStateResult<ValueType> const& pivotStateResult, storm::dd::Odd const& odd) const;
 
             void performRefinement(std::vector<RefinementCommand> const& refinementCommands) const;

src/storm/abstraction/jani/AutomatonAbstractor.cpp

@@ -51,6 +51,11 @@ namespace storm {
                 return edges[player1Choice].getGuard();
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            uint64_t AutomatonAbstractor<DdType, ValueType>::getNumberOfUpdates(uint64_t player1Choice) const {
+                return edges[player1Choice].getNumberOfUpdates(player1Choice);
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             std::map<storm::expressions::Variable, storm::expressions::Expression> AutomatonAbstractor<DdType, ValueType>::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const {
                 return edges[player1Choice].getVariableUpdates(auxiliaryChoice);

src/storm/abstraction/jani/AutomatonAbstractor.h

@@ -57,6 +57,11 @@ namespace storm {
                  */
                 storm::expressions::Expression const& getGuard(uint64_t player1Choice) const;
                 
+                /*!
+                 * Retrieves the number of updates of the specified player 1 choice.
+                 */
+                uint64_t getNumberOfUpdates(uint64_t player1Choice) const;
+
                 /*!
                  * Retrieves a mapping from variables to expressions that define their updates wrt. to the given player
                  * 1 choice and auxiliary choice.

src/storm/abstraction/jani/EdgeAbstractor.cpp

@@ -65,6 +65,11 @@ namespace storm {
                 return edge.get().getGuard();
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            uint64_t EdgeAbstractor<DdType, ValueType>::getNumberOfUpdates(uint64_t player1Choice) const {
+                return edge.get().getNumberOfDestinations();
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             std::map<storm::expressions::Variable, storm::expressions::Expression> EdgeAbstractor<DdType, ValueType>::getVariableUpdates(uint64_t auxiliaryChoice) const {
                 return edge.get().getDestination(auxiliaryChoice).getAsVariableToExpressionMap();

src/storm/abstraction/jani/EdgeAbstractor.h

@@ -72,6 +72,11 @@ namespace storm {
                  */
                 storm::expressions::Expression const& getGuard() const;
                 
+                /*!
+                 * Retrieves the number of updates of this edge.
+                 */
+                uint64_t getNumberOfUpdates(uint64_t player1Choice) const;
+                
                 /*!
                  * Retrieves a mapping from variables to expressions that define their updates wrt. to the given
                  * auxiliary choice.

src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp

@@ -119,6 +119,11 @@ namespace storm {
                 return automata.front().getGuard(player1Choice);
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            uint64_t JaniMenuGameAbstractor<DdType, ValueType>::getNumberOfUpdates(uint64_t player1Choice) const {
+                return automata.front().getNumberOfUpdates(player1Choice);
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             std::map<storm::expressions::Variable, storm::expressions::Expression> JaniMenuGameAbstractor<DdType, ValueType>::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const {
                 return automata.front().getVariableUpdates(player1Choice, auxiliaryChoice);

src/storm/abstraction/jani/JaniMenuGameAbstractor.h

@@ -75,6 +75,11 @@ namespace storm {
                  */
                 storm::expressions::Expression const& getGuard(uint64_t player1Choice) const override;
                 
+                /*!
+                 * Retrieves the number of updates of the specified player 1 choice.
+                 */
+                virtual uint64_t getNumberOfUpdates(uint64_t player1Choice) const override;
+
                 /*!
                  * Retrieves a mapping from variables to expressions that define their updates wrt. to the given player
                  * 1 choice and auxiliary choice.

src/storm/abstraction/prism/CommandAbstractor.cpp

@@ -65,6 +65,11 @@ namespace storm {
                 return command.get().getGuardExpression();
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            uint64_t CommandAbstractor<DdType, ValueType>::getNumberOfUpdates(uint64_t player1Choice) const {
+                return command.get().getNumberOfUpdates();
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             std::map<storm::expressions::Variable, storm::expressions::Expression> CommandAbstractor<DdType, ValueType>::getVariableUpdates(uint64_t auxiliaryChoice) const {
                 return command.get().getUpdate(auxiliaryChoice).getAsVariableToExpressionMap();

src/storm/abstraction/prism/CommandAbstractor.h

@@ -70,6 +70,11 @@ namespace storm {
                  */
                 storm::expressions::Expression const& getGuard() const;
                 
+                /*!
+                 * Retrieves the number of updates of this command.
+                 */
+                uint64_t getNumberOfUpdates(uint64_t player1Choice) const;
+                
                 /*!
                  * Retrieves a mapping from variables to expressions that define their updates wrt. to the given
                  * auxiliary choice.

src/storm/abstraction/prism/ModuleAbstractor.cpp

@@ -45,6 +45,11 @@ namespace storm {
                 return commands[player1Choice].getGuard();
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            uint64_t ModuleAbstractor<DdType, ValueType>::getNumberOfUpdates(uint64_t player1Choice) const {
+                return commands[player1Choice].getNumberOfUpdates(player1Choice);
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             std::map<storm::expressions::Variable, storm::expressions::Expression> ModuleAbstractor<DdType, ValueType>::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const {
                 return commands[player1Choice].getVariableUpdates(auxiliaryChoice);

src/storm/abstraction/prism/ModuleAbstractor.h

@@ -60,6 +60,11 @@ namespace storm {
                  */
                 storm::expressions::Expression const& getGuard(uint64_t player1Choice) const;
                 
+                /*!
+                 * Retrieves the number of updates of the specified player 1 choice.
+                 */
+                uint64_t getNumberOfUpdates(uint64_t player1Choice) const;
+                
                 /*!
                  * Retrieves a mapping from variables to expressions that define their updates wrt. to the given player
                  * 1 choice and auxiliary choice.

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -115,6 +115,11 @@ namespace storm {
                 return modules.front().getGuard(player1Choice);
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            uint64_t PrismMenuGameAbstractor<DdType, ValueType>::getNumberOfUpdates(uint64_t player1Choice) const {
+                return modules.front().getNumberOfUpdates(player1Choice);
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             std::map<storm::expressions::Variable, storm::expressions::Expression> PrismMenuGameAbstractor<DdType, ValueType>::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const {
                 return modules.front().getVariableUpdates(player1Choice, auxiliaryChoice);

src/storm/abstraction/prism/PrismMenuGameAbstractor.h

@@ -74,6 +74,11 @@ namespace storm {
                  * @return The guard of the player 1 choice.
                  */
                 storm::expressions::Expression const& getGuard(uint64_t player1Choice) const override;
+
+                /*!
+                 * Retrieves the number of updates of the specified player 1 choice.
+                 */
+                virtual uint64_t getNumberOfUpdates(uint64_t player1Choice) const override;
                 
                 /*!
                  * Retrieves a mapping from variables to expressions that define their updates wrt. to the given player

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -27,6 +27,7 @@
 #include "storm/abstraction/ExplicitGameStrategyPair.h"
 
 #include "storm/abstraction/ExplicitQualitativeGameResultMinMax.h"
+#include "storm/abstraction/ExplicitQuantitativeResultMinMax.h"
 
 #include "storm/logic/FragmentSpecification.h"
 
@@ -49,7 +50,10 @@ namespace storm {
         
         using storm::abstraction::SymbolicQuantitativeGameResult;
         using storm::abstraction::SymbolicQuantitativeGameResultMinMax;
-        
+        using storm::abstraction::ExplicitQuantitativeResult;
+        using storm::abstraction::ExplicitQuantitativeResultMinMax;
+        using storm::abstraction::ExplicitGameStrategyPair;
+
         template<storm::dd::DdType Type, typename ModelType>
         GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(false), solveMode(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getSolveMode()) {
             model.requireNoUndefinedConstants();
@@ -385,6 +389,35 @@ namespace storm {
             return result;
         }
         
+        template<typename ValueType>
+        ExplicitQuantitativeResult<ValueType> computeQuantitativeResult(Environment const& env, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1Groups, ExplicitQualitativeGameResultMinMax const& qualitativeResult, storm::storage::BitVector const& maybeStates, ExplicitGameStrategyPair& minStrategyPair) {
+            
+            bool player2Min = player2Direction == storm::OptimizationDirection::Minimize;
+            auto const& player2Prob0States = player2Min ? qualitativeResult.getProb0Min().asExplicitQualitativeGameResult().getPlayer2States() : qualitativeResult.getProb0Max().asExplicitQualitativeGameResult().getPlayer2States();
+            auto const& player2Prob1States = player2Min ? qualitativeResult.getProb1Min().asExplicitQualitativeGameResult().getPlayer2States() : qualitativeResult.getProb1Max().asExplicitQualitativeGameResult().getPlayer2States();
+
+            // Determine which rows to keep.
+            storm::storage::BitVector rows(transitionMatrix.getRowCount());
+            for (uint64_t player2State = 0; player2State < transitionMatrix.getRowGroupCount(); ++player2State) {
+                if (!player2Prob0States.get(player2State) && !player2Prob1States.get(player2State)) {
+                    // Mark all rows that have a maybe state as a successor.
+                    for (uint64_t row = transitionMatrix.getRowGroupIndices()[player2State]; row < transitionMatrix.getRowGroupIndices()[player2State + 1]; ++row) {
+                        bool hasMaybeStateSuccessor = false;
+                        for (auto const& entry : transitionMatrix.getRow(row)) {
+                            if (maybeStates.get(entry.getColumn())) {
+                                hasMaybeStateSuccessor = true;
+                            }
+                        }
+                        if (!hasMaybeStateSuccessor) {
+                            rows.set(row);
+                        }
+                    }
+                }
+            }
+            
+            storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, player2MaybeStates, <#const storm::storage::BitVector &columnConstraint#>)
+        }
+        
         template<storm::dd::DdType Type, typename ModelType>
         std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ModelType>::performGameBasedAbstractionRefinement(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) {
             STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states.");
@@ -430,7 +463,7 @@ namespace storm {
                 auto abstractionStart = std::chrono::high_resolution_clock::now();
                 storm::abstraction::MenuGame<Type, ValueType> game = abstractor->abstract();
                 auto abstractionEnd = std::chrono::high_resolution_clock::now();
-                STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states (computed in " << std::chrono::duration_cast<std::chrono::milliseconds>(abstractionEnd - abstractionStart).count() << "ms).");
+                STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " player 1 states, " << game.getNumberOfPlayer2States() << " player 2 states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states (computed in " << std::chrono::duration_cast<std::chrono::milliseconds>(abstractionEnd - abstractionStart).count() << "ms).");
                 
                 // (2) Prepare initial, constraint and target state BDDs for later use.
                 storm::dd::Bdd<Type> initialStates = game.getInitialStates();
@@ -517,7 +550,6 @@ namespace storm {
                 // At this point, we know that we cannot answer the query without further numeric computation.
                 STORM_LOG_TRACE("Starting numerical solution step.");
                 
-                STORM_LOG_TRACE("Using dd-based solving.");
                 storm::dd::Add<Type, ValueType> initialStatesAdd = initialStates.template toAdd<ValueType>();
                 
                 auto quantitativeStart = std::chrono::high_resolution_clock::now();
@@ -660,6 +692,57 @@ namespace storm {
                 return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), ValueType(0.5));
             }
             
+            // (4) if we arrived at this point and no refinement was made, we need to compute the quantitative solution.
+            if (!qualitativeRefinement) {
+                // At this point, we know that we cannot answer the query without further numeric computation.
+                STORM_LOG_TRACE("Starting numerical solution step.");
+                
+                auto quantitativeStart = std::chrono::high_resolution_clock::now();
+
+                ExplicitQuantitativeResultMinMax<ValueType> quantitativeResult;
+                quantitativeResult.setMin(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, transitionMatrix, player1Groups, qualitativeResult, maybeMin, minStrategyPair));
+                
+//                SymbolicQuantitativeGameResultMinMax<Type, ValueType> quantitativeResult;
+//
+//                // (7) Solve the min values and check whether we can give the answer already.
+//                quantitativeResult.min = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin, reuseQuantitativeResults ? previousMinQuantitativeResult : boost::none);
+//                previousMinQuantitativeResult = quantitativeResult.min;
+//                result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.getInitialStatesRange());
+//                if (result) {
+//                    return result;
+//                }
+//
+//                // (8) Solve the max values and check whether we can give the answer already.
+//                quantitativeResult.max = computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min));
+//                result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.getInitialStatesRange());
+//                if (result) {
+//                    return result;
+//                }
+//
+                auto quantitativeEnd = std::chrono::high_resolution_clock::now();
+                STORM_LOG_DEBUG("Obtained quantitative bounds [" << quantitativeResult.getMin().getRange(initialStates).first << ", " << quantitativeResult.getMax().getRange(initialStates).second << "] on the actual value for the initial states in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeEnd - quantitativeStart).count() << "ms.");
+//
+//                // (9) Check whether the lower and upper bounds are close enough to terminate with an answer.
+//                result = checkForResultAfterQuantitativeCheck<ValueType>(quantitativeResult.min.getInitialStatesRange().first, quantitativeResult.max.getInitialStatesRange().second, comparator);
+//                if (result) {
+//                    return result;
+//                }
+//
+//                // Make sure that all strategies are still valid strategies.
+//                STORM_LOG_ASSERT(quantitativeResult.min.getPlayer1Strategy().isZero() || quantitativeResult.min.getPlayer1Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal.");
+//                STORM_LOG_ASSERT(quantitativeResult.max.getPlayer1Strategy().isZero() || quantitativeResult.max.getPlayer1Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal.");
+//                STORM_LOG_ASSERT(quantitativeResult.min.getPlayer2Strategy().isZero() || quantitativeResult.min.getPlayer2Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal.");
+//                STORM_LOG_ASSERT(quantitativeResult.max.getPlayer2Strategy().isZero() || quantitativeResult.max.getPlayer2Strategy().template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal.");
+//
+                auto quantitativeRefinementStart = std::chrono::high_resolution_clock::now();
+//
+//                // (10) If we arrived at this point, it means that we have all qualitative and quantitative
+//                // information about the game, but we could not yet answer the query. In this case, we need to refine.
+//                refiner.refine(game, transitionMatrixBdd, quantitativeResult);
+                auto quantitativeRefinementEnd = std::chrono::high_resolution_clock::now();
+                STORM_LOG_DEBUG("Quantitative refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeRefinementEnd - quantitativeRefinementStart).count() << "ms.");
+            }
+            
             return nullptr;
         }
         

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h

@@ -39,6 +39,13 @@ namespace storm {
         
         class ExplicitQualitativeGameResult;
         class ExplicitQualitativeGameResultMinMax;
+        
+        template<typename ValueType>
+        class ExplicitQuantitativeResult;
+
+        template<typename ValueType>
+        class ExplicitQuantitativeResultMinMax;
+        
         class ExplicitGameStrategy;
         class ExplicitGameStrategyPair;
     }

src/storm/models/symbolic/StochasticTwoPlayerGame.cpp

@@ -100,6 +100,11 @@ namespace storm {
 
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            uint64_t StochasticTwoPlayerGame<Type, ValueType>::getNumberOfPlayer2States() const {
+                return this->getQualitativeTransitionMatrix().existsAbstract(this->getColumnVariables()).getNonZeroCount();
+            }
+            
             // Explicitly instantiate the template class.
 			template class StochasticTwoPlayerGame<storm::dd::DdType::CUDD, double>;
 			template class StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, double>;

src/storm/models/symbolic/StochasticTwoPlayerGame.h

@@ -120,6 +120,11 @@ namespace storm {
                 template<typename NewValueType>
                 std::shared_ptr<StochasticTwoPlayerGame<Type, NewValueType>> toValueType() const;
                 
+                /*!
+                 * Retrieves the number of player 2 states in the game.
+                 */
+                uint64_t getNumberOfPlayer2States() const;
+                
             private:
                 /*!
                  * Prepare all illegal masks.