fixed symbolic game solver wrt. illegal masks. numerical solving step in game-based model checker working, but no refinement yet.

Former-commit-id: 6189a1e538

resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc

@@ -2648,7 +2648,16 @@ ADD::MinAbstract(const ADD& cube) const
     checkReturnValue(result);
     return ADD(p, result);
 } // ADD::MinAbstract
-    
+
+ADD
+ADD::MinAbstractExcept0(const ADD& cube) const
+{
+    DdManager *mgr = checkSameManager(cube);
+    DdNode *result = Cudd_addMinExcept0Abstract(mgr, node, cube.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+} // ADD::MinAbstractExcept0
+
 ADD
 ADD::MaxAbstract(const ADD& cube) const
 {

resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh

@@ -334,6 +334,7 @@ public:
     ADD UnivAbstract(const ADD& cube) const;
     ADD OrAbstract(const ADD& cube) const;
     ADD MinAbstract(const ADD& cube) const;
+    ADD MinAbstractExcept0(const ADD& cube) const;
     ADD MaxAbstract(const ADD& cube) const;
     ADD MinAbstractRepresentative(const ADD& cube) const;
     ADD MaxAbstractRepresentative(const ADD& cube) const;

resources/3rdparty/cudd-3.0.0/cudd/cudd.h

@@ -667,6 +667,7 @@ extern DdNode * Cudd_addExistAbstract(DdManager *manager, DdNode *f, DdNode *cub
 extern DdNode * Cudd_addUnivAbstract(DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * Cudd_addOrAbstract(DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * Cudd_addMinAbstract(DdManager * manager, DdNode * f, DdNode * cube);
+extern DdNode * Cudd_addMinExcept0Abstract(DdManager * manager, DdNode * f, DdNode * cube);
 extern DdNode * Cudd_addMaxAbstract(DdManager * manager, DdNode * f, DdNode * cube);
 extern DdNode * Cudd_addMinAbstractRepresentative(DdManager * manager, DdNode * f, DdNode * cube);
 extern DdNode * Cudd_addMaxAbstractRepresentative(DdManager * manager, DdNode * f, DdNode * cube);
@@ -679,6 +680,7 @@ extern DdNode * Cudd_addSetNZ(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addDivide(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addMinus(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addMinimum(DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addMinimumExcept0(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addMaximum(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addOneZeroMaximum(DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addDiff(DdManager *dd, DdNode **f, DdNode **g);

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

@@ -243,6 +243,44 @@ Cudd_addMinAbstract(
 } /* end of Cudd_addMinAbstract */
 
 
+/**Function********************************************************************
+ 
+ Synopsis    [Abstracts all the variables in cube from the
+ ADD f by taking the minimum.]
+ 
+ Description [Abstracts all the variables in cube from the ADD f
+ by taking the minimum over all possible values taken by the
+ variables.  Returns the abstracted ADD if successful; NULL
+ otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     [Cudd_addUnivAbstract Cudd_addExistAbstract]
+ 
+ Note: Added by Christian Dehnert 24/08/2016
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addMinExcept0Abstract(
+                    DdManager * manager,
+                    DdNode * f,
+                    DdNode * cube)
+{
+    DdNode *res;
+    
+    if (addCheckPositiveCube(manager, cube) == 0) {
+        (void) fprintf(manager->err,"Error: Can only abstract cubes");
+        return(NULL);
+    }
+    
+    do {
+        manager->reordered = 0;
+        res = cuddAddMinExcept0AbstractRecur(manager, f, cube);
+    } while (manager->reordered == 1);
+    return(res);
+    
+} /* end of Cudd_addMinExcept0Abstract */
+
 /**Function********************************************************************
  
  Synopsis    [Abstracts all the variables in cube from the
@@ -750,6 +788,98 @@ cuddAddMinAbstractRecur(
     
 } /* end of cuddAddMinAbstractRecur */
 
+/**Function********************************************************************
+ 
+ Synopsis    [Performs the recursive step of Cudd_addMinAbstract.]
+ 
+ Description [Performs the recursive step of Cudd_addMinAbstract.
+ Returns the ADD obtained by abstracting the variables of cube from f,
+ if successful; NULL otherwise.]
+ 
+ SideEffects [None]
+ 
+ SeeAlso     []
+ 
+ added 24/08/2016 by Christian Dehnert
+ 
+ ******************************************************************************/
+DdNode *
+cuddAddMinExcept0AbstractRecur(
+                        DdManager * manager,
+                        DdNode * f,
+                        DdNode * cube)
+{
+    DdNode	*T, *E, *res, *res1, *res2, *zero;
+    
+    zero = DD_ZERO(manager);
+    
+    /* Cube is guaranteed to be a cube at this point. */
+    if (f == zero || cuddIsConstant(cube)) {
+        return(f);
+    }
+    
+    /* Abstract a variable that does not appear in f. */
+    if (cuddI(manager,f->index) > cuddI(manager,cube->index)) {
+        res = cuddAddMinAbstractRecur(manager, f, cuddT(cube));
+       	return(res);
+    }
+    
+    if ((res = cuddCacheLookup2(manager, Cudd_addMinAbstract, f, cube)) != NULL) {
+        return(res);
+    }
+    
+    
+    T = cuddT(f);
+    E = cuddE(f);
+    
+    /* If the two indices are the same, so are their levels. */
+    if (f->index == cube->index) {
+        res1 = cuddAddMinAbstractRecur(manager, T, cuddT(cube));
+        if (res1 == NULL) return(NULL);
+        cuddRef(res1);
+        res2 = cuddAddMinAbstractRecur(manager, E, cuddT(cube));
+        if (res2 == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            return(NULL);
+        }
+        cuddRef(res2);
+        res = cuddAddApplyRecur(manager, Cudd_addMinimumExcept0, res1, res2);
+        if (res == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            Cudd_RecursiveDeref(manager,res2);
+            return(NULL);
+        }
+        cuddRef(res);
+        Cudd_RecursiveDeref(manager,res1);
+        Cudd_RecursiveDeref(manager,res2);
+        cuddCacheInsert2(manager, Cudd_addMinAbstract, f, cube, res);
+        cuddDeref(res);
+        return(res);
+    }
+    else { /* if (cuddI(manager,f->index) < cuddI(manager,cube->index)) */
+        res1 = cuddAddMinAbstractRecur(manager, T, cube);
+        if (res1 == NULL) return(NULL);
+        cuddRef(res1);
+        res2 = cuddAddMinAbstractRecur(manager, E, cube);
+        if (res2 == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            return(NULL);
+        }
+        cuddRef(res2);
+        res = (res1 == res2) ? res1 :
+        cuddUniqueInter(manager, (int) f->index, res1, res2);
+        if (res == NULL) {
+            Cudd_RecursiveDeref(manager,res1);
+            Cudd_RecursiveDeref(manager,res2);
+            return(NULL);
+        }
+        cuddDeref(res1);
+        cuddDeref(res2);
+        cuddCacheInsert2(manager, Cudd_addMinAbstract, f, cube, res);
+        return(res);
+    }
+    
+} /* end of cuddAddMinAbstractRecur */
 
 /**Function********************************************************************
  

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

@@ -406,6 +406,53 @@ Cudd_addMinimum(
 
 } /* end of Cudd_addMinimum */
 
+/**
+ @brief Integer and floating point min.
+ 
+ @details Integer and floating point min for Cudd_addApply.
+ 
+ @return NULL if not a terminal case; min(f,g) otherwise.
+ 
+ @sideeffect None
+ 
+ @see Cudd_addApply
+ 
+ added 24/08/2016
+ 
+ */
+DdNode *
+Cudd_addMinimumExcept0(
+                DdManager * dd,
+                DdNode ** f,
+                DdNode ** g)
+{
+    DdNode *F, *G;
+    
+    F = *f; G = *g;
+    if (F == DD_ZERO(dd)) return(G);
+    if (G == DD_ZERO(dd)) return(F);
+    if (F == DD_PLUS_INFINITY(dd)) return(G);
+    if (G == DD_PLUS_INFINITY(dd)) return(F);
+    if (F == G) return(F);
+#if 0
+    /* These special cases probably do not pay off. */
+    if (F == DD_MINUS_INFINITY(dd)) return(F);
+    if (G == DD_MINUS_INFINITY(dd)) return(G);
+#endif
+    if (cuddIsConstant(F) && cuddIsConstant(G)) {
+        if (cuddV(F) <= cuddV(G)) {
+            return(F);
+        } else {
+            return(G);
+        }
+    }
+    if (F > G) { /* swap f and g */
+        *f = G;
+        *g = F;
+    }
+    return(NULL);
+    
+} /* end of Cudd_addMinimumExcept0 */
 
 /**
   @brief Integer and floating point max.

resources/3rdparty/cudd-3.0.0/cudd/cuddInt.h

@@ -1062,6 +1062,7 @@ extern DdNode * cuddAddExistAbstractRecur(DdManager *manager, DdNode *f, DdNode
 extern DdNode * cuddAddUnivAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * cuddAddOrAbstractRecur(DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * cuddAddMinAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube);
+extern DdNode * cuddAddMinExcept0AbstractRecur (DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * cuddAddMaxAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube);
 extern DdNode * cuddAddMinAbstractRepresentativeRecur(DdManager * manager, DdNode * f, DdNode * cube);
 extern DdNode * cuddAddMaxAbstractRepresentativeRecur(DdManager * manager, DdNode * f, DdNode * cube);

src/abstraction/prism/AbstractProgram.cpp

@@ -154,13 +154,13 @@ namespace storm {
                 // 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.");
+                    STORM_LOG_TRACE("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);
+                    STORM_LOG_TRACE("Derived new predicate: " << newPredicate);
                     this->refine({newPredicate});
                 } else {
-                    STORM_LOG_DEBUG("No bottom state successor. Deriving a new predicate using weakest precondition.");
+                    STORM_LOG_TRACE("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);
@@ -187,8 +187,15 @@ namespace storm {
                         }
                     }
                     
+                    STORM_LOG_TRACE("Derived new predicate: " << newPredicate);
+                    
                     this->refine({newPredicate});
                 }
+                
+                STORM_LOG_TRACE("Current set of predicates:");
+                for (auto const& predicate : abstractionInformation.getPredicates()) {
+                    STORM_LOG_TRACE(predicate);
+                }
             }
             
             template <storm::dd::DdType DdType, typename ValueType>

src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -13,6 +13,9 @@
 
 #include "src/logic/FragmentSpecification.h"
 
+#include "src/solver/SymbolicGameSolver.h"
+
+#include "src/utility/solver.h"
 #include "src/utility/dd.h"
 #include "src/utility/macros.h"
 
@@ -115,6 +118,55 @@ namespace storm {
             
             return result;
         }
+
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> checkForResultAfterQuantitativeCheck(CheckTask<storm::logic::Formula> const& checkTask, storm::OptimizationDirection const& player2Direction, ValueType const& value) {
+            std::unique_ptr<CheckResult> result;
+            
+            // If the minimum value exceeds an upper threshold or the maximum value is below a lower threshold, we can
+            // return the value because the property will definitely hold. Vice versa, if the minimum value exceeds an
+            // upper bound or the maximum value is below a lower bound, the property will definitely not hold and we can
+            // return the value.
+            if (checkTask.isBoundSet() && storm::logic::isLowerBound(checkTask.getBoundComparisonType())) {
+                if (player2Direction == storm::OptimizationDirection::Minimize) {
+                    if ((storm::logic::isStrict(checkTask.getBoundComparisonType()) && value > checkTask.getBoundThreshold())
+                        || (!storm::logic::isStrict(checkTask.getBoundComparisonType()) && value >= checkTask.getBoundThreshold())) {
+                        result = std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), value);
+                    }
+                } else {
+                    if ((storm::logic::isStrict(checkTask.getBoundComparisonType()) && value <= checkTask.getBoundThreshold())
+                        || (!storm::logic::isStrict(checkTask.getBoundComparisonType()) && value < checkTask.getBoundThreshold())) {
+                        result = std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), value);
+                    }
+                }
+            } else if (checkTask.isBoundSet() && !storm::logic::isLowerBound(checkTask.getBoundComparisonType())) {
+                if (player2Direction == storm::OptimizationDirection::Maximize) {
+                    if ((storm::logic::isStrict(checkTask.getBoundComparisonType()) && value < checkTask.getBoundThreshold()) ||
+                        (!storm::logic::isStrict(checkTask.getBoundComparisonType()) && value <= checkTask.getBoundThreshold())) {
+                        result = std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), value);
+                    }
+                } else {
+                    if ((storm::logic::isStrict(checkTask.getBoundComparisonType()) && value >= checkTask.getBoundThreshold()) ||
+                        (!storm::logic::isStrict(checkTask.getBoundComparisonType()) && value > checkTask.getBoundThreshold())) {
+                        result = std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), value);
+                    }
+                }
+            }
+            
+            return result;
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> checkForResultAfterQuantitativeCheck(CheckTask<storm::logic::Formula> const& checkTask, ValueType const& minValue, ValueType const& maxValue) {
+            std::unique_ptr<CheckResult> result;
+
+            // If the lower and upper bounds are close enough, we can return the result.
+            if (maxValue - minValue < storm::utility::convertNumber<ValueType>(1e-3)) {
+                result = std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), (minValue + maxValue) / ValueType(2));
+            }
+
+            return result;
+        }
         
         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) {
@@ -180,6 +232,30 @@ namespace storm {
             }
         }
         
+        template<storm::dd::DdType Type, typename ValueType>
+        storm::dd::Add<Type, ValueType> solveMaybeStates(storm::OptimizationDirection const& player1Direction, storm::OptimizationDirection const& player2Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Bdd<Type> const& maybeStates, storm::dd::Bdd<Type> const& prob1States, boost::optional<storm::dd::Add<Type, ValueType>> startVector = boost::none) {
+            
+            // Compute the ingredients of the equation system.
+            storm::dd::Add<Type, ValueType> maybeStatesAdd = maybeStates.template toAdd<ValueType>();
+            storm::dd::Add<Type, ValueType> submatrix = maybeStatesAdd * game.getTransitionMatrix();
+            storm::dd::Add<Type, ValueType> prob1StatesAsColumn = prob1States.template toAdd<ValueType>().swapVariables(game.getRowColumnMetaVariablePairs());
+            storm::dd::Add<Type, ValueType> subvector = submatrix * prob1StatesAsColumn;
+            subvector = subvector.sumAbstract(game.getColumnVariables());
+
+            // Cut away all columns targeting non-maybe states.
+            submatrix *= maybeStatesAdd.swapVariables(game.getRowColumnMetaVariablePairs());
+
+            // Cut the starting vector to the maybe states of this query.
+            if (startVector) {
+                startVector.get() *= maybeStatesAdd;
+            }
+            
+            // Create the solver and solve the equation system.
+            storm::utility::solver::SymbolicGameSolverFactory<Type, ValueType> solverFactory;
+            std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> solver = solverFactory.create(submatrix, maybeStates, game.getIllegalPlayer1Mask(), game.getIllegalPlayer2Mask(), game.getRowVariables(), game.getColumnVariables(), game.getRowColumnMetaVariablePairs(), game.getPlayer1Variables(), game.getPlayer2Variables());
+            return solver->solveGame(player1Direction, player2Direction, startVector ? startVector.get() : game.getManager().template getAddZero<ValueType>(), subvector);
+        }
+        
         template<storm::dd::DdType Type, typename ValueType>
         std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::performGameBasedAbstractionRefinement(CheckTask<storm::logic::Formula> const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) {
             STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states.");
@@ -195,7 +271,9 @@ namespace storm {
             
             // Derive the optimization direction for player 1 (assuming menu-game abstraction).
             storm::OptimizationDirection player1Direction;
-            if (checkTask.isOptimizationDirectionSet()) {
+            if (originalProgram.isDeterministicModel()) {
+                player1Direction = storm::OptimizationDirection::Maximize;
+            } else if (checkTask.isOptimizationDirectionSet()) {
                 player1Direction = checkTask.getOptimizationDirection();
             } else if (checkTask.isBoundSet() && !originalProgram.isDeterministicModel()) {
                 player1Direction = storm::logic::isLowerBound(checkTask.getBoundComparisonType()) ? storm::OptimizationDirection::Minimize : storm::OptimizationDirection::Maximize;
@@ -239,8 +317,13 @@ namespace storm {
                 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();
                 
+                maybeMin.template toAdd<ValueType>().exportToDot("maybemin.dot");
+                maybeMax.template toAdd<ValueType>().exportToDot("maybemax.dot");
+                game.getInitialStates().template toAdd<ValueType>().exportToDot("init.dot");
+                
                 // 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);
+                initialMaybeStates.template toAdd<ValueType>().exportToDot("initmaybe.dot");
                 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.");
@@ -255,13 +338,57 @@ namespace storm {
                         return result;
                     }
                     
+                    STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states.");
+
                     // 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 {
+
+                    // At this point, we know that we cannot answer the query without further numeric computation.
+                    STORM_LOG_TRACE("Starting numerical solution step.");
+                    
+                    // Prepare some storage that we use on-demand during the quantitative solving step.
+                    storm::dd::Add<Type, ValueType> minResult = prob01.min.second.states.template toAdd<ValueType>();
+                    storm::dd::Add<Type, ValueType> maxResult = prob01.max.second.states.template toAdd<ValueType>();
+                    storm::dd::Add<Type, ValueType> initialStatesAdd = game.getInitialStates().template toAdd<ValueType>();
+
+                    ValueType minValue = (prob01.min.second.states && game.getInitialStates()) == game.getInitialStates() ? storm::utility::one<ValueType>() : storm::utility::zero<ValueType>();
+                    if (!maybeMin.isZero()) {
+                        minResult += solveMaybeStates(player1Direction, storm::OptimizationDirection::Minimize, game, maybeMin, prob01.min.second.states);
+                        storm::dd::Add<Type, ValueType> initialStateMin = initialStatesAdd * minResult;
+                        STORM_LOG_ASSERT(initialStateMin.getNonZeroCount() == 1, "Wrong number of results for initial states.");
+                        minValue = initialStateMin.getMax();
+                    }
+                    STORM_LOG_TRACE("Obtained quantitative lower bound " << minValue);
                     
-                    // If we can already answer the question, do not solve the game numerically.
+                    // Check whether we can abort the computation because of the lower value.
+                    result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, minValue);
+                    if (result) {
+                        return result;
+                    }
                     
+                    ValueType maxValue = (prob01.max.second.states && game.getInitialStates()) == game.getInitialStates() ? storm::utility::one<ValueType>() : storm::utility::zero<ValueType>();
+                    if (!maybeMax.isZero()) {
+                        maxResult += solveMaybeStates(player1Direction, storm::OptimizationDirection::Maximize, game, maybeMax, prob01.max.second.states, boost::optional<storm::dd::Add<Type, ValueType>>(minResult));
+                        storm::dd::Add<Type, ValueType> initialStateMax = (initialStatesAdd * maxResult);
+                        STORM_LOG_ASSERT(initialStateMax.getNonZeroCount() == 1, "Wrong number of results for initial states.");
+                        maxValue = initialStateMax.getMax();
+                    }
+                    STORM_LOG_TRACE("Obtained quantitative upper bound " << minValue);
+
+                    // Check whether we can abort the computation because of the upper value.
+                    result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, maxValue);
+                    if (result) {
+                        return result;
+                    }
+                    
+                    STORM_LOG_DEBUG("Obtained quantitative bounds [" << minValue << ", " << maxValue << "] on the actual value for the initial states.");
+
+                    result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, minValue, maxValue);
+                    if (result) {
+                        return result;
+                    }
                     
                     STORM_LOG_ASSERT(false, "Quantiative refinement not yet there. :)");
                 }
@@ -279,8 +406,8 @@ namespace storm {
             
             STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Minimize || prob0.hasPlayer1Strategy(), "Unable to proceed without strategy.");
             STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Minimize || prob0.hasPlayer2Strategy(), "Unable to proceed without strategy.");
-            STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || prob0.hasPlayer1Strategy(), "Unable to proceed without strategy.");
-            STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || prob0.hasPlayer2Strategy(), "Unable to proceed without strategy.");
+            STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || prob1.hasPlayer1Strategy(), "Unable to proceed without strategy.");
+            STORM_LOG_ASSERT(player2Direction != storm::OptimizationDirection::Maximize || prob1.hasPlayer2Strategy(), "Unable to proceed without strategy.");
 
             STORM_LOG_TRACE("Player 1: " << player1Direction << ", player 2: " << player2Direction << ": " << prob0.states.getNonZeroCount() << " 'no' states, " << prob1.states.getNonZeroCount() << " 'yes' states.");
             return std::make_pair(prob0, prob1);

src/solver/SymbolicGameSolver.cpp

@@ -10,12 +10,12 @@ namespace storm {
     namespace solver {
         
         template<storm::dd::DdType Type, typename ValueType>
-        SymbolicGameSolver<Type, ValueType>::SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& gameMatrix, 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) : gameMatrix(gameMatrix), allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables) {
+        SymbolicGameSolver<Type, ValueType>::SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& gameMatrix, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables) : gameMatrix(gameMatrix), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.template toAdd<ValueType>()), illegalPlayer2Mask(illegalPlayer2Mask.template toAdd<ValueType>()), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables) {
             // Intentionally left empty.
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        SymbolicGameSolver<Type, ValueType>::SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& gameMatrix, 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, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver(precision, maximalNumberOfIterations, relative), gameMatrix(gameMatrix), allRows(allRows), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables) {
+        SymbolicGameSolver<Type, ValueType>::SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& gameMatrix, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver(precision, maximalNumberOfIterations, relative), gameMatrix(gameMatrix), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.template toAdd<ValueType>()), illegalPlayer2Mask(illegalPlayer2Mask.template toAdd<ValueType>()), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables) {
             // Intentionally left empty.
         }
         
@@ -33,16 +33,18 @@ namespace storm {
                 tmp += b;
                 
                 // Now abstract from player 2 and player 1 variables.
-                switch (player2Goal) {
-                    case OptimizationDirection::Minimize: tmp = tmp.minAbstract(this->player2Variables); break;
-                    case OptimizationDirection::Maximize: tmp = tmp.maxAbstract(this->player2Variables); break;
+                if (player2Goal == storm::OptimizationDirection::Maximize) {
+                    tmp = tmp.maxAbstract(this->player2Variables);
+                } else {
+                    tmp = (tmp + illegalPlayer2Mask).minAbstract(this->player2Variables);
                 }
-                
-                switch (player1Goal) {
-                    case OptimizationDirection::Minimize: tmp = tmp.minAbstract(this->player1Variables); break;
-                    case OptimizationDirection::Maximize: tmp = tmp.maxAbstract(this->player1Variables); break;
+
+                if (player1Goal == storm::OptimizationDirection::Maximize) {
+                    tmp = tmp.maxAbstract(this->player1Variables);
+                } else {
+                    tmp = (tmp + illegalPlayer1Mask).minAbstract(this->player1Variables);
                 }
-                
+
                 // Now check if the process already converged within our precision.
                 converged = xCopy.equalModuloPrecision(tmp, precision, relative);
                 

src/solver/SymbolicGameSolver.h

@@ -25,6 +25,8 @@ namespace storm {
              *
              * @param gameMatrix The matrix defining the coefficients of the game.
              * @param allRows A BDD characterizing all rows of the equation system.
+             * @param illegalPlayer1Mask A BDD characterizing the illegal choices of player 1.
+             * @param illegalPlayer2Mask A BDD characterizing the illegal choices of player 2.
              * @param rowMetaVariables The meta variables used to encode the rows of the matrix.
              * @param columnMetaVariables The meta variables used to encode the columns of the matrix.
              * @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta
@@ -32,13 +34,15 @@ namespace storm {
              * @param player1Variables The meta variables used to encode the player 1 choices.
              * @param player2Variables The meta variables used to encode the player 2 choices.
              */
-            SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& gameMatrix, 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);
+            SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& gameMatrix, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables);
             
             /*!
              * Constructs a symbolic game solver with the given meta variable sets and pairs.
              *
              * @param gameMatrix The matrix defining the coefficients of the game.
              * @param allRows A BDD characterizing all rows of the equation system.
+             * @param illegalPlayer1Mask A BDD characterizing the illegal choices of player 1.
+             * @param illegalPlayer2Mask A BDD characterizing the illegal choices of player 2.
              * @param rowMetaVariables The meta variables used to encode the rows of the matrix.
              * @param columnMetaVariables The meta variables used to encode the columns of the matrix.
              * @param rowColumnMetaVariablePairs The pairs of row meta variables and the corresponding column meta
@@ -50,7 +54,7 @@ namespace storm {
              * equation system iteratively.
              * @param relative Sets whether or not to use a relativ stopping criterion rather than an absolute one.
              */
-            SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& gameMatrix, 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, double precision, uint_fast64_t maximalNumberOfIterations, bool relative);
+            SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& gameMatrix, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative);
             
             /*!
              * Solves the equation system defined by the game matrix. Note that the game matrix has to be given upon
@@ -71,6 +75,12 @@ namespace storm {
             // A BDD characterizing all rows of the equation system.
             storm::dd::Bdd<Type> const& allRows;
             
+            // An ADD that can be used to compensate for the illegal choices of player 1.
+            storm::dd::Add<Type> illegalPlayer1Mask;
+
+            // An ADD that can be used to compensate for the illegal choices of player 2.
+            storm::dd::Add<Type> illegalPlayer2Mask;
+
             // The row variables.
             std::set<storm::expressions::Variable> const& rowMetaVariables;
             

src/storage/dd/Add.cpp

@@ -162,6 +162,12 @@ namespace storm {
             return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.minAbstract(cube), Dd<LibraryType>::subtractMetaVariables(*this, cube));
         }
         
+        template<DdType LibraryType, typename ValueType>
+        Add<LibraryType, ValueType> Add<LibraryType, ValueType>::minAbstractExcept0(std::set<storm::expressions::Variable> const& metaVariables) const {
+            Bdd<LibraryType> cube = Bdd<LibraryType>::getCube(this->getDdManager(), metaVariables);
+            return Add<LibraryType, ValueType>(this->getDdManager(), internalAdd.minAbstractExcept0(cube), Dd<LibraryType>::subtractMetaVariables(*this, cube));
+        }
+        
         template<DdType LibraryType, typename ValueType>
         Add<LibraryType, ValueType> Add<LibraryType, ValueType>::maxAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
             Bdd<LibraryType> cube = Bdd<LibraryType>::getCube(this->getDdManager(), metaVariables);

src/storage/dd/Add.h

@@ -256,7 +256,14 @@ namespace storm {
              * @param metaVariables The meta variables from which to abstract.
              */
             Add<LibraryType, ValueType> minAbstract(std::set<storm::expressions::Variable> const& metaVariables) const;
-            
+
+            /*!
+             * Min-abstracts from the given meta variables but treats 0 as the largest possible value.
+             *
+             * @param metaVariables The meta variables from which to abstract.
+             */
+            Add<LibraryType, ValueType> minAbstractExcept0(std::set<storm::expressions::Variable> const& metaVariables) const;
+
             /*!
              * Max-abstracts from the given meta variables.
              *

src/storage/dd/cudd/InternalCuddAdd.cpp

@@ -146,6 +146,11 @@ namespace storm {
             return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MinAbstract(cube.toAdd<ValueType>().getCuddAdd()));
         }
         
+        template<typename ValueType>
+        InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::minAbstractExcept0(InternalBdd<DdType::CUDD> const& cube) const {
+            return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MinAbstractExcept0(cube.toAdd<ValueType>().getCuddAdd()));
+        }
+        
         template<typename ValueType>
         InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::maxAbstract(InternalBdd<DdType::CUDD> const& cube) const {
             return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().MaxAbstract(cube.toAdd<ValueType>().getCuddAdd()));

src/storage/dd/cudd/InternalCuddAdd.h

@@ -259,7 +259,14 @@ namespace storm {
              * @param cube The cube from which to abstract.
              */
             InternalAdd<DdType::CUDD, ValueType> minAbstract(InternalBdd<DdType::CUDD> const& cube) const;
-            
+
+            /*!
+             * Min-abstracts from the given cube, but treats 0 as the largest possible value.
+             *
+             * @param cube The cube from which to abstract.
+             */
+            InternalAdd<DdType::CUDD, ValueType> minAbstractExcept0(InternalBdd<DdType::CUDD> const& cube) const;
+
             /*!
              * Max-abstracts from the given cube.
              *

src/storage/dd/sylvan/InternalSylvanAdd.cpp

@@ -305,13 +305,25 @@ namespace storm {
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::minAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.AbstractMin(cube.sylvanBdd));
         }
-
+        
 #ifdef STORM_HAVE_CARL
 		template<>
         InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::minAbstract(InternalBdd<DdType::Sylvan> const& cube) const {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstract");
         }
 #endif
+        
+        template<typename ValueType>
+        InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::minAbstractExcept0(InternalBdd<DdType::Sylvan> const& cube) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstractExcept0");
+        }
+
+#ifdef STORM_HAVE_CARL
+        template<>
+        InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalAdd<DdType::Sylvan, storm::RationalFunction>::minAbstractExcept0(InternalBdd<DdType::Sylvan> const& cube) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented: minAbstractExcept0");
+        }
+#endif
 
         template<typename ValueType>
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::maxAbstract(InternalBdd<DdType::Sylvan> const& cube) const {

src/storage/dd/sylvan/InternalSylvanAdd.h

@@ -261,7 +261,14 @@ namespace storm {
              * @param cube The cube from which to abstract.
              */
             InternalAdd<DdType::Sylvan, ValueType> minAbstract(InternalBdd<DdType::Sylvan> const& cube) const;
-            
+
+            /*!
+             * Min-abstracts from the given cube, but treats 0 as the largest possible value.
+             *
+             * @param cube The cube from which to abstract.
+             */
+            InternalAdd<DdType::Sylvan, ValueType> minAbstractExcept0(InternalBdd<DdType::Sylvan> const& cube) const;
+
             /*!
              * Max-abstracts from the given cube.
              *

src/utility/graph.cpp

@@ -955,7 +955,7 @@ namespace storm {
                     solution = tmp;
                     ++iterations;
                 }
-
+                
                 // Since we have determined the inverse of the desired set, we need to complement it now.
                 solution = !solution && model.getReachableStates();
 

src/utility/solver.cpp

@@ -35,8 +35,8 @@ namespace storm {
             }
             
             template<storm::dd::DdType Type, typename ValueType>
-            std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> SymbolicGameSolverFactory<Type, ValueType>::create(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables) const {
-                return std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>>(new storm::solver::SymbolicGameSolver<Type, ValueType>(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables));
+            std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>> SymbolicGameSolverFactory<Type, ValueType>::create(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables) const {
+                return std::unique_ptr<storm::solver::SymbolicGameSolver<Type, ValueType>>(new storm::solver::SymbolicGameSolver<Type, ValueType>(A, allRows, illegalPlayer1Mask, illegalPlayer2Mask, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables));
             }
             
             template<typename ValueType>

src/utility/solver.h

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

test/functional/solver/FullySymbolicGameSolverTest.cpp

@@ -35,7 +35,14 @@ TEST(FullySymbolicGameSolverTest, Solve_Cudd) {
     matrix += manager->getEncoding(state.first, 1).template toAdd<double>() * manager->getEncoding(state.second, 1).template toAdd<double>() * manager->getEncoding(pl1.first, 1).template toAdd<double>() * manager->getEncoding(pl2.first, 1).template toAdd<double>() * manager->getConstant<double>(1);
     
     std::unique_ptr<storm::utility::solver::SymbolicGameSolverFactory<storm::dd::DdType::CUDD, double>> solverFactory(new storm::utility::solver::SymbolicGameSolverFactory<storm::dd::DdType::CUDD, double>());
-    std::unique_ptr<storm::solver::SymbolicGameSolver<storm::dd::DdType::CUDD>> solver = solverFactory->create(matrix, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables,player2Variables);
+
+    storm::dd::Bdd<storm::dd::DdType::CUDD> tmp = matrix.toBdd().existsAbstract({state.second});
+    storm::dd::Bdd<storm::dd::DdType::CUDD> illegalPlayer2Mask = !tmp && manager->getRange(state.first);
+    storm::dd::Bdd<storm::dd::DdType::CUDD> illegalPlayer1Mask = tmp.existsAbstract({pl2.first});
+    illegalPlayer2Mask &= illegalPlayer1Mask;
+    illegalPlayer1Mask &= !illegalPlayer1Mask && manager->getRange(state.first);
+    
+    std::unique_ptr<storm::solver::SymbolicGameSolver<storm::dd::DdType::CUDD>> solver = solverFactory->create(matrix, allRows, illegalPlayer1Mask, illegalPlayer2Mask, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables, player2Variables);
     
     // Create solution and target state vector.
     storm::dd::Add<storm::dd::DdType::CUDD, double> x = manager->template getAddZero<double>();
@@ -93,7 +100,14 @@ TEST(FullySymbolicGameSolverTest, Solve_Sylvan) {
     matrix += manager->getEncoding(state.first, 1).template toAdd<double>() * manager->getEncoding(state.second, 1).template toAdd<double>() * manager->getEncoding(pl1.first, 1).template toAdd<double>() * manager->getEncoding(pl2.first, 1).template toAdd<double>() * manager->getConstant<double>(1);
     
     std::unique_ptr<storm::utility::solver::SymbolicGameSolverFactory<storm::dd::DdType::Sylvan, double>> solverFactory(new storm::utility::solver::SymbolicGameSolverFactory<storm::dd::DdType::Sylvan, double>());
-    std::unique_ptr<storm::solver::SymbolicGameSolver<storm::dd::DdType::Sylvan>> solver = solverFactory->create(matrix, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables,player2Variables);
+    
+    storm::dd::Bdd<storm::dd::DdType::Sylvan> tmp = matrix.toBdd().existsAbstract({state.second});
+    storm::dd::Bdd<storm::dd::DdType::Sylvan> illegalPlayer2Mask = !tmp && manager->getRange(state.first);
+    storm::dd::Bdd<storm::dd::DdType::Sylvan> illegalPlayer1Mask = tmp.existsAbstract({pl2.first});
+    illegalPlayer2Mask &= illegalPlayer1Mask;
+    illegalPlayer1Mask &= !illegalPlayer1Mask && manager->getRange(state.first);
+
+    std::unique_ptr<storm::solver::SymbolicGameSolver<storm::dd::DdType::Sylvan>> solver = solverFactory->create(matrix, allRows, illegalPlayer1Mask, illegalPlayer2Mask, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables,player2Variables);
     
     // Create solution and target state vector.
     storm::dd::Add<storm::dd::DdType::Sylvan, double> x = manager->template getAddZero<double>();