ADD iterator working for sylvan. enabled more tests for sylvan. symbolic Dtmc model checker now working.

Former-commit-id: b11b2f7476

resources/3rdparty/sylvan/src/sylvan_mtbdd.c

@@ -1134,8 +1134,8 @@ TASK_IMPL_2(MTBDD, mtbdd_op_times, MTBDD*, pa, MTBDD*, pb)
             else if (val_b == 0) return b;
             else {
                 MTBDD result;
-                if (val_a == 1) result = b;
-                else if (val_b == 1) result = a;
+                if (val_a == 1) result = mtbdd_regular(b);
+                else if (val_b == 1) result = mtbdd_regular(a);
                 else result = mtbdd_uint64(val_a*val_b);
                 int nega = mtbdd_isnegated(a);
                 int negb = mtbdd_isnegated(b);
@@ -1150,13 +1150,16 @@ TASK_IMPL_2(MTBDD, mtbdd_op_times, MTBDD*, pa, MTBDD*, pb)
             else if (vval_b == 0.0) return b;
             else {
                 MTBDD result;
-                if (vval_a == 1.0) result = b;
-                else if (vval_b == 1.0) result = a;
+                if (vval_a == 1.0) result = mtbdd_regular(b);
+                else if (vval_b == 1.0) result = mtbdd_regular(a);
                 else result = mtbdd_double(vval_a*vval_b);
                 int nega = mtbdd_isnegated(a);
                 int negb = mtbdd_isnegated(b);
-                if (nega ^ negb) return mtbdd_negate(result);
-                else return result;
+                if (nega ^ negb) {
+                    return mtbdd_negate(result);
+                } else {
+                    return result;
+                }
             }
         } else if (mtbddnode_gettype(na) == 2 && mtbddnode_gettype(nb) == 2) {
             // both fraction
@@ -1560,8 +1563,7 @@ TASK_4(MTBDD, mtbdd_equal_norm_rel_d2, MTBDD, a, MTBDD, b, size_t, svalue, int*,
         double vb = mtbdd_getdouble(b);
         if (mtbdd_isnegated(b)) vb = -vb;
         if (va == 0) return mtbdd_false;
-        va = (va - vb) / va;
-        if (va < 0) va = -va;
+        va = fabs((va - vb) / va);
         return (va < *(double*)&svalue) ? mtbdd_true : mtbdd_false;
     }
 
@@ -2558,7 +2560,7 @@ mtbdd_fprintdot_rec(FILE *out, MTBDD mtbdd, print_terminal_label_cb cb)
     } else if (mtbddnode_isleaf(n)) {
         uint32_t type = mtbddnode_gettype(n);
         uint64_t value = mtbddnode_getvalue(n);
-        fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"", MTBDD_STRIPMARK(mtbdd));
+        fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"", mtbdd_regular(mtbdd));
         switch (type) {
         case 0:
             fprintf(out, "%" PRIu64, value);
@@ -2576,16 +2578,16 @@ mtbdd_fprintdot_rec(FILE *out, MTBDD mtbdd, print_terminal_label_cb cb)
         fprintf(out, "\"];\n");
     } else {
         fprintf(out, "%" PRIu64 " [label=\"%" PRIu32 "\"];\n",
-                MTBDD_STRIPMARK(mtbdd), mtbddnode_getvariable(n));
+                mtbdd_regular(mtbdd), mtbddnode_getvariable(n));
 
-        mtbdd_fprintdot_rec(out, mtbddnode_getlow(n), cb);
-        mtbdd_fprintdot_rec(out, mtbddnode_gethigh(n), cb);
+        mtbdd_fprintdot_rec(out, mtbdd_regular(mtbddnode_getlow(n)), cb);
+        mtbdd_fprintdot_rec(out, mtbdd_regular(mtbddnode_gethigh(n)), cb);
 
-        fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=dashed];\n",
-                mtbdd, mtbddnode_getlow(n));
+        fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=dashed dir=both arrowtail=%s];\n",
+                mtbdd, mtbdd_regular(mtbddnode_getlow(n)), mtbdd_isnegated(mtbddnode_getlow(n)) ? "dot" : "none");
         fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=solid dir=both arrowtail=%s];\n",
-                mtbdd, MTBDD_STRIPMARK(mtbddnode_gethigh(n)),
-                mtbddnode_getcomp(n) ? "dot" : "none");
+                mtbdd, mtbdd_regular(mtbddnode_gethigh(n)),
+                mtbdd_isnegated(mtbddnode_gethigh(n)) ? "dot" : "none");
     }
 }
 
@@ -2598,9 +2600,9 @@ mtbdd_fprintdot(FILE *out, MTBDD mtbdd, print_terminal_label_cb cb)
     fprintf(out, "edge [dir = forward];\n");
     fprintf(out, "root [style=invis];\n");
     fprintf(out, "root -> %" PRIu64 " [style=solid dir=both arrowtail=%s];\n",
-            MTBDD_STRIPMARK(mtbdd), MTBDD_HASMARK(mtbdd) ? "dot" : "none");
+            mtbdd_regular(mtbdd), mtbdd_isnegated(mtbdd) ? "dot" : "none");
 
-    mtbdd_fprintdot_rec(out, mtbdd, cb);
+    mtbdd_fprintdot_rec(out, mtbdd_regular(mtbdd), cb);
     mtbdd_unmark_rec(mtbdd);
 
     fprintf(out, "}\n");

resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c

@@ -539,4 +539,8 @@ int mtbdd_iszero(MTBDD dd) {
         return mtbdd_getnumer(dd) == 0;
     }
     return 0;
+}
+
+int mtbdd_isnonzero(MTBDD dd) {
+    return mtbdd_iszero(dd) ? 0 : 1;
 }

resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h

@@ -1,8 +1,3 @@
-/**
- * Compute a - b
- */
-#define mtbdd_minus(a, b) mtbdd_plus(a, mtbdd_negate(b))
-
 /**
  * Binary operation Divide (for MTBDDs of same type)
  * Only for MTBDDs where all leaves are Integer or Double.
@@ -107,7 +102,8 @@ TASK_DECL_1(MTBDD, mtbdd_bool_to_uint64, MTBDD)
 TASK_DECL_2(double, mtbdd_non_zero_count, MTBDD, size_t);
 #define mtbdd_non_zero_count(dd, nvars) CALL(mtbdd_non_zero_count, dd, nvars)
 
-// Checks whether the given MTBDD represents a zero leaf.
+// Checks whether the given MTBDD (does represents a zero leaf.
 int mtbdd_iszero(MTBDD);
+int mtbdd_isnonzero(MTBDD);
 
 #define mtbdd_regular(dd) (dd & ~mtbdd_complement)

resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp

@@ -15,11 +15,11 @@
     Bdd Less(const Mtbdd& other) const;
 
     Bdd LessOrEqual(const Mtbdd& other) const;
-    
-    double getDoubleMax() const;
 
-    double getDoubleMin() const;
-    
+    Mtbdd Minimum() const;
+
+    Mtbdd Maximum() const;
+
     bool EqualNorm(const Mtbdd& other, double epsilon) const;
 
     bool EqualNormRel(const Mtbdd& other, double epsilon) const;
@@ -41,4 +41,11 @@
      */
     double NonZeroCount(size_t variableCount) const;
 
