Merge remote-tracking branch 'remotes/origin/menu_games' into sylvanRationalFunctions

# Conflicts:
#	src/abstraction/MenuGame.cpp


Former-commit-id: 7cc51da103

resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c

@@ -542,15 +542,12 @@ cuddBddExistAbstractRepresentativeRecur(
         if (cube == one) {
 //            printf("return in preprocessing...\n");
             return one;
-        } else {
-//            printf("return in preprocessing...\n");
-            return cube;
         }
     } else if (cube == one) {
 //        printf("return in preprocessing...\n");
         return f;
     }
-    /* From now on, f and cube are non-constant. */
+    /* From now on, cube is non-constant, but f might be constant. */
     
 //    printf("F perm %i and cube perm %i\n", manager->perm[F->index], manager->perm[cube->index]);
     
@@ -591,27 +588,10 @@ cuddBddExistAbstractRepresentativeRecur(
     
     /* If the two indices are the same, so are their levels. */
     if (F->index == cube->index) {
-//        if (E == one) {
-//            cuddRef(zero);
-//            cuddRef(cuddT(cube));
-//            res1 = cuddUniqueInter(manager, (int) F->index, zero, cuddT(cube));
-//            cuddDeref(zero);
-//            cuddDeref(cuddT(cube));
-//            return res1;
-//        } else if (T == one) {
-//            cuddRef(zero);
-//            cuddRef(cuddT(cube));
-//            res1 = cuddUniqueInter(manager, (int) F->index, cuddT(cube), zero);
-//            cuddDeref(zero);
-//            cuddDeref(cuddT(cube));
-//            return res1;
-//        }
-        
         res1 = cuddBddExistAbstractRepresentativeRecur(manager, E, cuddT(cube));
         if (res1 == NULL) {
             return(NULL);
         }
-        // FIXME
         if (res1 == one) {
             if (F->ref != 1) {
                 cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, Cudd_Not(cube));

src/abstraction/AbstractionInformation.cpp

@@ -57,6 +57,7 @@ namespace storm {
             allPredicateIdentities &= predicateIdentities.back();
             sourceVariables.insert(newMetaVariable.first);
             successorVariables.insert(newMetaVariable.second);
+            orderedSuccessorVariables.push_back(newMetaVariable.second);
             ddVariableIndexToPredicateIndexMap[predicateIdentities.back().getIndex()] = predicateIndex;
             return predicateIndex;
         }
@@ -122,6 +123,11 @@ namespace storm {
             return predicateBdds[indexIt->second].first;
         }
         
+        template<storm::dd::DdType DdType>
+        bool AbstractionInformation<DdType>::hasPredicate(storm::expressions::Expression const& predicate) const {
+            return predicateToIndexMap.find(predicate) != predicateToIndexMap.end();
+        }
+
         template<storm::dd::DdType DdType>
         std::size_t AbstractionInformation<DdType>::getNumberOfPredicates() const {
             return predicates.size();
@@ -167,16 +173,31 @@ namespace storm {
             return encodeChoice(index, 0, end, player1VariableBdds);
         }
         
+        template<storm::dd::DdType DdType>
+        uint_fast64_t AbstractionInformation<DdType>::decodePlayer1Choice(storm::expressions::Valuation const& valuation, uint_fast64_t end) const {
+            return decodeChoice(valuation, 0, end, player1Variables);
+        }
+        
         template<storm::dd::DdType DdType>
         storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodePlayer2Choice(uint_fast64_t index, uint_fast64_t end) const {
             return encodeChoice(index, 0, end, player2VariableBdds);
         }
-        
+
+        template<storm::dd::DdType DdType>
+        uint_fast64_t AbstractionInformation<DdType>::decodePlayer2Choice(storm::expressions::Valuation const& valuation, uint_fast64_t end) const {
+            return decodeChoice(valuation, 0, end, player2Variables);
+        }
+
         template<storm::dd::DdType DdType>
         storm::dd::Bdd<DdType> AbstractionInformation<DdType>::encodeAux(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end) const {
             return encodeChoice(index, start, end, auxVariableBdds);
         }
         
+        template<storm::dd::DdType DdType>
+        uint_fast64_t AbstractionInformation<DdType>::decodeAux(storm::expressions::Valuation const& valuation, uint_fast64_t start, uint_fast64_t end) const {
+            return decodeChoice(valuation, start, end, auxVariables);
+        }
+
         template<storm::dd::DdType DdType>
         storm::dd::Bdd<DdType> AbstractionInformation<DdType>::getPlayer2ZeroCube(uint_fast64_t start, uint_fast64_t end) const {
             storm::dd::Bdd<DdType> result = ddManager->getBddOne();
@@ -232,6 +253,11 @@ namespace storm {
             return successorVariables;
         }
         
+        template<storm::dd::DdType DdType>
+        std::vector<storm::expressions::Variable> const& AbstractionInformation<DdType>::getOrderedSuccessorVariables() const {
+            return orderedSuccessorVariables;
+        }
+        
         template<storm::dd::DdType DdType>
         storm::dd::Bdd<DdType> const& AbstractionInformation<DdType>::getAllPredicateIdentities() const {
             return allPredicateIdentities;
@@ -356,6 +382,18 @@ namespace storm {
             return result;
         }
         
+        template<storm::dd::DdType DdType>
+        uint_fast64_t AbstractionInformation<DdType>::decodeChoice(storm::expressions::Valuation const& valuation, uint_fast64_t start, uint_fast64_t end, std::vector<storm::expressions::Variable> const& variables) const {
+            uint_fast64_t result = 0;
+            for (uint_fast64_t variableIndex = start; variableIndex < end; ++variableIndex) {
+                result <<= 1;
+                if (valuation.getBooleanValue(variables[variableIndex])) {
+                    result |= 1;
+                }
+            }
+            return result;
+        }
+        
         template class AbstractionInformation<storm::dd::DdType::CUDD>;
         template class AbstractionInformation<storm::dd::DdType::Sylvan>;
     }

src/abstraction/AbstractionInformation.h

@@ -148,6 +148,13 @@ namespace storm {
              */
             storm::dd::Bdd<DdType> getPredicateSourceVariable(storm::expressions::Expression const& predicate) const;
             
+            /*!
+             * Determines whether the given predicate is in the set of known predicates.
+             *
+             * @param predicate The predicate for which to query membership.
+             */
+            bool hasPredicate(storm::expressions::Expression const& predicate) const;
+            
             /*!
              * Retrieves the number of predicates.
              *
@@ -180,6 +187,15 @@ namespace storm {
              */
             storm::dd::Bdd<DdType> encodePlayer1Choice(uint_fast64_t index, uint_fast64_t end) const;
             
+            /*!
+             * Decodes the player 1 choice in the given valuation.
+             *
+             * @param valuation The valuation to decode.
+             * @param end The index of the variable past the end of the range that is used to encode the index.
+             * @return The decoded player 1 choice.
+             */
+            uint_fast64_t decodePlayer1Choice(storm::expressions::Valuation const& valuation, uint_fast64_t end) const;
+            
             /*!
              * Encodes the given index using the indicated player 2 variables.
              *
@@ -190,7 +206,16 @@ namespace storm {
             storm::dd::Bdd<DdType> encodePlayer2Choice(uint_fast64_t index, uint_fast64_t end) const;
 
             /*!
-             * Encodes the given index using the indicated probabilistic branching variables.
+             * Decodes the player 2 choice in the given valuation.
+             *
+             * @param valuation The valuation to decode.
+             * @param end The index of the variable past the end of the range that is used to encode the index.
+             * @return The decoded player 2 choice.
+             */
+            uint_fast64_t decodePlayer2Choice(storm::expressions::Valuation const& valuation, uint_fast64_t end) const;
+            
+            /*!
+             * Encodes the given index using the indicated auxiliary variables.
              *
              * @param index The index to encode.
              * @param start The index of the first variable of the range that is used to encode the index.
@@ -199,6 +224,16 @@ namespace storm {
              */
             storm::dd::Bdd<DdType> encodeAux(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end) const;
             
+            /*!
+             * Decodes the auxiliary index in the given valuation.
+             *
+             * @param valuation The valuation to decode.
+             * @param start The index of the first variable of the range that is used to encode the index.
+             * @param end The index of the variable past the end of the range that is used to encode the index.
+             * @return The decoded auxiliary index.
+             */
+            uint_fast64_t decodeAux(storm::expressions::Valuation const& valuation, uint_fast64_t start, uint_fast64_t end) const;
+
             /*!
              * Retrieves the cube of player 2 variables in the given range [offset, numberOfVariables).
              *
@@ -298,6 +333,13 @@ namespace storm {
              */
             std::set<storm::expressions::Variable> const& getSuccessorVariables() const;
 
+            /*!
+             * Retrieves the ordered collection of successor meta variables.
+             *
+             * @return All successor meta variables.
+             */
+            std::vector<storm::expressions::Variable> const& getOrderedSuccessorVariables() const;
+            
             /*!
              * Retrieves a BDD representing the identities of all predicates.
              *
@@ -392,16 +434,27 @@ namespace storm {
              * @param start The index of the first variable to use for the encoding.
              * @param end The index of the variable past the end of the range to use for the encoding.
              * @param variables The BDDs of the variables to use to encode the index.
+             * @return The BDD encoding the index.
              */
             storm::dd::Bdd<DdType> encodeChoice(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end, std::vector<storm::dd::Bdd<DdType>> const& variables) const;
-                        
+
+            /*!
+             * Decodes the index encoded in the valuation using the given variables.
+             *
+             * @param valuation The valuation to decode.
+             * @param start The index of the first variable to use for the encoding.
+             * @param end The index of the variable past the end of the range to use for the encoding.
+             * @param variables The variables used to encode the index.
+             * @return The encoded index.
+             */
+            uint_fast64_t decodeChoice(storm::expressions::Valuation const& valuation, uint_fast64_t start, uint_fast64_t end, std::vector<storm::expressions::Variable> const& variables) const;
+
             // The expression related data.
             
             /// The manager responsible for the expressions of the program and the SMT solvers.
             std::reference_wrapper<storm::expressions::ExpressionManager> expressionManager;
             
             /// A mapping from predicates to their indices in the predicate list.
-            // FIXME: Does this properly store the expressions? What about equality checking?
             std::unordered_map<storm::expressions::Expression, uint64_t> predicateToIndexMap;
             
             /// The current set of predicates used in the abstraction.
@@ -427,9 +480,12 @@ namespace storm {
             /// The set of all source variables.
             std::set<storm::expressions::Variable> sourceVariables;
             
-            /// The set of all source variables.
+            /// The set of all successor variables.
             std::set<storm::expressions::Variable> successorVariables;
             
+            /// An ordered collection of the successor variables.
+            std::vector<storm::expressions::Variable> orderedSuccessorVariables;
+            
             /// The BDDs corresponding to the predicates.
             std::vector<std::pair<storm::dd::Bdd<DdType>, storm::dd::Bdd<DdType>>> predicateBdds;
             

src/abstraction/MenuGame.cpp

@@ -29,7 +29,7 @@ namespace storm {
                                             std::set<storm::expressions::Variable> const& player2Variables,
                                             std::set<storm::expressions::Variable> const& allNondeterminismVariables,
                                             std::set<storm::expressions::Variable> const& probabilisticBranchingVariables,
-                                            std::map<storm::expressions::Expression, storm::dd::Bdd<Type>> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType>(manager, reachableStates, initialStates, deadlockStates, transitionMatrix.sumAbstract(probabilisticBranchingVariables), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), probabilisticBranchingVariables(probabilisticBranchingVariables), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) {
+                                            std::map<storm::expressions::Expression, storm::dd::Bdd<Type>> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType>(manager, reachableStates, initialStates, deadlockStates, transitionMatrix.sumAbstract(probabilisticBranchingVariables), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), extendedTransitionMatrix(transitionMatrix), probabilisticBranchingVariables(probabilisticBranchingVariables), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) {
             // Intentionally left empty.
         }
         
@@ -64,6 +64,16 @@ namespace storm {
             return bottomStates;
         }
         
+        template<storm::dd::DdType Type, typename ValueType>
+        storm::dd::Add<Type, ValueType> const& MenuGame<Type, ValueType>::getExtendedTransitionMatrix() const {
+            return extendedTransitionMatrix;
+        }
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        std::set<storm::expressions::Variable> const& MenuGame<Type, ValueType>::getProbabilisticBranchingVariables() const {
+            return probabilisticBranchingVariables;
+        }
+        
         template<storm::dd::DdType Type, typename ValueType>
         bool MenuGame<Type, ValueType>::hasLabel(std::string const& label) const {
             return false;

src/abstraction/MenuGame.h

@@ -84,9 +84,28 @@ namespace storm {
                  */
                 storm::dd::Bdd<Type> getBottomStates() const;
                 
+                /*!
+                 * Retrieves the transition matrix extended by variables that encode additional information for the
+                 * probabilistic branching.
+                 *
+                 * @reutrn Th extended transition matrix.
+                 */
+                storm::dd::Add<Type, ValueType> const& getExtendedTransitionMatrix() const;
+                
+                /*!
+                 * Retrieves the variables used to encode additional information for the probabilistic branching in the
+                 * extended transition matrix.
+                 *
+                 * @return The probabilistic branching variables.
+                 */
+                std::set<storm::expressions::Variable> const& getProbabilisticBranchingVariables() const;
+                
                 virtual bool hasLabel(std::string const& label) const override;
                 
             private:
+                // The transition relation extended byt the probabilistic branching variables.
+                storm::dd::Add<Type, ValueType> extendedTransitionMatrix;
+                
                 // The meta variables used to probabilistic branching.
                 std::set<storm::expressions::Variable> probabilisticBranchingVariables;
                 

src/abstraction/MenuGameAbstractor.h

@@ -12,6 +12,7 @@ namespace storm {
         public:
             virtual storm::abstraction::MenuGame<DdType, ValueType> abstract() = 0;
             virtual void refine(std::vector<storm::expressions::Expression> const& predicates) = 0;
+            virtual void refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice) = 0;
         };
         
     }

src/abstraction/prism/AbstractCommand.cpp

@@ -340,6 +340,16 @@ namespace storm {
                 return result;
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::prism::Command const& AbstractCommand<DdType, ValueType>::getConcreteCommand() const {
+                return command.get();
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void AbstractCommand<DdType, ValueType>::notifyGuardIsPredicate() {
+                guardIsPredicate = true;
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             AbstractionInformation<DdType> const& AbstractCommand<DdType, ValueType>::getAbstractionInformation() const {
                 return abstractionInformation.get();

src/abstraction/prism/AbstractCommand.h

@@ -92,6 +92,19 @@ namespace storm {
                  */
                 storm::dd::Add<DdType, ValueType> getCommandUpdateProbabilitiesAdd() const;
                 
+                /*!
+                 * Retrieves the concrete command that is abstracted by this abstract command.
+                 *
+                 * @return The concrete command.
+                 */
+                storm::prism::Command const& getConcreteCommand() const;
+                
+                /*!
+                 * Notifies this abstract command that its guard is now a predicate. This affects the computation of the
+                 * bottom states.
+                 */
+                void notifyGuardIsPredicate();
+                
             private:
                 /*!
                  * Determines the relevant predicates for source as well as successor states wrt. to the given assignments

src/abstraction/prism/AbstractModule.cpp

@@ -75,6 +75,16 @@ namespace storm {
                 return result;
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::vector<AbstractCommand<DdType, ValueType>> const& AbstractModule<DdType, ValueType>::getCommands() const {
+                return commands;
+            }
+
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::vector<AbstractCommand<DdType, ValueType>>& AbstractModule<DdType, ValueType>::getCommands() {
+                return commands;
+            }
+
             template <storm::dd::DdType DdType, typename ValueType>
             AbstractionInformation<DdType> const& AbstractModule<DdType, ValueType>::getAbstractionInformation() const {
                 return abstractionInformation.get();

src/abstraction/prism/AbstractModule.h

@@ -73,6 +73,20 @@ namespace storm {
                  */
                 storm::dd::Add<DdType, ValueType> getCommandUpdateProbabilitiesAdd() const;
                 
+                /*!
+                 * Retrieves the abstract commands of this abstract module.
+                 *
+                 * @return The abstract commands.
+                 */
+                std::vector<AbstractCommand<DdType, ValueType>> const& getCommands() const;
+
+                /*!
+                 * Retrieves the abstract commands of this abstract module.
+                 *
+                 * @return The abstract commands.
+                 */
+                std::vector<AbstractCommand<DdType, ValueType>>& getCommands();
+
             private:
                 /*!
                  * Retrieves the abstraction information.

src/abstraction/prism/AbstractProgram.cpp

@@ -2,6 +2,8 @@
 
 #include "src/abstraction/BottomStateResult.h"
 
+#include "src/storage/BitVector.h"
+
 #include "src/storage/prism/Program.h"
 
 #include "src/storage/dd/DdManager.h"
@@ -9,6 +11,7 @@
 
 #include "src/models/symbolic/StandardRewardModel.h"
 
+#include "src/utility/dd.h"
 #include "src/utility/macros.h"
 #include "src/utility/solver.h"
 #include "src/exceptions/WrongFormatException.h"
@@ -111,6 +114,83 @@ namespace storm {
                 currentGame = buildGame();
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::map<uint_fast64_t, storm::storage::BitVector> AbstractProgram<DdType, ValueType>::decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const {
+                std::map<uint_fast64_t, storm::storage::BitVector> result;
+                
+                storm::dd::Add<DdType, ValueType> lowerChoiceAsAdd = choice.template toAdd<ValueType>();
+                for (auto const& successorValuePair : lowerChoiceAsAdd) {
+                    uint_fast64_t updateIndex = abstractionInformation.decodeAux(successorValuePair.first, 0, currentGame->getProbabilisticBranchingVariables().size());
+                    
+                    storm::storage::BitVector successor(abstractionInformation.getNumberOfPredicates());
+                    for (uint_fast64_t index = 0; index < abstractionInformation.getOrderedSuccessorVariables().size(); ++index) {
+                        auto const& successorVariable = abstractionInformation.getOrderedSuccessorVariables()[index];
+                        if (successorValuePair.first.getBooleanValue(successorVariable)) {
+                            successor.set(index);
+                        }
+                    }
+                    
+                    result[updateIndex] = successor;
+                }
+                return result;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void AbstractProgram<DdType, ValueType>::refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice) {
+                // Decode the index of the command chosen by player 1.
+                storm::dd::Add<DdType, ValueType> player1ChoiceAsAdd = player1Choice.template toAdd<ValueType>();
+                auto pl1It = player1ChoiceAsAdd.begin();
+                uint_fast64_t commandIndex = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount());
+                storm::abstraction::prism::AbstractCommand<DdType, ValueType>& abstractCommand = modules.front().getCommands()[commandIndex];
+                storm::prism::Command const& concreteCommand = abstractCommand.getConcreteCommand();
+
+                // Check whether there are bottom states in the game and whether one of the choices actually picks the
+                // bottom state as the successor.
+                bool buttomStateSuccessor = false;
+                if (!currentGame->getBottomStates().isZero()) {
+                    buttomStateSuccessor = !((abstractionInformation.getBottomStateBdd(false, false) && lowerChoice) || (abstractionInformation.getBottomStateBdd(false, false) && upperChoice)).isZero();
+                }
+                
+                // If one of the choices picks the bottom state, the new predicate is based on the guard of the appropriate
+                // command (that is the player 1 choice).
+                if (buttomStateSuccessor) {
+                    STORM_LOG_DEBUG("One of the successors is a bottom state, taking a guard as a new predicate.");
+                    abstractCommand.notifyGuardIsPredicate();
+                    storm::expressions::Expression newPredicate = concreteCommand.getGuardExpression();
+                    STORM_LOG_DEBUG("Derived new predicate: " << newPredicate);
+                    this->refine({newPredicate});
+                } else {
+                    STORM_LOG_DEBUG("No bottom state successor. Deriving a new predicate using weakest precondition.");
+                    
+                    // Decode both choices to explicit mappings.
+                    std::map<uint_fast64_t, storm::storage::BitVector> lowerChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(lowerChoice);
+                    std::map<uint_fast64_t, storm::storage::BitVector> upperChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(upperChoice);
+                    STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode.");
+
+                    // Now go through the mappings and find points of deviation. Currently, we take the first deviation.
+                    storm::expressions::Expression newPredicate;
+                    auto lowerIt = lowerChoiceUpdateToSuccessorMapping.begin();
+                    auto lowerIte = lowerChoiceUpdateToSuccessorMapping.end();
+                    auto upperIt = upperChoiceUpdateToSuccessorMapping.begin();
+                    for (; lowerIt != lowerIte; ++lowerIt, ++upperIt) {
+                        STORM_LOG_ASSERT(lowerIt->first == upperIt->first, "Update indices mismatch.");
+                        uint_fast64_t updateIndex = lowerIt->first;
+                        bool deviates = lowerIt->second != upperIt->second;
+                        if (deviates) {
+                            for (uint_fast64_t predicateIndex = 0; predicateIndex < lowerIt->second.size(); ++predicateIndex) {
+                                if (lowerIt->second.get(predicateIndex) != upperIt->second.get(predicateIndex)) {
+                                    // Now we know the point of the deviation (command, update, predicate).
+                                    newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap());
+                                    break;
+                                }
+                            }
+                        }
+                    }
+                    
+                    this->refine({newPredicate});
+                }
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             MenuGame<DdType, ValueType> AbstractProgram<DdType, ValueType>::getAbstractGame() {
                 STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created.");
@@ -138,7 +218,7 @@ namespace storm {
                 // Do a reachability analysis on the raw transition relation.
                 storm::dd::Bdd<DdType> transitionRelation = game.bdd.existsAbstract(variablesToAbstract);
                 storm::dd::Bdd<DdType> initialStates = initialStateAbstractor.getAbstractStates();
-                storm::dd::Bdd<DdType> reachableStates = this->getReachableStates(initialStates, transitionRelation);
+                storm::dd::Bdd<DdType> reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
                 
                 // Find the deadlock states in the model. Note that this does not find the 'deadlocks' in bottom states,
                 // as the bottom states are not contained in the reachable states.
@@ -167,6 +247,7 @@ namespace storm {
                     transitionMatrix *= (abstractionInformation.getBottomStateBdd(true, true) && abstractionInformation.getBottomStateBdd(false, true)).template toAdd<ValueType>();
                     transitionMatrix += bottomStateResult.transitions.template toAdd<ValueType>();
                     reachableStates &= abstractionInformation.getBottomStateBdd(true, true);
+                    initialStates &= abstractionInformation.getBottomStateBdd(true, true);
                     reachableStates |= bottomStateResult.states;
                 }
             
@@ -186,25 +267,7 @@ namespace storm {
                 
                 return std::make_unique<MenuGame<DdType, ValueType>>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, hasBottomStates ? abstractionInformation.getExtendedSourceSuccessorVariablePairs() : abstractionInformation.getSourceSuccessorVariablePairs(), std::set<storm::expressions::Variable>(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap());
             }
-            
-            template <storm::dd::DdType DdType, typename ValueType>
-            storm::dd::Bdd<DdType> AbstractProgram<DdType, ValueType>::getReachableStates(storm::dd::Bdd<DdType> const& initialStates, storm::dd::Bdd<DdType> const& transitionRelation) {
-                storm::dd::Bdd<DdType> frontier = initialStates;
-
-                storm::dd::Bdd<DdType> reachableStates = initialStates;
-                uint_fast64_t reachabilityIteration = 0;
-                while (!frontier.isZero()) {
-                    ++reachabilityIteration;
-                    frontier = frontier.andExists(transitionRelation, abstractionInformation.getSourceVariables());
-                    frontier = frontier.swapVariables(abstractionInformation.getSourceSuccessorVariablePairs());
-                    frontier &= !reachableStates;
-                    reachableStates |= frontier;
-                    STORM_LOG_TRACE("Iteration " << reachabilityIteration << " of reachability analysis.");
-                }
-                
-                return reachableStates;
-            }
-            
+                        
             template <storm::dd::DdType DdType, typename ValueType>
             void AbstractProgram<DdType, ValueType>::exportToDot(std::string const& filename) const {
                 std::ofstream out(filename);
@@ -244,13 +307,7 @@ namespace storm {
                             stateName << "0";
                         }
                     }
-                    uint_fast64_t index = 0;
-                    for (uint_fast64_t player1VariableIndex = 0; player1VariableIndex < abstractionInformation.getPlayer1VariableCount(); ++player1VariableIndex) {
-                        index <<= 1;
-                        if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer1Variables()[player1VariableIndex])) {
-                            index |= 1;
-                        }
-                    }
+                    uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount());
                     out << stateName.str() << "_" << index;
                     out << " [ shape=\"square\", width=0, height=0, margin=0, label=\"" << index << "\" ];" << std::endl;
                     out << "\tpl1_" << stateName.str() << " -> " << "pl2_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl;
@@ -268,21 +325,9 @@ namespace storm {
                             stateName << "0";
                         }
                     }
-                    uint_fast64_t index = 0;
-                    for (uint_fast64_t player1VariableIndex = 0; player1VariableIndex < abstractionInformation.getPlayer1VariableCount(); ++player1VariableIndex) {
-                        index <<= 1;
-                        if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer1Variables()[player1VariableIndex])) {
-                            index |= 1;
-                        }
-                    }
+                    uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount());
                     stateName << "_" << index;
-                    index = 0;
-                    for (uint_fast64_t player2VariableIndex = 0; player2VariableIndex < currentGame->getPlayer2Variables().size(); ++player2VariableIndex) {
-                        index <<= 1;
-                        if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer2Variables()[player2VariableIndex])) {
-                            index |= 1;
-                        }
-                    }
+                    index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size());
                     out << stateName.str() << "_" << index;
                     out << " [ shape=\"point\", label=\"\" ];" << std::endl;
                     out << "\tpl2_" << stateName.str() << " -> " << "plp_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl;
@@ -305,20 +350,8 @@ namespace storm {
                             successorStateName << "0";
                         }
                     }
-                    uint_fast64_t pl1Index = 0;
-                    for (uint_fast64_t player1VariableIndex = 0; player1VariableIndex < abstractionInformation.getPlayer1VariableCount(); ++player1VariableIndex) {
-                        pl1Index <<= 1;
-                        if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer1Variables()[player1VariableIndex])) {
-                            pl1Index |= 1;
-                        }
-                    }
-                    uint_fast64_t pl2Index = 0;
-                    for (uint_fast64_t player2VariableIndex = 0; player2VariableIndex < currentGame->getPlayer2Variables().size(); ++player2VariableIndex) {
-                        pl2Index <<= 1;
-                        if (stateValue.first.getBooleanValue(abstractionInformation.getPlayer2Variables()[player2VariableIndex])) {
-                            pl2Index |= 1;
-                        }
-                    }
+                    uint_fast64_t pl1Index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount());
+                    uint_fast64_t pl2Index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size());
                     out << "\tplp_" << sourceStateName.str() << "_" << pl1Index << "_" << pl2Index << " -> pl1_" << successorStateName.str() << " [ label=\"" << stateValue.second << "\"];" << std::endl;
                 }
                 

src/abstraction/prism/AbstractProgram.h

@@ -75,23 +75,24 @@ namespace storm {
                 void refine(std::vector<storm::expressions::Expression> const& predicates);
                 
                 /*!
-                 * Exports the current state of the abstraction in the dot format to the given file.
+                 * Refines the abstract program using the pivot state, and player 1 choice. The refinement guarantees that
+                 * the two provided choices are not possible from the same pivot state using the given player 1 choice.
                  *
-                 * @param filename The name of the file to which to write the dot output.
+                 * @param pivotState The pivot state on which to base the refinement.
+                 * @param player1Choice The player 1 choice that needs to be refined.
+                 * @param lowerChoice The first of the two choices on which to base the refinement.
+                 * @param upperChoice The first of the two choices on which to base the refinement.
                  */
-                void exportToDot(std::string const& filename) const;
+                void refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice);
                 
-            private:
                 /*!
-                 * Computes the reachable states of the transition relation.
+                 * Exports the current state of the abstraction in the dot format to the given file.
                  *
-                 * @param initialStates The BDD representing the initial states of the model.
-                 * @param transitionRelation The BDD representing the transition relation that does only contain state
-                 * and successor variables.
-                 * @return The BDD representing the reachable states.
+                 * @param filename The name of the file to which to write the dot output.
                  */
-                storm::dd::Bdd<DdType> getReachableStates(storm::dd::Bdd<DdType> const& initialStates, storm::dd::Bdd<DdType> const& transitionRelation);
+                void exportToDot(std::string const& filename) const;
                 
+            private:                
                 /*!
                  * Builds the stochastic game representing the abstraction of the program.
                  *
@@ -99,6 +100,14 @@ namespace storm {
                  */
                 std::unique_ptr<MenuGame<DdType, ValueType>> buildGame();
                 
+                /*!
+                 * Decodes the given choice over the auxiliary and successor variables to a mapping from update indices
+                 * to bit vectors representing the successors under these updates.
+                 *
+                 * @param choice The choice to decode.
+                 */
+                std::map<uint_fast64_t, storm::storage::BitVector> decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const;
+                
                 // The concrete program this abstract program refers to.
                 std::reference_wrapper<storm::prism::Program const> program;
 

src/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -24,6 +24,11 @@ namespace storm {
                 abstractProgram.refine(predicates);
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            void PrismMenuGameAbstractor<DdType, ValueType>::refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice) {
+                abstractProgram.refine(pivotState, player1Choice, lowerChoice, upperChoice);
+            }
+            
             template <storm::dd::DdType DdType, typename ValueType>
             void PrismMenuGameAbstractor<DdType, ValueType>::exportToDot(std::string const& filename) const {
                 abstractProgram.exportToDot(filename);

src/abstraction/prism/PrismMenuGameAbstractor.h

@@ -15,6 +15,7 @@ namespace storm {
                 
                 virtual storm::abstraction::MenuGame<DdType, ValueType> abstract() override;
                 virtual void refine(std::vector<storm::expressions::Expression> const& predicates) override;
+                virtual void refine(storm::dd::Bdd<DdType> const& pivotState, storm::dd::Bdd<DdType> const& player1Choice, storm::dd::Bdd<DdType> const& lowerChoice, storm::dd::Bdd<DdType> const& upperChoice) override;
 
                 void exportToDot(std::string const& filename) const;
                 

src/exceptions/InvalidModelException.h

@@ -0,0 +1,13 @@
+#pragma once
+
+#include "src/exceptions/BaseException.h"
+#include "src/exceptions/ExceptionMacros.h"
+
+namespace storm {
+    namespace exceptions {
+        
+        STORM_NEW_EXCEPTION(InvalidModelException)
+        
+    } // namespace exceptions
+} // namespace storm
+

src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -1,7 +1,7 @@
 #include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h"
 
-#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
-#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 
 #include "src/models/symbolic/StandardRewardModel.h"
 
@@ -13,10 +13,12 @@
 
 #include "src/logic/FragmentSpecification.h"
 
+#include "src/utility/dd.h"
 #include "src/utility/macros.h"
 
 #include "src/exceptions/NotSupportedException.h"
 #include "src/exceptions/InvalidPropertyException.h"
+#include "src/exceptions/InvalidModelException.h"
 
 #include "src/modelchecker/results/CheckResult.h"
 
@@ -56,7 +58,7 @@ namespace storm {
         template<storm::dd::DdType Type, typename ValueType>
         std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) {
             storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
-            return performGameBasedAbstractionRefinement(CheckTask<storm::logic::Formula>(pathFormula), getExpression(pathFormula.getLeftSubformula()), getExpression(pathFormula.getRightSubformula()));
+            return performGameBasedAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(pathFormula), getExpression(pathFormula.getLeftSubformula()), getExpression(pathFormula.getRightSubformula()));
         }
         
         template<storm::dd::DdType Type, typename ValueType>
@@ -84,11 +86,70 @@ namespace storm {
         
         template<storm::dd::DdType Type, typename ValueType>
         std::unique_ptr<CheckResult> getResultAfterQualitativeCheck(CheckTask<storm::logic::Formula> const& checkTask, storm::dd::DdManager<Type> const& ddManager, storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& initialStates, bool prob0) {
-            if (checkTask.isBoundSet()) {
-                bool result = getResultConsideringBound(prob0 ? storm::utility::zero<ValueType>() : storm::utility::one<ValueType>(), checkTask.getBound());
-                return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<Type>>(reachableStates, initialStates, result ? initialStates : ddManager.getBddZero());
+            return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), prob0 ? storm::utility::zero<ValueType>() : storm::utility::one<ValueType>());
+        }
+        
+        template<storm::dd::DdType Type>
+        storm::dd::Bdd<Type> pickPivotState(storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& transitions, std::set<storm::expressions::Variable> const& rowVariables, std::set<storm::expressions::Variable> const& columnVariables, storm::dd::Bdd<Type> const& pivotStates) {
+            // Perform a BFS and pick the first pivot state we encounter.
+            storm::dd::Bdd<Type> pivotState;
+            storm::dd::Bdd<Type> frontier = initialStates;
+            storm::dd::Bdd<Type> frontierPivotStates = frontier && pivotStates;
+
+            bool foundPivotState = !frontierPivotStates.isZero();
+            if (foundPivotState) {
+                pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables);
             } else {
-                return std::make_unique<storm::modelchecker::SymbolicQuantitativeCheckResult<Type>>(reachableStates, initialStates, prob0 ? ddManager.template getAddZero<ValueType>() : initialStates.template toAdd<ValueType>());
+                while (!foundPivotState) {
+                    frontier = frontier.relationalProduct(transitions, rowVariables, columnVariables);
+                    frontierPivotStates = frontier && pivotStates;
+                
+                    if (!frontierPivotStates.isZero()) {
+                        pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables);
+                        foundPivotState = true;
+                    }
+                }
+            }
+            
+            return pivotState;
+        }
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        void refineAfterQualitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType>& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game, detail::GameProb01Result<Type> const& prob01, storm::dd::Bdd<Type> const& transitionMatrixBdd) {
+            storm::dd::Bdd<Type> transitionsInIntersection = transitionMatrixBdd && prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy() && prob01.max.second.getPlayer1Strategy() && prob01.max.second.getPlayer2Strategy();
+            
+            // First, we have to find the pivot state candidates. Start by constructing the reachable fragment of the
+            // state space *under both* strategy pairs.
+            storm::dd::Bdd<Type> pivotStates = storm::utility::dd::computeReachableStates(game.getInitialStates(), transitionsInIntersection.existsAbstract(game.getNondeterminismVariables()), game.getRowVariables(), game.getColumnVariables());
+            
+            // Then constrain this set by requiring that the two stratey pairs resolve the nondeterminism differently.
+            pivotStates &= (prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy()).exclusiveOr(prob01.max.second.getPlayer1Strategy() && prob01.max.second.getPlayer2Strategy()).existsAbstract(game.getNondeterminismVariables());
+            STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates.");
+            
+            // Now that we have the pivot state candidates, we need to pick one.
+            storm::dd::Bdd<Type> pivotState = pickPivotState<Type>(game.getInitialStates(), transitionsInIntersection, game.getRowVariables(), game.getColumnVariables(), pivotStates);
+            
+            // Compute the lower and the upper choice for the pivot state.
+            std::set<storm::expressions::Variable> variablesToAbstract = game.getNondeterminismVariables();
+            variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end());
+            storm::dd::Bdd<Type> lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && prob01.min.first.getPlayer1Strategy();
+            storm::dd::Bdd<Type> lowerChoice1 = (lowerChoice && prob01.min.first.getPlayer2Strategy()).existsAbstract(variablesToAbstract);
+            storm::dd::Bdd<Type> lowerChoice2 = (lowerChoice && prob01.max.second.getPlayer2Strategy()).existsAbstract(variablesToAbstract);
+                        
+            bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero();
+            if (lowerChoicesDifferent) {
+                abstractor.refine(pivotState, (pivotState && prob01.min.first.getPlayer1Strategy()).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2);
+            } else {
+                storm::dd::Bdd<Type> upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && prob01.max.second.getPlayer1Strategy();
+                storm::dd::Bdd<Type> upperChoice1 = (upperChoice && prob01.min.first.getPlayer2Strategy()).existsAbstract(variablesToAbstract);
+                storm::dd::Bdd<Type> upperChoice2 = (upperChoice && prob01.max.second.getPlayer2Strategy()).existsAbstract(variablesToAbstract);
+                
+                bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero();
+                if (upperChoicesDifferent) {
+                    abstractor.refine(pivotState, (pivotState && prob01.max.second.getPlayer1Strategy()).existsAbstract(game.getRowVariables()), upperChoice1, upperChoice2);
+                } else {
+                    STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates.");
+                }
             }
         }
         
@@ -106,60 +167,73 @@ namespace storm {
             }
             
             // Derive the optimization direction for player 1 (assuming menu-game abstraction).
-            storm::OptimizationDirection player1Direction = checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize;
+            storm::OptimizationDirection player1Direction;
+            if (checkTask.isOptimizationDirectionSet()) {
+                player1Direction = checkTask.getOptimizationDirection();
+            } else if (checkTask.isBoundSet() && !originalProgram.isDeterministicModel()) {
+                player1Direction = storm::logic::isLowerBound(checkTask.getBoundComparisonType()) ? storm::OptimizationDirection::Minimize : storm::OptimizationDirection::Maximize;
+            } else {
+                STORM_LOG_THROW(originalProgram.isDeterministicModel(), storm::exceptions::InvalidPropertyException, "Requiring either min or max annotation in property for nondeterministic models.");
+                player1Direction = storm::OptimizationDirection::Maximize;
+            }
             
             storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType> abstractor(preprocessedProgram, initialPredicates, smtSolverFactory);
             
-            // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression.
-            storm::abstraction::MenuGame<Type, ValueType> game = abstractor.abstract();
-            STORM_LOG_DEBUG("Initial abstraction has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions.");
+            for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) {
+                STORM_LOG_TRACE("Starting iteration " << iterations);
+                abstractor.exportToDot("game" + std::to_string(iterations) + ".dot");
 
-            // 2. compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max).
-            detail::GameProb01Result<Type> prob01 = computeProb01States(player1Direction, game, constraintExpression, targetStateExpression);
-            
-            // 3. compute the states for which we know the result/for which we know there is more work to be done.
-            storm::dd::Bdd<Type> maybeMin = !(prob01.min.first.states || prob01.min.second.states) && game.getReachableStates();
-            storm::dd::Bdd<Type> maybeMax = !(prob01.max.first.states || prob01.max.second.states) && game.getReachableStates();
-            
-            // 4. if the initial states are not maybe states, then we can refine at this point.
-            storm::dd::Bdd<Type> initialMaybeStates = game.getInitialStates() && (maybeMin || maybeMax);
-            if (initialMaybeStates.isZero()) {
-                // In this case, we know the result for the initial states for both player 2 minimizing and maximizing.
-                
-                // If the result is 0 independent of the player 2 strategy, then we know the final result and can return it.
-                storm::dd::Bdd<Type> tmp = game.getInitialStates() && prob01.min.first.states && prob01.max.first.states;
-                if (tmp == game.getInitialStates()) {
-                    getResultAfterQualitativeCheck<Type, ValueType>(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), true);
-                }
+                // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression.
+                storm::abstraction::MenuGame<Type, ValueType> game = abstractor.abstract();
+                STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions.");
+                STORM_LOG_THROW(game.getInitialStates().getNonZeroCount(), storm::exceptions::InvalidModelException, "Cannot treat models with more than one (abstract) initial state.");
                 
-                // If the result is 1 independent of the player 2 strategy, then we know the final result and can return it.
-                tmp = game.getInitialStates() && prob01.min.second.states && prob01.max.second.states;
-                if (tmp == game.getInitialStates()) {
-                    getResultAfterQualitativeCheck<Type, ValueType>(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), false);
-                }
+                // 1.5 build a BDD from the transition matrix for various later uses.
+                storm::dd::Bdd<Type> transitionMatrixBdd = game.getTransitionMatrix().toBdd();
                 
-                // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1)
-                // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine.
+                // 2. compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max).
+                detail::GameProb01Result<Type> prob01 = computeProb01States(player1Direction, game, transitionMatrixBdd, constraintExpression, targetStateExpression);
                 
+                // 3. compute the states for which we know the result/for which we know there is more work to be done.
+                storm::dd::Bdd<Type> maybeMin = !(prob01.min.first.states || prob01.min.second.states) && game.getReachableStates();
+                storm::dd::Bdd<Type> maybeMax = !(prob01.max.first.states || prob01.max.second.states) && game.getReachableStates();
                 
+                // 4. if the initial states are not maybe states, then we can refine at this point.
+                storm::dd::Bdd<Type> initialMaybeStates = (game.getInitialStates() && maybeMin) || (game.getInitialStates() && maybeMax);
+                if (initialMaybeStates.isZero()) {
+                    // In this case, we know the result for the initial states for both player 2 minimizing and maximizing.
+                    STORM_LOG_TRACE("No initial state is a 'maybe' state. Refining abstraction based on qualitative check.");
+                    
+                    // If the result is 0 independent of the player 2 strategy, then we know the final result and can return it.
+                    storm::dd::Bdd<Type> tmp = game.getInitialStates() && prob01.min.first.states && prob01.max.first.states;
+                    if (tmp == game.getInitialStates()) {
+                        return getResultAfterQualitativeCheck<Type, ValueType>(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), true);
+                    }
+                    
+                    // If the result is 1 independent of the player 2 strategy, then we know the final result and can return it.
+                    tmp = game.getInitialStates() && prob01.min.second.states && prob01.max.second.states;
+                    if (tmp == game.getInitialStates()) {
+                        return getResultAfterQualitativeCheck<Type, ValueType>(checkTask, game.getManager(), game.getReachableStates(), game.getInitialStates(), false);
+                    }
+                    
+                    // If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1)
+                    // depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine.
+                    refineAfterQualitativeCheck(abstractor, game, prob01, transitionMatrixBdd);
+                } else {
+                    
+                    // If we can already answer the question, do not solve the game numerically.
+                    
+                    
+                    STORM_LOG_ASSERT(false, "Quantiative refinement not yet there. :)");
+                }
             }
-            
-            
-            
-//            std::unique_ptr<storm::utility::solver::SymbolicGameSolverFactory<Type, ValueType>> gameSolverFactory = std::make_unique<storm::utility::solver::SymbolicGameSolverFactory<Type, ValueType>>();
-//            gameSolverFactory->create(game.getTransitionMatrix(), game.getReachableStates());
-//            storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables
-            
-            // 3. if the bounds suffice to complete checkTask, return result now.
-            
-            // 4. if the bounds do not suffice
-            
+
+            STORM_LOG_ASSERT(false, "This point must not be reached.");
             return nullptr;
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        detail::GameProb01Result<Type> GameBasedMdpModelChecker<Type, ValueType>::computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) {
-            storm::dd::Bdd<Type> transitionMatrixBdd = game.getTransitionMatrix().toBdd();
+        detail::GameProb01Result<Type> GameBasedMdpModelChecker<Type, ValueType>::computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) {
             storm::dd::Bdd<Type> bottomStatesBdd = game.getBottomStates();
             
             storm::dd::Bdd<Type> targetStates = game.getStates(targetStateExpression);
@@ -168,27 +242,35 @@ namespace storm {
             }
             
             // Start by computing the states with probability 0/1 when player 2 minimizes.
-            storm::utility::graph::GameProb01Result<Type> prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, true);
-            storm::utility::graph::GameProb01Result<Type> prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, false);
+            storm::utility::graph::GameProb01Result<Type> prob0Min = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, true, true);
+            storm::utility::graph::GameProb01Result<Type> prob1Min = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Minimize, false, false);
             
             // Now compute the states with probability 0/1 when player 2 maximizes.
-            storm::utility::graph::GameProb01Result<Type> prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, false);
-            storm::utility::graph::GameProb01Result<Type> prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true);
+            storm::utility::graph::GameProb01Result<Type> prob0Max = storm::utility::graph::performProb0(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, false, false);
+            storm::utility::graph::GameProb01Result<Type> prob1Max = storm::utility::graph::performProb1(game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates, player1Direction, storm::OptimizationDirection::Maximize, true, true);
+            prob1Max.getPlayer1Strategy().template toAdd<ValueType>().exportToDot("prob1maxstrat.dot");
             
