Qualitative modelchecking algorithms for MDPs using BDDs. Not yet bugfixed.

Former-commit-id: 3215a38c44

src/builder/DdPrismModelBuilder.cpp

@@ -709,7 +709,7 @@ namespace storm {
                 STORM_LOG_TRACE("Iteration " << iteration << " of computing reachable states.");
                 changed = false;
                 storm::dd::Dd<Type> tmp = reachableStatesBdd.andExists(transitionBdd, generationInfo.rowMetaVariables);
-                tmp.swapVariables(generationInfo.rowColumnMetaVariablePairs);
+                tmp = tmp.swapVariables(generationInfo.rowColumnMetaVariablePairs);
 
                 storm::dd::Dd<Type> newReachableStates = tmp && (!reachableStatesBdd);
                 

src/models/symbolic/Model.cpp

@@ -53,6 +53,7 @@ namespace storm {
             
             template<storm::dd::DdType Type>
             storm::dd::Dd<Type> Model<Type>::getStates(std::string const& label) const {
+                STORM_LOG_THROW(labelToExpressionMap.find(label) != labelToExpressionMap.end(), storm::exceptions::InvalidArgumentException, "The label " << label << " is invalid for the labeling of the model.");
                 return rowExpressionAdapter->translateExpression(labelToExpressionMap.at(label)) && this->reachableStates;
             }
             

src/models/symbolic/NondeterministicModel.cpp

@@ -20,7 +20,10 @@ namespace storm {
                                                                boost::optional<storm::dd::Dd<Type>> const& optionalStateRewardVector,
                                                                boost::optional<storm::dd::Dd<Type>> const& optionalTransitionRewardMatrix)
             : Model<Type>(modelType, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, labelToExpressionMap, optionalStateRewardVector, optionalTransitionRewardMatrix), nondeterminismVariables(nondeterminismVariables) {
-                // Intentionally left empty.
+                
+                // Prepare the mask of illegal nondeterministic choices.
+                illegalMask = transitionMatrix.notZero().existsAbstract(this->getColumnVariables());
+                illegalMask = !illegalMask && reachableStates;
             }
             
             template<storm::dd::DdType Type>
@@ -37,6 +40,11 @@ namespace storm {
                 return nondeterminismVariables;
             }
             
+            template<storm::dd::DdType Type>
+            storm::dd::Dd<Type> const& NondeterministicModel<Type>::getIllegalMask() const {
+                return illegalMask;
+            }
+            
             template<storm::dd::DdType Type>
             void NondeterministicModel<Type>::printModelInformationToStream(std::ostream& out) const {
                 out << "-------------------------------------------------------------- " << std::endl;

src/models/symbolic/NondeterministicModel.h

@@ -71,12 +71,22 @@ namespace storm {
                  */
                 std::set<storm::expressions::Variable> const& getNondeterminismVariables() const;
                 
+                /*!
+                 * Retrieves a BDD characterizing all illegal nondeterminism encodings in the model.
+                 *
+                 * @return A BDD characterizing all illegal nondeterminism encodings in the model.
+                 */
+                storm::dd::Dd<Type> const& getIllegalMask() const;
+                
                 virtual void printModelInformationToStream(std::ostream& out) const override;
                 
             private:
                 
                 // The meta variables encoding the nondeterminism in the model.
                 std::set<storm::expressions::Variable> nondeterminismVariables;
+                
+                // A mask that characterizes all legal nondeterministic choices.
+                storm::dd::Dd<Type> illegalMask;
             };
             
         } // namespace symbolic

src/storage/dd/CuddDd.cpp

@@ -252,7 +252,6 @@ namespace storm {
                 STORM_LOG_WARN_COND(false, "Performing logical iff on two DDs of different type.");
                 return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables);
             }
-            return *this;
         }
 
         Dd<DdType::CUDD> Dd<DdType::CUDD>::exclusiveOr(Dd<DdType::CUDD> const& other) const {
@@ -263,12 +262,18 @@ namespace storm {
             } else if (this->isMtbdd() && other.isMtbdd()) {
                 // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that
                 // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise.
-                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Xnor(other.getCuddMtbdd()), metaVariables);
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Xor(other.getCuddMtbdd()), metaVariables);
             } else {
                 STORM_LOG_WARN_COND(false, "Performing logical iff on two DDs of different type.");
                 return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables);
             }
