first working version of sparse game-based abstraction refinement

src/storm/abstraction/MenuGameRefiner.cpp

@@ -6,6 +6,7 @@
 #include "storm/storage/BitVector.h"
 #include "storm/abstraction/ExplicitQualitativeGameResultMinMax.h"
 #include "storm/abstraction/ExplicitGameStrategyPair.h"
+#include "storm/abstraction/ExplicitQuantitativeResultMinMax.h"
 
 #include "storm/storage/dd/DdManager.h"
 #include "storm/storage/dd/Odd.h"
@@ -667,11 +668,12 @@ namespace storm {
                     prefix.push_back(step);
                     storm::expressions::Expression interpolant = interpolatingSolver.getInterpolant(prefix).substitute(variableSubstitution).changeManager(abstractionInformation.getExpressionManager());
                     if (!interpolant.isTrue() && !interpolant.isFalse()) {
-                        STORM_LOG_DEBUG("Derived new predicate (based on interpolation): " << interpolant);
+                        STORM_LOG_DEBUG("Derived new predicate (based on interpolation at step " << step << " out of " << stepCounter << "): " << interpolant);
                         interpolants.push_back(interpolant);
-                    } else {
-                        STORM_LOG_ASSERT(false, "The found interpolant is '" << interpolant << "', which shouldn't happen.");
                     }
+//                    else {
+//                        STORM_LOG_ASSERT(step == 0false, "The found interpolant (based on interpolation at step " << step << " out of " << stepCounter << ") is '" << interpolant << "', which shouldn't happen.");
+//                    }
                 }
                 return boost::make_optional(RefinementPredicates(RefinementPredicates::Source::Interpolation, interpolants));
             } else {
@@ -805,7 +807,7 @@ 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, 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) {
+        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, 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.");
@@ -954,7 +956,7 @@ namespace storm {
             // 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, player1Labeling, initialStates, relevantStates, targetStates, qualitativeResult, minStrategyPair, maxStrategyPair);
+            boost::optional<ExplicitPivotStateResult<ValueType>> optionalPivotStateResult = pickPivotState(useInterpolation, pivotSelectionHeuristic, transitionMatrix, player1Grouping, player1Labeling, initialStates, relevantStates, targetStates, minStrategyPair, maxStrategyPair);
             
             // If there was no pivot state, continue the search.
             if (!optionalPivotStateResult) {
@@ -1002,11 +1004,76 @@ namespace storm {
                     maxPlayer2Strategy |= maxPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size());
                 }
             }
-//            symbolicPivotState.template toAdd<ValueType>().exportToDot("pivot.dot");
-//            minPlayer1Strategy.template toAdd<ValueType>().exportToDot("minpl1.dot");
-//            minPlayer2Strategy.template toAdd<ValueType>().exportToDot("minpl2.dot");
-//            maxPlayer1Strategy.template toAdd<ValueType>().exportToDot("maxpl1.dot");
-//            maxPlayer2Strategy.template toAdd<ValueType>().exportToDot("maxpl2.dot");
+
+            boost::optional<RefinementPredicates> predicates;
+            if (useInterpolation) {
+                predicates = derivePredicatesFromInterpolation(game, pivotStateResult, odd);
+            }
+            if (!predicates) {
+                predicates = derivePredicatesFromPivotState(game, symbolicPivotState, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy);
+            }
+            STORM_LOG_THROW(static_cast<bool>(predicates), storm::exceptions::InvalidStateException, "Predicates needed to continue.");
+            
+            std::vector<storm::expressions::Expression> preparedPredicates = preprocessPredicates(predicates.get().getPredicates(), predicates.get().getSource());
+            performRefinement(createGlobalRefinement(preparedPredicates));
+            return true;
+        }
+        
+        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, ExplicitQuantitativeResultMinMax<ValueType> const& quantitativeResult, 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(odd.getTotalOffset(), true);
+            
+            boost::optional<ExplicitPivotStateResult<ValueType>> optionalPivotStateResult = pickPivotState(useInterpolation, pivotSelectionHeuristic, transitionMatrix, player1Grouping, player1Labeling, initialStates, relevantStates, targetStates, minStrategyPair, maxStrategyPair, &quantitativeResult.getMin().getValues(), &quantitativeResult.getMax().getValues());
+            
+            // If there was no pivot state, continue the search.
+            if (!optionalPivotStateResult) {
+                STORM_LOG_TRACE("Did not find pivot state in qualitative fragment.");
+                return false;
+            }
+            
+            // Otherwise, we can refine.
+            auto const& pivotStateResult = optionalPivotStateResult.get();
+            STORM_LOG_TRACE("Found pivot state " << pivotStateResult.pivotState << " with distance " << pivotStateResult.distance << ".");
+            
+            // Translate the explicit states/choices to the symbolic ones, so we can reuse the predicate derivation techniques.
+            auto const& abstractionInformation = abstractor.get().getAbstractionInformation();
+            uint64_t pivotState = pivotStateResult.pivotState;
+            storm::dd::Bdd<Type> symbolicPivotState = storm::dd::Bdd<Type>::getEncoding(game.getManager(), pivotState, odd, game.getRowVariables());
+            storm::dd::Bdd<Type> minPlayer1Strategy = game.getManager().getBddZero();
+            storm::dd::Bdd<Type> maxPlayer1Strategy = game.getManager().getBddZero();
+            storm::dd::Bdd<Type> minPlayer2Strategy = game.getManager().getBddZero();
+            storm::dd::Bdd<Type> maxPlayer2Strategy = game.getManager().getBddZero();
+            if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(pivotState)) {
+                uint64_t player2State = minStrategyPair.getPlayer1Strategy().getChoice(pivotState);
+                STORM_LOG_ASSERT(player1Grouping[pivotState] <= player2State && player2State < player1Grouping[pivotState + 1], "Illegal choice for player 1.");
+                minPlayer1Strategy |= symbolicPivotState && abstractionInformation.encodePlayer1Choice(player1Labeling[player2State], abstractionInformation.getPlayer1VariableCount());
+                
+                if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2State)) {
+                    uint64_t player2Choice = minStrategyPair.getPlayer2Strategy().getChoice(player2State);
+                    minPlayer2Strategy |= minPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size());
+                }
+                if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2State)) {
+                    uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(player2State);
+                    maxPlayer2Strategy |= minPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size());
+                }
+            }
+            if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(pivotState)) {
+                uint64_t player2State = maxStrategyPair.getPlayer1Strategy().getChoice(pivotState);
+                STORM_LOG_ASSERT(player1Grouping[pivotState] <= player2State && player2State < player1Grouping[pivotState + 1], "Illegal choice for player 1.");
+                maxPlayer1Strategy |= symbolicPivotState && abstractionInformation.encodePlayer1Choice(player1Labeling[player2State], abstractionInformation.getPlayer1VariableCount());
+                
+                if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2State)) {
+                    uint64_t player2Choice = minStrategyPair.getPlayer2Strategy().getChoice(player2State);
+                    minPlayer2Strategy |= maxPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size());
+                }
+                if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(player2State)) {
+                    uint64_t player2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(player2State);
+                    maxPlayer2Strategy |= maxPlayer1Strategy && abstractionInformation.encodePlayer2Choice(player2Labeling[player2Choice], 0, game.getPlayer2Variables().size());
+                }
+            }
+            
             boost::optional<RefinementPredicates> predicates;
             if (useInterpolation) {
                 predicates = derivePredicatesFromInterpolation(game, pivotStateResult, odd);

src/storm/abstraction/MenuGameRefiner.h

@@ -91,7 +91,10 @@ namespace storm {
         
         class ExplicitQualitativeGameResultMinMax;
         class ExplicitGameStrategyPair;
-        
+
+        template<typename ValueType>
+        class ExplicitQuantitativeResultMinMax;
+
         template<storm::dd::DdType Type, typename ValueType>
         class MenuGameRefiner {
         public:
@@ -121,6 +124,13 @@ namespace storm {
              */
             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 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, ExplicitQuantitativeResultMinMax<ValueType> const& qualitativeResult, ExplicitGameStrategyPair const& minStrategyPair, ExplicitGameStrategyPair const& maxStrategyPair) const;
+            
             /*!
              * Refines the abstractor based on the quantitative result by trying to derive suitable predicates.
              *

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -391,30 +391,34 @@ namespace storm {
         }
         
         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& strategyPair) {
+        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& strategyPair, ExplicitQuantitativeResult<ValueType> const* startingQuantitativeResult = nullptr, ExplicitGameStrategyPair const* startingStrategyPair = nullptr) {
 
-            bool player1Min = player1Direction == storm::OptimizationDirection::Minimize;
             bool player2Min = player2Direction == storm::OptimizationDirection::Minimize;
-            auto const& player1Prob0States = player2Min ? qualitativeResult.getProb0Min().asExplicitQualitativeGameResult().getPlayer1States() : qualitativeResult.getProb0Max().asExplicitQualitativeGameResult().getPlayer1States();
             auto const& player1Prob1States = player2Min ? qualitativeResult.getProb1Min().asExplicitQualitativeGameResult().getPlayer1States() : qualitativeResult.getProb1Max().asExplicitQualitativeGameResult().getPlayer1States();
             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 row groups to keep.
-            storm::storage::BitVector player2MaybeStates = ~(player2Prob0States | player2Prob1States);
             
-            // Create the sub-game.
-            storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, player2MaybeStates, maybeStates);
-            std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(player2MaybeStates, player1Prob1States);
+            // If there are no maybe states, we construct the quantitative result from the qualitative result alone.
+            if (maybeStates.empty()) {
+                ExplicitQuantitativeResult<ValueType> result(maybeStates.size());
+                storm::utility::vector::setVectorValues(result.getValues(), player1Prob1States, storm::utility::one<ValueType>());
+                return result;
+            }
+            
+            // Otherwise, we need to solve a (sub)game.
+            
+            // Create the game by selecting all maybe player 2 states (non-prob0/1) of all maybe player 1 states.
             std::vector<uint64_t> subPlayer1Groups(maybeStates.getNumberOfSetBits() + 1);
             uint64_t position = 0;
             uint64_t previousPlayer2States = 0;
+            storm::storage::BitVector player2MaybeStates(transitionMatrix.getRowGroupCount());
             for (auto state : maybeStates) {
                 subPlayer1Groups[position] = previousPlayer2States;
                 
                 bool hasMaybePlayer2Successor = false;
                 for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) {
-                    if (player2MaybeStates.get(player2State)) {
+                    if (!player2Prob0States.get(player2State) && !player2Prob1States.get(player2State)) {
+                        player2MaybeStates.set(player2State);
                         hasMaybePlayer2Successor = true;
                         ++previousPlayer2States;
                     }
@@ -423,23 +427,57 @@ namespace storm {
                 ++position;
             }
             subPlayer1Groups.back() = previousPlayer2States;
-
-            // Solve the sub-game.
+            
+            // Create the player 2 matrix using the maybe player 2 states.
+            storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, player2MaybeStates, maybeStates);
+            std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(player2MaybeStates, player1Prob1States);
+            
+            // Set up game solver.
             auto gameSolver = storm::solver::GameSolverFactory<ValueType>().create(env, subPlayer1Groups, submatrix);
-            gameSolver->setTrackSchedulers(true);
-            std::vector<ValueType> lowerValues(maybeStates.getNumberOfSetBits());
-            gameSolver->solveGame(env, player1Direction, player2Direction, lowerValues, b);
+            
+            // Prepare the value storage for the maybe states. If the starting values were given, extract them now.
+            std::vector<ValueType> values(maybeStates.getNumberOfSetBits());
+            if (startingQuantitativeResult) {
+                storm::utility::vector::selectVectorValues(values, maybeStates, startingQuantitativeResult->getValues());
+            }
+            
+            // Prepare scheduler storage.
+            std::vector<uint64_t> player1Scheduler(subPlayer1Groups.size() - 1);
+            std::vector<uint64_t> player2Scheduler(submatrix.getRowGroupCount());
+            if (startingStrategyPair) {
+                // If the starting strategy pair was provided, we need to extract the choices of the maybe states here.
+                uint64_t maybeStatePosition = 0;
+                previousPlayer2States = 0;
+                for (auto state : maybeStates) {
+                    uint64_t chosenPlayer2State = startingStrategyPair->getPlayer1Strategy().getChoice(state);
+                    
+                    uint64_t previousPlayer2StatesForState = 0;
+                    for (uint64_t player2State = player1Groups[state]; player2State < player1Groups[state + 1]; ++player2State) {
+                        if (player2MaybeStates.get(player2State)) {
+                            if (player2State == chosenPlayer2State) {
+                                player1Scheduler[maybeStatePosition] = previousPlayer2StatesForState;
+                            }
+
+                            // Copy over the player 2 action (modulo making it local) as all rows for the state are taken.
+                            player2Scheduler[previousPlayer2States] = startingStrategyPair->getPlayer2Strategy().getChoice(player2State) - transitionMatrix.getRowGroupIndices()[player2State];
+                            
+                            ++previousPlayer2StatesForState;
+                            ++previousPlayer2States;
+                        }
+                    }
+                    
+                    ++maybeStatePosition;
+                }
+            }
+            
+            // Solve actual game and track schedulers.
+            gameSolver->solveGame(env, player1Direction, player2Direction, values, b, &player1Scheduler, &player2Scheduler);
             
             // Create combined result for all states.
             ExplicitQuantitativeResult<ValueType> result(maybeStates.size());
             storm::utility::vector::setVectorValues(result.getValues(), player1Prob1States, storm::utility::one<ValueType>());
-            storm::utility::vector::setVectorValues(result.getValues(), maybeStates, lowerValues);
-
-            STORM_LOG_ASSERT(gameSolver->hasSchedulers(), "Expected to have schedulers available after solving game.");
-            
-            std::vector<uint_fast64_t> const& player1Scheduler = gameSolver->getPlayer1SchedulerChoices();
-            std::vector<uint_fast64_t> const& player2Scheduler = gameSolver->getPlayer2SchedulerChoices();
-
+            storm::utility::vector::setVectorValues(result.getValues(), maybeStates, values);
+                        
             // Obtain strategies from solver and fuse them with the pre-existing strategy pair for the qualitative result.
             uint64_t previousPlayer1MaybeStates = 0;
             uint64_t previousPlayer2MaybeStates = 0;
@@ -650,6 +688,7 @@ namespace storm {
             STORM_LOG_TRACE("Using sparse solving.");
 
             // (0) Start by transforming the necessary symbolic elements to explicit ones.
+            auto translationStart = std::chrono::high_resolution_clock::now();
             storm::dd::Odd odd = game.getReachableStates().createOdd();
             
             std::vector<std::set<storm::expressions::Variable>> labelingVariableSets = {game.getPlayer1Variables(), game.getPlayer2Variables()};
@@ -701,6 +740,8 @@ namespace storm {
             storm::storage::BitVector initialStates = initialStatesBdd.toVector(odd);
             storm::storage::BitVector constraintStates = constraintStatesBdd.toVector(odd);
             storm::storage::BitVector targetStates = targetStatesBdd.toVector(odd);
+            auto translationEnd = std::chrono::high_resolution_clock::now();
+            STORM_LOG_DEBUG("Translation to explicit representation completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(translationEnd - translationStart).count() << "ms.");
 
             // Prepare the two strategies.
             abstraction::ExplicitGameStrategyPair minStrategyPair(initialStates.size(), transitionMatrix.getRowGroupCount());
@@ -715,12 +756,6 @@ namespace storm {
             }
             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.");
-
-//            std::cout << transitionMatrix << std::endl;
-//            std::cout << labeling.size() << std::endl;
-//            std::cout << initialStates << std::endl;
-//            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());
@@ -751,12 +786,10 @@ namespace storm {
             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;
 
                 // (7) Solve the min values and check whether we can give the answer already.
+                auto quantitativeStart = std::chrono::high_resolution_clock::now();
                 quantitativeResult.setMin(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Minimize, transitionMatrix, player1Groups, qualitativeResult, maybeMin, minStrategyPair));
                 result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.getMin().getRange(initialStates));
                 if (result) {
@@ -764,12 +797,11 @@ namespace storm {
                 }
 
                 // (8) Solve the max values and check whether we can give the answer already.
-                quantitativeResult.setMax(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, transitionMatrix, player1Groups, qualitativeResult, maybeMax, maxStrategyPair));
+                quantitativeResult.setMax(computeQuantitativeResult(env, player1Direction, storm::OptimizationDirection::Maximize, transitionMatrix, player1Groups, qualitativeResult, maybeMax, maxStrategyPair, &quantitativeResult.getMin(), &minStrategyPair));
                 result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.getMax().getRange(initialStates));
                 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.");
                 
@@ -780,15 +812,13 @@ namespace storm {
                 }
 
                 // Make sure that all strategies are still valid strategies.
-                STORM_LOG_ASSERT(minStrategyPair.getNumberOfUndefinedPlayer1States() == targetStates.getNumberOfSetBits() && minStrategyPair.getNumberOfUndefinedPlayer2States() == 0, "Minimal strategy pair has undefined choices for some relevant states.");
-                STORM_LOG_ASSERT(maxStrategyPair.getNumberOfUndefinedPlayer1States() == targetStates.getNumberOfSetBits() && maxStrategyPair.getNumberOfUndefinedPlayer2States() == 0, "Maximal strategy pair has undefined choices for some relevant states.");
-
-                exit(-1);
+                STORM_LOG_ASSERT(minStrategyPair.getNumberOfUndefinedPlayer1States() <= targetStates.getNumberOfSetBits(), "Expected at most " << targetStates.getNumberOfSetBits() << " (number of target states) player 1 states with undefined choice but got " << minStrategyPair.getNumberOfUndefinedPlayer1States() << ".");
+                STORM_LOG_ASSERT(maxStrategyPair.getNumberOfUndefinedPlayer1States() <= targetStates.getNumberOfSetBits(), "Expected at most " << targetStates.getNumberOfSetBits() << " (number of target states) player 1 states with undefined choice but got " << maxStrategyPair.getNumberOfUndefinedPlayer1States() << ".");
 
                 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);
+                // (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, odd, transitionMatrix, player1Groups, player1Labeling, player2Labeling, initialStates, constraintStates, targetStates, quantitativeResult, minStrategyPair, maxStrategyPair);
                 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.");
             }

src/storm/solver/GameSolver.h

@@ -39,8 +39,12 @@ namespace storm {
              * @param player2Dir Sets whether player 2 wants to minimize or maximize.
              * @param x The initial guess of the solution. For correctness, the guess has to be less (or equal) to the final solution (unless both players minimize)
              * @param b The vector to add after matrix-vector multiplication.
+             * @param player1Choices If provided along with the storage for player 2 choices, the scheduler decisions
+             * are tracked within these two vectors.
+             * @param player2Choices If provided along with the storage for player 1 choices, the scheduler decisions
+             * are tracked within these two vectors.
              */
-            virtual bool solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const = 0;
+            virtual bool solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint64_t>* player1Choices = nullptr, std::vector<uint64_t>* player2Choices = nullptr) const = 0;
             
             /*!
              * Performs (repeated) matrix-vector multiplication with the given parameters, i.e. computes

src/storm/solver/StandardGameSolver.cpp

@@ -57,12 +57,12 @@ namespace storm {
         }
         
         template<typename ValueType>
-        bool StandardGameSolver<ValueType>::solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
+        bool StandardGameSolver<ValueType>::solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint64_t>* player1Choices, std::vector<uint64_t>* player2Choices) const {
             switch (getMethod(env, std::is_same<ValueType, storm::RationalNumber>::value)) {
                 case GameMethod::ValueIteration:
-                    return solveGameValueIteration(env, player1Dir, player2Dir, x, b);
+                    return solveGameValueIteration(env, player1Dir, player2Dir, x, b, player1Choices, player2Choices);
                 case GameMethod::PolicyIteration:
-                    return solveGamePolicyIteration(env, player1Dir, player2Dir, x, b);
+                    return solveGamePolicyIteration(env, player1Dir, player2Dir, x, b, player1Choices, player2Choices);
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::InvalidEnvironmentException, "This solver does not implement the selected solution method");
             }
@@ -70,21 +70,39 @@ namespace storm {
         }
         
         template<typename ValueType>
-        bool StandardGameSolver<ValueType>::solveGamePolicyIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
+        bool StandardGameSolver<ValueType>::solveGamePolicyIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint64_t>* providedPlayer1Choices, std::vector<uint64_t>* providedPlayer2Choices) const {
             
             // Create the initial choice selections.
-            std::vector<storm::storage::sparse::state_type> player1Choices;
+            std::vector<storm::storage::sparse::state_type>* player1Choices;
+            std::unique_ptr<std::vector<storm::storage::sparse::state_type>> localPlayer1Choices;
+            std::vector<storm::storage::sparse::state_type>* player2Choices;
+            std::unique_ptr<std::vector<storm::storage::sparse::state_type>> localPlayer2Choices;
+
+            if (providedPlayer1Choices && providedPlayer2Choices) {
+                player1Choices = providedPlayer1Choices;
+                player2Choices = providedPlayer2Choices;
+            } else {
+                localPlayer1Choices = std::make_unique<std::vector<uint64_t>>();
+                player1Choices = localPlayer1Choices.get();
+                localPlayer2Choices = std::make_unique<std::vector<uint64_t>>();
+                player2Choices = localPlayer2Choices.get();
+            }
+            
             if (this->hasSchedulerHints()) {
-                player1Choices = this->player1ChoicesHint.get();
+                *player1Choices = this->player1ChoicesHint.get();
             } else if (this->player1RepresentedByMatrix()) {
                 // Player 1 represented by matrix.
-                player1Choices = std::vector<storm::storage::sparse::state_type>(this->getPlayer1Matrix().getRowGroupCount(), 0);
+                *player1Choices = std::vector<storm::storage::sparse::state_type>(this->getPlayer1Matrix().getRowGroupCount(), 0);
             } else {
                 // Player 1 represented by grouping of player 2 states.
-                player1Choices = this->getPlayer1Grouping();
-                player1Choices.resize(player1Choices.size() - 1);
+                *player1Choices = this->getPlayer1Grouping();
+                player1Choices->resize(player1Choices->size() - 1);
+            }
+            if (this->hasSchedulerHints()) {
+                *player2Choices = this->player2ChoicesHint.get();
+            } else if (!(providedPlayer1Choices && providedPlayer2Choices)) {
+                player2Choices->resize(this->player2Matrix.getRowGroupCount());
             }
-            std::vector<storm::storage::sparse::state_type> player2Choices = this->hasSchedulerHints() ? this->player2ChoicesHint.get() : std::vector<storm::storage::sparse::state_type>(this->player2Matrix.getRowGroupCount(), 0);
             
             if (!auxiliaryP2RowGroupVector) {
                 auxiliaryP2RowGroupVector = std::make_unique<std::vector<ValueType>>(this->player2Matrix.getRowGroupCount());
@@ -119,7 +137,7 @@ namespace storm {
             
             // Solve the equation system induced by the two schedulers.
             storm::storage::SparseMatrix<ValueType> submatrix;
-            getInducedMatrixVector(x, b, player1Choices, player2Choices, submatrix, subB);
+            getInducedMatrixVector(x, b, *player1Choices, *player2Choices, submatrix, subB);
             if (this->linearEquationSolverFactory->getEquationProblemFormat(environmentOfSolver) == LinearEquationSolverProblemFormat::EquationSystem) {
                 submatrix.convertToEquationSystem();
             }
@@ -140,14 +158,14 @@ namespace storm {
                 // FIXME: we need to remove the 0- and 1- states to make the solution unique.
                 submatrixSolver->solveEquations(environmentOfSolver, x, subB);
                 
-                bool schedulerImproved = extractChoices(player1Dir, player2Dir, x, b, *auxiliaryP2RowGroupVector, player1Choices, player2Choices);
+                bool schedulerImproved = extractChoices(player1Dir, player2Dir, x, b, *auxiliaryP2RowGroupVector, *player1Choices, *player2Choices);
                 
                 // If the scheduler did not improve, we are done.
                 if (!schedulerImproved) {
                     status = Status::Converged;
                 } else {
                     // Update the solver.
-                    getInducedMatrixVector(x, b, player1Choices, player2Choices, submatrix, subB);
+                    getInducedMatrixVector(x, b, *player1Choices, *player2Choices, submatrix, subB);
                     submatrix.convertToEquationSystem();
                     submatrixSolver->setMatrix(std::move(submatrix));
                 }
@@ -160,9 +178,9 @@ namespace storm {
             reportStatus(status, iterations);
             
             // If requested, we store the scheduler for retrieval.
-            if (this->isTrackSchedulersSet()) {
-                this->player1SchedulerChoices = std::move(player1Choices);
-                this->player2SchedulerChoices = std::move(player2Choices);
+            if (this->isTrackSchedulersSet() && !(providedPlayer1Choices && providedPlayer2Choices)) {
+                this->player1SchedulerChoices = std::move(*player1Choices);
+                this->player2SchedulerChoices = std::move(*player2Choices);
             }
             
             if (!this->isCachingEnabled()) {
@@ -182,7 +200,7 @@ namespace storm {
         }
 
         template<typename ValueType>
-        bool StandardGameSolver<ValueType>::solveGameValueIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
+        bool StandardGameSolver<ValueType>::solveGameValueIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint64_t>* player1Choices, std::vector<uint64_t>* player2Choices) const {
                          
             if (!multiplierPlayer2Matrix) {
                 multiplierPlayer2Matrix = storm::solver::MultiplierFactory<ValueType>().create(env, player2Matrix);
@@ -202,7 +220,9 @@ namespace storm {
             
             std::vector<ValueType>& reducedPlayer2Result = *auxiliaryP2RowGroupVector;
             
-            bool trackSchedulersInValueIteration = this->isTrackSchedulersSet() && !this->hasUniqueSolution();
+            bool trackingSchedulersInProvidedStorage = player1Choices && player2Choices;
+            bool trackSchedulers = this->isTrackSchedulersSet() || trackingSchedulersInProvidedStorage;
+            bool trackSchedulersInValueIteration = trackSchedulers && !this->hasUniqueSolution();
             if (this->hasSchedulerHints()) {
                 // Solve the equation system induced by the two schedulers.
                 storm::storage::SparseMatrix<ValueType> submatrix;
@@ -221,11 +241,11 @@ namespace storm {
                 submatrixSolver->solveEquations(env, x, *auxiliaryP1RowGroupVector);
                 
                 // If requested, we store the scheduler for retrieval. Initialize the schedulers to the hint we have.
-                if (trackSchedulersInValueIteration) {
+                if (trackSchedulersInValueIteration && !trackingSchedulersInProvidedStorage) {
                     this->player1SchedulerChoices = this->player1ChoicesHint.get();
                     this->player2SchedulerChoices = this->player2ChoicesHint.get();
                 }
-            } else if (trackSchedulersInValueIteration) {
+            } else if (trackSchedulersInValueIteration && !trackingSchedulersInProvidedStorage) {
                 // If requested, we store the scheduler for retrieval. Create empty schedulers here so we can fill them
                 // during VI.
                 this->player1SchedulerChoices = std::vector<uint_fast64_t>(this->getNumberOfPlayer1States(), 0);
@@ -240,7 +260,9 @@ namespace storm {
 
             Status status = Status::InProgress;
             while (status == Status::InProgress) {
-                multiplyAndReduce(env, player1Dir, player2Dir, *currentX, &b, *multiplierPlayer2Matrix, reducedPlayer2Result, *newX, trackSchedulersInValueIteration ? &this->player1SchedulerChoices.get() : nullptr, trackSchedulersInValueIteration ? &this->player2SchedulerChoices.get() : nullptr);
+                multiplyAndReduce(env, player1Dir, player2Dir, *currentX, &b, *multiplierPlayer2Matrix, reducedPlayer2Result, *newX,
+                                  trackSchedulersInValueIteration ? (trackingSchedulersInProvidedStorage ? player1Choices : &this->player1SchedulerChoices.get()) : nullptr,
+                                  trackSchedulersInValueIteration ? (trackingSchedulersInProvidedStorage ? player2Choices : &this->player2SchedulerChoices.get()) : nullptr);
 
                 // Determine whether the method converged.
                 if (storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, precision, relative)) {
@@ -262,10 +284,14 @@ namespace storm {
             }
             
             // If requested, we store the scheduler for retrieval.
-            if (this->isTrackSchedulersSet() && this->hasUniqueSolution()) {
-                this->player1SchedulerChoices = std::vector<uint_fast64_t>(this->getNumberOfPlayer1States(), 0);
-                this->player2SchedulerChoices = std::vector<uint_fast64_t>(this->getNumberOfPlayer2States(), 0);
-                extractChoices(player1Dir, player2Dir, x, b, *auxiliaryP2RowGroupVector, this->player1SchedulerChoices.get(), this->player2SchedulerChoices.get());
+            if (trackSchedulers && this->hasUniqueSolution()) {
+                if (trackingSchedulersInProvidedStorage) {
+                    extractChoices(player1Dir, player2Dir, x, b, *auxiliaryP2RowGroupVector, *player1Choices, *player2Choices);
+                } else {
+                    this->player1SchedulerChoices = std::vector<uint_fast64_t>(this->getNumberOfPlayer1States(), 0);
+                    this->player2SchedulerChoices = std::vector<uint_fast64_t>(this->getNumberOfPlayer2States(), 0);
+                    extractChoices(player1Dir, player2Dir, x, b, *auxiliaryP2RowGroupVector, this->player1SchedulerChoices.get(), this->player2SchedulerChoices.get());
+                }
             }
             
             if (!this->isCachingEnabled()) {

src/storm/solver/StandardGameSolver.h

@@ -19,7 +19,7 @@ namespace storm {
             StandardGameSolver(std::vector<uint64_t> const& player1Groups, storm::storage::SparseMatrix<ValueType> const& player2Matrix, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
             StandardGameSolver(std::vector<uint64_t>&& player1Groups, storm::storage::SparseMatrix<ValueType>&& player2Matrix, std::unique_ptr<LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
             
-            virtual bool solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
+            virtual bool solveGame(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint64_t>* player1Choices = nullptr, std::vector<uint64_t>* player2Choices = nullptr) const override;
             virtual void repeatedMultiply(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint_fast64_t n = 1) const override;
 
             virtual void clearCache() const override;
@@ -27,8 +27,8 @@ namespace storm {
         private:
             GameMethod getMethod(Environment const& env, bool isExactMode) const;
             
-            bool solveGamePolicyIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
-            bool solveGameValueIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;
+            bool solveGamePolicyIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint64_t>* player1Choices = nullptr, std::vector<uint64_t>* player2Choices = nullptr) const;
+            bool solveGameValueIteration(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<uint64_t>* player1Choices = nullptr, std::vector<uint64_t>* player2Choices = nullptr) const;
 
             // Computes p2Matrix * x + b, reduces the result w.r.t. player 2 choices, and then reduces the result w.r.t. player 1 choices.
             void multiplyAndReduce(Environment const& env, OptimizationDirection player1Dir, OptimizationDirection player2Dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, storm::solver::Multiplier<ValueType> const& multiplier, std::vector<ValueType>& player2ReducedResult, std::vector<ValueType>& player1ReducedResult, std::vector<uint64_t>* player1SchedulerChoices = nullptr, std::vector<uint64_t>* player2SchedulerChoices = nullptr) const;

src/storm/utility/graph.cpp

@@ -1395,7 +1395,7 @@ namespace storm {
                         
                         // If we were asked to produce strategies, we propagate that by triggering another iteration.
                         // We only do this if at least one strategy will be produced.
-                        produceStrategiesInIteration = !produceStrategiesInIteration && ((player1Strategy && player1Direction == OptimizationDirection::Maximize) || (player2Strategy && player2Direction == OptimizationDirection::Maximize));
+                        produceStrategiesInIteration = !produceStrategiesInIteration && (player1Strategy || player2Strategy);
                     } else {
                         result.player1States = player1Solution;
                         result.player2States = player2Solution;