-            STORM_LOG_DEBUG("Min: " << prob0Min.states.getNonZeroCount() << " no states, " << prob1Min.states.getNonZeroCount() << " yes states.");
-            STORM_LOG_DEBUG("Max: " << prob0Max.states.getNonZeroCount() << " no states, " << prob1Max.states.getNonZeroCount() << " yes states.");
+            STORM_LOG_ASSERT(prob0Min.hasPlayer1Strategy(), "Unable to proceed without strategy.");
+            STORM_LOG_ASSERT(prob0Min.hasPlayer2Strategy(), "Unable to proceed without strategy.");
+            STORM_LOG_ASSERT(prob1Max.hasPlayer1Strategy(), "Unable to proceed without strategy.");
+            STORM_LOG_ASSERT(prob1Max.hasPlayer2Strategy(), "Unable to proceed without strategy.");
+
+            STORM_LOG_TRACE("Min: " << prob0Min.states.getNonZeroCount() << " no states, " << prob1Min.states.getNonZeroCount() << " yes states.");
+            STORM_LOG_TRACE("Max: " << prob0Max.states.getNonZeroCount() << " no states, " << prob1Max.states.getNonZeroCount() << " yes states.");
             
             return detail::GameProb01Result<Type>(prob0Min, prob1Min, prob0Max, prob1Max);
         }
         
         template<storm::dd::DdType Type, typename ValueType>
         storm::expressions::Expression GameBasedMdpModelChecker<Type, ValueType>::getExpression(storm::logic::Formula const& formula) {
-            STORM_LOG_THROW(formula.isAtomicExpressionFormula() || formula.isAtomicLabelFormula(), storm::exceptions::InvalidPropertyException, "The target states have to be given as label or an expression.");
+            STORM_LOG_THROW(formula.isBooleanLiteralFormula() || formula.isAtomicExpressionFormula() || formula.isAtomicLabelFormula(), storm::exceptions::InvalidPropertyException, "The target states have to be given as label or an expression.");
             storm::expressions::Expression result;
             if (formula.isAtomicLabelFormula()) {
                 result = preprocessedProgram.getLabelExpression(formula.asAtomicLabelFormula().getLabel());
-            } else {
+            } else if (formula.isAtomicExpressionFormula()) {
                 result = formula.asAtomicExpressionFormula().getExpression();
+            } else {
+                result = formula.asBooleanLiteralFormula().isTrueFormula() ? originalProgram.getManager().boolean(true) : originalProgram.getManager().boolean(false);
             }
             return result;
         }

