more work on the dd stuff *sigh*

Former-commit-id: df8e227336

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

@@ -543,10 +543,17 @@ Cudd_DumpDot(
 		scan = nodelist[j];
 		while (scan != NULL) {
 		    if (st_is_member(visited,(char *) scan)) {
-            retval = fprintf(fp,
+                if (inames != NULL) {
+                    retval = fprintf(fp,
                     "\"%p\" [label = \"%s\"];\n",
                     (void *) ((mask & (ptrint) scan) /
                     sizeof(DdNode)), inames[dd->invperm[i]]);
+                } else {
+                    retval = fprintf(fp,
+                    "\"%p\" [label = \"%i\"];\n",
+                    (void *) ((mask & (ptrint) scan) /
+                    sizeof(DdNode)), i);
+                }
             if (retval == EOF) goto failure;
             if (cuddT(scan) != Cudd_ReadZero(dd)) {
 			retval = fprintf(fp,

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

@@ -43,7 +43,7 @@ TASK_IMPL_2(MTBDD, mtbdd_op_divide, MTBDD*, pa, MTBDD*, pb)
                 
                 int nega = mtbdd_isnegated(a);
                 int negb = mtbdd_isnegated(b);
-                result = mtbdd_double(a / b);
+                result = mtbdd_double(vval_a / vval_b);
                 if (nega ^ negb) return mtbdd_negate(result);
                 else return result;
             }

resources/3rdparty/xercesc-3.1.2/Makefile

@@ -305,7 +305,7 @@ ICU_FLAGS =
 ICU_LIBS = -licuuc -licudata
 ICU_PRESENT = no
 ICU_SBIN = 
-INSTALL = /usr/local/bin/ginstall -c
+INSTALL = /usr/bin/install -c
 INSTALL_DATA = ${INSTALL} -m 644
 INSTALL_PROGRAM = ${INSTALL}
 INSTALL_SCRIPT = ${INSTALL}
@@ -322,7 +322,7 @@ LT_SYS_LIBRARY_PATH =
 MAINT = #
 MAKEINFO = ${SHELL} /Users/chris/work/storm/resources/3rdparty/xercesc-3.1.2/config/missing makeinfo
 MANIFEST_TOOL = :
-MKDIR_P = /usr/local/bin/gmkdir -p
+MKDIR_P = config/install-sh -c -d
 NM = /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/nm
 NMEDIT = nmedit
 OBJDUMP = objdump

resources/3rdparty/xercesc-3.1.2/config.status

@@ -439,8 +439,8 @@ gives unlimited permission to copy, distribute and modify it."
 
 ac_pwd='/Users/chris/work/storm/resources/3rdparty/xercesc-3.1.2'
 srcdir='.'
-INSTALL='/usr/local/bin/ginstall -c'
-MKDIR_P='/usr/local/bin/gmkdir -p'
+INSTALL='/usr/bin/install -c'
+MKDIR_P='config/install-sh -c -d'
 AWK='awk'
 test -n "$AWK" || AWK=awk
 # The default lists apply if the user does not specify any file.
@@ -998,7 +998,7 @@ S["am__leading_dot"]="."
 S["SET_MAKE"]=""
 S["AWK"]="awk"
 S["mkdir_p"]="$(MKDIR_P)"
-S["MKDIR_P"]="/usr/local/bin/gmkdir -p"
+S["MKDIR_P"]="config/install-sh -c -d"
 S["INSTALL_STRIP_PROGRAM"]="$(install_sh) -c -s"
 S["STRIP"]="strip"
 S["install_sh"]="${SHELL} /Users/chris/work/storm/resources/3rdparty/xercesc-3.1.2/config/install-sh"

resources/3rdparty/xercesc-3.1.2/libtool

@@ -1,6 +1,6 @@
 #! /bin/sh
 # Generated automatically by config.status (xerces-c) 3.1.2
-# Libtool was configured on host Christians-iMac.fritz.box:
+# Libtool was configured on host tartaros.informatik.rwth-aachen.de:
 # NOTE: Changes made to this file will be lost: look at ltmain.sh.
 
 # Provide generalized library-building support services.

resources/3rdparty/xercesc-3.1.2/samples/Makefile

@@ -358,7 +358,7 @@ ICU_FLAGS =
 ICU_LIBS = -licuuc -licudata
 ICU_PRESENT = no
 ICU_SBIN = 
-INSTALL = /usr/local/bin/ginstall -c
+INSTALL = /usr/bin/install -c
 INSTALL_DATA = ${INSTALL} -m 644
 INSTALL_PROGRAM = ${INSTALL}
 INSTALL_SCRIPT = ${INSTALL}
@@ -375,7 +375,7 @@ LT_SYS_LIBRARY_PATH =
 MAINT = #
 MAKEINFO = ${SHELL} /Users/chris/work/storm/resources/3rdparty/xercesc-3.1.2/config/missing makeinfo
 MANIFEST_TOOL = :
-MKDIR_P = /usr/local/bin/gmkdir -p
+MKDIR_P = ../config/install-sh -c -d
 NM = /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/nm
 NMEDIT = nmedit
 OBJDUMP = objdump

resources/3rdparty/xercesc-3.1.2/src/Makefile

@@ -1426,7 +1426,7 @@ ICU_FLAGS =
 ICU_LIBS = -licuuc -licudata
 ICU_PRESENT = no
 ICU_SBIN = 
-INSTALL = /usr/local/bin/ginstall -c
+INSTALL = /usr/bin/install -c
 INSTALL_DATA = ${INSTALL} -m 644
 INSTALL_PROGRAM = ${INSTALL}
 INSTALL_SCRIPT = ${INSTALL}
@@ -1443,7 +1443,7 @@ LT_SYS_LIBRARY_PATH =
 MAINT = #
 MAKEINFO = ${SHELL} /Users/chris/work/storm/resources/3rdparty/xercesc-3.1.2/config/missing makeinfo
 MANIFEST_TOOL = :
-MKDIR_P = /usr/local/bin/gmkdir -p
+MKDIR_P = ../config/install-sh -c -d
 NM = /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/nm
 NMEDIT = nmedit
 OBJDUMP = objdump

resources/3rdparty/xercesc-3.1.2/src/xercesc/util/MsgLoaders/MsgCatalog/Makefile

@@ -3,7 +3,7 @@ srcdir = .
 top_srcdir = ../../../../..
 top_builddir = ../../../../..
 prefix = /Users/chris/work/storm/build_xcode/resources/3rdparty/xercesc-3.1.2
-INSTALL = /usr/local/bin/ginstall -c
+INSTALL = /usr/bin/install -c
 INSTALL_PROGRAM = ${INSTALL}
 mkdir_p = $(MKDIR_P)
 

resources/3rdparty/xercesc-3.1.2/tests/Makefile

@@ -342,7 +342,7 @@ ICU_FLAGS =
 ICU_LIBS = -licuuc -licudata
 ICU_PRESENT = no
 ICU_SBIN = 
-INSTALL = /usr/local/bin/ginstall -c
+INSTALL = /usr/bin/install -c
 INSTALL_DATA = ${INSTALL} -m 644
 INSTALL_PROGRAM = ${INSTALL}
 INSTALL_SCRIPT = ${INSTALL}
@@ -359,7 +359,7 @@ LT_SYS_LIBRARY_PATH =
 MAINT = #
 MAKEINFO = ${SHELL} /Users/chris/work/storm/resources/3rdparty/xercesc-3.1.2/config/missing makeinfo
 MANIFEST_TOOL = :
-MKDIR_P = /usr/local/bin/gmkdir -p
+MKDIR_P = ../config/install-sh -c -d
 NM = /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin/nm
 NMEDIT = nmedit
 OBJDUMP = objdump

src/adapters/AddExpressionAdapter.cpp

@@ -17,20 +17,33 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        storm::dd::Add<Type> AddExpressionAdapter<Type, ValueType>::translateExpression(storm::expressions::Expression const& expression) {
+        storm::dd::Add<Type, ValueType> AddExpressionAdapter<Type, ValueType>::translateExpression(storm::expressions::Expression const& expression) {
             if (expression.hasBooleanType()) {
                 return boost::any_cast<storm::dd::Bdd<Type>>(expression.accept(*this)).template toAdd<ValueType>();
             } else {
-                return boost::any_cast<storm::dd::Add<Type>>(expression.accept(*this));
+                return boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.accept(*this));
             }
         }
         
+        template<storm::dd::DdType Type, typename ValueType>
+        storm::dd::Bdd<Type> AddExpressionAdapter<Type, ValueType>::translateBooleanExpression(storm::expressions::Expression const& expression) {
+            STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expected expression of boolean type.");
+            return boost::any_cast<storm::dd::Bdd<Type>>(expression.accept(*this));
+        }
+        
         template<storm::dd::DdType Type, typename ValueType>
         boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::IfThenElseExpression const& expression) {
-            storm::dd::Add<Type> elseDd = boost::any_cast<storm::dd::Add<Type>>(expression.getElseExpression()->accept(*this));
-            storm::dd::Add<Type> thenDd = boost::any_cast<storm::dd::Add<Type>>(expression.getThenExpression()->accept(*this));
-            storm::dd::Add<Type> conditionDd = boost::any_cast<storm::dd::Add<Type>>(expression.getCondition()->accept(*this));
-            return conditionDd.ite(thenDd, elseDd);
+            if (expression.hasBooleanType()) {
+                storm::dd::Bdd<Type> elseDd = boost::any_cast<storm::dd::Bdd<Type>>(expression.getElseExpression()->accept(*this));
+                storm::dd::Bdd<Type> thenDd = boost::any_cast<storm::dd::Bdd<Type>>(expression.getThenExpression()->accept(*this));
+                storm::dd::Bdd<Type> conditionDd = boost::any_cast<storm::dd::Bdd<Type>>(expression.getCondition()->accept(*this));
+                return conditionDd.ite(thenDd, elseDd);
+            } else {
+                storm::dd::Add<Type, ValueType> elseDd = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getElseExpression()->accept(*this));
+                storm::dd::Add<Type, ValueType> thenDd = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getThenExpression()->accept(*this));
+                storm::dd::Add<Type, ValueType> conditionDd = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getCondition()->accept(*this));
+                return conditionDd.ite(thenDd, elseDd);
+            }
         }
         
         template<storm::dd::DdType Type, typename ValueType>
@@ -62,10 +75,10 @@ namespace storm {
         
         template<storm::dd::DdType Type, typename ValueType>
         boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression) {
-            storm::dd::Add<Type> leftResult = boost::any_cast<storm::dd::Add<Type>>(expression.getFirstOperand()->accept(*this));
-            storm::dd::Add<Type> rightResult = boost::any_cast<storm::dd::Add<Type>>(expression.getSecondOperand()->accept(*this));
+            storm::dd::Add<Type, ValueType> leftResult = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getFirstOperand()->accept(*this));
+            storm::dd::Add<Type, ValueType> rightResult = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getSecondOperand()->accept(*this));
             
