introduced relational product operations to prob0/1 algorithms (where possible)

Former-commit-id: 7fcd642030

src/builder/DdPrismModelBuilder.cpp

@@ -1175,15 +1175,6 @@ namespace storm {
                 STORM_LOG_TRACE("Iteration " << iteration << " of reachability analysis.");
                 changed = false;
                 storm::dd::Bdd<Type> tmp = reachableStates.relationalProduct(transitionBdd, generationInfo.rowMetaVariables, generationInfo.columnMetaVariables);
-                
-                storm::dd::Bdd<Type> tmp2 = reachableStates.andExists(transitionBdd, generationInfo.rowMetaVariables);
-                tmp2 = tmp2.swapVariables(generationInfo.rowColumnMetaVariablePairs);
-                
-                tmp2.exportToDot("tmp2.dot");
-                tmp.exportToDot("tmp.dot");
-
-                assert(tmp == tmp2);
-                
                 storm::dd::Bdd<Type> newReachableStates = tmp && (!reachableStates);
                                 
                 // Check whether new states were indeed discovered.
@@ -1193,8 +1184,6 @@ namespace storm {
                 
                 reachableStates |= newReachableStates;
                 
-                std::cout << "iter: " << iteration << " with nnz: " << reachableStates.getNonZeroCount() << std::endl;
-                
                 ++iteration;
             } while (changed);
             

src/storage/dd/Bdd.cpp

@@ -144,9 +144,8 @@ namespace storm {
         
         template<DdType LibraryType>
         Bdd<LibraryType> Bdd<LibraryType>::relationalProduct(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) const {
-            std::set<storm::expressions::Variable> tmpMetaVariables = Dd<LibraryType>::joinMetaVariables(*this, relation);
             std::set<storm::expressions::Variable> newMetaVariables;
-            std::set_difference(tmpMetaVariables.begin(), tmpMetaVariables.end(), columnMetaVariables.begin(), columnMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin()));
+            std::set_difference(relation.getContainedMetaVariables().begin(), relation.getContainedMetaVariables().end(), columnMetaVariables.begin(), columnMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin()));
             
             std::vector<InternalBdd<LibraryType>> rowVariables;
             for (auto const& metaVariable : rowMetaVariables) {
@@ -169,9 +168,8 @@ namespace storm {
         
         template<DdType LibraryType>
         Bdd<LibraryType> Bdd<LibraryType>::inverseRelationalProduct(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) const {
-            std::set<storm::expressions::Variable> tmpMetaVariables = Dd<LibraryType>::joinMetaVariables(*this, relation);
             std::set<storm::expressions::Variable> newMetaVariables;
-            std::set_difference(tmpMetaVariables.begin(), tmpMetaVariables.end(), rowMetaVariables.begin(), rowMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin()));
+            std::set_difference(relation.getContainedMetaVariables().begin(), relation.getContainedMetaVariables().end(), columnMetaVariables.begin(), columnMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin()));
             
             std::vector<InternalBdd<LibraryType>> rowVariables;
             for (auto const& metaVariable : rowMetaVariables) {
@@ -192,6 +190,30 @@ namespace storm {
             return Bdd<LibraryType>(this->getDdManager(), internalBdd.inverseRelationalProduct(relation, rowVariables, columnVariables), newMetaVariables);
         }
         
+        template<DdType LibraryType>
+        Bdd<LibraryType> Bdd<LibraryType>::inverseRelationalProductWithExtendedRelation(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) const {
+            std::set<storm::expressions::Variable> newMetaVariables;
+            std::set_difference(relation.getContainedMetaVariables().begin(), relation.getContainedMetaVariables().end(), columnMetaVariables.begin(), columnMetaVariables.end(), std::inserter(newMetaVariables, newMetaVariables.begin()));
+            
+            std::vector<InternalBdd<LibraryType>> rowVariables;
+            for (auto const& metaVariable : rowMetaVariables) {
+                DdMetaVariable<LibraryType> const& variable = this->getDdManager()->getMetaVariable(metaVariable);
+                for (auto const& ddVariable : variable.getDdVariables()) {
+                    rowVariables.push_back(ddVariable);
+                }
+            }
+            
+            std::vector<InternalBdd<LibraryType>> columnVariables;
+            for (auto const& metaVariable : columnMetaVariables) {
+                DdMetaVariable<LibraryType> const& variable = this->getDdManager()->getMetaVariable(metaVariable);
+                for (auto const& ddVariable : variable.getDdVariables()) {
+                    columnVariables.push_back(ddVariable);
+                }
+            }
+            
+            return Bdd<LibraryType>(this->getDdManager(), internalBdd.inverseRelationalProductWithExtendedRelation(relation, rowVariables, columnVariables), newMetaVariables);
+        }
+        
         template<DdType LibraryType>
         Bdd<LibraryType> Bdd<LibraryType>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) const {
             std::set<storm::expressions::Variable> newContainedMetaVariables;

src/storage/dd/Bdd.h

@@ -187,8 +187,9 @@ namespace storm {
             Bdd<LibraryType> restrict(Bdd<LibraryType> const& constraint) const;
             
             /*!
-             * Computes the relational product of the current BDD and the given BDD representing a relation. Note that
-             * this operation assumes that the row and column variables are interleaved.
+             * Computes the relational product of the current BDD and the given BDD representing a relation.
+             * Note that this operation assumes that the row and column variables are interleaved and that the relation
+             * only contains the row and column variables.
              *
              * @param relation The relation to use.
              * @param rowMetaVariables The row meta variables used in the relation.
@@ -199,7 +200,8 @@ namespace storm {
             
             /*!
              * Computes the inverse relational product of the current BDD and the given BDD representing a relation.
-             * Note that this operation assumes that the row and column variables are interleaved.
+             * Note that this operation assumes that the row and column variables are interleaved and that the relation
+             * only contains the row and column variables.
              *
              * @param relation The relation to use.
              * @param rowMetaVariables The row meta variables used in the relation.
@@ -208,6 +210,18 @@ namespace storm {
              */
             Bdd<LibraryType> inverseRelationalProduct(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) const;
             
+            /*!
+             * Computes the inverse relational product of the current BDD and the given BDD representing a relation that
+             * contains more variables than just the row and column variables.
+             * Note that this operation assumes that the row and column variables are interleaved.
+             *
+             * @param relation The relation to use.
+             * @param rowMetaVariables The row meta variables used in the relation.
+             * @param columnMetaVariables The row meta variables used in the relation.
+             * @return The inverse relational product.
+             */
+            Bdd<LibraryType> inverseRelationalProductWithExtendedRelation(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) const;
+            
             /*!
              * Swaps the given pairs of meta variables in the BDD. The pairs of meta variables must be guaranteed to have
              * the same number of underlying BDD variables.

src/storage/dd/cudd/InternalCuddBdd.cpp

@@ -46,11 +46,14 @@ namespace storm {
                 cube &= variable;
             }
             
-            InternalBdd<DdType::CUDD> result = this->andExists(relation, cube);
-            result = result.swapVariables(rowVariables, columnVariables);
+            InternalBdd<DdType::CUDD> result = this->swapVariables(rowVariables, columnVariables).andExists(relation, cube);
             return result;
         }
         
+        InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::inverseRelationalProductWithExtendedRelation(InternalBdd<DdType::CUDD> const& relation, std::vector<InternalBdd<DdType::CUDD>> const& rowVariables, std::vector<InternalBdd<DdType::CUDD>> const& columnVariables) const {
+            return this->inverseRelationalProduct(relation, rowVariables, columnVariables);
+        }
+        
         InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::ite(InternalBdd<DdType::CUDD> const& thenDd, InternalBdd<DdType::CUDD> const& elseDd) const {
             return InternalBdd<DdType::CUDD>(ddManager, this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()));
         }

src/storage/dd/cudd/InternalCuddBdd.h

@@ -95,6 +95,17 @@ namespace storm {
              * @return The ralational product.
              */
             InternalBdd<DdType::CUDD> inverseRelationalProduct(InternalBdd<DdType::CUDD> const& relation, std::vector<InternalBdd<DdType::CUDD>> const& rowVariables, std::vector<InternalBdd<DdType::CUDD>> const& columnVariables) const;
+            
+            /*!
+             * Computes the inverse relational product of the current BDD and the given BDD representing a relation that
+             * contains more than just the row and column variables.
+             *
+             * @param relation The relation to use.
+             * @param rowVariables The row variables of the relation represented as individual BDDs.
+             * @param columnVariables The row variables of the relation represented as individual BDDs.
+             * @return The ralational product.
+             */
+            InternalBdd<DdType::CUDD> inverseRelationalProductWithExtendedRelation(InternalBdd<DdType::CUDD> const& relation, std::vector<InternalBdd<DdType::CUDD>> const& rowVariables, std::vector<InternalBdd<DdType::CUDD>> const& columnVariables) const;
 
             /*!
              * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero

src/storage/dd/sylvan/InternalSylvanBdd.cpp

@@ -31,25 +31,22 @@ namespace storm {
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::relationalProduct(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables, std::vector<InternalBdd<DdType::Sylvan>> const& columnVariables) const {
-            InternalBdd<DdType::Sylvan> cube = ddManager->getBddOne();
-            for (auto const& variable : rowVariables) {
-                cube &= variable;
-            }
-            for (auto const& variable : columnVariables) {
-                cube &= variable;
-            }
-            
-            this->exportToDot("set.dot", {});
-            relation.exportToDot("relation.dot", {});
-            cube.exportToDot("cube.dot", {});
-            
-            InternalBdd<DdType::Sylvan> result(ddManager, this->sylvanBdd.RelNext(relation.sylvanBdd, cube.sylvanBdd));
-            result.exportToDot("result.dot", {});
-            return result;
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd.RelNext(relation.sylvanBdd, sylvan::Bdd(sylvan_false)));
         }
 
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::inverseRelationalProduct(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables, std::vector<InternalBdd<DdType::Sylvan>> const& columnVariables) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd.RelPrev(relation.sylvanBdd, sylvan::Bdd(sylvan_false)));
+        }
+        
+        InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::inverseRelationalProductWithExtendedRelation(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables, std::vector<InternalBdd<DdType::Sylvan>> const& columnVariables) const {
+            // Currently, there is no specialized version to perform this operation, so we fall back to the regular operations.
+            
+            InternalBdd<DdType::Sylvan> columnCube = ddManager->getBddOne();
+            for (auto const& variable : columnVariables) {
+                columnCube &= variable;
+            }
+
+            return this->swapVariables(rowVariables, columnVariables).andExists(relation, columnCube);
         }
         
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::ite(InternalBdd<DdType::Sylvan> const& thenDd, InternalBdd<DdType::Sylvan> const& elseDd) const {

src/storage/dd/sylvan/InternalSylvanBdd.h

@@ -85,6 +85,17 @@ namespace storm {
              */
             InternalBdd<DdType::Sylvan> inverseRelationalProduct(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables, std::vector<InternalBdd<DdType::Sylvan>> const& columnVariables) const;
             
+            /*!
+             * Computes the inverse relational product of the current BDD and the given BDD representing a relation that
+             * contains more than just the row and column variables.
+             *
+             * @param relation The relation to use.
+             * @param rowVariables The row variables of the relation represented as individual BDDs.
+             * @param columnVariables The row variables of the relation represented as individual BDDs.
+             * @return The ralational product.
+             */
+            InternalBdd<DdType::Sylvan> inverseRelationalProductWithExtendedRelation(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables, std::vector<InternalBdd<DdType::Sylvan>> const& columnVariables) const;
+            
             /*!
              * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero
              * function value to the function values specified by the first DD and all others to the function values

src/storage/dd/sylvan/InternalSylvanDdManager.cpp

@@ -29,6 +29,11 @@ namespace storm {
         InternalDdManager<DdType::Sylvan>::~InternalDdManager() {
             --numberOfInstances;
             if (numberOfInstances == 0) {
+                // Enable this to print the sylvan statistics to a file.
+//                FILE* filePointer = fopen("sylvan.stats", "w");
+//                sylvan_stats_report(filePointer, 0);
+//                fclose(filePointer);
+                
                 sylvan::Sylvan::quitPackage();
                 lace_exit();
             }

src/utility/graph.cpp

@@ -194,9 +194,7 @@ namespace storm {
                     }
                     
                     lastIterationStates = statesWithProbabilityGreater0;
-                    statesWithProbabilityGreater0 = statesWithProbabilityGreater0.swapVariables(model.getRowColumnMetaVariablePairs());
-                    statesWithProbabilityGreater0 &= transitionMatrix;
-                    statesWithProbabilityGreater0 = statesWithProbabilityGreater0.existsAbstract(model.getColumnVariables());
+                    statesWithProbabilityGreater0 = statesWithProbabilityGreater0.inverseRelationalProduct(transitionMatrix, model.getRowVariables(), model.getColumnVariables());
                     statesWithProbabilityGreater0 &= phiStates;
                     statesWithProbabilityGreater0 |= lastIterationStates;
                     ++iterations;
@@ -677,8 +675,7 @@ namespace storm {
                 storm::dd::Bdd<Type> abstractedTransitionMatrix = transitionMatrix.existsAbstract(model.getNondeterminismVariables());
                 while (lastIterationStates != statesWithProbabilityGreater0E) {
                     lastIterationStates = statesWithProbabilityGreater0E;
-                    statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.swapVariables(model.getRowColumnMetaVariablePairs());
-                    statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.andExists(abstractedTransitionMatrix, model.getColumnVariables());
+                    statesWithProbabilityGreater0E = statesWithProbabilityGreater0E.inverseRelationalProduct(abstractedTransitionMatrix, model.getRowVariables(), model.getColumnVariables());
                     statesWithProbabilityGreater0E &= phiStates;
                     statesWithProbabilityGreater0E |= lastIterationStates;
                     ++iterations;
@@ -702,8 +699,7 @@ namespace storm {
                 uint_fast64_t iterations = 0;
                 while (lastIterationStates != statesWithProbabilityGreater0A) {
                     lastIterationStates = statesWithProbabilityGreater0A;
-                    statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.swapVariables(model.getRowColumnMetaVariablePairs());
-                    statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.andExists(transitionMatrix, model.getColumnVariables());
+                    statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.inverseRelationalProductWithExtendedRelation(transitionMatrix, model.getRowVariables(), model.getColumnVariables());
                     statesWithProbabilityGreater0A |= model.getIllegalMask();
                     statesWithProbabilityGreater0A = statesWithProbabilityGreater0A.universalAbstract(model.getNondeterminismVariables());
                     statesWithProbabilityGreater0A &= phiStates;
@@ -757,8 +753,7 @@ namespace storm {
                         storm::dd::Bdd<Type> temporary = statesWithProbability1E.swapVariables(model.getRowColumnMetaVariablePairs());
                         temporary = transitionMatrix.implies(temporary).universalAbstract(model.getColumnVariables());
                         
-                        storm::dd::Bdd<Type> temporary2 = innerStates.swapVariables(model.getRowColumnMetaVariablePairs());
-                        temporary2 = transitionMatrix.andExists(temporary2, model.getColumnVariables());
+                        storm::dd::Bdd<Type> temporary2 = innerStates.inverseRelationalProductWithExtendedRelation(transitionMatrix, model.getRowVariables(), model.getColumnVariables());
                         
                         temporary = temporary.andExists(temporary2, model.getNondeterminismVariables());
                         temporary &= phiStates;
@@ -1051,7 +1046,6 @@ namespace storm {
             
 #ifdef STORM_HAVE_CARL
             
-            
             template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates);
             
             template std::vector<std::size_t> getDistances(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& initialStates);
@@ -1107,6 +1101,8 @@ namespace storm {
             
 #endif
             
+            // Instantiations for CUDD.
+            
             template storm::dd::Bdd<storm::dd::DdType::CUDD> performProbGreater0(storm::models::symbolic::Model<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, boost::optional<uint_fast64_t> const& stepBound = boost::optional<uint_fast64_t>());
             
             template storm::dd::Bdd<storm::dd::DdType::CUDD> performProb1(storm::models::symbolic::Model<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& statesWithProbabilityGreater0);
@@ -1133,6 +1129,36 @@ namespace storm {
             
             template std::pair<storm::dd::Bdd<storm::dd::DdType::CUDD>, storm::dd::Bdd<storm::dd::DdType::CUDD>> performProb01Min(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::CUDD, double> const& model, storm::dd::Bdd<storm::dd::DdType::CUDD> const& phiStates, storm::dd::Bdd<storm::dd::DdType::CUDD> const& psiStates);
             
+            
+            
+            // Instantiations for Sylvan.
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProbGreater0(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, boost::optional<uint_fast64_t> const& stepBound = boost::optional<uint_fast64_t>());
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb1(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& statesWithProbabilityGreater0);
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb1(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
+            template std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> performProb01(storm::models::symbolic::DeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
+            template std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> performProb01(storm::models::symbolic::Model<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Add<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProbGreater0E(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb0A(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProbGreater0A(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb0E(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb1A(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& statesWithProbabilityGreater0A);
+            
+            template storm::dd::Bdd<storm::dd::DdType::Sylvan> performProb1E(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& transitionMatrix, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& statesWithProbabilityGreater0E);
+            
+            template std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> performProb01Max(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
+            template std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> performProb01Min(storm::models::symbolic::NondeterministicModel<storm::dd::DdType::Sylvan, double> const& model, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& phiStates, storm::dd::Bdd<storm::dd::DdType::Sylvan> const& psiStates);
+            
         } // namespace graph
     } // namespace utility
 } // namespace storm

test/functional/utility/GraphTest.cpp

@@ -15,7 +15,7 @@
 #include "src/storage/dd/Bdd.h"
 #include "src/storage/dd/DdManager.h"
 
-TEST(GraphTest, SymbolicProb01) {
+TEST(GraphTest, SymbolicProb01_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
     
@@ -36,7 +36,29 @@ TEST(GraphTest, SymbolicProb01) {
     EXPECT_EQ(1032ul, statesWithProbability01.second.getNonZeroCount());
 }
 
-TEST(GraphTest, SymbolicProb01MinMax) {
+// FIXME: re-enable as soon as the ADD iterator of sylvan works.
+TEST(DISABLED_GraphTest, SymbolicProb01_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+    
+    ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
+    
+    std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> statesWithProbability01;
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("observe0Greater1")));
+    EXPECT_EQ(4409ul, statesWithProbability01.first.getNonZeroCount());
+    EXPECT_EQ(1316ul, statesWithProbability01.second.getNonZeroCount());
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("observeIGreater1")));
+    EXPECT_EQ(1091ul, statesWithProbability01.first.getNonZeroCount());
+    EXPECT_EQ(4802ul, statesWithProbability01.second.getNonZeroCount());
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("observeOnlyTrueSender")));
+    EXPECT_EQ(5829ul, statesWithProbability01.first.getNonZeroCount());
+    EXPECT_EQ(1032ul, statesWithProbability01.second.getNonZeroCount());
+}
+
+TEST(GraphTest, SymbolicProb01MinMax_Cudd) {
     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);
     
@@ -87,6 +109,57 @@ TEST(GraphTest, SymbolicProb01MinMax) {
     EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount());
 }
 
+TEST(GraphTest, SymbolicProb01MinMax_Sylvan) {
+    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::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+    
+    ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+    
+    std::pair<storm::dd::Bdd<storm::dd::DdType::Sylvan>, storm::dd::Bdd<storm::dd::DdType::Sylvan>> statesWithProbability01;
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("elected")));
+    EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount());
+    EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount());
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("elected")));
+    EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount());
+    EXPECT_EQ(364ul, 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::Sylvan>::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::Sylvan>>(), model->getReachableStates(), model->getStates("all_coins_equal_0")));
+    EXPECT_EQ(77ul, statesWithProbability01.first.getNonZeroCount());
+    EXPECT_EQ(149ul, statesWithProbability01.second.getNonZeroCount());
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("all_coins_equal_0")));
+    EXPECT_EQ(74ul, statesWithProbability01.first.getNonZeroCount());
+    EXPECT_EQ(198ul, statesWithProbability01.second.getNonZeroCount());
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("all_coins_equal_1")));
+    EXPECT_EQ(94ul, statesWithProbability01.first.getNonZeroCount());
+    EXPECT_EQ(33ul, statesWithProbability01.second.getNonZeroCount());
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("all_coins_equal_1")));
+    EXPECT_EQ(83ul, statesWithProbability01.first.getNonZeroCount());
+    EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::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::Sylvan>>(), model->getReachableStates(), model->getStates("collision_max_backoff")));
+    EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount());
+    EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount());
+    
+    ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>(), model->getReachableStates(), model->getStates("collision_max_backoff")));
+    EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount());
+    EXPECT_EQ(16ul, 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);