src/modelchecker/abstraction/GameBasedMdpModelChecker.h

@@ -50,7 +50,7 @@ namespace storm {
         private:
             std::unique_ptr<CheckResult> performGameBasedAbstractionRefinement(CheckTask<storm::logic::Formula> const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression);
             
-            detail::GameProb01Result<Type> computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression);
+            detail::GameProb01Result<Type> computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression);
             
             storm::expressions::Expression getExpression(storm::logic::Formula const& formula);
             

src/utility/dd.cpp

@@ -27,7 +27,6 @@ namespace storm {
                         changed = true;
                     }
                     
-                    
                     reachableStates |= newReachableStates;
 
                     ++iteration;

src/utility/graph.cpp

@@ -924,7 +924,7 @@ namespace storm {
             }
             
             template <storm::dd::DdType Type, typename ValueType>
-            GameProb01Result<Type> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies) {
+            GameProb01Result<Type> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) {
 
                 // The solution set.
                 storm::dd::Bdd<Type> solution = psiStates;
@@ -966,13 +966,13 @@ namespace storm {
                 storm::dd::Bdd<Type> onlyProb0Successors = (transitionsBetweenProb0States || model.getIllegalSuccessorMask()).universalAbstract(model.getColumnVariables());
                 
                 boost::optional<storm::dd::Bdd<Type>> player2StrategyBdd;
-                if (produceStrategies && player2Strategy == OptimizationDirection::Minimize) {
+                if (producePlayer2Strategy) {
                     // Pick a distribution that has only prob0 successors.
                     player2StrategyBdd = onlyProb0Successors.existsAbstractRepresentative(model.getPlayer2Variables());
                 }
                 
                 boost::optional<storm::dd::Bdd<Type>> player1StrategyBdd;
-                if (produceStrategies && player1Strategy == OptimizationDirection::Minimize) {
+                if (producePlayer1Strategy) {
                     // Move from player 2 choices with only prob0 successors to player 1 choices with only prob 0 successors.
                     onlyProb0Successors = onlyProb0Successors.existsAbstract(model.getPlayer2Variables());
                     
@@ -984,12 +984,11 @@ namespace storm {
             }
             
             template <storm::dd::DdType Type, typename ValueType>
-            GameProb01Result<Type> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies) {
+            GameProb01Result<Type> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy) {
                 
                 // Create two sets of states. Those states for which we definitely know that their probability is 1 and
                 // those states that potentially have a probability of 1.
                 storm::dd::Bdd<Type> maybeStates = model.getReachableStates();
-                storm::dd::Bdd<Type> solution = psiStates;
 
                 // A flag that governs whether strategies are produced in the current iteration.
                 bool produceStrategiesInIteration = false;
@@ -1012,6 +1011,7 @@ namespace storm {
                         consideredPlayer2States = model.getManager().getBddZero();
                     }
                     
+                    storm::dd::Bdd<Type> solution = psiStates;
                     while (!solutionStatesDone) {
                         // Start by computing the transitions that have only maybe states as successors. Note that at
                         // this point, there may be illegal transitions.
@@ -1024,7 +1024,7 @@ namespace storm {
                         // The valid distributions are then those that emanate from phi states, stay completely in the
                         // maybe states and have at least one successor with probability 1.
                         storm::dd::Bdd<Type> valid = phiStates && distributionsStayingInMaybe && distributionsWithProb1Successor;
-                        
+
                         // Depending on the strategy of player 2, we need to check whether all choices are valid or
                         // there exists a valid choice.
                         if (player2Strategy == OptimizationDirection::Minimize) {
@@ -1079,7 +1079,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 && produceStrategies && (player1Strategy == OptimizationDirection::Maximize || player2Strategy == OptimizationDirection::Maximize);
+                        produceStrategiesInIteration = !produceStrategiesInIteration && ((producePlayer1Strategy && player1Strategy == OptimizationDirection::Maximize) || (producePlayer2Strategy && player2Strategy == OptimizationDirection::Maximize));
                     } else {
                         // Otherwise, we use the current hypothesis for the states with probability 1 as the new maybe
                         // state set.
@@ -1088,7 +1088,23 @@ namespace storm {
                     ++maybeStateIterations;
                 }
                 
-                return GameProb01Result<Type>(solution, player1StrategyBdd, player2StrategyBdd);
+                // From now on, the solution is stored in maybeStates (as it coincides with the previous solution).
+                
+                // If we were asked to produce strategies that do not need to pick a certain successor but are
+                // 'arbitrary', do so now.
+                bool strategiesToCompute = (producePlayer1Strategy && !player1StrategyBdd) || (producePlayer2Strategy && !player2StrategyBdd);
+                if (strategiesToCompute) {
+                    storm::dd::Bdd<Type> relevantStates = (transitionMatrix && maybeStates).existsAbstract(model.getColumnVariables());
+                    if (producePlayer2Strategy && !player2StrategyBdd) {
+                        player2StrategyBdd = relevantStates.existsAbstractRepresentative(model.getPlayer2Variables());
+                    }
+                    if (producePlayer1Strategy && !player1StrategyBdd) {
+                        relevantStates = relevantStates.existsAbstract(model.getPlayer2Variables());
+                        player1StrategyBdd = relevantStates.existsAbstractRepresentative(model.getPlayer1Variables());
+                    }
+                }
+                
+                return GameProb01Result<Type>(maybeStates, player1StrategyBdd, player2StrategyBdd);
             }
             
             template <typename T>
@@ -1488,9 +1504,9 @@ namespace storm {
             
             template std::pair<storm::dd::Bdd<storm::dd::DdType::CUDD>, storm::dd::Bdd<storm::dd::DdType::CUDD>> performProb01Min(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates);
             
-            template GameProb01Result<storm::dd::DdType::CUDD> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies);
+            template GameProb01Result<storm::dd::DdType::CUDD> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy);
             
-            template GameProb01Result<storm::dd::DdType::CUDD> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies);
+            template GameProb01Result<storm::dd::DdType::CUDD> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy);
 
             // Instantiations for Sylvan.
             
@@ -1520,9 +1536,9 @@ namespace storm {
             
             template std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> performProb01Min(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
 
-            template GameProb01Result<storm::dd::DdType::Sylvan> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies);
+            template GameProb01Result<storm::dd::DdType::Sylvan> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy);
 
-            template GameProb01Result<storm::dd::DdType::Sylvan> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies);
+            template GameProb01Result<storm::dd::DdType::Sylvan> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::Sylvan> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy, bool producePlayer2Strategy);
 
         } // namespace graph
     } // namespace utility