-            storm::dd::Add<Type> result;
+            storm::dd::Add<Type, ValueType> result;
             switch (expression.getOperatorType()) {
                 case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus:
                     result = leftResult + rightResult;
@@ -97,8 +110,8 @@ namespace storm {
         
         template<storm::dd::DdType Type, typename ValueType>
         boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::BinaryRelationExpression const& expression) {
-            storm::dd::Add<Type> leftResult = boost::any_cast<storm::dd::Add<Type>>(expression.getFirstOperand()->accept(*this));
-            storm::dd::Add<Type> rightResult = boost::any_cast<storm::dd::Add<Type>>(expression.getSecondOperand()->accept(*this));
+            storm::dd::Add<Type, ValueType> leftResult = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getFirstOperand()->accept(*this));
+            storm::dd::Add<Type, ValueType> rightResult = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getSecondOperand()->accept(*this));
 
             storm::dd::Bdd<Type> result;
             switch (expression.getRelationType()) {
@@ -151,7 +164,7 @@ namespace storm {
         
         template<storm::dd::DdType Type, typename ValueType>
         boost::any AddExpressionAdapter<Type, ValueType>::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) {
-            storm::dd::Add<Type> result = boost::any_cast<storm::dd::Add<Type>>(expression.getOperand()->accept(*this));
+            storm::dd::Add<Type, ValueType> result = boost::any_cast<storm::dd::Add<Type, ValueType>>(expression.getOperand()->accept(*this));
             
             switch (expression.getOperatorType()) {
                 case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus:
@@ -187,6 +200,7 @@ namespace storm {
         
         // Explicitly instantiate the symbolic expression adapter
         template class AddExpressionAdapter<storm::dd::DdType::CUDD, double>;
+        template class AddExpressionAdapter<storm::dd::DdType::Sylvan, double>;
         
     } // namespace adapters
 } // namespace storm

src/adapters/AddExpressionAdapter.h

@@ -6,6 +6,7 @@
 #include "storage/expressions/ExpressionVisitor.h"
 
 #include "src/storage/dd/Add.h"
+#include "src/storage/dd/Bdd.h"
 #include "src/storage/dd/DdManager.h"
 
 namespace storm {
@@ -16,7 +17,8 @@ namespace storm {
         public:
             AddExpressionAdapter(std::shared_ptr<storm::dd::DdManager<Type>> ddManager, std::map<storm::expressions::Variable, storm::expressions::Variable> const& variableMapping);
             
-            storm::dd::Add<Type> translateExpression(storm::expressions::Expression const& expression);
+            storm::dd::Add<Type, ValueType> translateExpression(storm::expressions::Expression const& expression);
+            storm::dd::Bdd<Type> translateBooleanExpression(storm::expressions::Expression const& expression);
             
             virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression) override;
             virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) override;

src/builder/DdPrismModelBuilder.cpp

@@ -144,8 +144,8 @@ namespace storm {
 
                     // Create meta variables for each of the modules' variables.
                     for (storm::prism::Module const& module : program.getModules()) {
-                        storm::dd::Add<Type, ValueType> moduleIdentity = manager->template getAddOne<ValueType>();
-                        storm::dd::Add<Type, ValueType> moduleRange = manager->template getAddOne<ValueType>();
+                        storm::dd::Bdd<Type> moduleIdentity = manager->getBddOne();
+                        storm::dd::Bdd<Type> moduleRange = manager->getBddOne();
                         
                         for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) {
                             int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt();
@@ -159,10 +159,10 @@ namespace storm {
                             columnMetaVariables.insert(variablePair.second);
                             variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second);
                             
-                            storm::dd::Add<Type, ValueType> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>() * manager->getRange(variablePair.first).template toAdd<ValueType>() * manager->getRange(variablePair.second).template toAdd<ValueType>();
-                            variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity);
-                            moduleIdentity *= variableIdentity;
-                            moduleRange *= manager->getRange(variablePair.first).template toAdd<ValueType>();
+                            storm::dd::Bdd<Type> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second);
+                            variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
+                            moduleIdentity &= variableIdentity;
+                            moduleRange &= manager->getRange(variablePair.first);
                             
                             rowColumnMetaVariablePairs.push_back(variablePair);
                         }
@@ -176,15 +176,15 @@ namespace storm {
                             columnMetaVariables.insert(variablePair.second);
                             variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second);
                             
-                            storm::dd::Add<Type, ValueType> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>() * manager->getRange(variablePair.first).template toAdd<ValueType>() * manager->getRange(variablePair.second).template toAdd<ValueType>();
-                            variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity);
-                            moduleIdentity *= variableIdentity;
-                            moduleRange *= manager->getRange(variablePair.first).template toAdd<ValueType>();
+                            storm::dd::Bdd<Type> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second);
+                            variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
+                            moduleIdentity &= variableIdentity;
+                            moduleRange &= manager->getRange(variablePair.first);
 
                             rowColumnMetaVariablePairs.push_back(variablePair);
                         }
