fixed some bugs, added some test, added some prob1 algorithm, and did some stuff, you know?

Former-commit-id: 00fa21d1fe

resources/3rdparty/cudd-2.5.0/src/cudd/cuddBddAbs.c

@@ -540,11 +540,12 @@ cuddBddExistAbstractRepresentativeRecur(
   DdNode * f,
   DdNode * cube)
 {
+//    printf("entering exists abstract...\n");
     DdNode	*F, *T, *E, *res, *res1, *res2, *one, *zero, *left, *right, *tmp, *res1Inf, *res2Inf;
     
     statLine(manager);
     one = DD_ONE(manager);
-    zero = DD_ZERO(manager);
+    zero = Cudd_Not(one);
     F = Cudd_Regular(f);
     
     // Store whether f is negated.
@@ -553,45 +554,57 @@ cuddBddExistAbstractRepresentativeRecur(
     /* Cube is guaranteed to be a cube at this point. */
     if (F == one) {
         if (fIsNegated) {
+//            printf("return in preprocessing...\n");
             return f;
         }
         
         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. */
     
+//    printf("F perm %i and cube perm %i\n", manager->perm[F->index], manager->perm[cube->index]);
+    
     /* Abstract a variable that does not appear in f. */
     if (manager->perm[F->index] > manager->perm[cube->index]) {
         res = cuddBddExistAbstractRepresentativeRecur(manager, f, cuddT(cube));
         if (res == NULL) {
             return(NULL);
         }
-        
         cuddRef(res);
-        cuddRef(zero);
-        res1 = cuddUniqueInter(manager, (int) cube->index, zero, res);
+        
+//        res1 = cuddUniqueInter(manager, (int) cube->index, zero, res);
+        res1 = cuddBddIteRecur(manager, manager->vars[cube->index], zero, res);
+
         if (res1 == NULL) {
-            Cudd_RecursiveDeref(manager,res);
-            Cudd_RecursiveDeref(manager,zero);
+            Cudd_IterDerefBdd(manager,res);
+            Cudd_IterDerefBdd(manager,zero);
             return(NULL);
         }
-        Cudd_IterDerefBdd(manager, res);
-        cuddDeref(zero);
+        cuddDeref(res);
+
+//        printf("return after abstr. var that does not appear in f...\n");
        	return(res1);
     }
     
     /* Check the cache. */
     if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstractRepresentative, f, cube)) != NULL) {
+//        printf("return because of cache hit...\n");
         return(res);
     }
     
     /* Compute the cofactors of f. */
     T = cuddT(F); E = cuddE(F);
     if (f != F) {
+//        printf("negating T and E\n");
         T = Cudd_Not(T); E = Cudd_Not(E);
     }
     
@@ -618,8 +631,9 @@ cuddBddExistAbstractRepresentativeRecur(
             return(NULL);
         }
         if (res1 == one) {
-            if (F->ref != 1)
+            if (F->ref != 1) {
                 cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, one);
+            }
             return(one);
         }
         cuddRef(res1);
@@ -639,7 +653,6 @@ cuddBddExistAbstractRepresentativeRecur(
         }
         cuddRef(left);
 