-    bool isValid() const;
+    bool isValid() const;
+
+    /**
+     * @brief Writes .dot file of this Bdd. Not thread-safe!
+     */
+    void PrintDot(FILE *out) const;
+
+    

resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp

@@ -49,20 +49,6 @@ Mtbdd::LessOrEqual(const Mtbdd& other) const {
     return mtbdd_less_or_equal_as_bdd(mtbdd, other.mtbdd);
 }
 
-double
-Mtbdd::getDoubleMax() const {
-    LACE_ME;
-    MTBDD maxNode = mtbdd_maximum(mtbdd);
-    return mtbdd_getdouble(maxNode);
-}
-
-double
-Mtbdd::getDoubleMin() const {
-    LACE_ME;
-    MTBDD minNode = mtbdd_minimum(mtbdd);
-    return mtbdd_getdouble(minNode);
-}
-
 bool
 Mtbdd::EqualNorm(const Mtbdd& other, double epsilon) const {
     LACE_ME;
@@ -122,3 +108,20 @@ Mtbdd::isValid() const {
     LACE_ME;
     return mtbdd_test_isvalid(mtbdd) == 1;
 }
+
+Mtbdd
+Mtbdd::Minimum() const {
+    LACE_ME;
+    return mtbdd_minimum(mtbdd);
+}
+
+Mtbdd
+Mtbdd::Maximum() const {
+    LACE_ME;
+    return mtbdd_maximum(mtbdd);
+}
+
+void
+Mtbdd::PrintDot(FILE *out) const {
+    mtbdd_fprintdot(out, mtbdd, NULL);
+}

src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp

@@ -91,5 +91,6 @@ namespace storm {
         }
         
         template class SymbolicDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double>;
+        template class SymbolicDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double>;
     }
 }

src/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp

@@ -132,7 +132,6 @@ namespace storm {
             
             template<storm::dd::DdType DdType, typename ValueType>
             storm::dd::Add<DdType, ValueType> SymbolicDtmcPrctlHelper<DdType, ValueType>::computeReachabilityRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, bool qualitative, storm::utility::solver::SymbolicLinearEquationSolverFactory<DdType, ValueType> const& linearEquationSolverFactory) {
-                
                 // Only compute the result if there is at least one reward model.
                 STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
                 
@@ -179,6 +178,7 @@ namespace storm {
             }
             
             template class SymbolicDtmcPrctlHelper<storm::dd::DdType::CUDD, double>;
+            template class SymbolicDtmcPrctlHelper<storm::dd::DdType::Sylvan, double>;
             
         }
     }

src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp

@@ -61,5 +61,11 @@ namespace storm {
         template storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double> const& SymbolicPropositionalModelChecker<storm::dd::DdType::CUDD, double>::getModelAs() const;
         template storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double> const& SymbolicPropositionalModelChecker<storm::dd::DdType::CUDD, double>::getModelAs() const;
         template class SymbolicPropositionalModelChecker<storm::dd::DdType::CUDD, double>;
+
+        template storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double> const& SymbolicPropositionalModelChecker<storm::dd::DdType::Sylvan, double>::getModelAs() const;
+        template storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double> const& SymbolicPropositionalModelChecker<storm::dd::DdType::Sylvan, double>::getModelAs() const;
+        template storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double> const& SymbolicPropositionalModelChecker<storm::dd::DdType::Sylvan, double>::getModelAs() const;
+        template class SymbolicPropositionalModelChecker<storm::dd::DdType::Sylvan, double>;
+
     }
 }

src/modelchecker/results/CheckResult.cpp

@@ -130,6 +130,7 @@ namespace storm {
         // Explicitly instantiate the template functions.
         template ExplicitQuantitativeCheckResult<double>& CheckResult::asExplicitQuantitativeCheckResult();
         template ExplicitQuantitativeCheckResult<double> const& CheckResult::asExplicitQuantitativeCheckResult() const;
+
         template SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>& CheckResult::asSymbolicQualitativeCheckResult();
         template SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD> const& CheckResult::asSymbolicQualitativeCheckResult() const;
         template SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>& CheckResult::asSymbolicQuantitativeCheckResult();
@@ -137,6 +138,13 @@ namespace storm {
         template HybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>& CheckResult::asHybridQuantitativeCheckResult();
         template HybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double> const& CheckResult::asHybridQuantitativeCheckResult() const;
 
+        template SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>& CheckResult::asSymbolicQualitativeCheckResult();
+        template SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan> const& CheckResult::asSymbolicQualitativeCheckResult() const;
+        template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asSymbolicQuantitativeCheckResult();
+        template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asSymbolicQuantitativeCheckResult() const;
+        template HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asHybridQuantitativeCheckResult();
+        template HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asHybridQuantitativeCheckResult() const;
+
 #ifdef STORM_HAVE_CARL
         template ExplicitQuantitativeCheckResult<storm::RationalFunction>& CheckResult::asExplicitQuantitativeCheckResult();
         template ExplicitQuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asExplicitQuantitativeCheckResult() const;

src/modelchecker/results/SymbolicQualitativeCheckResult.cpp

@@ -66,5 +66,6 @@ namespace storm {
         }
         
         template class SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>;
+        template class SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>;
     }
 }

src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp

@@ -91,5 +91,6 @@ namespace storm {
         
         // Explicitly instantiate the class.
         template class SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>;
+        template class SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>;
     }
 }

src/solver/SymbolicGameSolver.cpp

@@ -58,6 +58,7 @@ namespace storm {
         }
         
         template class SymbolicGameSolver<storm::dd::DdType::CUDD, double>;
+        template class SymbolicGameSolver<storm::dd::DdType::Sylvan, double>;
         
     }
 }

src/solver/SymbolicLinearEquationSolver.cpp

@@ -45,6 +45,7 @@ namespace storm {
             
             while (!converged && iterationCount < maximalNumberOfIterations) {
                 storm::dd::Add<DdType, ValueType> xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs);
+
                 storm::dd::Add<DdType, ValueType> tmp = lu.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables);
                 tmp = b - tmp;
                 tmp = tmp.swapVariables(this->rowColumnMetaVariablePairs);
@@ -82,6 +83,7 @@ namespace storm {
         }
         
         template class SymbolicLinearEquationSolver<storm::dd::DdType::CUDD, double>;
+        template class SymbolicLinearEquationSolver<storm::dd::DdType::Sylvan, double>;
         
     }
 }

src/storage/dd/Add.cpp