-                        moduleToIdentityMap[module.getName()] = moduleIdentity;
-                        moduleToRangeMap[module.getName()] = moduleRange;
+                        moduleToIdentityMap[module.getName()] = moduleIdentity.template toAdd<ValueType>();
+                        moduleToRangeMap[module.getName()] = moduleRange.template toAdd<ValueType>();
                     }
                 }
             };
@@ -347,6 +347,7 @@ namespace storm {
             std::set<storm::expressions::Variable> assignedGlobalVariables;
             std::set_intersection(assignedVariables.begin(), assignedVariables.end(), generationInfo.allGlobalVariables.begin(), generationInfo.allGlobalVariables.end(), std::inserter(assignedGlobalVariables, assignedGlobalVariables.begin()));
             
+            int index = 0;
             // All unassigned boolean variables need to keep their value.
             for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) {
                 if (assignedVariables.find(booleanVariable.getExpressionVariable()) == assignedVariables.end()) {
@@ -369,14 +370,14 @@ namespace storm {
         template <storm::dd::DdType Type, typename ValueType>
         typename DdPrismModelBuilder<Type, ValueType>::ActionDecisionDiagram DdPrismModelBuilder<Type, ValueType>::createCommandDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::prism::Command const& command) {
             STORM_LOG_TRACE("Translating guard " << command.getGuardExpression());
-            storm::dd::Add<Type, ValueType> guardDd = generationInfo.rowExpressionAdapter->translateExpression(command.getGuardExpression()) * generationInfo.moduleToRangeMap[module.getName()];
-            STORM_LOG_WARN_COND(!guardDd.isZero(), "The guard '" << command.getGuardExpression() << "' is unsatisfiable.");
+            storm::dd::Add<Type, ValueType> guard = generationInfo.rowExpressionAdapter->translateExpression(command.getGuardExpression()) * generationInfo.moduleToRangeMap[module.getName()];
+            STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << command.getGuardExpression() << "' is unsatisfiable.");
             
-            if (!guardDd.isZero()) {
+            if (!guard.isZero()) {
                 // Create the DDs representing the individual updates.
                 std::vector<UpdateDecisionDiagram> updateResults;
                 for (storm::prism::Update const& update : command.getUpdates()) {
-                    updateResults.push_back(createUpdateDecisionDiagram(generationInfo, module, guardDd, update));
+                    updateResults.push_back(createUpdateDecisionDiagram(generationInfo, module, guard, update));
                     
                     STORM_LOG_WARN_COND(!updateResults.back().updateDd.isZero(), "Update '" << update << "' does not have any effect.");
                 }
@@ -412,7 +413,7 @@ namespace storm {
                     commandDd += updateResultsIt->updateDd * probabilityDd;
                 }
                 
-                return ActionDecisionDiagram(guardDd, guardDd * commandDd, globalVariablesInSomeUpdate);
+                return ActionDecisionDiagram(guard, guard * commandDd, globalVariablesInSomeUpdate);
             } else {
                 return ActionDecisionDiagram(*generationInfo.manager);
             }
@@ -516,7 +517,7 @@ namespace storm {
                 STORM_LOG_WARN_COND(temporary.isZero() || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC, "Guard of a command overlaps with previous guards.");
                 
                 allGuards += commandDd.guardDd;
-                allCommands += commandDd.guardDd * commandDd.transitionsDd ;
+                allCommands += commandDd.guardDd * commandDd.transitionsDd;
             }
             
             return ActionDecisionDiagram(allGuards, allCommands, assignedGlobalVariables);
@@ -1028,6 +1029,7 @@ namespace storm {
 
             SystemResult system = createSystemDecisionDiagram(generationInfo);
             storm::dd::Add<Type, ValueType> transitionMatrix = system.allTransitionsDd;
+            
             ModuleDecisionDiagram const& globalModule = system.globalModule;
             storm::dd::Add<Type, ValueType> stateActionDd = system.stateActionDd;
             
@@ -1073,7 +1075,7 @@ namespace storm {
             storm::dd::Add<Type, ValueType> reachableStatesAdd = reachableStates.template toAdd<ValueType>();
             transitionMatrix *= reachableStatesAdd;
             stateActionDd *= reachableStatesAdd;
-
+            
             // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise.
             storm::dd::Bdd<Type> statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables);
             storm::dd::Add<Type, ValueType> deadlockStates = (reachableStates && !statesWithTransition).template toAdd<ValueType>();
@@ -1172,11 +1174,9 @@ namespace storm {
             do {
                 STORM_LOG_TRACE("Iteration " << iteration << " of reachability analysis.");
                 changed = false;
-                storm::dd::Bdd<Type> tmp = reachableStates.andExists(transitionBdd, generationInfo.rowMetaVariables);
-                tmp = tmp.swapVariables(generationInfo.rowColumnMetaVariablePairs);
-
+                storm::dd::Bdd<Type> tmp = reachableStates.relationalProduct(transitionBdd, generationInfo.rowMetaVariables);
                 storm::dd::Bdd<Type> newReachableStates = tmp && (!reachableStates);
-                
+                                
                 // Check whether new states were indeed discovered.
                 if (!newReachableStates.isZero()) {
                     changed = true;
@@ -1189,9 +1189,10 @@ namespace storm {
             return reachableStates;
         }
         
-        // Explicitly instantiate the symbolic expression adapter
+        // Explicitly instantiate the symbolic model builder.
         template class DdPrismModelBuilder<storm::dd::DdType::CUDD>;
-        
+        template class DdPrismModelBuilder<storm::dd::DdType::Sylvan>;
+
     } // namespace adapters
 } // namespace storm
 

src/models/symbolic/Ctmc.cpp

@@ -33,6 +33,7 @@ namespace storm {
             
             // Explicitly instantiate the template class.
             template class Ctmc<storm::dd::DdType::CUDD, double>;
+            template class Ctmc<storm::dd::DdType::Sylvan, double>;
             
         } // namespace symbolic
     } // namespace models

src/models/symbolic/DeterministicModel.cpp

@@ -29,6 +29,7 @@ namespace storm {
             
             // Explicitly instantiate the template class.
             template class DeterministicModel<storm::dd::DdType::CUDD>;
+            template class DeterministicModel<storm::dd::DdType::Sylvan>;
             
         } // namespace symbolic
     } // namespace models

src/models/symbolic/Dtmc.cpp

@@ -28,6 +28,7 @@ namespace storm {
             
             // Explicitly instantiate the template class.
             template class Dtmc<storm::dd::DdType::CUDD, double>;
+            template class Dtmc<storm::dd::DdType::Sylvan, double>;
             
         } // namespace symbolic
     } // namespace models

src/models/symbolic/Mdp.cpp

@@ -28,7 +28,8 @@ namespace storm {
             }
             
             // Explicitly instantiate the template class.
-            template class Mdp<storm::dd::DdType::CUDD>;
+            template class Mdp<storm::dd::DdType::CUDD, double>;
+            template class Mdp<storm::dd::DdType::Sylvan, double>;
             
         } // namespace symbolic
     } // namespace models