src/utility/graph.h

@@ -568,11 +568,11 @@ namespace storm {
              * @param transitionMatrix The transition matrix of the model as a BDD.
              * @param phiStates The BDD containing all phi states of the model.
              * @param psiStates The BDD containing all psi states of the model.
-             * @param produceStrategies A flag indicating whether strategies should be produced. Note that the strategies
-             * are only produced in case the choices of the player are not irrelevant.
+             * @param producePlayer1Strategy A flag indicating whether the strategy of player 1 shall be produced.
+             * @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced.
              */
             template <storm::dd::DdType Type, typename ValueType>
-            GameProb01Result<Type> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool produceStrategies = false);
+            GameProb01Result<Type> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false);
             
             /*!
              * Computes the set of states that have probability 1 given the strategies of the two players.
@@ -581,11 +581,11 @@ namespace storm {
              * @param transitionMatrix The transition matrix of the model as a BDD.
              * @param phiStates The BDD containing all phi states of the model.
              * @param psiStates The BDD containing all psi states of the model.
-             * @param produceStrategies A flag indicating whether strategies should be produced. Note that the strategies
-             * are only produced in case the choices of the player are not irrelevant.
+             * @param producePlayer1Strategy A flag indicating whether the strategy of player 1 shall be produced.
+             * @param producePlayer2Strategy A flag indicating whether the strategy of player 2 shall be produced.
              */
             template <storm::dd::DdType Type, typename ValueType>