-        cuddRef(zero);
         res1Inf = cuddBddIteRecur(manager, left, res1, zero);
         if (res1Inf == NULL) {
             Cudd_IterDerefBdd(manager,res1);
@@ -648,11 +661,9 @@ cuddBddExistAbstractRepresentativeRecur(
             return(NULL);
         }
         cuddRef(res1Inf);
-        cuddDeref(zero);
         
         Cudd_IterDerefBdd(manager,res1);
 
-        cuddRef(zero);
         res2Inf = cuddBddIteRecur(manager, left, zero, res2);
         if (res2Inf == NULL) {
             Cudd_IterDerefBdd(manager,res1);
@@ -662,36 +673,42 @@ cuddBddExistAbstractRepresentativeRecur(
             return(NULL);
         }
         cuddRef(res2Inf);
-        cuddDeref(zero);
         
         Cudd_IterDerefBdd(manager,res2);
         Cudd_IterDerefBdd(manager,left);
         
-        cuddRef(zero);
-        res = (res1Inf == res2Inf) ? cuddUniqueInter(manager, (int) f->index, zero, res1Inf) : cuddUniqueInter(manager, (int) f->index, res2Inf, res1Inf);
+        assert(res1Inf != res2Inf);
+//        res = cuddUniqueInter(manager, (int) f->index, res2Inf, res1Inf);
+        res = cuddBddIteRecur(manager, manager->vars[F->index], res2Inf, res1Inf);
+
+        if (res == NULL) {
+            Cudd_IterDerefBdd(manager,res1Inf);
+            Cudd_IterDerefBdd(manager,res2Inf);
+            return(NULL);
+        }
         cuddRef(res);
-        cuddDeref(zero);
 
         Cudd_IterDerefBdd(manager,res1Inf);
         Cudd_IterDerefBdd(manager,res2Inf);
 
-        if (res == NULL) {
-            Cudd_IterDerefBdd(manager,res);
-            return(NULL);
-        }
         cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, res);
         cuddDeref(res);
+//        printf("return properly computed result...\n");
         return(res);
     } else { /* if (cuddI(manager,F->index) < cuddI(manager,cube->index)) */
         res1 = cuddBddExistAbstractRepresentativeRecur(manager, E, cube);
-        if (res1 == NULL) return(NULL);
+        if (res1 == NULL){
+            return(NULL);
+        }
         cuddRef(res1);
+        
         res2 = cuddBddExistAbstractRepresentativeRecur(manager, T, cube);
         if (res2 == NULL) {
             Cudd_IterDerefBdd(manager, res1);
             return(NULL);
         }
         cuddRef(res2);
+        
         /* ITE takes care of possible complementation of res1 and of the
          ** case in which res1 == res2. */
         res = cuddBddIteRecur(manager, manager->vars[F->index], res2, res1);
@@ -702,8 +719,10 @@ cuddBddExistAbstractRepresentativeRecur(
         }
         cuddDeref(res1);
         cuddDeref(res2);
-        if (F->ref != 1)
+        if (F->ref != 1) {
             cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, res);
+        }
+//        printf("return of last case...\n");
         return(res);
     }	    
     

src/models/symbolic/StochasticTwoPlayerGame.cpp