src/models/symbolic/Model.cpp

@@ -228,7 +228,9 @@ namespace storm {
             }
             
             // Explicitly instantiate the template class.
-            template class Model<storm::dd::DdType::CUDD>;
+            template class Model<storm::dd::DdType::CUDD, double>;
+            template class Model<storm::dd::DdType::Sylvan, double>;
+
         } // namespace symbolic
     } // namespace models
 } // namespace storm

src/models/symbolic/NondeterministicModel.cpp

@@ -69,6 +69,7 @@ namespace storm {
             
             // Explicitly instantiate the template class.
             template class NondeterministicModel<storm::dd::DdType::CUDD, double>;
+            template class NondeterministicModel<storm::dd::DdType::Sylvan, double>;
             
         } // namespace symbolic
     } // namespace models

src/models/symbolic/StandardRewardModel.cpp

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

src/models/symbolic/StochasticTwoPlayerGame.cpp

@@ -40,7 +40,8 @@ namespace storm {
             }
             
             // Explicitly instantiate the template class.
-            template class StochasticTwoPlayerGame<storm::dd::DdType::CUDD>;
+            template class StochasticTwoPlayerGame<storm::dd::DdType::CUDD, double>;
+            template class StochasticTwoPlayerGame<storm::dd::DdType::Sylvan, double>;
             
         } // namespace symbolic
     } // namespace models