-            GameProb01Result<Type> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategybool, bool produceStrategies = false);
+            GameProb01Result<Type> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<Type, ValueType> const& model, storm::dd::Bdd<Type> const& transitionMatrix, storm::dd::Bdd<Type> const& phiStates, storm::dd::Bdd<Type> const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy, bool producePlayer1Strategy = false, bool producePlayer2Strategy = false);
             
             /*!
              * Performs a topological sort of the states of the system according to the given transitions.

test/functional/utility/GraphTest.cpp

@@ -214,33 +214,33 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
     // The target states are those states where !(s < 3).
     storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = game.getStates(initialPredicates[0], true);
     
-    storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true);
+    storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
     EXPECT_EQ(2, result.states.getNonZeroCount());
-    EXPECT_TRUE(static_cast<bool>(result.player1Strategy));
-    EXPECT_TRUE(static_cast<bool>(result.player2Strategy));
+    EXPECT_TRUE(result.hasPlayer1Strategy());
+    EXPECT_TRUE(result.hasPlayer2Strategy());
     
-    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true);
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize);
     EXPECT_EQ(2, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
     EXPECT_EQ(2, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
     EXPECT_EQ(2, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
     EXPECT_EQ(2, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
     EXPECT_EQ(2, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize);
     EXPECT_EQ(1, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true);
     EXPECT_EQ(3, result.states.getNonZeroCount());
-    EXPECT_TRUE(static_cast<bool>(result.player1Strategy));
-    EXPECT_TRUE(static_cast<bool>(result.player2Strategy));
+    EXPECT_TRUE(result.hasPlayer1Strategy());
+    EXPECT_TRUE(result.hasPlayer2Strategy());
     
     abstractProgram.refine({manager.getVariableExpression("s") < manager.integer(2)});
     game = abstractProgram.getAbstractGame();
@@ -248,10 +248,10 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
     // We need to create a new BDD for the target states since the reachable states might have changed.
     targetStates = game.getStates(initialPredicates[0], true);
     
-    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true);
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
     EXPECT_EQ(2, result.states.getNonZeroCount());
-    EXPECT_TRUE(static_cast<bool>(result.player1Strategy));
-    EXPECT_TRUE(static_cast<bool>(result.player2Strategy));
+    ASSERT_TRUE(result.hasPlayer1Strategy());
+    ASSERT_TRUE(result.hasPlayer2Strategy());
     
     // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy.
     storm::dd::Bdd<storm::dd::DdType::CUDD> nonProb0StatesWithStrategy = !result.states && result.player1Strategy.get();
@@ -265,28 +265,28 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
     storm::dd::Add<storm::dd::DdType::CUDD> stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
     EXPECT_EQ(1, stateDistributionCount.getMax());
     
-    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true);
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize);
     EXPECT_EQ(3, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
     EXPECT_EQ(1, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
     EXPECT_EQ(4, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
     EXPECT_EQ(2, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
     EXPECT_EQ(3, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize);
     EXPECT_EQ(1, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true);
     EXPECT_EQ(4, result.states.getNonZeroCount());
-    EXPECT_TRUE(static_cast<bool>(result.player1Strategy));
-    EXPECT_TRUE(static_cast<bool>(result.player2Strategy));
+    EXPECT_TRUE(result.hasPlayer1Strategy());
+    EXPECT_TRUE(result.hasPlayer2Strategy());
     
     // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy.
     storm::dd::Bdd<storm::dd::DdType::CUDD> nonProb1StatesWithStrategy = !result.states && result.player1Strategy.get();
@@ -350,10 +350,10 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) {
     // The target states are those states where s1 == 7 & s2 == 7 & d1 + d2 == 1.
     storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = game.getStates(initialPredicates[7], false) && game.getStates(initialPredicates[22], false) && game.getStates(initialPredicates[9], false) && game.getStates(initialPredicates[24], false);
     
-    storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true);
+    storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
     EXPECT_EQ(153, result.states.getNonZeroCount());
-    EXPECT_TRUE(static_cast<bool>(result.player1Strategy));
-    EXPECT_TRUE(static_cast<bool>(result.player2Strategy));
+    ASSERT_TRUE(result.hasPlayer1Strategy());
+    ASSERT_TRUE(result.hasPlayer2Strategy());
     
     // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy.
     storm::dd::Bdd<storm::dd::DdType::CUDD> nonProb0StatesWithStrategy = !result.states && result.player1Strategy.get();
@@ -366,28 +366,28 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) {
     storm::dd::Add<storm::dd::DdType::CUDD> stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
     EXPECT_EQ(1, stateDistributionCount.getMax());
     
-    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true);
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize);
     EXPECT_EQ(1, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
     EXPECT_EQ(153, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
     EXPECT_EQ(1, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
     EXPECT_EQ(153, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
     EXPECT_EQ(1, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize);
     EXPECT_EQ(153, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true);
     EXPECT_EQ(1, result.states.getNonZeroCount());
-    EXPECT_TRUE(static_cast<bool>(result.player1Strategy));
-    EXPECT_TRUE(static_cast<bool>(result.player2Strategy));
+    EXPECT_TRUE(result.hasPlayer1Strategy());
+    EXPECT_TRUE(result.hasPlayer2Strategy());
     
     // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy.
     storm::dd::Bdd<storm::dd::DdType::CUDD> nonProb1StatesWithStrategy = !result.states && result.player1Strategy.get();
@@ -519,10 +519,10 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) {
     // The target states are those states where col == 2.
     storm::dd::Bdd<storm::dd::DdType::CUDD> targetStates = game.getStates(initialPredicates[2], false);
     
-    storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true);
+    storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true);
     EXPECT_EQ(2831, result.states.getNonZeroCount());
-    ASSERT_TRUE(static_cast<bool>(result.player1Strategy));
-    ASSERT_TRUE(static_cast<bool>(result.player2Strategy));
+    EXPECT_TRUE(result.hasPlayer1Strategy());
+    EXPECT_TRUE(result.hasPlayer2Strategy());
     
     // Check the validity of the strategies. Start by checking whether only prob0 states have a strategy.
     storm::dd::Bdd<storm::dd::DdType::CUDD> nonProb0StatesWithStrategy = !result.states && result.player1Strategy.get();
@@ -536,28 +536,28 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) {
     storm::dd::Add<storm::dd::DdType::CUDD> stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables());
     EXPECT_EQ(1, stateDistributionCount.getMax());
     
-    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true);
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize);
     EXPECT_EQ(2692, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
     EXPECT_EQ(2831, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
     EXPECT_EQ(2692, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
     EXPECT_EQ(2064, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
     EXPECT_EQ(2884, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize);
     EXPECT_EQ(2064, result.states.getNonZeroCount());
     
-    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true);
     EXPECT_EQ(2884, result.states.getNonZeroCount());
-    EXPECT_TRUE(static_cast<bool>(result.player1Strategy));
-    EXPECT_TRUE(static_cast<bool>(result.player2Strategy));
+    EXPECT_TRUE(result.hasPlayer1Strategy());
+    EXPECT_TRUE(result.hasPlayer2Strategy());
     
     // Check the validity of the strategies. Start by checking whether only prob1 states have a strategy.
     storm::dd::Bdd<storm::dd::DdType::CUDD> nonProb1StatesWithStrategy = !result.states && result.player1Strategy.get();