-            return *this;
+        }
+        
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::implies(Dd<DdType::CUDD> const& other) const {
+            std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+            metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+            STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operatiorn on MTBDDs.");
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getOne().getCuddBdd()), metaVariables);
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::equals(Dd<DdType::CUDD> const& other) const {
@@ -422,7 +427,8 @@ namespace storm {
             }
         }
         
-        void Dd<DdType::CUDD>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) {
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) {
+            std::set<storm::expressions::Variable> newContainedMetaVariables;
             if (this->isBdd()) {
                 std::vector<BDD> from;
                 std::vector<BDD> to;
@@ -431,19 +437,14 @@ namespace storm {
                     DdMetaVariable<DdType::CUDD> const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second);
                     
                     // Check if it's legal so swap the meta variables.
-                    if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) {
-                        throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size.";
-                    }
+                    STORM_LOG_THROW(variable1.getNumberOfDdVariables() == variable2.getNumberOfDdVariables(), storm::exceptions::InvalidArgumentException, "Unable to swap meta variables with different size.");
                     
                     // Keep track of the contained meta variables in the DD.
-                    bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first);
-                    bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second);
-                    if (containsVariable1 && !containsVariable2) {
-                        this->removeContainedMetaVariable(metaVariablePair.first);
-                        this->addContainedMetaVariable(metaVariablePair.second);
-                    } else if (!containsVariable1 && containsVariable2) {
-                        this->removeContainedMetaVariable(metaVariablePair.second);
-                        this->addContainedMetaVariable(metaVariablePair.first);
+                    if (this->containsMetaVariable(metaVariablePair.first)) {
+                        newContainedMetaVariables.insert(metaVariablePair.second);
+                    }
+                    if (this->containsMetaVariable(metaVariablePair.second)) {
+                        newContainedMetaVariables.insert(metaVariablePair.first);
                     }
                     
                     // Add the variables to swap to the corresponding vectors.
@@ -456,7 +457,7 @@ namespace storm {
                 }
                 
                 // Finally, call CUDD to swap the variables.
-                this->cuddDd = this->getCuddBdd().SwapVariables(from, to);
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().SwapVariables(from, to), newContainedMetaVariables);
             } else {
                 std::vector<ADD> from;
                 std::vector<ADD> to;
@@ -470,14 +471,11 @@ namespace storm {
                     }
                     
                     // Keep track of the contained meta variables in the DD.
-                    bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first);
-                    bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second);
-                    if (containsVariable1 && !containsVariable2) {
-                        this->removeContainedMetaVariable(metaVariablePair.first);
-                        this->addContainedMetaVariable(metaVariablePair.second);
-                    } else if (!containsVariable1 && containsVariable2) {
-                        this->removeContainedMetaVariable(metaVariablePair.second);
-                        this->addContainedMetaVariable(metaVariablePair.first);
+                    if (this->containsMetaVariable(metaVariablePair.first)) {
+                        newContainedMetaVariables.insert(metaVariablePair.second);
+                    }
+                    if (this->containsMetaVariable(metaVariablePair.second)) {
+                        newContainedMetaVariables.insert(metaVariablePair.first);
                     }
                     
                     // Add the variables to swap to the corresponding vectors.
@@ -490,7 +488,7 @@ namespace storm {
                 }
                 
                 // Finally, call CUDD to swap the variables.
-                this->cuddDd = this->getCuddMtbdd().SwapVariables(from, to);
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().SwapVariables(from, to), newContainedMetaVariables);
             }
         }
         

src/storage/dd/CuddDd.h