@@ -28,7 +28,6 @@ namespace storm {
             : NondeterministicModel<Type>(storm::models::ModelType::S2pg, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, rewardModels), player1Variables(player1Variables), player2Variables(player2Variables) {
                 
                 // Compute legal player 1 mask.
-                transitionMatrix.exportToDot("trans.dot");
                 illegalPlayer1Mask = transitionMatrix.notZero().existsAbstract(this->getColumnVariables()).existsAbstract(this->getPlayer2Variables());
 
                 // Correct the mask for player 2. This is necessary, because it is not yet restricted to the legal choices of player 1.

src/storage/dd/CuddAdd.cpp

@@ -19,12 +19,12 @@
 
 namespace storm {
     namespace dd {
-        Add<DdType::CUDD>::Add(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddAdd, std::set<storm::expressions::Variable> const& containedMetaVariables) : Dd<DdType::CUDD>(ddManager, containedMetaVariables), cuddAdd(cuddAdd) {
+        Add<DdType::CUDD>::Add(std::weak_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddAdd, std::set<storm::expressions::Variable> const& containedMetaVariables) : Dd<DdType::CUDD>(ddManager, containedMetaVariables), cuddAdd(cuddAdd) {
             // Intentionally left empty.
         }
         
-        Add<DdType::CUDD>::Add(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables) : Dd<DdType::CUDD>(ddManager, metaVariables) {
-            cuddAdd = fromVector(ddManager, values, odd, metaVariables);
+        Add<DdType::CUDD>::Add(std::weak_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables) : Dd<DdType::CUDD>(ddManager, metaVariables) {
+            cuddAdd = fromVector(ddManager.lock(), values, odd, metaVariables);
         }
         
         Bdd<DdType::CUDD> Add<DdType::CUDD>::toBdd() const {

src/storage/dd/CuddAdd.h

@@ -46,7 +46,7 @@ namespace storm {
              * @param odd An ODD that is used to do the translation.
              * @param metaVariables The meta variables to use to encode the vector.
              */
-            Add(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables);
+            Add(std::weak_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& values, Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables);
             
             // Instantiate all copy/move constructors/assignments with the default implementation.
             Add() = default;
@@ -695,7 +695,7 @@ namespace storm {
              * @param cuddAdd The CUDD ADD to store.
              * @param containedMetaVariables The meta variables that appear in the DD.
              */
-            Add(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddAdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
+            Add(std::weak_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddAdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
             
             /*!
              * Converts the ADD to a row-grouped (sparse) double matrix. If the optional vector is given, it is also

src/storage/dd/CuddBdd.cpp

@@ -16,23 +16,23 @@
 
 namespace storm {
     namespace dd {
-        Bdd<DdType::CUDD>::Bdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddBdd, std::set<storm::expressions::Variable> const& containedMetaVariables) : Dd<DdType::CUDD>(ddManager, containedMetaVariables), cuddBdd(cuddBdd) {
+        Bdd<DdType::CUDD>::Bdd(std::weak_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddBdd, std::set<storm::expressions::Variable> const& containedMetaVariables) : Dd<DdType::CUDD>(ddManager, containedMetaVariables), cuddBdd(cuddBdd) {
             // Intentionally left empty.
         }
         
-        Bdd<DdType::CUDD>::Bdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value) : Dd<DdType::CUDD>(ddManager, metaVariables) {
+        Bdd<DdType::CUDD>::Bdd(std::weak_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value) : Dd<DdType::CUDD>(ddManager, metaVariables) {
             switch (comparisonType) {
                 case storm::logic::ComparisonType::Less:
-                    this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater<double>(), value, std::placeholders::_1));
+                    this->cuddBdd = fromVector<double>(ddManager.lock(), explicitValues, odd, metaVariables, std::bind(std::greater<double>(), value, std::placeholders::_1));
                     break;
                 case storm::logic::ComparisonType::LessEqual:
-                    this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal<double>(), value, std::placeholders::_1));
+                    this->cuddBdd = fromVector<double>(ddManager.lock(), explicitValues, odd, metaVariables, std::bind(std::greater_equal<double>(), value, std::placeholders::_1));
                     break;
                 case storm::logic::ComparisonType::Greater:
-                    this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less<double>(), value, std::placeholders::_1));
+                    this->cuddBdd = fromVector<double>(ddManager.lock(), explicitValues, odd, metaVariables, std::bind(std::less<double>(), value, std::placeholders::_1));
                     break;
                 case storm::logic::ComparisonType::GreaterEqual:
-                    this->cuddBdd = fromVector<double>(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal<double>(), value, std::placeholders::_1));
+                    this->cuddBdd = fromVector<double>(ddManager.lock(), explicitValues, odd, metaVariables, std::bind(std::less_equal<double>(), value, std::placeholders::_1));
                     break;
             }
         }

src/storage/dd/CuddBdd.h

@@ -43,7 +43,7 @@ namespace storm {
              * @param comparisonType The relation that needs to hold for the values (wrt. to the given value).
              * @param value The value to compare with.
              */
-            Bdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value);
+            Bdd(std::weak_ptr<DdManager<DdType::CUDD> const> ddManager, std::vector<double> const& explicitValues, storm::dd::Odd<DdType::CUDD> const& odd, std::set<storm::expressions::Variable> const& metaVariables, storm::logic::ComparisonType comparisonType, double value);
             
             // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD.
             friend class DdManager<DdType::CUDD>;
@@ -325,7 +325,7 @@ namespace storm {
              * @param cuddBdd The CUDD BDD to store.
              * @param containedMetaVariables The meta variables that appear in the DD.
              */
-            Bdd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddBdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
+            Bdd(std::weak_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddBdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
             
             /*!
              * Builds a BDD representing the values that make the given filter function evaluate to true.

src/storage/dd/CuddDd.cpp

@@ -5,7 +5,7 @@
 
 namespace storm {
     namespace dd {
-        Dd<DdType::CUDD>::Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), containedMetaVariables(containedMetaVariables) {
+        Dd<DdType::CUDD>::Dd(std::weak_ptr<DdManager<DdType::CUDD> const> ddManager, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), containedMetaVariables(containedMetaVariables) {
             // Intentionally left empty.
         }
                 
@@ -26,7 +26,7 @@ namespace storm {
         }
         
         std::shared_ptr<DdManager<DdType::CUDD> const> Dd<DdType::CUDD>::getDdManager() const {
-            return this->ddManager;
+            return this->ddManager.lock();
         }
 
         void Dd<DdType::CUDD>::addMetaVariables(std::set<storm::expressions::Variable> const& metaVariables) {

src/storage/dd/CuddDd.h

@@ -173,12 +173,12 @@ namespace storm {
              * @param ddManager The manager responsible for this DD.
              * @param containedMetaVariables The meta variables that appear in the DD.
              */
-            Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
+            Dd(std::weak_ptr<DdManager<DdType::CUDD> const> ddManager, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
             
         private:
             
             // A pointer to the manager responsible for this DD.
-            std::shared_ptr<DdManager<DdType::CUDD> const> ddManager;
+            std::weak_ptr<DdManager<DdType::CUDD> const> ddManager;
             
             // The meta variables that appear in this DD.
             std::set<storm::expressions::Variable> containedMetaVariables;

src/storage/dd/CuddDdManager.cpp

@@ -2,6 +2,8 @@
 #include <string>
 #include <algorithm>
 
+#include "storm-config.h"
+
 #include "src/storage/dd/CuddDdManager.h"
 #include "src/utility/macros.h"
 #include "src/storage/expressions/Variable.h"
@@ -10,12 +12,11 @@
 #include "src/settings/modules/CuddSettings.h"
 #include "src/storage/expressions/ExpressionManager.h"
 #include "src/storage/dd/CuddAdd.h"
-#include "CuddBdd.h"
-
+#include "src/storage/dd/CuddBdd.h"
 
 namespace storm {
     namespace dd {
-        DdManager<DdType::CUDD>::DdManager() : metaVariableMap(), cuddManager(), reorderingTechnique(CUDD_REORDER_NONE), manager(new storm::expressions::ExpressionManager()) {
+        DdManager<DdType::CUDD>::DdManager() : cuddManager(), metaVariableMap(), reorderingTechnique(CUDD_REORDER_NONE), manager(new storm::expressions::ExpressionManager()) {
             this->cuddManager.SetMaxMemory(static_cast<unsigned long>(storm::settings::cuddSettings().getMaximalMemory() * 1024ul * 1024ul));
             this->cuddManager.SetEpsilon(storm::settings::cuddSettings().getConstantPrecision());
             
@@ -43,6 +44,12 @@ namespace storm {
             }
         }
         
+        DdManager<DdType::CUDD>::~DdManager() {
+#ifndef NDEBUG
+            cuddManager.DebugCheck();
+#endif
+        }
+        
         Bdd<DdType::CUDD> DdManager<DdType::CUDD>::getBddOne() const {
             return Bdd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddOne());
         }

src/storage/dd/CuddDdManager.h

@@ -34,6 +34,11 @@ namespace storm {
              */
             DdManager();
             
+            /*!
+             * Destroys the manager. In debug mode, this will check for errors with CUDD.
+             */
+            ~DdManager();
+            
             // Explictly forbid copying a DdManager, but allow moving it.
             DdManager(DdManager<DdType::CUDD> const& other) = delete;
 			DdManager<DdType::CUDD>& operator=(DdManager<DdType::CUDD> const& other) = delete;
@@ -225,12 +230,14 @@ namespace storm {
              */
             storm::expressions::ExpressionManager& getExpressionManager();
             
+            // The manager responsible for the DDs created/modified with this DdManager. This member strictly needs to
+            // the first member of the class: upon destruction, the meta variables still destruct DDs that are managed
+            // by this manager, so we have to make sure it still exists at this point and is destructed later.
+            Cudd cuddManager;
+
             // A mapping from variables to the meta variable information.
             std::unordered_map<storm::expressions::Variable, DdMetaVariable<DdType::CUDD>> metaVariableMap;
             
-            // The manager responsible for the DDs created/modified with this DdManager.
-            Cudd cuddManager;
-            
             // The technique that is used for dynamic reordering.
             Cudd_ReorderingType reorderingTechnique;
 

src/storage/dd/CuddDdMetaVariable.cpp

@@ -3,14 +3,14 @@
 
 namespace storm {
     namespace dd {
-        DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Bdd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), cube(manager->getBddOne()), manager(manager) {
+        DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Bdd<DdType::CUDD>> const& ddVariables, std::weak_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), cube(manager.lock()->getBddOne()), manager(manager) {
             // Create the cube of all variables of this meta variable.
             for (auto const& ddVariable : this->ddVariables) {
                 this->cube &= ddVariable;
             }
         }
         
-        DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, std::vector<Bdd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Bool), low(0), high(1), ddVariables(ddVariables), cube(manager->getBddOne()), manager(manager) {
+        DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, std::vector<Bdd<DdType::CUDD>> const& ddVariables, std::weak_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Bool), low(0), high(1), ddVariables(ddVariables), cube(manager.lock()->getBddOne()), manager(manager) {
             // Create the cube of all variables of this meta variable.
             for (auto const& ddVariable : this->ddVariables) {
                 this->cube &= ddVariable;
@@ -38,7 +38,7 @@ namespace storm {
         }
         
         std::shared_ptr<DdManager<DdType::CUDD>> DdMetaVariable<DdType::CUDD>::getDdManager() const {
-            return this->manager;
+            return this->manager.lock();
         }
 
         std::vector<Bdd<DdType::CUDD>> const& DdMetaVariable<DdType::CUDD>::getDdVariables() const {

src/storage/dd/CuddDdMetaVariable.h

@@ -42,7 +42,7 @@ namespace storm {
              * @param ddVariables The vector of variables used to encode this variable.
              * @param manager A pointer to the manager that is responsible for this meta variable.
              */
-            DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Bdd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager);
+            DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Bdd<DdType::CUDD>> const& ddVariables, std::weak_ptr<DdManager<DdType::CUDD>> manager);
             
             /*!
              * Creates a boolean meta variable with the given name.
@@ -50,7 +50,7 @@ namespace storm {
              * @param ddVariables The vector of variables used to encode this variable.
              * @param manager A pointer to the manager that is responsible for this meta variable.
              */
-            DdMetaVariable(std::string const& name, std::vector<Bdd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager);
+            DdMetaVariable(std::string const& name, std::vector<Bdd<DdType::CUDD>> const& ddVariables, std::weak_ptr<DdManager<DdType::CUDD>> manager);
             
             // Explictly generate all default versions of copy/move constructors/assignments.
             DdMetaVariable(DdMetaVariable const& other) = default;
@@ -136,7 +136,7 @@ namespace storm {
             Bdd<DdType::CUDD> cube;
             
             // A pointer to the manager responsible for this meta variable.
-            std::shared_ptr<DdManager<DdType::CUDD>> manager;
+            std::weak_ptr<DdManager<DdType::CUDD>> manager;
         };
     }
 }

src/utility/graph.cpp

@@ -690,7 +690,7 @@ namespace storm {
             }
             
             template <storm::dd::DdType Type>
-            GameProb01Result<Type> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<Type> 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) {
+            GameProb01Result<Type> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<Type> 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) {
 
                 // The solution set.
                 storm::dd::Bdd<Type> solution = psiStates;
@@ -724,29 +724,136 @@ namespace storm {
                 
                 // Since we have determined the inverse of the desired set, we need to complement it now.
                 solution = !solution && model.getReachableStates();
+
+                // Determine all transitions between prob0 states.
+                storm::dd::Bdd<Type> transitionsBetweenProb0States = solution && (transitionMatrix && solution.swapVariables(model.getRowColumnMetaVariablePairs()));
+                
+                // Determine the distributions that have only successors that are prob0 states.
+                storm::dd::Bdd<Type> onlyProb0Successors = (transitionsBetweenProb0States || model.getIllegalSuccessorMask()).universalAbstract(model.getColumnVariables());
+                
+                boost::optional<storm::dd::Bdd<Type>> player2StrategyBdd;
+                if (produceStrategies && player2Strategy == OptimizationDirection::Minimize) {
+                    // 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) {
+                    // Move from player 2 choices with only prob0 successors to player 1 choices with only prob 0 successors.
+                    onlyProb0Successors = onlyProb0Successors.existsAbstract(model.getPlayer2Variables());
+                    
+                    // Pick a prob0 player 2 state.
+                    player1StrategyBdd = onlyProb0Successors.existsAbstractRepresentative(model.getPlayer1Variables());
+                }
+                
+                return GameProb01Result<Type>(solution, player1StrategyBdd, player2StrategyBdd);
+            }
+            
+            template <storm::dd::DdType Type>
+            GameProb01Result<Type> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<Type> 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) {
                 
-                return GameProb01Result<Type>(solution);
+                // 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;
+                boost::optional<storm::dd::Bdd<Type>> player1StrategyBdd;
+                boost::optional<storm::dd::Bdd<Type>> consideredPlayer1States;
+                boost::optional<storm::dd::Bdd<Type>> player2StrategyBdd;
+                boost::optional<storm::dd::Bdd<Type>> consideredPlayer2States;
+
+                bool maybeStatesDone = false;
+                uint_fast64_t maybeStateIterations = 0;
+                while (!maybeStatesDone || produceStrategiesInIteration) {
+                    bool solutionStatesDone = false;
+                    uint_fast64_t solutionStateIterations = 0;
+                    
+                    // If we are to produce strategies in this iteration, we prepare some storage.
+                    if (produceStrategiesInIteration) {
+                        player1StrategyBdd = model.getManager().getBddZero();
+                        consideredPlayer1States = model.getManager().getBddZero();
+                        player2StrategyBdd = model.getManager().getBddZero();
+                        consideredPlayer2States = model.getManager().getBddZero();
+                    }
+                    
+                    while (!solutionStatesDone) {
+                        // Start by computing the transitions that have only maybe states as successors. Note that at
+                        // this point, there may be illegal transitions.
+                        storm::dd::Bdd<Type> distributionsStayingInMaybe = (!transitionMatrix || maybeStates.swapVariables(model.getRowColumnMetaVariablePairs())).universalAbstract(model.getColumnVariables());
+                        
+                        // Then, determine all distributions that have at least one successor in the states that have
+                        // probability 1.
+                        storm::dd::Bdd<Type> distributionsWithProb1Successor = (transitionMatrix && solution.swapVariables(model.getRowColumnMetaVariablePairs())).existsAbstract(model.getColumnVariables());
+                        
+                        // 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) {
+                            valid = (valid || model.getIllegalPlayer2Mask()).universalAbstract(model.getPlayer2Variables());
+                        } else {
+                            if (produceStrategiesInIteration) {
+                                storm::dd::Bdd<Type> newValidDistributions = valid && !consideredPlayer2States.get();
+                                player2StrategyBdd.get() = player2StrategyBdd.get() || newValidDistributions.existsAbstractRepresentative(model.getPlayer2Variables());
+                            }
+
+                            valid = valid.existsAbstract(model.getPlayer2Variables());
+                            
+                            if (produceStrategiesInIteration) {
+                                consideredPlayer2States.get() |= valid;
+                            }
+                        }
+                        
+                        // And do the same for player 1.
+                        if (player1Strategy == OptimizationDirection::Minimize) {
+                            valid = (valid || model.getIllegalPlayer1Mask()).universalAbstract(model.getPlayer1Variables());
+                        } else {
+                            if (produceStrategiesInIteration) {
+                                storm::dd::Bdd<Type> newValidDistributions = valid && !consideredPlayer1States.get();
+                                player1StrategyBdd.get() = player1StrategyBdd.get() || newValidDistributions.existsAbstractRepresentative(model.getPlayer1Variables());
+                            }
+
+                            valid = valid.existsAbstract(model.getPlayer1Variables());
+                            
+                            if (produceStrategiesInIteration) {
+                                consideredPlayer1States.get() |= valid;
+                            }
+                        }
+                        
+                        // Add psi states to result.
+                        valid |= psiStates;
+                        
+                        // If no new states were added, we have found the current hypothesis for the states with
+                        // probability 1.
+                        if (valid == solution) {
+                            solutionStatesDone = true;
+                        } else {
+                            solution = valid;
+                        }
+                        ++solutionStateIterations;
+                    }
+                    
+                    // If the states with probability 1 and the potential probability 1 states coincide, we have found
+                    // the solution.
+                    if (solution == maybeStates) {
+                        maybeStatesDone = true;
+                        
+                        // 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 = produceStrategies && (player1Strategy == OptimizationDirection::Maximize || player2Strategy == OptimizationDirection::Maximize);
+                    } else {
+                        // Otherwise, we use the current hypothesis for the states with probability 1 as the new maybe
+                        // state set.
+                        maybeStates = solution;
+                    }
+                    ++maybeStateIterations;
+                }
                 
-//                // Determine all transitions between prob0 states.
-//                storm::dd::Bdd<Type> transitionsBetweenProb0States = solution && (transitionMatrix && solution.swapVariables(model.getRowColumnMetaVariablePairs()));
-//                
-//                // Determine the distributions that have only successors that are prob0 states.
-//                storm::dd::Bdd<Type> onlyProb0Successors = (transitionsBetweenProb0States || model.getIllegalSuccessorMask()).universalAbstract(model.getColumnVariables());
-//                
-//                boost::optional<storm::dd::Bdd<Type>> player2StrategyBdd;
-//                if (player2Strategy == OptimizationDirection::Minimize) {
-//                    // Pick a distribution that has only prob0 successors.
-//                    player2StrategyBdd = onlyProb0Successors.existsAbstractRepresentative(model.getPlayer2Variables());
-//                }
-//                
-//                boost::optional<storm::dd::Bdd<Type>> player1StrategyBdd;
-//                if (player1Strategy == OptimizationDirection::Minimize) {
-//                    // Move from player 2 choices with only prob0 successors to player 1 choices with only prob 0 successors.
-//                    onlyProb0Successors = onlyProb0Successors.existsAbstract(model.getPlayer2Variables());
-//                    
-//                    // Pick a prob0 player 2 state.
-//                    onlyProb0Successors.existsAbstractRepresentative(model.getPlayer1Variables());
-//                }
+                return GameProb01Result<Type>(solution, player1StrategyBdd, player2StrategyBdd);
             }
             
             template <typename T>
@@ -1081,8 +1188,10 @@ 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> 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> 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);
-            
+            template GameProb01Result<storm::dd::DdType::CUDD> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<storm::dd::DdType::CUDD> 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> 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);
+
         } // namespace graph
     } // namespace utility
 } // namespace storm

src/utility/graph.h

@@ -451,9 +451,24 @@ 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.
              */
             template <storm::dd::DdType Type>
-            GameProb01Result<Type> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<Type> 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);
+            GameProb01Result<Type> performProb0(storm::models::symbolic::StochasticTwoPlayerGame<Type> 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);
+            
+            /*!
+             * Computes the set of states that have probability 1 given the strategies of the two players.
+             *
+             * @param model The (symbolic) model for which to compute the set of states.
+             * @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.
+             */
+            template <storm::dd::DdType Type>
+            GameProb01Result<Type> performProb1(storm::models::symbolic::StochasticTwoPlayerGame<Type> 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);
             
             /*!
              * Performs a topological sort of the states of the system according to the given transitions.

test/functional/abstraction/PrismMenuGameTest.cpp

@@ -29,7 +29,7 @@ TEST(PrismMenuGame, DieAbstractionTest) {
     
     storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
     
-    EXPECT_EQ(15, game.getNumberOfTransitions());
+    EXPECT_EQ(10, game.getNumberOfTransitions());
     EXPECT_EQ(2, game.getNumberOfStates());
 }
 
@@ -47,7 +47,7 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest) {
 
     storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
     
-    EXPECT_EQ(15, game.getNumberOfTransitions());
+    EXPECT_EQ(10, game.getNumberOfTransitions());
     EXPECT_EQ(3, game.getNumberOfStates());
 }
 
@@ -95,7 +95,7 @@ TEST(PrismMenuGame, CrowdsAbstractionTest) {
     
     storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
     
-    EXPECT_EQ(16, game.getNumberOfTransitions());
+    EXPECT_EQ(11, game.getNumberOfTransitions());
     EXPECT_EQ(2, game.getNumberOfStates());
 }
 
@@ -114,7 +114,7 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) {
     
     storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
     
-    EXPECT_EQ(38, game.getNumberOfTransitions());
+    EXPECT_EQ(28, game.getNumberOfTransitions());
     EXPECT_EQ(4, game.getNumberOfStates());
 }
 
@@ -204,7 +204,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest) {
     
     storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
     
-    EXPECT_EQ(58, game.getNumberOfTransitions());
+    EXPECT_EQ(34, game.getNumberOfTransitions());
     EXPECT_EQ(4, game.getNumberOfStates());
 }
 
@@ -225,7 +225,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) {
 
     storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
 
-    EXPECT_EQ(212, game.getNumberOfTransitions());
+    EXPECT_EQ(164, game.getNumberOfTransitions());
     EXPECT_EQ(8, game.getNumberOfStates());
 }
 
@@ -295,7 +295,7 @@ TEST(PrismMenuGame, WlanAbstractionTest) {
     
     storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
     
-    EXPECT_EQ(307, game.getNumberOfTransitions());
+    EXPECT_EQ(277, game.getNumberOfTransitions());
     EXPECT_EQ(4, game.getNumberOfStates());
 }
 
@@ -317,7 +317,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) {
 
     storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
 
-    EXPECT_EQ(612, game.getNumberOfTransitions());
+    EXPECT_EQ(556, game.getNumberOfTransitions());
     EXPECT_EQ(8, game.getNumberOfStates());
 }
 

test/functional/builder/die.pm

@@ -29,4 +29,4 @@ label "three" = s=7&d=3;
 label "four" = s=7&d=4;
 label "five" = s=7&d=5;
 label "six" = s=7&d=6;
-label "done" = s=7;
+label "done" = s=7;

test/functional/utility/GraphTest.cpp

@@ -96,7 +96,7 @@ TEST(GraphTest, SymbolicProb01MinMax) {
 
 #include "src/utility/solver.h"
 
-TEST(GraphTest, SymbolicProb0StochasticGame) {
+TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
     
     std::vector<storm::expressions::Expression> initialPredicates;
@@ -107,18 +107,148 @@ TEST(GraphTest, SymbolicProb0StochasticGame) {
     storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
     
     storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
+
+    game.getQualitativeTransitionMatrix().toAdd().exportToDot("trans.dot");
+    
+    // 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);
+    EXPECT_EQ(1, result.states.getNonZeroCount());
+    EXPECT_TRUE(static_cast<bool>(result.player1Strategy));
+    EXPECT_TRUE(static_cast<bool>(result.player2Strategy));
     
-    storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result1 = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), game.getStates(initialPredicates.front(), true), storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize);
-    EXPECT_EQ(1, result1.states.getNonZeroCount());
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true);
+    EXPECT_EQ(1, result.states.getNonZeroCount());
+    
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
+    EXPECT_EQ(1, result.states.getNonZeroCount());
+
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
+    EXPECT_EQ(1, result.states.getNonZeroCount());
     
-    storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result2 = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), game.getStates(initialPredicates.front(), true), storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize);
-    EXPECT_EQ(1, result2.states.getNonZeroCount());
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
+    EXPECT_EQ(0, result.states.getNonZeroCount());
 
-    storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result3 = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), game.getStates(initialPredicates.front(), true), storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize);
-    EXPECT_EQ(0, result3.states.getNonZeroCount());
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
+    EXPECT_EQ(2, result.states.getNonZeroCount());
+    
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
+    EXPECT_EQ(0, result.states.getNonZeroCount());
+    
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
+    EXPECT_EQ(2, result.states.getNonZeroCount());
+    
+    EXPECT_TRUE(static_cast<bool>(result.player1Strategy));
+    EXPECT_TRUE(static_cast<bool>(result.player2Strategy));
+    
+    result.player1Strategy.get().toAdd().exportToDot("player1.dot");
+    result.player2Strategy.get().toAdd().exportToDot("player2.dot");
+    exit(-1);
+    
+    abstractProgram.refine({manager.getVariableExpression("s") < manager.integer(2)});
+    game = abstractProgram.getAbstractGame();
 
-    storm::utility::graph::GameProb01Result<storm::dd::DdType::CUDD> result4 = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), game.getStates(initialPredicates.front(), true), storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize);
-    EXPECT_EQ(0, result4.states.getNonZeroCount());
+    // 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);
+    EXPECT_EQ(0, result.states.getNonZeroCount());
+
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true);
+    EXPECT_EQ(3, result.states.getNonZeroCount());
+    
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
+    EXPECT_EQ(0, result.states.getNonZeroCount());
+
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
+    EXPECT_EQ(3, result.states.getNonZeroCount());
+
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
+    EXPECT_EQ(0, result.states.getNonZeroCount());
+
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
+    EXPECT_EQ(3, result.states.getNonZeroCount());
+    
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
+    EXPECT_EQ(0, result.states.getNonZeroCount());
+
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
+    EXPECT_EQ(3, result.states.getNonZeroCount());
+}
+
+TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    program = program.substituteConstants();
+    program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(7));
+    
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(6));
+    
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(7));
+    
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6));
+    
+    storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
+
+    // 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);
+    EXPECT_EQ(153, result.states.getNonZeroCount());
+    
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true);
+    EXPECT_EQ(1, result.states.getNonZeroCount());
+    
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
+    EXPECT_EQ(153, result.states.getNonZeroCount());
+    
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, true);
+    EXPECT_EQ(1, result.states.getNonZeroCount());
+    
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
+    EXPECT_EQ(153, result.states.getNonZeroCount());
+    
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, true);
+    EXPECT_EQ(1, result.states.getNonZeroCount());
+    
+    result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
+    EXPECT_EQ(153, result.states.getNonZeroCount());
+    
+    result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true);
+    EXPECT_EQ(1, result.states.getNonZeroCount());
 }
 
 #endif