@@ -725,12 +725,18 @@ namespace storm {
         
         template<DdType LibraryType, typename ValueType>
         AddIterator<LibraryType, ValueType> Add<LibraryType, ValueType>::begin(bool enumerateDontCareMetaVariables) const {
-            return internalAdd.begin(this->getDdManager(), this->getContainedMetaVariables(), enumerateDontCareMetaVariables);
+            uint_fast64_t numberOfDdVariables = 0;
+            for (auto const& metaVariable : this->getContainedMetaVariables()) {
+                auto const& ddMetaVariable = this->getDdManager().getMetaVariable(metaVariable);
+                numberOfDdVariables += ddMetaVariable.getNumberOfDdVariables();
+            }
+            
+            return internalAdd.begin(this->getDdManager(), Bdd<LibraryType>::getCube(this->getDdManager(), this->getContainedMetaVariables()), numberOfDdVariables, this->getContainedMetaVariables(), enumerateDontCareMetaVariables);
         }
         
         template<DdType LibraryType, typename ValueType>
         AddIterator<LibraryType, ValueType> Add<LibraryType, ValueType>::end(bool enumerateDontCareMetaVariables) const {
-            return internalAdd.end(this->getDdManager(), enumerateDontCareMetaVariables);
+            return internalAdd.end(this->getDdManager());
         }
         
         template<DdType LibraryType, typename ValueType>

src/storage/dd/cudd/InternalCuddAdd.cpp

@@ -316,7 +316,7 @@ namespace storm {
         }
         
         template<typename ValueType>
-        AddIterator<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::begin(DdManager<DdType::CUDD> const& fullDdManager, std::set<storm::expressions::Variable> const& metaVariables, bool enumerateDontCareMetaVariables) const {
+        AddIterator<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::begin(DdManager<DdType::CUDD> const& fullDdManager, InternalBdd<DdType::CUDD> const& variableCube, uint_fast64_t numberOfDdVariables, std::set<storm::expressions::Variable> const& metaVariables, bool enumerateDontCareMetaVariables) const {
             int* cube;
             double value;
             DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value);
@@ -324,8 +324,8 @@ namespace storm {
         }
         
         template<typename ValueType>
-        AddIterator<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::end(DdManager<DdType::CUDD> const& fullDdManager, bool enumerateDontCareMetaVariables) const {
-            return AddIterator<DdType::CUDD, ValueType>(fullDdManager, nullptr, nullptr, 0, true, nullptr, enumerateDontCareMetaVariables);
+        AddIterator<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::end(DdManager<DdType::CUDD> const& fullDdManager) const {
+            return AddIterator<DdType::CUDD, ValueType>(fullDdManager, nullptr, nullptr, 0, true, nullptr, false);
         }
         
         template<typename ValueType>

src/storage/dd/cudd/InternalCuddAdd.h

@@ -461,22 +461,22 @@ namespace storm {
              * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value.
              *
              * @param fullDdManager The DD manager responsible for this ADD.
+             * @param variableCube The cube of variables contained in this ADD.
+             * @param numberOfDdVariables The number of variables contained in this ADD.
              * @param metaVariables The meta variables contained in the ADD.
              * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even
              * if a meta variable does not at all influence the the function value.
              * @return An iterator that points to the first meta variable assignment with a non-zero function value.
              */
-            AddIterator<DdType::CUDD, ValueType> begin(DdManager<DdType::CUDD> const& fullDdManager, std::set<storm::expressions::Variable> const& metaVariables, bool enumerateDontCareMetaVariables = true) const;
+            AddIterator<DdType::CUDD, ValueType> begin(DdManager<DdType::CUDD> const& fullDdManager, InternalBdd<DdType::CUDD> const& variableCube, uint_fast64_t numberOfDdVariables, std::set<storm::expressions::Variable> const& metaVariables, bool enumerateDontCareMetaVariables = true) const;
             
             /*!
              * Retrieves an iterator that points past the end of the container.
              *
              * @param fullDdManager The DD manager responsible for this ADD.
-             * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even
-             * if a meta variable does not at all influence the the function value.
              * @return An iterator that points past the end of the container.
              */
-            AddIterator<DdType::CUDD, ValueType> end(DdManager<DdType::CUDD> const& fullDdManager, bool enumerateDontCareMetaVariables = true) const;
+            AddIterator<DdType::CUDD, ValueType> end(DdManager<DdType::CUDD> const& fullDdManager) const;
             
             /*!
              * Composes the ADD with an explicit vector by performing a specified function between the entries of this

src/storage/dd/sylvan/InternalSylvanAdd.cpp

@@ -1,6 +1,8 @@
 #include "src/storage/dd/sylvan/InternalSylvanAdd.h"
 
+#include "src/storage/dd/sylvan/SylvanAddIterator.h"
 #include "src/storage/dd/sylvan/InternalSylvanDdManager.h"
+#include "src/storage/dd/DdManager.h"
 
 #include "src/storage/SparseMatrix.h"
 
@@ -246,12 +248,12 @@ namespace storm {
         
         template<typename ValueType>
         ValueType InternalAdd<DdType::Sylvan, ValueType>::getMin() const {
-            return static_cast<ValueType>(this->sylvanMtbdd.getDoubleMin());
+            return getValue(this->sylvanMtbdd.Minimum().GetMTBDD());
         }
         
         template<typename ValueType>
         ValueType InternalAdd<DdType::Sylvan, ValueType>::getMax() const {
-            return static_cast<ValueType>(this->sylvanMtbdd.getDoubleMax());
+            return getValue(this->sylvanMtbdd.Maximum().GetMTBDD());
         }
         
         template<typename ValueType>
@@ -283,18 +285,18 @@ namespace storm {
         void InternalAdd<DdType::Sylvan, ValueType>::exportToDot(std::string const& filename, std::vector<std::string> const& ddVariableNamesAsStrings) const {
             // Open the file, dump the DD and close it again.
             FILE* filePointer = fopen(filename.c_str() , "w");
-            mtbdd_fprintdot(filePointer, this->sylvanMtbdd.GetMTBDD(), nullptr);
+            this->sylvanMtbdd.PrintDot(filePointer);
             fclose(filePointer);
         }
         
         template<typename ValueType>
-        AddIterator<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::begin(DdManager<DdType::Sylvan> const& fullDdManager, std::set<storm::expressions::Variable> const& metaVariables, bool enumerateDontCareMetaVariables) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+        AddIterator<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::begin(DdManager<DdType::Sylvan> const& fullDdManager, InternalBdd<DdType::Sylvan> const& variableCube, uint_fast64_t numberOfDdVariables, std::set<storm::expressions::Variable> const& metaVariables, bool enumerateDontCareMetaVariables) const {
+            return AddIterator<DdType::Sylvan, ValueType>::createBeginIterator(fullDdManager, this->getSylvanMtbdd(), variableCube.getSylvanBdd(), numberOfDdVariables, &metaVariables, enumerateDontCareMetaVariables);
         }
         
         template<typename ValueType>
-        AddIterator<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::end(DdManager<DdType::Sylvan> const& fullDdManager, bool enumerateDontCareMetaVariables) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+        AddIterator<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::end(DdManager<DdType::Sylvan> const& fullDdManager) const {
+            return AddIterator<DdType::Sylvan, ValueType>::createEndIterator(fullDdManager);
         }
         
         template<typename ValueType>

src/storage/dd/sylvan/InternalSylvanAdd.h

@@ -40,6 +40,8 @@ namespace storm {
         template<typename ValueType>
         class InternalAdd<DdType::Sylvan, ValueType> {
         public:
+            friend class AddIterator<DdType::Sylvan, ValueType>;
+            
             /*!
              * Creates an ADD that encapsulates the given Sylvan MTBDD.
              *
@@ -459,22 +461,22 @@ namespace storm {
              * Retrieves an iterator that points to the first meta variable assignment with a non-zero function value.
              *
              * @param fullDdManager The DD manager responsible for this ADD.
+             * @param variableCube The cube of variables contained in this ADD.
+             * @param numberOfDdVariables The number of variables contained in this ADD.
              * @param metaVariables The meta variables contained in the ADD.
              * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even
              * if a meta variable does not at all influence the the function value.
              * @return An iterator that points to the first meta variable assignment with a non-zero function value.
              */
-            AddIterator<DdType::Sylvan, ValueType> begin(DdManager<DdType::Sylvan> const& fullDdManager, std::set<storm::expressions::Variable> const& metaVariables, bool enumerateDontCareMetaVariables = true) const;
+            AddIterator<DdType::Sylvan, ValueType> begin(DdManager<DdType::Sylvan> const& fullDdManager, InternalBdd<DdType::Sylvan> const& variableCube, uint_fast64_t numberOfDdVariables, std::set<storm::expressions::Variable> const& metaVariables, bool enumerateDontCareMetaVariables = true) const;
             
             /*!
              * Retrieves an iterator that points past the end of the container.
              *
              * @param fullDdManager The DD manager responsible for this ADD.
-             * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even
-             * if a meta variable does not at all influence the the function value.
              * @return An iterator that points past the end of the container.
              */
-            AddIterator<DdType::Sylvan, ValueType> end(DdManager<DdType::Sylvan> const& fullDdManager, bool enumerateDontCareMetaVariables = true) const;
+            AddIterator<DdType::Sylvan, ValueType> end(DdManager<DdType::Sylvan> const& fullDdManager) const;
             
             /*!
              * Composes the ADD with an explicit vector by performing a specified function between the entries of this

src/storage/dd/sylvan/SylvanAddIterator.cpp

@@ -1,5 +1,10 @@
 #include "src/storage/dd/sylvan/SylvanAddIterator.h"
 
+#include "src/storage/dd/sylvan/InternalSylvanAdd.h"
+
+#include "src/storage/dd/DdManager.h"
+#include "src/storage/expressions/ExpressionManager.h"
+
 #include "src/utility/macros.h"
 #include "src/exceptions/NotImplementedException.h"
 
@@ -10,24 +15,172 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        template<typename ValueType>
+        AddIterator<DdType::Sylvan, ValueType>::AddIterator(DdManager<DdType::Sylvan> const& ddManager, sylvan::Mtbdd mtbdd, sylvan::Bdd variables, uint_fast64_t numberOfDdVariables, bool isAtEnd, std::set<storm::expressions::Variable> const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(&ddManager), mtbdd(mtbdd), variables(variables), cube(numberOfDdVariables), leaf(), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(0), relevantDontCareDdVariables(), currentValuation(ddManager.getExpressionManager().getSharedPointer()) {
+            // If the given generator is not yet at its end, we need to create the current valuation from the cube from
+            // scratch.
+            if (!this->isAtEnd) {
+                this->createGlobalToLocalIndexMapping();
+                
+                // And then get ready for treating the first cube.
+                leaf = mtbdd_enum_first(mtbdd.GetMTBDD(), variables.GetBDD(), cube.data(), &mtbdd_isnonzero);
+                
+                if (leaf != mtbdd_false) {
+                    this->treatNewCube();
+                } else {
+                    this->isAtEnd = true;
+                }
+            }
+        }
+        
+        template<typename ValueType>
+        void AddIterator<DdType::Sylvan, ValueType>::createGlobalToLocalIndexMapping() {
+            // Create the global to local index mapping.
+            std::vector<uint_fast64_t> globalIndices;
+            for (auto const& metaVariable : *this->metaVariables) {
+                auto const& ddMetaVariable = this->ddManager->getMetaVariable(metaVariable);
+                
+                for (auto const& ddVariable : ddMetaVariable.getDdVariables()) {
+                    globalIndices.push_back(ddVariable.getIndex());
+                }
+            }
+            
+            std::sort(globalIndices.begin(), globalIndices.end());
+            
+            for (auto it = globalIndices.begin(), ite = globalIndices.end(); it != ite; ++it) {
+                globalToLocalIndexMap[*it] = std::distance(globalIndices.begin(), it);
+            }
+        }
+        
+        template<typename ValueType>
+        AddIterator<DdType::Sylvan, ValueType> AddIterator<DdType::Sylvan, ValueType>::createBeginIterator(DdManager<DdType::Sylvan> const& ddManager, sylvan::Mtbdd mtbdd, sylvan::Bdd variables, uint_fast64_t numberOfDdVariables, std::set<storm::expressions::Variable> const* metaVariables, bool enumerateDontCareMetaVariables) {
+            return AddIterator<DdType::Sylvan, ValueType>(ddManager, mtbdd, variables, numberOfDdVariables, false, metaVariables, enumerateDontCareMetaVariables);
+        }
+        
+        template<typename ValueType>
+        AddIterator<DdType::Sylvan, ValueType> AddIterator<DdType::Sylvan, ValueType>::createEndIterator(DdManager<DdType::Sylvan> const& ddManager) {
+            return AddIterator<DdType::Sylvan, ValueType>(ddManager, sylvan::Mtbdd(), sylvan::Bdd(), 0, true, nullptr, false);
+        }
+        
         template<typename ValueType>
         AddIterator<DdType::Sylvan, ValueType>& AddIterator<DdType::Sylvan, ValueType>::operator++() {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            STORM_LOG_ASSERT(!this->isAtEnd, "Illegally incrementing iterator that is already at its end.");
+            
+            // If there were no (relevant) don't cares or we have enumerated all combination, we need to eliminate the
+            // found solutions and get the next "first" cube.
+            if (this->relevantDontCareDdVariables.empty() || this->cubeCounter >= std::pow(2, this->relevantDontCareDdVariables.size()) - 1) {
+                leaf = mtbdd_enum_next(mtbdd.GetMTBDD(), variables.GetBDD(), cube.data(), &mtbdd_isnonzero);
+
+                if (leaf != mtbdd_false) {
+                    this->treatNewCube();
+                } else {
+                    this->isAtEnd = true;
+                }
+            } else {
+                // Treat the next solution of the cube.
+                this->treatNextInCube();
+            }
+            
+            return *this;
         }
         
         template<typename ValueType>
         bool AddIterator<DdType::Sylvan, ValueType>::operator==(AddIterator<DdType::Sylvan, ValueType> const& other) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            if (this->isAtEnd && other.isAtEnd) {
+                return true;
+            } else {
+                return this->ddManager == other.ddManager && this->mtbdd == other.mtbdd && this->variables == other.variables
+                && this->cube == other.cube && this->leaf == other.leaf && this->isAtEnd == other.isAtEnd
+                && this->metaVariables == other.metaVariables && this->cubeCounter == other.cubeCounter
+                && this->relevantDontCareDdVariables == other.relevantDontCareDdVariables
+                && this->currentValuation == other.currentValuation;
+            }
         }
         
         template<typename ValueType>
         bool AddIterator<DdType::Sylvan, ValueType>::operator!=(AddIterator<DdType::Sylvan, ValueType> const& other) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return !(*this == other);
         }
         
         template<typename ValueType>
         std::pair<storm::expressions::SimpleValuation, ValueType> AddIterator<DdType::Sylvan, ValueType>::operator*() const {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+            return std::make_pair(currentValuation, static_cast<ValueType>(InternalAdd<DdType::Sylvan, ValueType>::getValue(leaf)));
+        }
+        
+        template<typename ValueType>
+        void AddIterator<DdType::Sylvan, ValueType>::treatNewCube() {
+            this->relevantDontCareDdVariables.clear();
+            
+            // Now loop through the bits of all meta variables and check whether they need to be set, not set or are
+            // don't cares. In the latter case, we add them to a special list, so we can iterate over their concrete
+            // valuations later.
+            for (auto const& metaVariable : *this->metaVariables) {
+                bool metaVariableAppearsInCube = false;
+                std::vector<std::tuple<storm::expressions::Variable, uint_fast64_t>> localRelenvantDontCareDdVariables;
+                auto const& ddMetaVariable = this->ddManager->getMetaVariable(metaVariable);
+                if (ddMetaVariable.getType() == MetaVariableType::Bool) {
+                    if (this->cube[globalToLocalIndexMap.at(ddMetaVariable.getDdVariables().front().getIndex())] == 0) {
+                        metaVariableAppearsInCube = true;
+                        currentValuation.setBooleanValue(metaVariable, false);
+                    } else if (this->cube[globalToLocalIndexMap.at(ddMetaVariable.getDdVariables().front().getIndex())] == 1) {
+                        metaVariableAppearsInCube = true;
+                        currentValuation.setBooleanValue(metaVariable, true);
+                    } else {
+                        localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable, 0));
+                    }
+                } else {
+                    int_fast64_t intValue = 0;
+                    for (uint_fast64_t bitIndex = 0; bitIndex < ddMetaVariable.getNumberOfDdVariables(); ++bitIndex) {
+                        if (cube[globalToLocalIndexMap.at(ddMetaVariable.getDdVariables()[bitIndex].getIndex())] == 0) {
+                            // Leave bit unset.
+                            metaVariableAppearsInCube = true;
+                        } else if (cube[globalToLocalIndexMap.at(ddMetaVariable.getDdVariables()[bitIndex].getIndex())] == 1) {
+                            intValue |= 1ull << (ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1);
+                            metaVariableAppearsInCube = true;
+                        } else {
+                            // Temporarily leave bit unset so we can iterate trough the other option later.
+                            // Add the bit to the relevant don't care bits.
+                            localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable, ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1));
+                        }
+                    }
+                    if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) {
+                        currentValuation.setBitVectorValue(metaVariable, intValue + ddMetaVariable.getLow());
+                    }
+                }
+                
+                // If all meta variables are to be enumerated or the meta variable appeared in the cube, we register the
+                // missing bits to later enumerate all possible valuations.
+                if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) {
+                    relevantDontCareDdVariables.insert(relevantDontCareDdVariables.end(), localRelenvantDontCareDdVariables.begin(), localRelenvantDontCareDdVariables.end());
+                }
+            }
+            
+            // Finally, reset the cube counter.
+            this->cubeCounter = 0;
+        }
+    
+        template<typename ValueType>
+        void AddIterator<DdType::Sylvan, ValueType>::treatNextInCube() {
+            // Start by increasing the counter and check which bits we need to set/unset in the new valuation.
+            ++this->cubeCounter;
+            
+            for (uint_fast64_t index = 0; index < this->relevantDontCareDdVariables.size(); ++index) {
+                auto const& ddMetaVariable = this->ddManager->getMetaVariable(std::get<0>(this->relevantDontCareDdVariables[index]));
+                if (ddMetaVariable.getType() == MetaVariableType::Bool) {
+                    if ((this->cubeCounter & (1ull << index)) != 0) {
+                        currentValuation.setBooleanValue(std::get<0>(this->relevantDontCareDdVariables[index]), true);
+                    } else {
+                        currentValuation.setBooleanValue(std::get<0>(this->relevantDontCareDdVariables[index]), false);
+                    }
+                } else {
+                    storm::expressions::Variable const& metaVariable = std::get<0>(this->relevantDontCareDdVariables[index]);
+                    if ((this->cubeCounter & (1ull << index)) != 0) {
+                        currentValuation.setBitVectorValue(metaVariable, ((currentValuation.getBitVectorValue(metaVariable) - ddMetaVariable.getLow()) | (1ull << std::get<1>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow());
+                    } else {
+                        currentValuation.setBitVectorValue(metaVariable, ((currentValuation.getBitVectorValue(metaVariable) - ddMetaVariable.getLow()) & ~(1ull << std::get<1>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow());
+                    }
+                }
+            }
         }
         
         template class AddIterator<DdType::Sylvan, double>;

src/storage/dd/sylvan/SylvanAddIterator.h

@@ -1,9 +1,13 @@
 #ifndef STORM_STORAGE_DD_SYLVAN_SYLVANADDITERATOR_H_
 #define STORM_STORAGE_DD_SYLVAN_SYLVANADDITERATOR_H_
 
+#include <unordered_map>
+
 #include "src/storage/dd/AddIterator.h"
 #include "src/storage/expressions/SimpleValuation.h"
 
+#include "sylvan_obj.hpp"
+
 namespace storm {
     namespace dd {
         // Forward-declare the DdManager class.
@@ -61,6 +65,94 @@ namespace storm {
             bool operator!=(AddIterator<DdType::Sylvan, ValueType> const& other) const;
             
         private:
+            /*!
+             * Constructs a forward iterator using the given generator with the given set of relevant meta variables.
+             *
+             * @param ddManager The manager responsible for the DD over which to iterate.
+             * @param mtbdd The MTBDD over which to iterate.
+             * @param variables The variables contained in the MTBDD, represented as a cube.
+             * @param numberOfDdVariables The number of DD variables contained in this MTBDD.
+             * @param isAtEnd A flag that indicates whether the iterator is at its end and may not be moved forward any
+             * more.
+             * @param metaVariables The meta variables that appear in the DD.
+             * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even
+             * if a meta variable does not at all influence the the function value.
+             */
+            AddIterator(DdManager<DdType::Sylvan> const& ddManager, sylvan::Mtbdd mtbdd, sylvan::Bdd variables, uint_fast64_t numberOfDdVariables, bool isAtEnd, std::set<storm::expressions::Variable> const* metaVariables, bool enumerateDontCareMetaVariables);
+            
+            /*!
+             * Creates an iterator to the function argument-value-pairs of the given MTBDD.
+             *
+             * @param ddManager The manager responsible for the DD over which to iterate.
+             * @param mtbdd The MTBDD over which to iterate.
+             * @param variables The variables contained in the MTBDD, represented as a cube.
+             * @param numberOfDdVariables The number of DD variables contained in this MTBDD.
+             * @param metaVariables The meta variables that appear in the DD.
+             * @param enumerateDontCareMetaVariables If set to true, all meta variable assignments are enumerated, even
+             * if a meta variable does not at all influence the the function value.
+             */
+            static AddIterator createBeginIterator(DdManager<DdType::Sylvan> const& ddManager, sylvan::Mtbdd mtbdd, sylvan::Bdd variables, uint_fast64_t numberOfDdVariables, std::set<storm::expressions::Variable> const* metaVariables, bool enumerateDontCareMetaVariables = true);
+            
+            /*!
+             * Creates an iterator that can be used to determine the end of the iteration process.
+             *
+             * @param ddManager The manager responsible for the DD over which to iterate.
+             */
+            static AddIterator createEndIterator(DdManager<DdType::Sylvan> const& ddManager);
+            
+            /*!
+             * Recreates the internal information when a new cube needs to be treated.
+             */
+            void treatNewCube();
+            
+            /*!
+             * Updates the internal information when the next solution of the current cube needs to be treated.
+             */
+            void treatNextInCube();
+            
+            /*!
+             * Creates the mapping of global variable indices to local ones.
+             */
+            void createGlobalToLocalIndexMapping();
+            
+            // The manager responsible for the meta variables (and therefore the underlying DD).
+            DdManager<DdType::Sylvan> const* ddManager;
+
+            // The MTBDD over which to iterate.
+            sylvan::Mtbdd mtbdd;
+            
+            // The cube of variables in the MTBDD.
+            sylvan::Bdd variables;
+            
+            // The currently considered cube of the DD.
+            std::vector<uint8_t> cube;
+            
+            // The function value of the current cube, represented by the corresponding leaf.
+            MTBDD leaf;
+            
+            // A flag that indicates whether the iterator is at its end and may not be moved further. This is also used
+            // for the check against the end iterator.
+            bool isAtEnd;
+            
+            // The set of meta variables appearing in the DD.
+            std::set<storm::expressions::Variable> const* metaVariables;
+            
+            // A mapping from global variable indices to local (i.e. appearing the MTBDD) ones.
+            std::unordered_map<uint_fast64_t, uint_fast64_t> globalToLocalIndexMap;
+            
+            // A flag that indicates whether the iterator is supposed to enumerate meta variable valuations even if
+            // they don't influence the function value.
+            bool enumerateDontCareMetaVariables;
+            
+            // A number that represents how many assignments of the current cube have already been returned previously.
+            // This is needed, because cubes may represent many assignments (if they have don't care variables).
+            uint_fast64_t cubeCounter;
+            
+            // A vector of tuples of the form <metaVariable, bitIndex>.
+            std::vector<std::tuple<storm::expressions::Variable, uint_fast64_t>> relevantDontCareDdVariables;
+            
+            // The current valuation of meta variables.
+            storm::expressions::SimpleValuation currentValuation;
             
         };
     }

src/utility/solver.cpp

@@ -189,8 +189,10 @@ namespace storm {
             }
 
             template class SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>;
+            template class SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>;
             template class SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>;
             template class SymbolicGameSolverFactory<storm::dd::DdType::CUDD, double>;
+            template class SymbolicGameSolverFactory<storm::dd::DdType::Sylvan, double>;
             template class LinearEquationSolverFactory<double>;
             template class GmmxxLinearEquationSolverFactory<double>;
             template class NativeLinearEquationSolverFactory<double>;

test/functional/builder/DdPrismModelBuilderTest.cpp

@@ -17,16 +17,15 @@ TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) {
     EXPECT_EQ(13ul, model->getNumberOfStates());
     EXPECT_EQ(20ul, model->getNumberOfTransitions());
     
-    // FIXME: re-enable as soon as sylvan ADD-iterator is done.
-//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
-//    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
-//    EXPECT_EQ(677ul, model->getNumberOfStates());
-//    EXPECT_EQ(867ul, model->getNumberOfTransitions());
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+    EXPECT_EQ(677ul, model->getNumberOfStates());
+    EXPECT_EQ(867ul, model->getNumberOfTransitions());
 
-//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
-//    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
-//    EXPECT_EQ(8607ul, model->getNumberOfStates());
-//    EXPECT_EQ(15113ul, model->getNumberOfTransitions());
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+    EXPECT_EQ(8607ul, model->getNumberOfStates());
+    EXPECT_EQ(15113ul, model->getNumberOfTransitions());
 
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
@@ -180,16 +179,15 @@ TEST(DdPrismModelBuilderTest_Sylvan, Mdp) {
     EXPECT_EQ(5585ul, mdp->getNumberOfTransitions());
     EXPECT_EQ(5519ul, mdp->getNumberOfChoices());
 
-    // FIXME: re-enable after Sylvan ADD iterator is done.
-//    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
-//    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
-//    
-//    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
-//    mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
-//    
-//    EXPECT_EQ(37ul, mdp->getNumberOfStates());
-//    EXPECT_EQ(59ul, mdp->getNumberOfTransitions());
-//    EXPECT_EQ(59ul, mdp->getNumberOfChoices());
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+    
+    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+    mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
+    
+    EXPECT_EQ(37ul, mdp->getNumberOfStates());
+    EXPECT_EQ(59ul, mdp->getNumberOfTransitions());
+    EXPECT_EQ(59ul, mdp->getNumberOfChoices());
 }
 
 TEST(DdPrismModelBuilderTest_Cudd, Mdp) {

test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp

@@ -17,7 +17,7 @@
 
 #include "src/settings/modules/GeneralSettings.h"
 
-TEST(SymbolicDtmcPrctlModelCheckerTest, Die) {
+TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
     
     // A parser that we use for conveniently constructing the formulas.
@@ -78,7 +78,68 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) {
     EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
 }
 
-TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) {
+TEST(SymbolicDtmcPrctlModelCheckerTest, Die_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+    
+    // Build the die model with its reward model.
+#ifdef WINDOWS
+    storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
+#else
+    typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
+#endif
+    options.buildAllRewardModels = false;
+    options.rewardModelsToBuild.insert("coin_flips");
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+    EXPECT_EQ(13ul, model->getNumberOfStates());
+    EXPECT_EQ(20ul, model->getNumberOfTransitions());
+    
+    ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
+    
+    std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>();
+    
+    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
+    
+    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
+    
+    EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
+    
+    result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
+    
+    EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
+    
+    result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
+    
+    EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
+    
+    result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
+    
+    EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    EXPECT_NEAR(3.6666622161865234, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
+}
+
+TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
     
     // A parser that we use for conveniently constructing the formulas.
@@ -122,7 +183,51 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) {
     EXPECT_NEAR(0.3215392962289586, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
 }
 
-TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) {
+TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+    
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+    EXPECT_EQ(8607ul, model->getNumberOfStates());
+    EXPECT_EQ(15113ul, model->getNumberOfTransitions());
+    
+    ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
+    
+    std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>();
+    
+    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
+    
+    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
+    
+    EXPECT_NEAR(0.33288236360191303, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    EXPECT_NEAR(0.33288236360191303, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
+    
+    result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
+    
+    EXPECT_NEAR(0.15222081144084315, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    EXPECT_NEAR(0.15222081144084315, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
+    
+    result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
+    
+    EXPECT_NEAR(0.3215392962289586, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    EXPECT_NEAR(0.3215392962289586, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
+}
+
+TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
     
     // A parser that we use for conveniently constructing the formulas.
@@ -174,3 +279,54 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) {
     EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
 }
 
+TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+    
+    // Build the die model with its reward model.
+#ifdef WINDOWS
+    storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
+#else
+    typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
+#endif
+    options.buildAllRewardModels = false;
+    options.rewardModelsToBuild.insert("num_rounds");
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
+    EXPECT_EQ(273ul, model->getNumberOfStates());
+    EXPECT_EQ(397ul, model->getNumberOfTransitions());
+    
+    ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
+    
+    std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>();
+    
+    storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
+    
+    std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
+    
+    EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
+    
+    result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
+    
+    EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
+    
+    result = checker.check(*formula);
+    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
+    storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
+    
+    EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    EXPECT_NEAR(1.0416666666666643, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
+}

test/functional/solver/FullySymbolicGameSolverTest.cpp

@@ -8,7 +8,7 @@
 #include "src/solver/SymbolicGameSolver.h"
 #include "src/settings/modules/NativeEquationSolverSettings.h"
 
-TEST(FullySymbolicGameSolverTest, Solve) {
+TEST(FullySymbolicGameSolverTest, Solve_Cudd) {
     // Create some variables.
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     std::pair<storm::expressions::Variable, storm::expressions::Variable> state = manager->addMetaVariable("x", 1, 4);
@@ -59,6 +59,64 @@ TEST(FullySymbolicGameSolverTest, Solve) {
     result = result.sumAbstract({state.first});
     EXPECT_NEAR(0.2, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision());
 
+    x = manager->getAddZero<double>();
+    result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, x, b);
+    result *= manager->getEncoding(state.first, 1).template toAdd<double>();
+    result = result.sumAbstract({state.first});
+    EXPECT_NEAR(0.99999892625817599, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision());
+}
+
+TEST(FullySymbolicGameSolverTest, Solve_Sylvan) {
+    // Create some variables.
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> state = manager->addMetaVariable("x", 1, 4);
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> pl1 = manager->addMetaVariable("a", 0, 1);
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> pl2 = manager->addMetaVariable("b", 0, 1);
+    
+    storm::dd::Bdd<storm::dd::DdType::Sylvan> allRows = manager->getBddZero();
+    std::set<storm::expressions::Variable> rowMetaVariables({state.first});
+    std::set<storm::expressions::Variable> columnMetaVariables({state.second});
+    std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs = {state};
+    std::set<storm::expressions::Variable> player1Variables({pl1.first});
+    std::set<storm::expressions::Variable> player2Variables({pl2.first});
+    
+    // Construct simple game.
+    storm::dd::Add<storm::dd::DdType::Sylvan, double> matrix = manager->getEncoding(state.first, 1).template toAdd<double>() * manager->getEncoding(state.second, 2).template toAdd<double>() * manager->getEncoding(pl1.first, 0).template toAdd<double>() * manager->getEncoding(pl2.first, 0).template toAdd<double>() * manager->getConstant(0.6);
+    matrix += manager->getEncoding(state.first, 1).template toAdd<double>() * manager->getEncoding(state.second, 1).template toAdd<double>() * manager->getEncoding(pl1.first, 0).template toAdd<double>() * manager->getEncoding(pl2.first, 0).template toAdd<double>() * manager->getConstant(0.4);
+    
+    matrix += manager->getEncoding(state.first, 1).template toAdd<double>() * manager->getEncoding(state.second, 2).template toAdd<double>() * manager->getEncoding(pl1.first, 0).template toAdd<double>() * manager->getEncoding(pl2.first, 1).template toAdd<double>() * manager->getConstant(0.2);
+    matrix += manager->getEncoding(state.first, 1).template toAdd<double>() * manager->getEncoding(state.second, 3).template toAdd<double>() * manager->getEncoding(pl1.first, 0).template toAdd<double>() * manager->getEncoding(pl2.first, 1).template toAdd<double>() * manager->getConstant(0.8);
+    
+    matrix += manager->getEncoding(state.first, 1).template toAdd<double>() * manager->getEncoding(state.second, 3).template toAdd<double>() * manager->getEncoding(pl1.first, 1).template toAdd<double>() * manager->getEncoding(pl2.first, 0).template toAdd<double>() * manager->getConstant(0.5);
+    matrix += manager->getEncoding(state.first, 1).template toAdd<double>() * manager->getEncoding(state.second, 4).template toAdd<double>() * manager->getEncoding(pl1.first, 1).template toAdd<double>() * manager->getEncoding(pl2.first, 0).template toAdd<double>() * manager->getConstant(0.5);
+    
+    matrix += manager->getEncoding(state.first, 1).template toAdd<double>() * manager->getEncoding(state.second, 1).template toAdd<double>() * manager->getEncoding(pl1.first, 1).template toAdd<double>() * manager->getEncoding(pl2.first, 1).template toAdd<double>() * manager->getConstant<double>(1);
+    
+    std::unique_ptr<storm::utility::solver::SymbolicGameSolverFactory<storm::dd::DdType::Sylvan, double>> solverFactory(new storm::utility::solver::SymbolicGameSolverFactory<storm::dd::DdType::Sylvan, double>());
+    std::unique_ptr<storm::solver::SymbolicGameSolver<storm::dd::DdType::Sylvan>> solver = solverFactory->create(matrix, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs, player1Variables,player2Variables);
+    
+    // Create solution and target state vector.
+    storm::dd::Add<storm::dd::DdType::Sylvan, double> x = manager->template getAddZero<double>();
+    storm::dd::Add<storm::dd::DdType::Sylvan, double> b = manager->getEncoding(state.first, 2).template toAdd<double>() + manager->getEncoding(state.first, 4).template toAdd<double>();
+    
+    // Now solve the game with different strategies for the players.
+    storm::dd::Add<storm::dd::DdType::Sylvan> result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, x, b);
+    result *= manager->getEncoding(state.first, 1).template toAdd<double>();
+    result = result.sumAbstract({state.first});
+    EXPECT_NEAR(0, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    
+    x = manager->getAddZero<double>();
+    result = solver->solveGame(storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize, x, b);
+    result *= manager->getEncoding(state.first, 1).template toAdd<double>();
+    result = result.sumAbstract({state.first});
+    EXPECT_NEAR(0.5, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    
+    x = manager->getAddZero<double>();
+    result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize, x, b);
+    result *= manager->getEncoding(state.first, 1).template toAdd<double>();
+    result = result.sumAbstract({state.first});
+    EXPECT_NEAR(0.2, result.getValue(), storm::settings::nativeEquationSolverSettings().getPrecision());
+    
     x = manager->getAddZero<double>();
     result = solver->solveGame(storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, x, b);
     result *= manager->getEncoding(state.first, 1).template toAdd<double>();

test/functional/storage/CuddDdTest.cpp

@@ -275,7 +275,7 @@ TEST(CuddDd, GetSetValueTest) {
     EXPECT_EQ(2, dd1.getValue(metaVariableToValueMap));
 }
 
-TEST(CuddDd, ForwardIteratorTest) {
+TEST(CuddDd, AddIteratorTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::CUDD>> manager(new storm::dd::DdManager<storm::dd::DdType::CUDD>());
     std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
     std::pair<storm::expressions::Variable, storm::expressions::Variable> y = manager->addMetaVariable("y", 0, 3);

test/functional/storage/SylvanDdTest.cpp

@@ -278,48 +278,49 @@ TEST(SylvanDd, GetSetValueTest) {
     EXPECT_EQ(2, dd1.getValue(metaVariableToValueMap));
 }
 
-//TEST(SylvanDd, ForwardIteratorTest) {
-//    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
-//    std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
-//    std::pair<storm::expressions::Variable, storm::expressions::Variable> y = manager->addMetaVariable("y", 0, 3);
-//    
-//    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd;
-//    ASSERT_NO_THROW(dd = manager->getRange(x.first).template toAdd<double>());
-//    
-//    storm::dd::AddIterator<storm::dd::DdType::Sylvan, double> it, ite;
-//    ASSERT_NO_THROW(it = dd.begin());
-//    ASSERT_NO_THROW(ite = dd.end());
-//    std::pair<storm::expressions::SimpleValuation, double> valuationValuePair;
-//    uint_fast64_t numberOfValuations = 0;
-//    while (it != ite) {
-//        ASSERT_NO_THROW(valuationValuePair = *it);
-//        ASSERT_NO_THROW(++it);
-//        ++numberOfValuations;
-//    }
-//    EXPECT_EQ(9ul, numberOfValuations);
-//    
-//    dd = manager->getRange(x.first).template toAdd<double>();
-//    dd = dd.ite(manager->template getAddOne<double>(), manager->template getAddOne<double>());
-//    ASSERT_NO_THROW(it = dd.begin());
-//    ASSERT_NO_THROW(ite = dd.end());
-//    numberOfValuations = 0;
-//    while (it != ite) {
-//        ASSERT_NO_THROW(valuationValuePair = *it);
-//        ASSERT_NO_THROW(++it);
-//        ++numberOfValuations;
-//    }
-//    EXPECT_EQ(16ul, numberOfValuations);
-//    
-//    ASSERT_NO_THROW(it = dd.begin(false));
-//    ASSERT_NO_THROW(ite = dd.end());
-//    numberOfValuations = 0;
-//    while (it != ite) {
-//        ASSERT_NO_THROW(valuationValuePair = *it);
-//        ASSERT_NO_THROW(++it);
-//        ++numberOfValuations;
-//    }
-//    EXPECT_EQ(1ul, numberOfValuations);
-//}
+TEST(SylvanDd, AddIteratorTest) {
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> y = manager->addMetaVariable("y", 0, 3);
+    
+    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd;
+    ASSERT_NO_THROW(dd = manager->getRange(x.first).template toAdd<double>());
+    
+    storm::dd::AddIterator<storm::dd::DdType::Sylvan, double> it, ite;
+    ASSERT_NO_THROW(it = dd.begin());
+    ASSERT_NO_THROW(ite = dd.end());
+    std::pair<storm::expressions::SimpleValuation, double> valuationValuePair;
+    uint_fast64_t numberOfValuations = 0;
+    dd.exportToDot("dd.dot");
+    while (it != ite) {
+        ASSERT_NO_THROW(valuationValuePair = *it);
+        ASSERT_NO_THROW(++it);
+        ++numberOfValuations;
+    }
+    EXPECT_EQ(9ul, numberOfValuations);
+    
+    dd = manager->getRange(x.first).template toAdd<double>();
+    dd = dd.ite(manager->template getAddOne<double>(), manager->template getAddOne<double>());
+    ASSERT_NO_THROW(it = dd.begin());
+    ASSERT_NO_THROW(ite = dd.end());
+    numberOfValuations = 0;
+    while (it != ite) {
+        ASSERT_NO_THROW(valuationValuePair = *it);
+        ASSERT_NO_THROW(++it);
+        ++numberOfValuations;
+    }
+    EXPECT_EQ(16ul, numberOfValuations);
+    
+    ASSERT_NO_THROW(it = dd.begin(false));
+    ASSERT_NO_THROW(ite = dd.end());
+    numberOfValuations = 0;
+    while (it != ite) {
+        ASSERT_NO_THROW(valuationValuePair = *it);
+        ASSERT_NO_THROW(++it);
+        ++numberOfValuations;
+    }
+    EXPECT_EQ(1ul, numberOfValuations);
+}
 
 TEST(SylvanDd, AddOddTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());

test/functional/utility/GraphTest.cpp

@@ -36,8 +36,7 @@ TEST(GraphTest, SymbolicProb01_Cudd) {
     EXPECT_EQ(1032ul, statesWithProbability01.second.getNonZeroCount());
 }
 
-// FIXME: re-enable as soon as the ADD iterator of sylvan works.
-TEST(DISABLED_GraphTest, SymbolicProb01_Sylvan) {
+TEST(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);