src/storage/dd/Bdd.cpp

@@ -142,6 +142,23 @@ namespace storm {
             return Bdd<LibraryType>(this->getDdManager(), internalBdd.restrict(constraint), Dd<LibraryType>::joinMetaVariables(*this, constraint));
         }
         
+        template<DdType LibraryType>
+        Bdd<LibraryType> Bdd<LibraryType>::relationalProduct(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables) 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::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);
+                }
+            }
+            
+            return Bdd<LibraryType>(this->getDdManager(), internalBdd.relationalProduct(relation, rowVariables), 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

@@ -186,6 +186,15 @@ 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.
+             *
+             * @param relation The relation to use.
+             * @param rowMetaVariables The row meta variables used in the relation.
+             * @return The ralational product.
+             */
+            Bdd<LibraryType> relationalProduct(Bdd<LibraryType> const& relation, std::set<storm::expressions::Variable> const& rowMetaVariables) 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

@@ -7,6 +7,8 @@
 
 #include "src/storage/BitVector.h"
 
+#include <iostream>
+
 namespace storm {
     namespace dd {
         InternalBdd<DdType::CUDD>::InternalBdd(InternalDdManager<DdType::CUDD> const* ddManager, cudd::BDD cuddBdd) : ddManager(ddManager), cuddBdd(cuddBdd) {
@@ -27,6 +29,24 @@ namespace storm {
             return !(*this == other);
         }
         
+        InternalBdd<DdType::CUDD> InternalBdd<DdType::CUDD>::relationalProduct(InternalBdd<DdType::CUDD> const& relation, std::vector<InternalBdd<DdType::CUDD>> const& rowVariables) const {
+            InternalBdd<DdType::CUDD> cube = ddManager->getBddOne();
+            for (auto const& variable : rowVariables) {
+                cube &= variable;
+            }
+            
+            InternalBdd<DdType::CUDD> result = this->andExists(relation, cube);
+            
+            // Create the corresponding "from" vector for the variable swap.
+            std::vector<InternalBdd<DdType::CUDD>> columnVariables;
+            for (auto const& variable : rowVariables) {
+                columnVariables.push_back(InternalBdd<DdType::CUDD>(ddManager, ddManager->getCuddManager().bddVar(variable.getIndex() + 1)));
+            }
+            result = result.swapVariables(rowVariables, columnVariables);
+            
+            return result;
+        }
+        
         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

@@ -76,6 +76,15 @@ namespace storm {
              */
             bool operator!=(InternalBdd<DdType::CUDD> const& other) const;
             
+            /*!
+             * Computes the relational product of the current BDD and the given BDD representing a relation.
+             *
+             * @param relation The relation to use.
+             * @param rowVariables The row variables of the relation represented as individual BDDs.
+             * @return The ralational product.
+             */
+            InternalBdd<DdType::CUDD> relationalProduct(InternalBdd<DdType::CUDD> const& relation, std::vector<InternalBdd<DdType::CUDD>> const& rowVariables) 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/InternalSylvanAdd.cpp

@@ -166,11 +166,11 @@ namespace storm {
         InternalAdd<DdType::Sylvan, ValueType> InternalAdd<DdType::Sylvan, ValueType>::swapVariables(std::vector<InternalBdd<DdType::Sylvan>> const& from, std::vector<InternalBdd<DdType::Sylvan>> const& to) const {
             std::vector<uint32_t> fromIndices;
             std::vector<uint32_t> toIndices;
-            uint_fast64_t var = 0;
             for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) {
                 fromIndices.push_back(it1->getIndex());
+                fromIndices.push_back(it2->getIndex());
                 toIndices.push_back(it2->getIndex());
-                ++var;
+                toIndices.push_back(it1->getIndex());
             }
             return InternalAdd<DdType::Sylvan, ValueType>(ddManager, this->sylvanMtbdd.Permute(fromIndices, toIndices));
         }

src/storage/dd/sylvan/InternalSylvanBdd.cpp

@@ -8,6 +8,9 @@
 #include "src/utility/macros.h"
 #include "src/exceptions/NotImplementedException.h"
 
+
+#include <iostream>
+
 namespace storm {
     namespace dd {
         InternalBdd<DdType::Sylvan>::InternalBdd(InternalDdManager<DdType::Sylvan> const* ddManager, sylvan::Bdd const& sylvanBdd) : ddManager(ddManager), sylvanBdd(sylvanBdd) {
@@ -27,6 +30,10 @@ namespace storm {
             return sylvanBdd != other.sylvanBdd;
         }
         
+        InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::relationalProduct(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented.");
+        }
+        
         InternalBdd<DdType::Sylvan> InternalBdd<DdType::Sylvan>::ite(InternalBdd<DdType::Sylvan> const& thenDd, InternalBdd<DdType::Sylvan> const& elseDd) const {
             return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd.Ite(thenDd.sylvanBdd, elseDd.sylvanBdd));
         }
@@ -95,7 +102,9 @@ namespace storm {
             std::vector<uint32_t> toIndices;
             for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) {
                 fromIndices.push_back(it1->getIndex());
+                fromIndices.push_back(it2->getIndex());
                 toIndices.push_back(it2->getIndex());
+                toIndices.push_back(it1->getIndex());
             }
             return InternalBdd<DdType::Sylvan>(ddManager, this->sylvanBdd.Permute(fromIndices, toIndices));
         }

src/storage/dd/sylvan/InternalSylvanBdd.h

@@ -65,6 +65,15 @@ namespace storm {
              */
             bool operator!=(InternalBdd<DdType::Sylvan> const& other) const;
             
+            /*!
+             * Computes the relational product of the current BDD and the given BDD representing a relation.
+             *
+             * @param relation The relation to use.
+             * @param rowVariables The row variables of the relation represented as individual BDDs.
+             * @return The ralational product.
+             */
+            InternalBdd<DdType::Sylvan> relationalProduct(InternalBdd<DdType::Sylvan> const& relation, std::vector<InternalBdd<DdType::Sylvan>> const& rowVariables) 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

test/functional/builder/DdPrismModelBuilderTest.cpp

@@ -10,7 +10,36 @@
 #include "src/parser/PrismParser.h"
 #include "src/builder/DdPrismModelBuilder.h"
 
-TEST(DdPrismModelBuilderTest, Dtmc) {
+TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+    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/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);
+    EXPECT_EQ(273ul, model->getNumberOfStates());
+    EXPECT_EQ(397ul, model->getNumberOfTransitions());
+
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+    EXPECT_EQ(1728ul, model->getNumberOfStates());
+    EXPECT_EQ(2505ul, model->getNumberOfTransitions());
+}
+
+TEST(DdPrismModelBuilderTest_Cudd, Dtmc) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
     
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
@@ -21,24 +50,55 @@ TEST(DdPrismModelBuilderTest, Dtmc) {
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::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::CUDD>::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::CUDD>::translateProgram(program);
     EXPECT_EQ(273ul, model->getNumberOfStates());
     EXPECT_EQ(397ul, model->getNumberOfTransitions());
-
+    
     program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
     model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
     EXPECT_EQ(1728ul, model->getNumberOfStates());
     EXPECT_EQ(2505ul, model->getNumberOfTransitions());
 }
 
-TEST(DdPrismModelBuilderTest, Ctmc) {
+TEST(DdPrismModelBuilderTest_Sylvan, Ctmc) {
+    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+    
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
+    
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+    EXPECT_EQ(276ul, model->getNumberOfStates());
+    EXPECT_EQ(1120ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+    EXPECT_EQ(3478ul, model->getNumberOfStates());
+    EXPECT_EQ(14639ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+    EXPECT_EQ(12ul, model->getNumberOfStates());
+    EXPECT_EQ(22ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+    EXPECT_EQ(810ul, model->getNumberOfStates());
+    EXPECT_EQ(3699ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+    EXPECT_EQ(66ul, model->getNumberOfStates());
+    EXPECT_EQ(189ul, model->getNumberOfTransitions());
+}
+
+TEST(DdPrismModelBuilderTest_Cudd, Ctmc) {
     // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
     std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
 
@@ -69,7 +129,70 @@ TEST(DdPrismModelBuilderTest, Ctmc) {
     EXPECT_EQ(189ul, model->getNumberOfTransitions());
 }
 
-TEST(DdPrismModelBuilderTest, Mdp) {
+TEST(DdPrismModelBuilderTest_Sylvan, Mdp) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
+    
+    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+    std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
+    
+    EXPECT_EQ(169ul, mdp->getNumberOfStates());
+    EXPECT_EQ(436ul, mdp->getNumberOfTransitions());
+    EXPECT_EQ(254ul, mdp->getNumberOfChoices());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.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(364ul, mdp->getNumberOfStates());
+    EXPECT_EQ(654ul, mdp->getNumberOfTransitions());
+    EXPECT_EQ(573ul, mdp->getNumberOfChoices());
+    
+    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);
+    
+    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+    mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
+    
+    EXPECT_EQ(272ul, mdp->getNumberOfStates());
+    EXPECT_EQ(492ul, mdp->getNumberOfTransitions());
+    EXPECT_EQ(400ul, mdp->getNumberOfChoices());
+    
+    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);
+    
+    EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
+    mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
+    
+    EXPECT_EQ(1038ul, mdp->getNumberOfStates());
+    EXPECT_EQ(1282ul, mdp->getNumberOfTransitions());
+    EXPECT_EQ(1054ul, mdp->getNumberOfChoices());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.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(4093ul, mdp->getNumberOfStates());
+    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());
+}
+
+TEST(DdPrismModelBuilderTest_Cudd, Mdp) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
     std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);