@@ -111,6 +111,14 @@ namespace storm {
              */
             Dd<DdType::CUDD> exclusiveOr(Dd<DdType::CUDD> const& other) const;
             
+            /*!
+             * Performs a logical implication of the current and the given DD.
+             *
+             * @param other The second DD used for the operation.
+             * @return The logical implication of the operands.
+             */
+            Dd<DdType::CUDD> implies(Dd<DdType::CUDD> const& other) const;
+            
             /*!
              * Adds the two DDs.
              *
@@ -317,8 +325,9 @@ namespace storm {
              * the same number of underlying DD variables.
              *
              * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another.
+             * @return The resulting DD.
              */
-            void swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs);
+            Dd<DdType::CUDD> swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs);
             
             /*!
              * Multiplies the current DD (representing a matrix) with the given matrix by summing over the given meta

src/utility/graph.h

@@ -274,7 +274,7 @@ namespace storm {
                 storm::dd::Dd<Type> transitionMatrixBdd = model.getTransitionMatrix().notZero();
                 while (lastIterationStates != statesWithProbabilityGreater0) {
                     lastIterationStates = statesWithProbabilityGreater0;
-                    statesWithProbabilityGreater0.swapVariables(model.getRowColumnMetaVariablePairs());
+                    statesWithProbabilityGreater0 = statesWithProbabilityGreater0.swapVariables(model.getRowColumnMetaVariablePairs());
                     statesWithProbabilityGreater0 &= transitionMatrixBdd;
                     statesWithProbabilityGreater0 = statesWithProbabilityGreater0.existsAbstract(model.getColumnVariables());
                     statesWithProbabilityGreater0 &= phiStatesBdd;
@@ -700,6 +700,194 @@ namespace storm {
                 return performProb01Min(model.getTransitionMatrix(), model.getTransitionMatrix().getRowGroupIndices(), model.getBackwardTransitions(), phiStates, psiStates);
             }
             
+            /*!
+             * Computes the set of states for which there exists a scheduler that achieves a probability greater than
+             * zero of satisfying phi until psi.
+             *
+             * @param model The (symbolic) model for which to compute the set of states.
+             * @param phiStates The phi states of the model.
+             * @param psiStates The psi states of the model.
+             * @return A DD representing all such states.
+             */
+            template <storm::dd::DdType Type>
+            storm::dd::Dd<Type> performProbGreater0E(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Dd<Type> const& phiStates, storm::dd::Dd<Type> const& psiStates) {
+                // Initialize environment for backward search.
+                storm::dd::DdManager<Type> const& manager = model.getManager();
+                storm::dd::Dd<Type> lastIterationStates = manager.getZero();
+                storm::dd::Dd<Type> statesWithProbabilityGreater0E = psiStates.toBdd();
+                storm::dd::Dd<Type> phiStatesBdd = phiStates.toBdd();
+
+                uint_fast64_t iterations = 0;
+                storm::dd::Dd<Type> transitionMatrixBdd = model.getTransitionMatrix().notZero().existsAbstract(model.getNondeterminismVariables());
+                while (lastIterationStates != statesWithProbabilityGreater0E) {
+                    lastIterationStates = statesWithProbabilityGreater0E;
+                    statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.swapVariables(model.getRowColumnMetaVariablePairs());
+                    statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.andExists(transitionMatrixBdd, model.getColumnVariables());
+                    statesWithProbabilityGreater0E &= phiStatesBdd;
+                    ++iterations;
+                }
+                
+                return statesWithProbabilityGreater0E;
+            }
+            
+            /*!
+             * Computes the set of states for which there does not exist a scheduler that achieves a probability greater
+             * than zero of satisfying phi until psi.
+             *
+             * @param model The (symbolic) model for which to compute the set of states.
+             * @param phiStates The phi states of the model.
+             * @param psiStates The psi states of the model.
+             * @return A DD representing all such states.
+             */
+            template <storm::dd::DdType Type>
+            storm::dd::Dd<Type> performProb0A(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Dd<Type> const& phiStates, storm::dd::Dd<Type> const& psiStates) {
+                return !performProbGreater0E(model, phiStates, psiStates) && model.getReachableStates();
+            }
+            
+            /*!
+             * Computes the set of states for which all schedulers achieve a probability greater than zero of satisfying
+             * phi until psi.
+             *
+             * @param model The (symbolic) model for which to compute the set of states.
+             * @param phiStates The phi states of the model.
+             * @param psiStates The psi states of the model.
+             * @return A DD representing all such states.
+             */
+            template <storm::dd::DdType Type>
+            storm::dd::Dd<Type> performProbGreater0A(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Dd<Type> const& phiStates, storm::dd::Dd<Type> const& psiStates) {
+                // Initialize environment for backward search.
+                storm::dd::DdManager<Type> const& manager = model.getManager();
+                storm::dd::Dd<Type> lastIterationStates = manager.getZero();
+                storm::dd::Dd<Type> statesWithProbabilityGreater0A = psiStates.toBdd();
+                storm::dd::Dd<Type> phiStatesBdd = phiStates.toBdd();
+                storm::dd::Dd<Type> psiStatesBdd = statesWithProbabilityGreater0A;
+                
+                uint_fast64_t iterations = 0;
+                storm::dd::Dd<Type> transitionMatrixBdd = model.getTransitionMatrix().notZero();
+                while (lastIterationStates != statesWithProbabilityGreater0A) {
+                    lastIterationStates = statesWithProbabilityGreater0A;
+                    statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.swapVariables(model.getRowColumnMetaVariablePairs());
+                    statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.andExists(transitionMatrixBdd, model.getColumnVariables());
+                    statesWithProbabilityGreater0A |= model.getIllegalMask();
+                    statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.universalAbstract(model.getNondeterminismVariables());
+                    statesWithProbabilityGreater0A &= phiStatesBdd;
+                    statesWithProbabilityGreater0A |= psiStatesBdd;
+                    ++iterations;
+                }
+                
+                return statesWithProbabilityGreater0A;
+            }
+            
+            /*!
+             * Computes the set of states for which there exists a scheduler that achieves probability zero of satisfying
+             * phi until psi.
+             *
+             * @param model The (symbolic) model for which to compute the set of states.
+             * @param phiStates The phi states of the model.
+             * @param psiStates The psi states of the model.
+             * @return A DD representing all such states.
+             */
+            template <storm::dd::DdType Type>
+            storm::dd::Dd<Type> performProb0E(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Dd<Type> const& phiStates, storm::dd::Dd<Type> const& psiStates) {
+                return !performProbGreater0A(model, phiStates, psiStates) && model.getReachableStates();
+            }
+            
+            /*!
+             * Computes the set of states for which all schedulers achieve probability one of satisfying phi until psi.
+             *
+             * @param model The (symbolic) model for which to compute the set of states.
+             * @param phiStates The phi states of the model.
+             * @param psiStates The psi states of the model.
+             * @param statesWithProbabilityGreater0A The states of the model that have a probability greater zero under
+             * all schedulers.
+             * @return A DD representing all such states.
+             */
+            template <storm::dd::DdType Type>
+            storm::dd::Dd<Type> performProb1A(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Dd<Type> const& phiStates, storm::dd::Dd<Type> const& psiStates, storm::dd::Dd<Type> const& statesWithProbabilityGreater0A) {
+                // Initialize environment for backward search.
+                storm::dd::DdManager<Type> const& manager = model.getManager();
+                storm::dd::Dd<Type> lastIterationStates = manager.getZero();
+                storm::dd::Dd<Type> statesWithProbability1A = psiStates.toBdd() || statesWithProbabilityGreater0A;
+                storm::dd::Dd<Type> psiStatesBdd = psiStates.toBdd();
+                
+                uint_fast64_t iterations = 0;
+                storm::dd::Dd<Type> transitionMatrixBdd = model.getTransitionMatrix().notZero();
+                while (lastIterationStates != statesWithProbability1A) {
+                    lastIterationStates = statesWithProbability1A;
+                    statesWithProbability1A = statesWithProbability1A.swapVariables(model.getRowColumnMetaVariablePairs());
+                    statesWithProbability1A = transitionMatrixBdd.implies(statesWithProbability1A).universalAbstract(model.getColumnVariables());
+                    statesWithProbability1A |= model.getIllegalMask();
+                    statesWithProbability1A = statesWithProbability1A.universalAbstract(model.getNondeterminismVariables());
+                    statesWithProbability1A &= statesWithProbabilityGreater0A;
+                    statesWithProbability1A |= psiStatesBdd;
+                    ++iterations;
+                }
+                
+                return statesWithProbability1A;
+            }
+            
+            /*!
+             * Computes the set of states for which there exists a scheduler that achieves probability one of satisfying
+             * phi until psi.
+             *
+             * @param model The (symbolic) model for which to compute the set of states.
+             * @param phiStates The phi states of the model.
+             * @param psiStates The psi states of the model.
+             * @param statesWithProbability0A The states of the model that have a probability zero under all schedulers.
+             * @return A DD representing all such states.
+             */
+            template <storm::dd::DdType Type>
+            storm::dd::Dd<Type> performProb1E(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Dd<Type> const& phiStates, storm::dd::Dd<Type> const& psiStates, storm::dd::Dd<Type> const& statesWithProbabilityGreater0E) {
+                // Initialize environment for backward search.
+                storm::dd::DdManager<Type> const& manager = model.getManager();
+                storm::dd::Dd<Type> innerStates = manager.getZero();
+                storm::dd::Dd<Type> statesWithProbability1E = statesWithProbabilityGreater0E;
+                storm::dd::Dd<Type> phiStatesBdd = phiStates.toBdd();
+                storm::dd::Dd<Type> psiStatesBdd = psiStates.toBdd();
+
+                uint_fast64_t iterations = 0;
+                storm::dd::Dd<Type> transitionMatrixBdd = model.getTransitionMatrix().notZero();
+                while (statesWithProbability1E != innerStates) {
+                    innerStates = manager.getZero();
+                    storm::dd::Dd<Type> temporary = manager.getOne();
+                    
+                    while (innerStates != temporary) {
+                        innerStates = temporary;
+                        temporary = statesWithProbability1E;
+                        temporary = temporary.swapVariables(model.getRowColumnMetaVariablePairs());
+                        temporary = transitionMatrixBdd.implies(temporary).universalAbstract(model.getColumnVariables());
+                        
+                        storm::dd::Dd<Type> temporary2 = innerStates;
+                        temporary2 = temporary2.swapVariables(model.getRowColumnMetaVariablePairs());
+                        temporary2 = transitionMatrixBdd.andExists(temporary2, model.getColumnVariables());
+                        
+                        temporary = temporary.andExists(temporary2, model.getNondeterminismVariables());
+                        temporary &= phiStatesBdd;
+                        temporary |= psiStatesBdd;
+                    }
+                    ++iterations;
+                }
+
+                return statesWithProbability1E;
+            }
+            
+            template <storm::dd::DdType Type>
+            std::pair<storm::dd::Dd<Type>, storm::dd::Dd<Type>> performProb01Max(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Dd<Type> const& phiStates, storm::dd::Dd<Type> const& psiStates) {
+                std::pair<storm::dd::Dd<Type>, storm::dd::Dd<Type>> result;
+                result.first = performProb0A(model, phiStates, psiStates);
+                std::cout << "first: " << result.first.getNonZeroCount() << std::endl;
+                result.second = performProb1E(model, phiStates, psiStates, !result.first && model.getReachableStates());
+                return result;
+            }
+
+            template <storm::dd::DdType Type>
+            std::pair<storm::dd::Dd<Type>, storm::dd::Dd<Type>> performProb01Min(storm::models::symbolic::NondeterministicModel<Type> const& model, storm::dd::Dd<Type> const& phiStates, storm::dd::Dd<Type> const& psiStates) {
+                std::pair<storm::dd::Dd<Type>, storm::dd::Dd<Type>> result;
+                result.first = performProb0E(model, phiStates, psiStates);
+                result.second = performProb1A(model, phiStates, psiStates, !result.first && model.getReachableStates());
+                return result;
+            }
+            
             /*!
              * Performs a topological sort of the states of the system according to the given transitions.
              *

test/functional/storage/CuddDdTest.cpp

@@ -234,8 +234,8 @@ TEST(CuddDd, SwapTest) {
     storm::dd::Dd<storm::dd::DdType::CUDD> dd2;
     
     dd1 = manager->getIdentity(x.first);
-    ASSERT_THROW(dd1.swapVariables({std::make_pair(x.first, z.first)}), storm::exceptions::InvalidArgumentException);
-    ASSERT_NO_THROW(dd1.swapVariables({std::make_pair(x.first, x.second)}));
+    ASSERT_THROW(dd1 = dd1.swapVariables({std::make_pair(x.first, z.first)}), storm::exceptions::InvalidArgumentException);
+    ASSERT_NO_THROW(dd1 = dd1.swapVariables({std::make_pair(x.first, x.second)}));
     EXPECT_TRUE(dd1 == manager->getIdentity(x.second));
 }
 
@@ -249,7 +249,7 @@ TEST(CuddDd, MultiplyMatrixTest) {
     dd1 *= manager->getConstant(2);
     
     ASSERT_NO_THROW(dd3 = dd1.multiplyMatrix(dd2, {x.second}));
-    ASSERT_NO_THROW(dd3.swapVariables({std::make_pair(x.first, x.second)}));
+    ASSERT_NO_THROW(dd3 = dd3.swapVariables({std::make_pair(x.first, x.second)}));
     EXPECT_TRUE(dd3 == dd2 * manager->getConstant(2));
 }
 

test/functional/utility/GraphTest.cpp

@@ -4,6 +4,7 @@
 #include "src/storage/dd/CuddDd.h"
 #include "src/parser/PrismParser.h"
 #include "src/models/symbolic/Dtmc.h"
+#include "src/models/symbolic/Mdp.h"
 #include "src/models/sparse/Dtmc.h"
 #include "src/builder/DdPrismModelBuilder.h"
 #include "src/builder/ExplicitPrismModelBuilder.h"
@@ -30,6 +31,44 @@ TEST(GraphTest, SymbolicProb01) {
     EXPECT_EQ(1032, statesWithProbability01.second.getNonZeroCount());
 }
 
+TEST(GraphTest, SymbolicProb01MinMax) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+    
+    ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+    
+    std::pair<storm::dd::Dd<storm::dd::DdType::CUDD>, storm::dd::Dd<storm::dd::DdType::CUDD>> statesWithProbability01;
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("elected")));
+    EXPECT_EQ(0, statesWithProbability01.first.getNonZeroCount());
+    EXPECT_EQ(364, statesWithProbability01.second.getNonZeroCount());
+
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("elected")));
+    EXPECT_EQ(0, statesWithProbability01.first.getNonZeroCount());
+    EXPECT_EQ(364, statesWithProbability01.second.getNonZeroCount());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+    
+    ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("all_coins_equal_0")));
+    EXPECT_EQ(77, statesWithProbability01.first.getNonZeroCount());
+    EXPECT_EQ(149, statesWithProbability01.second.getNonZeroCount());
+    
+//    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("all_coins_equal_0")));
+//    EXPECT_EQ(74, statesWithProbability01.first.getNonZeroCount());
+//    EXPECT_EQ(198, statesWithProbability01.second.getNonZeroCount());
+
+//    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("all_coins_equal_1")));
+//    EXPECT_EQ(0, statesWithProbability01.first.getNonZeroCount());
+//    EXPECT_EQ(364, statesWithProbability01.second.getNonZeroCount());
+//    
+//    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>(), model->getReachableStates(), model->getStates("all_coins_equal_1")));
+//    EXPECT_EQ(0, statesWithProbability01.first.getNonZeroCount());
+//    EXPECT_EQ(364, statesWithProbability01.second.getNonZeroCount());
+}
+
 TEST(GraphTest, ExplicitProb01) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
     std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);