Now DDs are either MTBDDs or BDDs. This makes it possible to use BDDs where possible, which is faster.

Former-commit-id: 07ffb5882d

src/adapters/DdExpressionAdapter.cpp

@@ -40,13 +40,13 @@ namespace storm {
                     result = leftResult || rightResult;
                     break;
                 case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff:
-                    result = leftResult.equals(rightResult);
+                    result = leftResult.iff(rightResult);
                     break;
                 case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies:
                     result = !leftResult || rightResult;
                     break;
                 case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor:
-                    result = (leftResult && !rightResult) || (!leftResult && rightResult);
+                    result = leftResult.exclusiveOr(rightResult);
                     break;
             }
             

src/builder/DdPrismModelBuilder.cpp

@@ -50,7 +50,7 @@ namespace storm {
         
         template <storm::dd::DdType Type>
         storm::dd::Dd<Type> DdPrismModelBuilder<Type>::createUpdateDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::dd::Dd<Type> const& guard, storm::prism::Update const& update) {
-            storm::dd::Dd<Type> updateDd = generationInfo.manager->getOne();
+            storm::dd::Dd<Type> updateDd = generationInfo.manager->getOne(true);
             
             STORM_LOG_TRACE("Translating update " << update);
             
@@ -77,7 +77,7 @@ namespace storm {
                 result *= guard;
                 
                 // Restrict the transitions to the range of the written variable.
-                result = result * generationInfo.manager->getRange(primedMetaVariable);
+                result = result * generationInfo.manager->getRange(primedMetaVariable, true);
                 
                 updateDd *= result;
             }
@@ -130,7 +130,7 @@ namespace storm {
             STORM_LOG_WARN_COND(!guardDd.isZero(), "The guard '" << command.getGuardExpression() << "' is unsatisfiable.");
             
             if (!guardDd.isZero()) {
-                storm::dd::Dd<Type> commandDd = generationInfo.manager->getZero();
+                storm::dd::Dd<Type> commandDd = generationInfo.manager->getZero(true);
                 for (storm::prism::Update const& update : command.getUpdates()) {
                     storm::dd::Dd<Type> updateDd = createUpdateDecisionDiagram(generationInfo, module, guardDd, update);
                     
@@ -183,8 +183,8 @@ namespace storm {
         
         template <storm::dd::DdType Type>
         typename DdPrismModelBuilder<Type>::ActionDecisionDiagram DdPrismModelBuilder<Type>::combineCommandsToActionDTMC(GenerationInformation& generationInfo, std::vector<ActionDecisionDiagram> const& commandDds) {
-            storm::dd::Dd<Type> allGuards = generationInfo.manager->getZero();
+            storm::dd::Dd<Type> allGuards = generationInfo.manager->getZero(true);
-            storm::dd::Dd<Type> allCommands = generationInfo.manager->getZero();
+            storm::dd::Dd<Type> allCommands = generationInfo.manager->getZero(true);
             storm::dd::Dd<Type> temporary;
             
             for (auto const& commandDd : commandDds) {
@@ -201,7 +201,7 @@ namespace storm {
         
         template <storm::dd::DdType Type>
         storm::dd::Dd<Type> DdPrismModelBuilder<Type>::encodeChoice(GenerationInformation& generationInfo, uint_fast64_t nondeterminismVariableOffset, uint_fast64_t numberOfBinaryVariables, int_fast64_t value) {
-            storm::dd::Dd<Type> result = generationInfo.manager->getZero();
+            storm::dd::Dd<Type> result = generationInfo.manager->getZero(true);
             
             STORM_LOG_TRACE("Encoding " << value << " with " << numberOfBinaryVariables << " binary variable(s) starting from offset " << nondeterminismVariableOffset << ".");
             
@@ -220,11 +220,11 @@ namespace storm {
         
         template <storm::dd::DdType Type>
         typename DdPrismModelBuilder<Type>::ActionDecisionDiagram DdPrismModelBuilder<Type>::combineCommandsToActionMDP(GenerationInformation& generationInfo, std::vector<ActionDecisionDiagram> const& commandDds, uint_fast64_t nondeterminismVariableOffset) {
-            storm::dd::Dd<Type> allGuards = generationInfo.manager->getZero();
+            storm::dd::Dd<Type> allGuards = generationInfo.manager->getZero(true);
-            storm::dd::Dd<Type> allCommands = generationInfo.manager->getZero();
+            storm::dd::Dd<Type> allCommands = generationInfo.manager->getZero(true);
             
             // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state.
-            storm::dd::Dd<Type> sumOfGuards = generationInfo.manager->getZero();
+            storm::dd::Dd<Type> sumOfGuards = generationInfo.manager->getZero(true);
             for (auto const& commandDd : commandDds) {
                 sumOfGuards += commandDd.guardDd;
                 allGuards = allGuards || commandDd.guardDd;
@@ -247,9 +247,9 @@ namespace storm {
                 // Calculate number of required variables to encode the nondeterminism.
                 uint_fast64_t numberOfBinaryVariables = static_cast<uint_fast64_t>(std::ceil(storm::utility::math::log2(maxChoices)));
                 
-                storm::dd::Dd<Type> equalsNumberOfChoicesDd = generationInfo.manager->getZero();
+                storm::dd::Dd<Type> equalsNumberOfChoicesDd = generationInfo.manager->getZero(true);
-                std::vector<storm::dd::Dd<Type>> choiceDds(maxChoices, generationInfo.manager->getZero());
+                std::vector<storm::dd::Dd<Type>> choiceDds(maxChoices, generationInfo.manager->getZero(true));
-                std::vector<storm::dd::Dd<Type>> remainingDds(maxChoices, generationInfo.manager->getZero());
+                std::vector<storm::dd::Dd<Type>> remainingDds(maxChoices, generationInfo.manager->getZero(true));
                 
                 for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) {
                     // Determine the set of states with exactly currentChoices choices.
@@ -262,7 +262,7 @@ namespace storm {
                     
                     // Reset the previously used intermediate storage.
                     for (uint_fast64_t j = 0; j < currentChoices; ++j) {
-                        choiceDds[j] = generationInfo.manager->getZero();
+                        choiceDds[j] = generationInfo.manager->getZero(true);
                         remainingDds[j] = equalsNumberOfChoicesDd;
                     }
                     
@@ -335,23 +335,23 @@ namespace storm {
                 // Bring both choices to the same number of variables that encode the nondeterminism.
                 uint_fast64_t numberOfUsedNondeterminismVariables = std::max(action1.numberOfUsedNondeterminismVariables, action2.numberOfUsedNondeterminismVariables);
                 if (action1.numberOfUsedNondeterminismVariables > action2.numberOfUsedNondeterminismVariables) {
-                    storm::dd::Dd<Type> nondeterminisimEncoding = generationInfo.manager->getOne();
+                    storm::dd::Dd<Type> nondeterminisimEncoding = generationInfo.manager->getOne(true);
                     
                     for (uint_fast64_t i = action2.numberOfUsedNondeterminismVariables; i < action1.numberOfUsedNondeterminismVariables; ++i) {
-                        nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0);
+                        nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0, true);
                     }
                     action2Extended *= nondeterminisimEncoding;
                 } else if (action2.numberOfUsedNondeterminismVariables > action1.numberOfUsedNondeterminismVariables) {
-                    storm::dd::Dd<Type> nondeterminisimEncoding = generationInfo.manager->getOne();
+                    storm::dd::Dd<Type> nondeterminisimEncoding = generationInfo.manager->getOne(true);
                     
                     for (uint_fast64_t i = action1.numberOfUsedNondeterminismVariables; i < action2.numberOfUsedNondeterminismVariables; ++i) {
-                        nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0);
+                        nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0, true);
                     }
                     action1Extended *= nondeterminisimEncoding;
                 }
                 
                 // Add a new variable that resolves the nondeterminism between the two choices.
-                storm::dd::Dd<Type> combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1).ite(action2Extended, action1Extended);
+                storm::dd::Dd<Type> combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1, true).ite(action2Extended, action1Extended);
                 
                 return ActionDecisionDiagram(action1.guardDd || action2.guardDd, combinedTransitions, numberOfUsedNondeterminismVariables + 1);
             } else {
@@ -381,44 +381,44 @@ namespace storm {
         storm::dd::Dd<Type> DdPrismModelBuilder<Type>::createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module) {
             // If the model is an MDP, we need to encode the nondeterminism using additional variables.
             if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
-                storm::dd::Dd<Type> result = generationInfo.manager->getZero();
+                storm::dd::Dd<Type> result = generationInfo.manager->getZero(true);
                 
                 // First, determine the highest number of nondeterminism variables that is used in any action and make
                 // all actions use the same amout of nondeterminism variables.
                 uint_fast64_t numberOfUsedNondeterminismVariables = module.numberOfUsedNondeterminismVariables;
 
                 // Add variables to independent action DD.
-                storm::dd::Dd<Type> nondeterminismEncoding = generationInfo.manager->getOne();
+                storm::dd::Dd<Type> nondeterminismEncoding = generationInfo.manager->getOne(true);
                 for (uint_fast64_t i = module.independentAction.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) {
-                    nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0);
+                    nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0, true);
                 }
                 result = module.independentAction.transitionsDd * nondeterminismEncoding;
 
                 // Add variables to synchronized action DDs.
                 std::map<uint_fast64_t, storm::dd::Dd<Type>> synchronizingActionToDdMap;
                 for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) {
-                    nondeterminismEncoding = generationInfo.manager->getOne();
+                    nondeterminismEncoding = generationInfo.manager->getOne(true);
                     for (uint_fast64_t i = synchronizingAction.second.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) {
-                        nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0);
+                        nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0, true);
                     }
                     synchronizingActionToDdMap.emplace(synchronizingAction.first, synchronizingAction.second.transitionsDd * nondeterminismEncoding);
                 }
                 
                 // Add variables for synchronization.
-                storm::dd::Dd<Type> synchronization = generationInfo.manager->getOne();
+                storm::dd::Dd<Type> synchronization = generationInfo.manager->getOne(true);
                 for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) {
-                    synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0);
+                    synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0, true);
                 }
                 result *= synchronization;
                 
                 for (auto& synchronizingAction : synchronizingActionToDdMap) {
-                    synchronization = generationInfo.manager->getOne();
+                    synchronization = generationInfo.manager->getOne(true);
                     
                     for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) {
                         if (i == synchronizingAction.first) {
-                            synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1);
+                            synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1, true);
                         } else {
-                            synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0);
+                            synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0, true);
                         }
                     }
                     
@@ -549,14 +549,24 @@ namespace storm {
             // In particular, this creates the meta variables used to encode the model.
             GenerationInformation generationInfo(preparedProgram);
 
-            auto clock = std::chrono::high_resolution_clock::now();
+            auto totalTimeStart = std::chrono::high_resolution_clock::now();
             std::pair<storm::dd::Dd<Type>, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo);
+            auto totalTimeEnd = std::chrono::high_resolution_clock::now();
+            std::cout << "building matrix took " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTimeEnd - totalTimeStart).count() << "ms" << std::endl;
+            
             storm::dd::Dd<Type> transitionMatrix = transitionMatrixModulePair.first;
             ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second;
             
             // Cut the transition matrix to the reachable fragment of the state space.
+            totalTimeStart = std::chrono::high_resolution_clock::now();
             storm::dd::Dd<Type> reachableStates = computeReachableStates(generationInfo, createInitialStatesDecisionDiagram(generationInfo), transitionMatrix);
-            transitionMatrix *= reachableStates;
+            totalTimeEnd = std::chrono::high_resolution_clock::now();
+            std::cout << "reachability took " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTimeEnd - totalTimeStart).count() << "ms" << std::endl;
+            
+            totalTimeStart = std::chrono::high_resolution_clock::now();
+            transitionMatrix *= reachableStates.toMtbdd();
+            totalTimeEnd = std::chrono::high_resolution_clock::now();
+            std::cout << "cutting trans to reachable took " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTimeEnd - totalTimeStart).count() << "ms" << std::endl;
 
             // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise.
             storm::dd::Dd<Type> statesWithTransition = transitionMatrix.notZero();
@@ -564,7 +574,7 @@ namespace storm {
                 statesWithTransition = statesWithTransition.existsAbstract(generationInfo.allNondeterminismVariables);
             }
             statesWithTransition = statesWithTransition.existsAbstract(generationInfo.columnMetaVariables);
-            storm::dd::Dd<Type> deadlockStates = reachableStates * !statesWithTransition;
+            storm::dd::Dd<Type> deadlockStates = (reachableStates && !statesWithTransition).toMtbdd();
 
             if (!deadlockStates.isZero()) {
                 // If we need to fix deadlocks, we do so now.
@@ -577,7 +587,7 @@ namespace storm {
                     } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
                         // For MDPs, however, we need to select an action associated with the self-loop, if we do not
                         // want to attach a lot of self-loops to the deadlock states.
-                        storm::dd::Dd<Type> action = generationInfo.manager->getOne();
+                        storm::dd::Dd<Type> action = generationInfo.manager->getOne(true);
                         std::for_each(generationInfo.allNondeterminismVariables.begin(), generationInfo.allNondeterminismVariables.end(), [&action,&generationInfo] (storm::expressions::Variable const& metaVariable) { action *= !generationInfo.manager->getIdentity(metaVariable); } );
                         transitionMatrix += deadlockStates * globalModule.identity * action;
                     }
@@ -592,10 +602,10 @@ namespace storm {
         
         template <storm::dd::DdType Type>
         storm::dd::Dd<Type> DdPrismModelBuilder<Type>::createInitialStatesDecisionDiagram(GenerationInformation& generationInfo) {
-            storm::dd::Dd<Type> initialStates = generationInfo.rowExpressionAdapter->translateExpression(generationInfo.program.getInitialConstruct().getInitialStatesExpression());
+            storm::dd::Dd<Type> initialStates = generationInfo.rowExpressionAdapter->translateExpression(generationInfo.program.getInitialConstruct().getInitialStatesExpression()).toBdd();
             
             for (auto const& metaVariable : generationInfo.rowMetaVariables) {
-                initialStates *= generationInfo.manager->getRange(metaVariable);
+                initialStates &= generationInfo.manager->getRange(metaVariable);
             }
             
             return initialStates;
@@ -603,7 +613,7 @@ namespace storm {
         
         template <storm::dd::DdType Type>
         storm::dd::Dd<Type> DdPrismModelBuilder<Type>::computeReachableStates(GenerationInformation& generationInfo, storm::dd::Dd<Type> const& initialStates, storm::dd::Dd<Type> const& transitions) {
-            storm::dd::Dd<Type> reachableStatesBdd = initialStates.notZero();
+            storm::dd::Dd<Type> reachableStatesBdd = initialStates.toBdd();
             
             // If the model is an MDP, we can abstract from the variables encoding the nondeterminism in the model.
             storm::dd::Dd<Type> transitionBdd = transitions.notZero();
@@ -617,18 +627,17 @@ namespace storm {
             do {
                 STORM_LOG_TRACE("Iteration " << iteration << " of computing reachable states.");
                 changed = false;
-                storm::dd::Dd<Type> tmp = reachableStatesBdd * transitionBdd;
+                storm::dd::Dd<Type> tmp = reachableStatesBdd.andExists(transitionBdd, generationInfo.rowMetaVariables);
-                tmp = tmp.existsAbstract(generationInfo.rowMetaVariables);
                 tmp.swapVariables(generationInfo.rowColumnMetaVariablePairs);
 
-                storm::dd::Dd<Type> newReachableStates = tmp * (!reachableStatesBdd);
+                storm::dd::Dd<Type> newReachableStates = tmp && (!reachableStatesBdd);
                 
                 // Check whether new states were indeed discovered.
                 if (!newReachableStates.isZero()) {
                     changed = true;
                 }
                 
-                reachableStatesBdd += newReachableStates;
+                reachableStatesBdd |= newReachableStates;
                 ++iteration;
             } while (changed);
             

src/builder/DdPrismModelBuilder.h

@@ -68,7 +68,7 @@ namespace storm {
                     // Intentionally left empty.
                 }
                 
-                ActionDecisionDiagram(storm::dd::DdManager<Type> const& manager, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(manager.getZero()), transitionsDd(manager.getZero()), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) {
+                ActionDecisionDiagram(storm::dd::DdManager<Type> const& manager, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(manager.getZero(true)), transitionsDd(manager.getZero(true)), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) {
                     // Intentionally left empty.
                 }
                 
@@ -95,7 +95,7 @@ namespace storm {
                     // Intentionally left empty.
                 }
                 
-                ModuleDecisionDiagram(storm::dd::DdManager<Type> const& manager) : independentAction(manager), synchronizingActionToDecisionDiagramMap(), identity(manager.getZero()), numberOfUsedNondeterminismVariables(0) {
+                ModuleDecisionDiagram(storm::dd::DdManager<Type> const& manager) : independentAction(manager), synchronizingActionToDecisionDiagramMap(), identity(manager.getZero(true)), numberOfUsedNondeterminismVariables(0) {
                     // Intentionally left empty.
                 }
 
@@ -209,7 +209,7 @@ namespace storm {
                         columnMetaVariables.insert(variablePair.second);
                         variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second);
                         
-                        storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first);
+                        storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first, true);
                         variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity);
                         rowColumnMetaVariablePairs.push_back(variablePair);
                     }
@@ -230,8 +230,8 @@ namespace storm {
 
                     // Create meta variables for each of the modules' variables.
                     for (storm::prism::Module const& module : program.getModules()) {
-                        storm::dd::Dd<Type> moduleIdentity = manager->getOne();
+                        storm::dd::Dd<Type> moduleIdentity = manager->getOne(true);
-                        storm::dd::Dd<Type> moduleRange = manager->getOne();
+                        storm::dd::Dd<Type> moduleRange = manager->getOne(true);
                         
                         for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) {
                             int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt();
@@ -245,11 +245,10 @@ namespace storm {
                             columnMetaVariables.insert(variablePair.second);
                             variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second);
                             
-                            storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first) * manager->getRange(variablePair.second);
+                            storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first, true) * manager->getRange(variablePair.second, true);
-                            variableIdentity.exportToDot(variablePair.first.getName() + "_ident.dot");
                             variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity);
                             moduleIdentity *= variableIdentity;
-                            moduleRange *= manager->getRange(variablePair.first);
+                            moduleRange *= manager->getRange(variablePair.first, true);
                             
                             rowColumnMetaVariablePairs.push_back(variablePair);
                         }
@@ -263,10 +262,10 @@ namespace storm {
                             columnMetaVariables.insert(variablePair.second);
                             variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second);
                             
-                            storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first) * manager->getRange(variablePair.second);
+                            storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first, true) * manager->getRange(variablePair.second, true);
                             variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity);
                             moduleIdentity *= variableIdentity;
-                            moduleRange *= manager->getRange(variablePair.first);
+                            moduleRange *= manager->getRange(variablePair.first, true);
 
                             rowColumnMetaVariablePairs.push_back(variablePair);
                         }

src/settings/modules/GeneralSettings.cpp

@@ -20,7 +20,7 @@ namespace storm {
             const std::string GeneralSettings::configOptionName = "config";
             const std::string GeneralSettings::configOptionShortName = "c";
             const std::string GeneralSettings::explicitOptionName = "explicit";
-            const std::string GeneralSettings::explicitOptionShortName = "e";
+            const std::string GeneralSettings::explicitOptionShortName = "exp";
             const std::string GeneralSettings::symbolicOptionName = "symbolic";
             const std::string GeneralSettings::symbolicOptionShortName = "s";
             const std::string GeneralSettings::propertyOptionName = "prop";
@@ -41,6 +41,8 @@ namespace storm {
             const std::string GeneralSettings::statisticsOptionShortName = "stats";
             const std::string GeneralSettings::bisimulationOptionName = "bisimulation";
             const std::string GeneralSettings::bisimulationOptionShortName = "bisim";
+            const std::string GeneralSettings::engineOptionName = "engine";
+            const std::string GeneralSettings::engineOptionShortName = "e";
             
 #ifdef STORM_HAVE_CARL
             const std::string GeneralSettings::parametricOptionName = "parametric";
@@ -76,6 +78,10 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build());
                 
+                std::vector<std::string> engines = {"sparse", "dd"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName)
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, dd}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build());
+                
                 std::vector<std::string> linearEquationSolver = {"gmm++", "native"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the solver to prefer. Available are: gmm++ and native.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(linearEquationSolver)).setDefaultValueString("gmm++").build()).build());
@@ -251,6 +257,16 @@ namespace storm {
                 return this->getOption(bisimulationOptionName).getHasOptionBeenSet();
             }
             
+            GeneralSettings::Engine GeneralSettings::getEngine() const {
+                std::string engine = this->getOption(engineOptionName).getArgumentByName("name").getValueAsString();
+                if (engine == "sparse") {
+                    return GeneralSettings::Engine::Sparse;
+                } else if (engine == "dd") {
+                    return GeneralSettings::Engine::Dd;
+                }
+                STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engine << "'.");
+            }
+            
 #ifdef STORM_HAVE_CARL
             bool GeneralSettings::isParametricSet() const {
                 return this->getOption(parametricOptionName).getHasOptionBeenSet();
@@ -265,6 +281,8 @@ namespace storm {
                 uint_fast64_t propertySources = 0 + (isPropertySet() ? 1 : 0) + (isPropertyFileSet() ? 1 : 0);
                 STORM_LOG_THROW(propertySources <= 1, storm::exceptions::InvalidSettingsException, "Please specify either a file that contains the properties or a property on the command line, but not both.");
                 
+                STORM_LOG_THROW(this->getEngine() != Engine::Dd || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "Decision-diagram engine can only be used with symbolic input models.");
+                
                 return true;
             }
             

src/settings/modules/GeneralSettings.h

@@ -13,6 +13,9 @@ namespace storm {
              */
             class GeneralSettings : public ModuleSettings {
             public:                
+                // An enumeration of all engines.
+                enum class Engine { Sparse, Dd };
+                
                 // An enumeration of all available LP solvers.
                 enum class LpSolver { Gurobi, glpk };
                 
@@ -287,6 +290,13 @@ namespace storm {
                  */
                 bool isBisimulationSet() const;
                 
+                /*!
+                 * Retrieves the selected engine.
+                 *
+                 * @return The selecte engine.
+                 */
+                Engine getEngine() const;
+                
 #ifdef STORM_HAVE_CARL
                 /*!
                  * Retrieves whether the option enabling parametric model checking is set.
@@ -335,6 +345,8 @@ namespace storm {
                 static const std::string statisticsOptionShortName;
                 static const std::string bisimulationOptionName;
                 static const std::string bisimulationOptionShortName;
+                static const std::string engineOptionName;
+                static const std::string engineOptionShortName;
                 
 #ifdef STORM_HAVE_CARL
                 static const std::string parametricOptionName;

src/storage/dd/CuddDd.cpp

@@ -7,21 +7,96 @@
 #include "src/utility/vector.h"
 #include "src/utility/macros.h"
 
+#include "src/exceptions/IllegalFunctionCallException.h"
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/exceptions/NotImplementedException.h"
 
 namespace storm {
     namespace dd {
-        Dd<DdType::CUDD>::Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddAdd, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), cuddAdd(cuddAdd), containedMetaVariables(containedMetaVariables) {
+        Dd<DdType::CUDD>::Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), cuddDd(cuddDd), containedMetaVariables(containedMetaVariables) {
             // Intentionally left empty.
         }
 
+        Dd<DdType::CUDD>::Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(ddManager), cuddDd(cuddDd), containedMetaVariables(containedMetaVariables) {
+            // Intentionally left empty.
+        }
+        
+        bool Dd<DdType::CUDD>::isBdd() const {
+            return this->cuddDd.which() == 0;
+        }
+        
+        bool Dd<DdType::CUDD>::isMtbdd() const {
+            return this->cuddDd.which() == 1;
+        }
+        
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::toBdd() const {
+            if (this->isBdd()) {
+                return *this;
+            } else {
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().BddPattern(), this->containedMetaVariables);
+            }
+        }
+        
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::toMtbdd() const {
+            if (this->isMtbdd()) {
+                return *this;
+            } else {
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Add(), this->containedMetaVariables);
+            }
+        }
+        
+        BDD Dd<DdType::CUDD>::getCuddBdd() const {
+            if (this->isBdd()) {
+                return boost::get<BDD>(this->cuddDd);
+            } else {
+                STORM_LOG_WARN_COND(false, "Implicitly converting MTBDD to BDD.");
+                return this->getCuddMtbdd().BddPattern();
+            }
+        }
+        
+        ADD Dd<DdType::CUDD>::getCuddMtbdd() const {
+            if (this->isMtbdd()) {
+                return boost::get<ADD>(this->cuddDd);
+            } else {
+                STORM_LOG_WARN_COND(false, "Implicitly converting BDD to MTBDD.");
+                return this->getCuddBdd().Add();
+            }
+        }
+        
+        ABDD const& Dd<DdType::CUDD>::getCuddDd() const {
+            if (this->isBdd()) {
+                return static_cast<ABDD const&>(boost::get<BDD>(this->cuddDd));
+            } else {
+                return static_cast<ABDD const&>(boost::get<ADD>(this->cuddDd));
+            }
+        }
+        
+        DdNode* Dd<DdType::CUDD>::getCuddDdNode() const {
+            if (this->isBdd()) {
+                return this->getCuddBdd().getNode();
+            } else {
+                return this->getCuddMtbdd().getNode();
+            }
+        }
+        
         bool Dd<DdType::CUDD>::operator==(Dd<DdType::CUDD> const& other) const {
-            return this->cuddAdd == other.getCuddAdd();
+            if (this->isBdd()) {
+                if (other.isBdd()) {
+                    return this->getCuddBdd() == other.getCuddBdd();
+                } else {
+                    return false;
+                }
+            } else {
+                if (other.isMtbdd()) {
+                    return this->getCuddMtbdd() == other.getCuddMtbdd();
+                } else {
+                    return false;
+                }
+            }
         }
         
         bool Dd<DdType::CUDD>::operator!=(Dd<DdType::CUDD> const& other) const {
-            return this->cuddAdd != other.getCuddAdd();
+            return !(*this == other);
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::ite(Dd<DdType::CUDD> const& thenDd, Dd<DdType::CUDD> const& elseDd) const {
@@ -29,7 +104,12 @@ namespace storm {
             metaVariableNames.insert(thenDd.getContainedMetaVariables().begin(), thenDd.getContainedMetaVariables().end());
             metaVariableNames.insert(elseDd.getContainedMetaVariables().begin(), elseDd.getContainedMetaVariables().end());
 
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Ite(thenDd.getCuddAdd(), elseDd.getCuddAdd()), metaVariableNames);
+            // If all involved DDs are BDDs, the result is also going to be a BDD.
+            if (this->isBdd() && thenDd.isBdd() && elseDd.isBdd()) {
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()), metaVariableNames);
+            } else {
+                return Dd<DdType::CUDD>(this->getDdManager(), this->toMtbdd().getCuddMtbdd().Ite(thenDd.toMtbdd().getCuddMtbdd(), elseDd.toMtbdd().getCuddMtbdd()), metaVariableNames);
+            }
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::operator+(Dd<DdType::CUDD> const& other) const {
@@ -39,11 +119,9 @@ namespace storm {
         }
         
         Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator+=(Dd<DdType::CUDD> const& other) {
-            this->cuddAdd += other.getCuddAdd();
+            STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing addition on BDDs.");
-            
-            // Join the variable sets of the two participating DDs.
             this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
-            
+            this->cuddDd = this->getCuddMtbdd() + other.getCuddMtbdd();
             return *this;
         }
         
@@ -54,45 +132,48 @@ namespace storm {
         }
         
         Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator*=(Dd<DdType::CUDD> const& other) {
-            this->cuddAdd *= other.getCuddAdd();
-            
-            // Join the variable sets of the two participating DDs.
             this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
-            
+            if (this->isMtbdd() && other.isMtbdd()) {
+                this->cuddDd = this->getCuddMtbdd() * other.getCuddMtbdd();
+            } else if (this->isBdd() && other.isBdd()) {
+                this->cuddDd = this->getCuddBdd() & other.getCuddBdd();
+            } else {
+                STORM_LOG_WARN_COND(false, "Performing multiplication on two DDs of different type.");
+                this->cuddDd = this->getCuddMtbdd() * other.getCuddMtbdd();
+            }
             return *this;
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::operator-(Dd<DdType::CUDD> const& other) const {
+            STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
             Dd<DdType::CUDD> result(*this);
             result -= other;
             return result;
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::operator-() const {
-            return this->getDdManager()->getZero() - *this;
+            STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
+            return this->getDdManager()->getZero(true) - *this;
         }
         
         Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator-=(Dd<DdType::CUDD> const& other) {
-            this->cuddAdd -= other.getCuddAdd();
+            STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
-            
+            this->cuddDd = this->getCuddMtbdd() - other.getCuddMtbdd();
-            // Join the variable sets of the two participating DDs.
             this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
-            
             return *this;
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::operator/(Dd<DdType::CUDD> const& other) const {
+            STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
             Dd<DdType::CUDD> result(*this);
             result /= other;
             return result;
         }
         
         Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator/=(Dd<DdType::CUDD> const& other) {
-            this->cuddAdd = this->cuddAdd.Divide(other.getCuddAdd());
+            STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
-            
+            this->cuddDd = this->getCuddMtbdd().Divide(other.getCuddMtbdd());
-            // Join the variable sets of the two participating DDs.
             this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
-            
             return *this;
         }
         
@@ -102,76 +183,154 @@ namespace storm {
             return result;
         }
         
+        Dd<DdType::CUDD>& Dd<DdType::CUDD>::complement() {
+            if (this->isBdd()) {
+                this->cuddDd = ~this->getCuddBdd();
+            } else {
+                this->cuddDd = ~this->getCuddMtbdd();
+            }
+            return *this;
+        }
+        
         Dd<DdType::CUDD> Dd<DdType::CUDD>::operator&&(Dd<DdType::CUDD> const& other) const {
-            std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+            Dd<DdType::CUDD> result(*this);
-            metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+            result &= other;
+            return result;
+        }
 
-            // Rewrite a and b to not((not a) or (not b)). 
+        Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator&=(Dd<DdType::CUDD> const& other) {
-            return Dd<DdType::CUDD>(this->getDdManager(), ~(~this->getCuddAdd()).Or(~other.getCuddAdd()), metaVariables);
+            this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+            if (this->isBdd() && other.isBdd()) {
+                this->cuddDd = this->getCuddBdd() & other.getCuddBdd();
+            } else if (this->isMtbdd() && other.isMtbdd()) {
+                // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that
+                // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise.
+                this->cuddDd = this->getCuddMtbdd() & other.getCuddMtbdd();
+            } else {
+                STORM_LOG_WARN_COND(false, "Performing logical and on two DDs of different type.");
+                this->cuddDd = this->getCuddBdd() & other.getCuddBdd();
+            }
+            return *this;
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::operator||(Dd<DdType::CUDD> const& other) const {
+            Dd<DdType::CUDD> result(*this);
+            result |= other;
+            return result;
+        }
+        
+        Dd<DdType::CUDD>& Dd<DdType::CUDD>::operator|=(Dd<DdType::CUDD> const& other) {
+            this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+            if (this->isBdd() && other.isBdd()) {
+                this->cuddDd = this->getCuddBdd() | other.getCuddBdd();
+            } else if (this->isMtbdd() && other.isMtbdd()) {
+                // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that
+                // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise.
+                this->cuddDd = this->getCuddMtbdd() | other.getCuddMtbdd();
+            } else {
+                STORM_LOG_WARN_COND(false, "Performing logical and on two DDs of different type.");
+                this->cuddDd = this->getCuddBdd() & other.getCuddBdd();
+            }
+            return *this;
+            
+            STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operation on MTBDD(s).");
+            this->cuddDd = this->getCuddBdd() | other.getCuddBdd();
+            this->getContainedMetaVariables().insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+            return *this;
+        }
+        
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::iff(Dd<DdType::CUDD> const& other) const {
             std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
             metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Or(other.getCuddAdd()), metaVariables);
+            if (this->isBdd() && other.isBdd()) {
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables);
+            } else if (this->isMtbdd() && other.isMtbdd()) {
+                // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that
+                // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise.
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Xnor(other.getCuddMtbdd()), metaVariables);
+            } else {
+                STORM_LOG_WARN_COND(false, "Performing logical iff on two DDs of different type.");
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables);
+            }
+            return *this;
         }
 
-        Dd<DdType::CUDD>& Dd<DdType::CUDD>::complement() {
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::exclusiveOr(Dd<DdType::CUDD> const& other) const {
-            this->cuddAdd = ~this->cuddAdd;
+            std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
+            metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
+            if (this->isBdd() && other.isBdd()) {
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables);
+            } else if (this->isMtbdd() && other.isMtbdd()) {
+                // We also tolerate (without a warning) if the two arguments are MTBDDs. The caller has to make sure that
+                // the two given DDs are 0-1-MTBDDs, because the operation may produce wrong results otherwise.
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Xnor(other.getCuddMtbdd()), metaVariables);
+            } else {
+                STORM_LOG_WARN_COND(false, "Performing logical iff on two DDs of different type.");
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables);
+            }
             return *this;
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::equals(Dd<DdType::CUDD> const& other) const {
+            STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
             std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
             metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Equals(other.getCuddAdd()), metaVariables);
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Equals(other.getCuddMtbdd()), metaVariables);
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::notEquals(Dd<DdType::CUDD> const& other) const {
+            STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
             std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
             metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().NotEquals(other.getCuddAdd()), metaVariables);
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().NotEquals(other.getCuddMtbdd()), metaVariables);
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::less(Dd<DdType::CUDD> const& other) const {
+            STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
             std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
             metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().LessThan(other.getCuddAdd()), metaVariables);
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().LessThan(other.getCuddMtbdd()), metaVariables);
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::lessOrEqual(Dd<DdType::CUDD> const& other) const {
+            STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
             std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
             metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().LessThanOrEqual(other.getCuddAdd()), metaVariables);
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().LessThanOrEqual(other.getCuddMtbdd()), metaVariables);
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::greater(Dd<DdType::CUDD> const& other) const {
+            STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
             std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
             metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().GreaterThan(other.getCuddAdd()), metaVariables);
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().GreaterThan(other.getCuddMtbdd()), metaVariables);
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::greaterOrEqual(Dd<DdType::CUDD> const& other) const {
+            STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
             std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
             metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()), metaVariables);
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().GreaterThanOrEqual(other.getCuddMtbdd()), metaVariables);
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::minimum(Dd<DdType::CUDD> const& other) const {
+            STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
             std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
             metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Minimum(other.getCuddAdd()), metaVariables);
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Minimum(other.getCuddMtbdd()), metaVariables);
         }
 
         Dd<DdType::CUDD> Dd<DdType::CUDD>::maximum(Dd<DdType::CUDD> const& other) const {
+            STORM_LOG_WARN_COND(this->isMtbdd() && other.isMtbdd(), "Performing arithmetical operation on BDD(s).");
             std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
             metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end());
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Maximum(other.getCuddAdd()), metaVariables);
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Maximum(other.getCuddMtbdd()), metaVariables);
         }
 
         Dd<DdType::CUDD> Dd<DdType::CUDD>::existsAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
-            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
+            STORM_LOG_WARN_COND(this->isBdd(), "Performing logical operation on MTBDD(s).");
             
+            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne(false));
             std::set<storm::expressions::Variable> newMetaVariables = this->getContainedMetaVariables();
             for (auto const& metaVariable : metaVariables) {
                 // First check whether the DD contains the meta variable and erase it, if this is the case.
@@ -179,15 +338,16 @@ namespace storm {
                 newMetaVariables.erase(metaVariable);
                 
                 DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
-                cubeDd *= ddMetaVariable.getCube();
+                cubeDd &= ddMetaVariable.getCube();
             }
             
-            return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.OrAbstract(cubeDd.getCuddAdd()), newMetaVariables);
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().ExistAbstract(cubeDd.getCuddBdd()), newMetaVariables);
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::universalAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
-            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
+            STORM_LOG_WARN_COND(this->isBdd(), "Performing logical operation on MTBDD(s).");
 
+            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
             std::set<storm::expressions::Variable> newMetaVariables = this->getContainedMetaVariables();
             for (auto const& metaVariable : metaVariables) {
                 // First check whether the DD contains the meta variable and erase it, if this is the case.
@@ -195,15 +355,16 @@ namespace storm {
                 newMetaVariables.erase(metaVariable);
                 
                 DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
-                cubeDd *= ddMetaVariable.getCube();
+                cubeDd &= ddMetaVariable.getCube();
             }
             
-            return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.UnivAbstract(cubeDd.getCuddAdd()), newMetaVariables);
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().UnivAbstract(cubeDd.getCuddBdd()), newMetaVariables);
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::sumAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
-            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
+            STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
 
+            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne(true));
             std::set<storm::expressions::Variable> newMetaVariables = this->getContainedMetaVariables();
             for (auto const& metaVariable : metaVariables) {
                 // First check whether the DD contains the meta variable and erase it, if this is the case.
@@ -211,15 +372,16 @@ namespace storm {
                 newMetaVariables.erase(metaVariable);
                 
                 DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
-                cubeDd *= ddMetaVariable.getCube();
+                cubeDd *= ddMetaVariable.getCubeAsMtbdd();
             }
             
-            return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.ExistAbstract(cubeDd.getCuddAdd()), newMetaVariables);
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().ExistAbstract(cubeDd.getCuddMtbdd()), newMetaVariables);
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::minAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
-            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
+            STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
 
+            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne(true));
             std::set<storm::expressions::Variable> newMetaVariables = this->getContainedMetaVariables();
             for (auto const& metaVariable : metaVariables) {
                 // First check whether the DD contains the meta variable and erase it, if this is the case.
@@ -227,15 +389,16 @@ namespace storm {
                 newMetaVariables.erase(metaVariable);
                 
                 DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
-                cubeDd *= ddMetaVariable.getCube();
+                cubeDd *= ddMetaVariable.getCubeAsMtbdd();
             }
             
-            return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.MinAbstract(cubeDd.getCuddAdd()), newMetaVariables);
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().MinAbstract(cubeDd.getCuddMtbdd()), newMetaVariables);
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::maxAbstract(std::set<storm::expressions::Variable> const& metaVariables) const {
-            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
+            STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
 
+            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne(true));
             std::set<storm::expressions::Variable> newMetaVariables = this->getContainedMetaVariables();
             for (auto const& metaVariable : metaVariables) {
                 // First check whether the DD contains the meta variable and erase it, if this is the case.
@@ -243,63 +406,102 @@ namespace storm {
                 newMetaVariables.erase(metaVariable);
                 
                 DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
-                cubeDd *= ddMetaVariable.getCube();
+                cubeDd *= ddMetaVariable.getCubeAsMtbdd();
             }
             
-            return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.MaxAbstract(cubeDd.getCuddAdd()), newMetaVariables);
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().MaxAbstract(cubeDd.getCuddMtbdd()), newMetaVariables);
         }
         
         bool Dd<DdType::CUDD>::equalModuloPrecision(Dd<DdType::CUDD> const& other, double precision, bool relative) const {
+            STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
+
             if (relative) {
-                return this->getCuddAdd().EqualSupNormRel(other.getCuddAdd(), precision);
+                return this->getCuddMtbdd().EqualSupNormRel(other.getCuddMtbdd(), precision);
             } else {
-                return this->getCuddAdd().EqualSupNorm(other.getCuddAdd(), precision);
+                return this->getCuddMtbdd().EqualSupNorm(other.getCuddMtbdd(), precision);
             }
         }
         
         void Dd<DdType::CUDD>::swapVariables(std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& metaVariablePairs) {
-            std::vector<ADD> from;
+            if (this->isBdd()) {
-            std::vector<ADD> to;
+                std::vector<BDD> from;
-            for (auto const& metaVariablePair : metaVariablePairs) {
+                std::vector<BDD> to;
-                DdMetaVariable<DdType::CUDD> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first);
+                for (auto const& metaVariablePair : metaVariablePairs) {
-                DdMetaVariable<DdType::CUDD> const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second);
+                    DdMetaVariable<DdType::CUDD> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first);
-
+                    DdMetaVariable<DdType::CUDD> const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second);
-                // Check if it's legal so swap the meta variables.
+                    // Check if it's legal so swap the meta variables.
-                if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) {
+                    if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) {
-                    throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size.";
+                        throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size.";
-                }
+                    }
                     
-                // Keep track of the contained meta variables in the DD.
+                    // Keep track of the contained meta variables in the DD.
-                bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first);
+                    bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first);
-                bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second);
+                    bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second);
-                if (containsVariable1 && !containsVariable2) {
+                    if (containsVariable1 && !containsVariable2) {
-                    this->removeContainedMetaVariable(metaVariablePair.first);
+                        this->removeContainedMetaVariable(metaVariablePair.first);
-                    this->addContainedMetaVariable(metaVariablePair.second);
+                        this->addContainedMetaVariable(metaVariablePair.second);
-                } else if (!containsVariable1 && containsVariable2) {
+                    } else if (!containsVariable1 && containsVariable2) {
-                    this->removeContainedMetaVariable(metaVariablePair.second);
+                        this->removeContainedMetaVariable(metaVariablePair.second);
-                    this->addContainedMetaVariable(metaVariablePair.first);
+                        this->addContainedMetaVariable(metaVariablePair.first);
-                }
+                    }
                     
-                // Add the variables to swap to the corresponding vectors.
+                    // Add the variables to swap to the corresponding vectors.
-                for (auto const& ddVariable : variable1.getDdVariables()) {
+                    for (auto const& ddVariable : variable1.getDdVariables()) {
-                    from.push_back(ddVariable.getCuddAdd());
+                        from.push_back(ddVariable.getCuddBdd());
+                    }
+                    for (auto const& ddVariable : variable2.getDdVariables()) {
+                        to.push_back(ddVariable.getCuddBdd());
+                    }
                 }
-                for (auto const& ddVariable : variable2.getDdVariables()) {
+                // Finally, call CUDD to swap the variables.
-                    to.push_back(ddVariable.getCuddAdd());
+                this->cuddDd = this->getCuddBdd().SwapVariables(from, to);
+            } else {
+                std::vector<ADD> from;
+                std::vector<ADD> to;
+                for (auto const& metaVariablePair : metaVariablePairs) {
+                    DdMetaVariable<DdType::CUDD> const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first);
+                    DdMetaVariable<DdType::CUDD> const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second);
+                    
+                    // Check if it's legal so swap the meta variables.
+                    if (variable1.getNumberOfDdVariables() != variable2.getNumberOfDdVariables()) {
+                        throw storm::exceptions::InvalidArgumentException() << "Unable to swap meta variables with different size.";
+                    }
+                    
+                    // Keep track of the contained meta variables in the DD.
+                    bool containsVariable1 = this->containsMetaVariable(metaVariablePair.first);
+                    bool containsVariable2 = this->containsMetaVariable(metaVariablePair.second);
+                    if (containsVariable1 && !containsVariable2) {
+                        this->removeContainedMetaVariable(metaVariablePair.first);
+                        this->addContainedMetaVariable(metaVariablePair.second);
+                    } else if (!containsVariable1 && containsVariable2) {
+                        this->removeContainedMetaVariable(metaVariablePair.second);
+                        this->addContainedMetaVariable(metaVariablePair.first);
+                    }
+                    
+                    // Add the variables to swap to the corresponding vectors.
+                    for (auto const& ddVariable : variable1.getDdVariables()) {
+                        from.push_back(ddVariable.getCuddMtbdd());
+                    }
+                    for (auto const& ddVariable : variable2.getDdVariables()) {
+                        to.push_back(ddVariable.getCuddMtbdd());
+                    }
                 }
-            }
                 
-            // Finally, call CUDD to swap the variables.
+                // Finally, call CUDD to swap the variables.
-            this->cuddAdd = this->cuddAdd.SwapVariables(from, to);
+                this->cuddDd = this->getCuddMtbdd().SwapVariables(from, to);
+            }
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::multiplyMatrix(Dd<DdType::CUDD> const& otherMatrix, std::set<storm::expressions::Variable> const& summationMetaVariables) const {
-            std::vector<ADD> summationDdVariables;
+            STORM_LOG_WARN_COND(this->isMtbdd() && otherMatrix.isMtbdd(), "Performing arithmetical operation on BDD(s).");
 
             // Create the CUDD summation variables.
+            std::vector<ADD> summationDdVariables;
             for (auto const& metaVariable : summationMetaVariables) {
                 for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariable).getDdVariables()) {
-                    summationDdVariables.push_back(ddVariable.getCuddAdd());
+                    summationDdVariables.push_back(ddVariable.getCuddMtbdd());
                 }
             }
             
@@ -308,37 +510,68 @@ namespace storm {
             std::set<storm::expressions::Variable> containedMetaVariables;
             std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin()));
             
-            return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariables);
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().MatrixMultiply(otherMatrix.getCuddMtbdd(), summationDdVariables), containedMetaVariables);
+        }
+        
+        Dd<DdType::CUDD> Dd<DdType::CUDD>::andExists(Dd<DdType::CUDD> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const {
+            STORM_LOG_WARN_COND(this->isBdd() && other.isBdd(), "Performing logical operation on MTBDD(s).");
+            
+            Dd<DdType::CUDD> cubeDd(this->getDdManager()->getOne());
+            for (auto const& metaVariable : existentialVariables) {
+                DdMetaVariable<DdType::CUDD> const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable);
+                cubeDd &= ddMetaVariable.getCube();
+            }
+            
+            std::set<storm::expressions::Variable> unionOfMetaVariables;
+            std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin()));
+            std::set<storm::expressions::Variable> containedMetaVariables;
+            std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), existentialVariables.begin(), existentialVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin()));
+            
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cubeDd.getCuddBdd()), containedMetaVariables);
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::greater(double value) const {
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().BddStrictThreshold(value).Add(), this->getContainedMetaVariables());
+            STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().BddStrictThreshold(value), this->getContainedMetaVariables());
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::greaterOrEqual(double value) const {
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().BddThreshold(value).Add(), this->getContainedMetaVariables());
+            STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
+            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().BddThreshold(value), this->getContainedMetaVariables());
         }
 
         Dd<DdType::CUDD> Dd<DdType::CUDD>::notZero() const {
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().BddPattern().Add(), this->getContainedMetaVariables());
+            return this->toBdd();
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::constrain(Dd<DdType::CUDD> const& constraint) const {
             std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
             metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end());
             
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Constrain(constraint.getCuddAdd()), metaVariables);
+            if (this->isBdd() && constraint.isBdd()) {
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables);
+            } else {
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Constrain(constraint.getCuddMtbdd()), metaVariables);
+            }
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::restrict(Dd<DdType::CUDD> const& constraint) const {
             std::set<storm::expressions::Variable> metaVariables(this->getContainedMetaVariables());
             metaVariables.insert(constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end());
             
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Restrict(constraint.getCuddAdd()), metaVariables);
+            if (this->isBdd() && constraint.isBdd()) {
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables);
+            } else {
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Restrict(constraint.getCuddMtbdd()), metaVariables);
+            }
         }
         
         Dd<DdType::CUDD> Dd<DdType::CUDD>::getSupport() const {
-            return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddAdd().Support().Add(), this->getContainedMetaVariables());
+            if (this->isBdd()) {
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables());
+            } else {
+                return Dd<DdType::CUDD>(this->getDdManager(), this->getCuddMtbdd().Support(), this->getContainedMetaVariables());
+            }
         }
 
         uint_fast64_t Dd<DdType::CUDD>::getNonZeroCount() const {
@@ -346,24 +579,40 @@ namespace storm {
             for (auto const& metaVariable : this->getContainedMetaVariables()) {
                 numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables();
             }
-            return static_cast<uint_fast64_t>(this->cuddAdd.CountMinterm(static_cast<int>(numberOfDdVariables)));
+            if (this->isBdd()) {
+                return static_cast<uint_fast64_t>(this->getCuddBdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
+            } else {
+                return static_cast<uint_fast64_t>(this->getCuddMtbdd().CountMinterm(static_cast<int>(numberOfDdVariables)));
+            }
         }
         
         uint_fast64_t Dd<DdType::CUDD>::getLeafCount() const {
-            return static_cast<uint_fast64_t>(this->cuddAdd.CountLeaves());
+            if (this->isBdd()) {
+                return static_cast<uint_fast64_t>(this->getCuddBdd().CountLeaves());
+            } else {
+                return static_cast<uint_fast64_t>(this->getCuddMtbdd().CountLeaves());
+            }
         }
 
         uint_fast64_t Dd<DdType::CUDD>::getNodeCount() const {
-            return static_cast<uint_fast64_t>(this->cuddAdd.nodeCount());
+            if (this->isBdd()) {
+                return static_cast<uint_fast64_t>(this->getCuddBdd().nodeCount());
+            } else {
+                return static_cast<uint_fast64_t>(this->getCuddMtbdd().nodeCount());
+            }
         }
         
         double Dd<DdType::CUDD>::getMin() const {
-            ADD constantMinAdd = this->cuddAdd.FindMin();
+            STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
+
+            ADD constantMinAdd = this->getCuddMtbdd().FindMin();
             return static_cast<double>(Cudd_V(constantMinAdd.getNode()));
         }
         
         double Dd<DdType::CUDD>::getMax() const {
-            ADD constantMaxAdd = this->cuddAdd.FindMax();
+            STORM_LOG_WARN_COND(this->isMtbdd(), "Performing arithmetical operation on BDD(s).");
+
+            ADD constantMaxAdd = this->getCuddMtbdd().FindMax();
             return static_cast<double>(Cudd_V(constantMaxAdd.getNode()));
         }
         
@@ -381,65 +630,102 @@ namespace storm {
         }
         
         void Dd<DdType::CUDD>::setValue(std::map<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap, double targetValue) {
-            Dd<DdType::CUDD> valueEncoding(this->getDdManager()->getOne());
+            if (this->isBdd()) {
-            for (auto const& nameValuePair : metaVariableToValueMap) {
+                STORM_LOG_THROW(targetValue == storm::utility::zero<double>() || targetValue == storm::utility::one<double>(), storm::exceptions::InvalidArgumentException, "Cannot set encoding to non-0, non-1 value " << targetValue << " in BDD.");
-                valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second);
+                Dd<DdType::CUDD> valueEncoding(this->getDdManager()->getOne());
-                // Also record that the DD now contains the meta variable.
+                for (auto const& nameValuePair : metaVariableToValueMap) {
-                this->addContainedMetaVariable(nameValuePair.first);
+                    valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second);
-            }
+                    // Also record that the DD now contains the meta variable.
+                    this->addContainedMetaVariable(nameValuePair.first);
+                }
+                if (targetValue == storm::utility::one<double>()) {
+                    this->cuddDd = valueEncoding.getCuddBdd().Ite(this->getDdManager()->getOne().getCuddBdd(), this->getCuddBdd());
+                } else {
+                    this->cuddDd = valueEncoding.getCuddBdd().Ite(this->getDdManager()->getZero().getCuddBdd(), this->getCuddBdd());
+                }
+            } else {
+                Dd<DdType::CUDD> valueEncoding(this->getDdManager()->getOne());
+                for (auto const& nameValuePair : metaVariableToValueMap) {
+                    valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second);
+                    // Also record that the DD now contains the meta variable.
+                    this->addContainedMetaVariable(nameValuePair.first);
+                }
                 
-            this->cuddAdd = valueEncoding.getCuddAdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddAdd(), this->cuddAdd);
+                this->cuddDd = valueEncoding.toMtbdd().getCuddMtbdd().Ite(this->getDdManager()->getConstant(targetValue).getCuddMtbdd(), this->getCuddMtbdd());
+            }
         }
         
         double Dd<DdType::CUDD>::getValue(std::map<storm::expressions::Variable, int_fast64_t> const& metaVariableToValueMap) const {
             std::set<storm::expressions::Variable> remainingMetaVariables(this->getContainedMetaVariables());
             Dd<DdType::CUDD> valueEncoding(this->getDdManager()->getOne());
             for (auto const& nameValuePair : metaVariableToValueMap) {
-                valueEncoding *= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second);
+                valueEncoding &= this->getDdManager()->getEncoding(nameValuePair.first, nameValuePair.second);
                 if (this->containsMetaVariable(nameValuePair.first)) {
                     remainingMetaVariables.erase(nameValuePair.first);
                 }
             }
             
-            if (!remainingMetaVariables.empty()) {
+            STORM_LOG_THROW(remainingMetaVariables.empty(), storm::exceptions::InvalidArgumentException, "Cannot evaluate function for which not all inputs were given.");
-                throw storm::exceptions::InvalidArgumentException() << "Cannot evaluate function for which not all inputs were given.";
-            }
             
-            Dd<DdType::CUDD> value = *this * valueEncoding;
+            if (this->isBdd()) {
-            value = value.sumAbstract(this->getContainedMetaVariables());
+                Dd<DdType::CUDD> value = *this && valueEncoding;
-            return static_cast<double>(Cudd_V(value.getCuddAdd().getNode()));
+                return value.isZero() ? 0 : 1;
+            } else {
+                Dd<DdType::CUDD> value = *this * valueEncoding;
+                value = value.sumAbstract(this->getContainedMetaVariables());
+                return static_cast<double>(Cudd_V(value.getCuddMtbdd().getNode()));
+            }
         }
         
         bool Dd<DdType::CUDD>::isOne() const {
-            return *this == this->getDdManager()->getOne();
+            if (this->isBdd()) {
+                return this->getCuddBdd().IsOne();
+            } else {
+                return this->getCuddMtbdd().IsOne();
+            }
         }
         
         bool Dd<DdType::CUDD>::isZero() const {
-            return *this == this->getDdManager()->getZero();
+            if (this->isBdd()) {
+                return this->getCuddBdd().IsZero();
+            } else {
+                return this->getCuddMtbdd().IsZero();
+            }
         }
         
         bool Dd<DdType::CUDD>::isConstant() const {
-            return Cudd_IsConstant(this->cuddAdd.getNode());
+            if (this->isBdd()) {
+                return Cudd_IsConstant(this->getCuddBdd().getNode());
+            } else {
+                return Cudd_IsConstant(this->getCuddMtbdd().getNode());
+            }
         }
         
         uint_fast64_t Dd<DdType::CUDD>::getIndex() const {
-            return static_cast<uint_fast64_t>(this->getCuddAdd().NodeReadIndex());
+            if (this->isBdd()) {
+                return static_cast<uint_fast64_t>(this->getCuddBdd().NodeReadIndex());
+            } else {
+                return static_cast<uint_fast64_t>(this->getCuddMtbdd().NodeReadIndex());
+            }
         }
         
         template<typename ValueType>
         std::vector<ValueType> Dd<DdType::CUDD>::toVector() const {
+            STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create vector from BDD.");
             return this->toVector<ValueType>(Odd<DdType::CUDD>(*this));
         }
         
         template<typename ValueType>
         std::vector<ValueType> Dd<DdType::CUDD>::toVector(Odd<DdType::CUDD> const& rowOdd) const {
+            STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create vector from BDD.");
             std::vector<ValueType> result(rowOdd.getTotalOffset());
             std::vector<uint_fast64_t> ddVariableIndices = this->getSortedVariableIndices();
-            addToVectorRec(this->getCuddAdd().getNode(), 0, ddVariableIndices.size(), 0, rowOdd, ddVariableIndices, result);
+            addToVectorRec(this->getCuddDdNode(), 0, ddVariableIndices.size(), 0, rowOdd, ddVariableIndices, result);
             return result;
         }
         
         storm::storage::SparseMatrix<double> Dd<DdType::CUDD>::toMatrix() const {
+            STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD.");
             std::set<storm::expressions::Variable> rowVariables;
             std::set<storm::expressions::Variable> columnVariables;
             
@@ -455,6 +741,7 @@ namespace storm {
         }
         
         storm::storage::SparseMatrix<double> Dd<DdType::CUDD>::toMatrix(storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const {
+            STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD.");
             std::set<storm::expressions::Variable> rowMetaVariables;
             std::set<storm::expressions::Variable> columnMetaVariables;
 
@@ -470,6 +757,7 @@ namespace storm {
         }
         
         storm::storage::SparseMatrix<double> Dd<DdType::CUDD>::toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const {
+            STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD.");
             std::vector<uint_fast64_t> ddRowVariableIndices;
             std::vector<uint_fast64_t> ddColumnVariableIndices;
             
@@ -500,7 +788,7 @@ namespace storm {
             
             // Use the toMatrixRec function to compute the number of elements in each row. Using the flag, we prevent
             // it from actually generating the entries in the entry vector.
-            toMatrixRec(this->getCuddAdd().getNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false);
+            toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false);
             
             // TODO: counting might be faster by just summing over the primed variables and then using the ODD to convert
             // the resulting (DD) vector to an explicit vector.
@@ -516,7 +804,7 @@ namespace storm {
             rowIndications[0] = 0;
             
             // Now actually fill the entry vector.
-            toMatrixRec(this->getCuddAdd().getNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true);
+            toMatrixRec(this->getCuddDdNode(), rowIndications, columnsAndValues, trivialRowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true);
             
             // Since the last call to toMatrixRec modified the rowIndications, we need to restore the correct values.
             for (uint_fast64_t i = rowIndications.size() - 1; i > 0; --i) {
@@ -529,6 +817,7 @@ namespace storm {
         }
         
         storm::storage::SparseMatrix<double> Dd<DdType::CUDD>::toMatrix(std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& groupMetaVariables, storm::dd::Odd<DdType::CUDD> const& rowOdd, storm::dd::Odd<DdType::CUDD> const& columnOdd) const {
+            STORM_LOG_THROW(this->isMtbdd(), storm::exceptions::IllegalFunctionCallException, "Cannot create matrix from BDD.");
             std::vector<uint_fast64_t> ddRowVariableIndices;
             std::vector<uint_fast64_t> ddColumnVariableIndices;
             std::vector<uint_fast64_t> ddGroupVariableIndices;
@@ -573,7 +862,7 @@ namespace storm {
             // Next, we split the matrix into one for each group. This only works if the group variables are at the very
             // top.
             std::vector<Dd<DdType::CUDD>> groups;
-            splitGroupsRec(this->getCuddAdd().getNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables);
+            splitGroupsRec(this->getCuddDdNode(), groups, ddGroupVariableIndices, 0, ddGroupVariableIndices.size(), rowAndColumnMetaVariables);
             
             // Create the actual storage for the non-zero entries.
             std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>> columnsAndValues(this->getNonZeroCount());
@@ -584,10 +873,10 @@ namespace storm {
             for (uint_fast64_t i = 0; i < groups.size(); ++i) {
                 auto const& dd = groups[i];
                 
-                toMatrixRec(dd.getCuddAdd().getNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false);
+                toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, false);
                 
                 statesWithGroupEnabled[i] = dd.notZero().existsAbstract(columnMetaVariables);
-                addToVectorRec(statesWithGroupEnabled[i].getCuddAdd().getNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices);
+                addToVectorRec(statesWithGroupEnabled[i].getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices);
             }
             
             // Since we modified the rowGroupIndices, we need to restore the correct values.
@@ -610,9 +899,9 @@ namespace storm {
             for (uint_fast64_t i = 0; i < groups.size(); ++i) {
                 auto const& dd = groups[i];
 
-                toMatrixRec(dd.getCuddAdd().getNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true);
+                toMatrixRec(dd.getCuddDdNode(), rowIndications, columnsAndValues, rowGroupIndices, rowOdd, columnOdd, 0, 0, ddRowVariableIndices.size() + ddColumnVariableIndices.size(), 0, 0, ddRowVariableIndices, ddColumnVariableIndices, true);
                 
-                addToVectorRec(statesWithGroupEnabled[i].getCuddAdd().getNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices);
+                addToVectorRec(statesWithGroupEnabled[i].getCuddDdNode(), 0, ddRowVariableIndices.size(), 0, rowOdd, ddRowVariableIndices, rowGroupIndices);
             }
             
             // Since we modified the rowGroupIndices, we need to restore the correct values.
@@ -632,7 +921,7 @@ namespace storm {
         
         void Dd<DdType::CUDD>::toMatrixRec(DdNode const* dd, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>>& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool generateValues) const {
             // For the empty DD, we do not need to add any entries.
-            if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) {
+            if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) {
                 return;
             }
 
@@ -684,7 +973,7 @@ namespace storm {
         
         void Dd<DdType::CUDD>::splitGroupsRec(DdNode* dd, std::vector<Dd<DdType::CUDD>>& groups, std::vector<uint_fast64_t> const& ddGroupVariableIndices, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::set<storm::expressions::Variable> const& remainingMetaVariables) const {
             // For the empty DD, we do not need to create a group.
-            if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) {
+            if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) {
                 return;
             }
             
@@ -702,7 +991,7 @@ namespace storm {
         template<typename ValueType>
         void Dd<DdType::CUDD>::addToVectorRec(DdNode const* dd, uint_fast64_t currentLevel, uint_fast64_t maxLevel, uint_fast64_t currentOffset, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector) const {
             // For the empty DD, we do not need to add any entries.
-            if (dd == this->getDdManager()->getZero().getCuddAdd().getNode()) {
+            if (dd == Cudd_ReadZero(this->getDdManager()->getCuddManager().getManager())) {
                 return;
             }
             
@@ -759,9 +1048,14 @@ namespace storm {
         }
         
         void Dd<DdType::CUDD>::exportToDot(std::string const& filename) const {
-			std::vector<ADD> cuddAddVector = { this->cuddAdd };
 			if (filename.empty()) {
-				this->getDdManager()->getCuddManager().DumpDot(cuddAddVector);
+                if (this->isBdd()) {
+                    std::vector<BDD> cuddBddVector = { this->getCuddBdd() };
+                    this->getDdManager()->getCuddManager().DumpDot(cuddBddVector);
+                } else {
+                    std::vector<ADD> cuddAddVector = { this->getCuddMtbdd() };
+                    this->getDdManager()->getCuddManager().DumpDot(cuddAddVector);
+                }
             } else {
                 // Build the name input of the DD.
                 std::vector<char*> ddNames;
@@ -779,7 +1073,13 @@ namespace storm {
                 
                 // Open the file, dump the DD and close it again.
                 FILE* filePointer = fopen(filename.c_str() , "w");
-				this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer);
+                if (this->isBdd()) {
+                    std::vector<BDD> cuddBddVector = { this->getCuddBdd() };
+                    this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer);
+                } else {
+                    std::vector<ADD> cuddAddVector = { this->getCuddMtbdd() };
+                    this->getDdManager()->getCuddManager().DumpDot(cuddAddVector, &ddVariableNames[0], &ddNames[0], filePointer);
+                }
                 fclose(filePointer);
                 
                 // Finally, delete the names.
@@ -792,14 +1092,6 @@ namespace storm {
             }
         }
         
-        ADD Dd<DdType::CUDD>::getCuddAdd() {
-            return this->cuddAdd;
-        }
-        
-        ADD const& Dd<DdType::CUDD>::getCuddAdd() const {
-            return this->cuddAdd;
-        }
-        
         void Dd<DdType::CUDD>::addContainedMetaVariable(storm::expressions::Variable const& metaVariable) {
             this->getContainedMetaVariables().insert(metaVariable);
         }
@@ -815,7 +1107,7 @@ namespace storm {
         DdForwardIterator<DdType::CUDD> Dd<DdType::CUDD>::begin(bool enumerateDontCareMetaVariables) const {
             int* cube;
             double value;
-            DdGen* generator = this->getCuddAdd().FirstCube(&cube, &value);
+            DdGen* generator = this->getCuddDd().FirstCube(&cube, &value);
             return DdForwardIterator<DdType::CUDD>(this->getDdManager(), generator, cube, value, (Cudd_IsGenEmpty(generator) != 0), &this->getContainedMetaVariables(), enumerateDontCareMetaVariables);
         }
         
@@ -824,14 +1116,13 @@ namespace storm {
         }
         
         storm::expressions::Expression Dd<DdType::CUDD>::toExpression() const {
-            return toExpressionRecur(this->getCuddAdd().getNode(), this->getDdManager()->getDdVariables());
+            return toExpressionRecur(this->getCuddDdNode(), this->getDdManager()->getDdVariables());
         }
         
         storm::expressions::Expression Dd<DdType::CUDD>::getMintermExpression() const {
             // Note that we first transform the ADD into a BDD to convert all non-zero terminals to ones and therefore
             // make the DD more compact.
-            Dd<DdType::CUDD> tmp(this->getDdManager(), this->getCuddAdd().BddPattern().Add(), this->getContainedMetaVariables());
+            return getMintermExpressionRecur(this->getDdManager()->getCuddManager().getManager(), this->toBdd().getCuddDdNode(), this->getDdManager()->getDdVariables());
-            return getMintermExpressionRecur(this->getDdManager()->getCuddManager().getManager(), this->getCuddAdd().BddPattern().getNode(), this->getDdManager()->getDdVariables());
         }
         
         storm::expressions::Expression Dd<DdType::CUDD>::toExpressionRecur(DdNode const* dd, std::vector<storm::expressions::Variable> const& variables) {
@@ -869,7 +1160,7 @@ namespace storm {
 //            }
         }
         
-        std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd) {
+        std::ostream& operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd) {
             dd.exportToDot();
             return out;
         }

src/storage/dd/CuddDd.h

@@ -5,6 +5,7 @@
 #include <set>
 #include <memory>
 #include <iostream>
+#include <boost/variant.hpp>
 
 #include "src/storage/dd/Dd.h"
 #include "src/storage/dd/CuddDdForwardIterator.h"
@@ -65,17 +66,51 @@ namespace storm {
             /*!
              * Performs a logical or of the current and the given DD.
              *
+             * @param other The second DD used for the operation.
              * @return The logical or of the operands.
              */
             Dd<DdType::CUDD> operator||(Dd<DdType::CUDD> const& other) const;
             
+            /*!
+             * Performs a logical or of the current and the given DD and assigns it to the current DD.
+             *
+             * @param other The second DD used for the operation.
+             * @return A reference to the current DD after the operation
+             */
+            Dd<DdType::CUDD>& operator|=(Dd<DdType::CUDD> const& other);
+            
             /*!
              * Performs a logical and of the current and the given DD.
              *
+             * @param other The second DD used for the operation.
              * @return The logical and of the operands.
              */
             Dd<DdType::CUDD> operator&&(Dd<DdType::CUDD> const& other) const;
             
+            /*!
+             * Performs a logical and of the current and the given DD and assigns it to the current DD.
+             *
+             * @param other The second DD used for the operation.
+             * @return A reference to the current DD after the operation
+             */
+            Dd<DdType::CUDD>& operator&=(Dd<DdType::CUDD> const& other);
+            
+            /*!
+             * Performs a logical iff of the current and the given DD.
+             *
+             * @param other The second DD used for the operation.
+             * @return The logical iff of the operands.
+             */
+            Dd<DdType::CUDD> iff(Dd<DdType::CUDD> const& other) const;
+            
+            /*!
+             * Performs a logical exclusive-or of the current and the given DD.
+             *
+             * @param other The second DD used for the operation.
+             * @return The logical exclusive-or of the operands.
+             */
+            Dd<DdType::CUDD> exclusiveOr(Dd<DdType::CUDD> const& other) const;
+            
             /*!
              * Adds the two DDs.
              *
@@ -296,6 +331,16 @@ namespace storm {
              */
             Dd<DdType::CUDD> multiplyMatrix(Dd<DdType::CUDD> const& otherMatrix, std::set<storm::expressions::Variable> const& summationMetaVariables) const;
             
+            /*!
+             * Computes the logical and of the current and the given DD and existentially abstracts from the given set
+             * of variables.
+             *
+             * @param other The second DD for the logical and.
+             * @param existentialVariables The variables from which to existentially abstract.
+             * @return A DD representing the result.
+             */
+            Dd<DdType::CUDD> andExists(Dd<DdType::CUDD> const& other, std::set<storm::expressions::Variable> const& existentialVariables) const;
+            
             /*!
              * Computes a DD that represents the function in which all assignments with a function value strictly larger
              * than the given value are mapped to one and all others to zero.
@@ -605,20 +650,64 @@ namespace storm {
             
             friend std::ostream & operator<<(std::ostream& out, const Dd<DdType::CUDD>& dd);
             
+            /*!
+             * Converts an MTBDD to a BDD by mapping all values unequal to zero to 1. This effectively does the same as
+             * a call to notZero().
+             *
+             * @return The corresponding BDD.
+             */
+            Dd<DdType::CUDD> toBdd() const;
+
+            /*!
+             * Converts a BDD to an equivalent MTBDD.
+             *
+             * @return The corresponding MTBDD.
+             */
+            Dd<DdType::CUDD> toMtbdd() const;
+            
+            /*!
+             * Retrieves whether this DD is a BDD.
+             *
+             * @return True iff this DD is a BDD.
+             */
+            bool isBdd() const;
+
+            /*!
+             * Retrieves whether this DD is an MTBDD. Even though MTBDDs technicall subsume BDDs, this will return false
+             * if the DD is actually a BDD.
+             *
+             * @return True iff this DD is an MTBDD.
+             */
+            bool isMtbdd() const;
+            
         private:
             /*!
-             * Retrieves a reference to the CUDD ADD object associated with this DD.
+             * Retrieves the CUDD BDD object associated with this DD.
              *
-             * @return The CUDD ADD object associated with this DD.
+             * @return The CUDD BDD object associated with this DD.
              */
-            ADD getCuddAdd();
+            BDD getCuddBdd() const;
             
             /*!
-             * Retrieves the CUDD ADD object associated with this DD.
+             * Retrieves the CUDD MTBDD object associated with this DD.
              *
-             * @return The CUDD ADD object assoicated with this DD.
+             * @return The CUDD MTBDD object associated with this DD.
              */
-            ADD const& getCuddAdd() const;
+            ADD getCuddMtbdd() const;
+            
+            /*!
+             * Retrieves the CUDD object associated with this DD.
+             *
+             * @return The CUDD object associated with this DD.
+             */
+            ABDD const& getCuddDd() const;
+            
+            /*!
+             * Retrieves the raw DD node of CUDD associated with this DD.
+             *
+             * @return The DD node of CUDD associated with this DD.
+             */
+            DdNode* getCuddDdNode() const;
             
             /*!
              * Adds the given meta variable to the set of meta variables that are contained in this DD.
@@ -657,10 +746,19 @@ namespace storm {
              * Creates a DD that encapsulates the given CUDD ADD.
              *
              * @param ddManager The manager responsible for this DD.
-             * @param cuddAdd The CUDD ADD to store.
+             * @param cuddDd The CUDD ADD to store.
+             * @param containedMetaVariables The meta variables that appear in the DD.
+             */
+            Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
+
+            /*!
+             * Creates a DD that encapsulates the given CUDD ADD.
+             *
+             * @param ddManager The manager responsible for this DD.
+             * @param cuddDd The CUDD ADD to store.
              * @param containedMetaVariables The meta variables that appear in the DD.
              */
-            Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, ADD cuddAdd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
+            Dd(std::shared_ptr<DdManager<DdType::CUDD> const> ddManager, BDD cuddDd, std::set<storm::expressions::Variable> const& containedMetaVariables = std::set<storm::expressions::Variable>());
             
             /*!
              * Helper function to convert the DD into a (sparse) matrix.
@@ -727,7 +825,7 @@ namespace storm {
             std::shared_ptr<DdManager<DdType::CUDD> const> ddManager;
             
             // The ADD created by CUDD.
-            ADD cuddAdd;
+            boost::variant<BDD, ADD> cuddDd;
             
             // The meta variables that appear in this DD.
             std::set<storm::expressions::Variable> containedMetaVariables;

src/storage/dd/CuddDdForwardIterator.cpp

@@ -80,19 +80,19 @@ namespace storm {
             ++this->cubeCounter;
             
             for (uint_fast64_t index = 0; index < this->relevantDontCareDdVariables.size(); ++index) {
-                auto const& ddMetaVariable = this->ddManager->getMetaVariable(std::get<1>(this->relevantDontCareDdVariables[index]));
+                auto const& ddMetaVariable = this->ddManager->getMetaVariable(std::get<0>(this->relevantDontCareDdVariables[index]));
                 if (ddMetaVariable.getType() == DdMetaVariable<DdType::CUDD>::MetaVariableType::Bool) {
                     if ((this->cubeCounter & (1ull << index)) != 0) {
-                        currentValuation.setBooleanValue(std::get<1>(this->relevantDontCareDdVariables[index]), true);
+                        currentValuation.setBooleanValue(std::get<0>(this->relevantDontCareDdVariables[index]), true);
                     } else {
-                        currentValuation.setBooleanValue(std::get<1>(this->relevantDontCareDdVariables[index]), false);
+                        currentValuation.setBooleanValue(std::get<0>(this->relevantDontCareDdVariables[index]), false);
                     }
                 } else {
-                    storm::expressions::Variable const& metaVariable = std::get<1>(this->relevantDontCareDdVariables[index]);
+                    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<2>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow());
+                        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<2>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow());
+                        currentValuation.setBitVectorValue(metaVariable, ((currentValuation.getBitVectorValue(metaVariable) - ddMetaVariable.getLow()) & ~(1ull << std::get<1>(this->relevantDontCareDdVariables[index]))) + ddMetaVariable.getLow());
                     }
                 }
             }
@@ -106,31 +106,31 @@ namespace storm {
             // valuations later.
             for (auto const& metaVariable : *this->metaVariables) {
                 bool metaVariableAppearsInCube = false;
-                std::vector<std::tuple<ADD, storm::expressions::Variable, uint_fast64_t>> localRelenvantDontCareDdVariables;
+                std::vector<std::tuple<storm::expressions::Variable, uint_fast64_t>> localRelenvantDontCareDdVariables;
                 auto const& ddMetaVariable = this->ddManager->getMetaVariable(metaVariable);
                 if (ddMetaVariable.getType() == DdMetaVariable<DdType::CUDD>::MetaVariableType::Bool) {
-                    if (this->cube[ddMetaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 0) {
+                    if (this->cube[ddMetaVariable.getDdVariables().front().getIndex()] == 0) {
                         metaVariableAppearsInCube = true;
                         currentValuation.setBooleanValue(metaVariable, false);
-                    } else if (this->cube[ddMetaVariable.getDdVariables()[0].getCuddAdd().NodeReadIndex()] == 1) {
+                    } else if (this->cube[ddMetaVariable.getDdVariables().front().getIndex()] == 1) {
                         metaVariableAppearsInCube = true;
                         currentValuation.setBooleanValue(metaVariable, true);
                     } else {
-                        localRelenvantDontCareDdVariables.push_back(std::make_tuple(ddMetaVariable.getDdVariables()[0].getCuddAdd(), metaVariable, 0));
+                        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[ddMetaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 0) {
+                        if (cube[ddMetaVariable.getDdVariables()[bitIndex].getIndex()] == 0) {
                             // Leave bit unset.
                             metaVariableAppearsInCube = true;
-                        } else if (cube[ddMetaVariable.getDdVariables()[bitIndex].getCuddAdd().NodeReadIndex()] == 1) {
+                        } else if (cube[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(ddMetaVariable.getDdVariables()[bitIndex].getCuddAdd(), metaVariable, ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1));
+                            localRelenvantDontCareDdVariables.push_back(std::make_tuple(metaVariable, ddMetaVariable.getNumberOfDdVariables() - bitIndex - 1));
                         }
                     }
                     if (this->enumerateDontCareMetaVariables || metaVariableAppearsInCube) {

src/storage/dd/CuddDdForwardIterator.h

@@ -124,8 +124,8 @@ namespace storm {
             // 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 <variable, metaVariable, bitIndex>.
+            // A vector of tuples of the form <metaVariable, bitIndex>.
-            std::vector<std::tuple<ADD, storm::expressions::Variable, uint_fast64_t>> relevantDontCareDdVariables;
+            std::vector<std::tuple<storm::expressions::Variable, uint_fast64_t>> relevantDontCareDdVariables;
             
             // The current valuation of meta variables.
             storm::expressions::SimpleValuation currentValuation;

src/storage/dd/CuddDdManager.cpp

@@ -37,19 +37,27 @@ namespace storm {
             }
         }
         
-        Dd<DdType::CUDD> DdManager<DdType::CUDD>::getOne() const {
+        Dd<DdType::CUDD> DdManager<DdType::CUDD>::getOne(bool asMtbdd) const {
-            return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addOne());
+            if (asMtbdd) {
+                return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addOne());
+            } else {
+                return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddOne());
+            }
         }
         
-        Dd<DdType::CUDD> DdManager<DdType::CUDD>::getZero() const {
+        Dd<DdType::CUDD> DdManager<DdType::CUDD>::getZero(bool asMtbdd) const {
-            return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addZero());
+            if (asMtbdd) {
+                return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addZero());
+            } else {
+                return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddZero());
+            }
         }
         
         Dd<DdType::CUDD> DdManager<DdType::CUDD>::getConstant(double value) const {
             return Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.constant(value));
         }
         
-        Dd<DdType::CUDD> DdManager<DdType::CUDD>::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) const {
+        Dd<DdType::CUDD> DdManager<DdType::CUDD>::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value, bool asMtbdd) const {
             DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(variable);
             
             STORM_LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << variable.getName() << "'.");
@@ -68,19 +76,23 @@ namespace storm {
             
             for (std::size_t i = 1; i < ddVariables.size(); ++i) {
                 if (value & (1ull << (ddVariables.size() - i - 1))) {
-                    result *= ddVariables[i];
+                    result &= ddVariables[i];
                 } else {
-                    result *= !ddVariables[i];
+                    result &= !ddVariables[i];
                 }
             }
             
-            return result;
+            if (asMtbdd) {
+                return result.toMtbdd();
+            } else {
+                return result;
+            }
         }
         
-        Dd<DdType::CUDD> DdManager<DdType::CUDD>::getRange(storm::expressions::Variable const& variable) const {
+        Dd<DdType::CUDD> DdManager<DdType::CUDD>::getRange(storm::expressions::Variable const& variable, bool asMtbdd) const {
             storm::dd::DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(variable);
             
-            Dd<DdType::CUDD> result = this->getZero();
+            Dd<DdType::CUDD> result = this->getZero(asMtbdd);
             
             for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
                 result.setValue(variable, value, static_cast<double>(1));
@@ -92,7 +104,7 @@ namespace storm {
         Dd<DdType::CUDD> DdManager<DdType::CUDD>::getIdentity(storm::expressions::Variable const& variable) const {
             storm::dd::DdMetaVariable<DdType::CUDD> const& metaVariable = this->getMetaVariable(variable);
             
-            Dd<DdType::CUDD> result = this->getZero();
+            Dd<DdType::CUDD> result = this->getZero(true);
             for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
                 result.setValue(variable, value, static_cast<double>(value));
             }
@@ -117,13 +129,13 @@ namespace storm {
             std::vector<Dd<DdType::CUDD>> variables;
             std::vector<Dd<DdType::CUDD>> variablesPrime;
             for (std::size_t i = 0; i < numberOfBits; ++i) {
-                variables.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {unprimed}));
+                variables.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {unprimed}));
-                variablesPrime.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {primed}));
+                variablesPrime.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {primed}));
             }
             
             // Now group the non-primed and primed variable.
             for (uint_fast64_t i = 0; i < numberOfBits; ++i) {
-                this->getCuddManager().MakeTreeNode(variables[i].getCuddAdd().NodeReadIndex(), 2, MTR_FIXED);
+                this->getCuddManager().MakeTreeNode(variables[i].getIndex(), 2, MTR_FIXED);
             }
             
             metaVariableMap.emplace(unprimed, DdMetaVariable<DdType::CUDD>(name, low, high, variables, this->shared_from_this()));
@@ -144,11 +156,11 @@ namespace storm {
 
             std::vector<Dd<DdType::CUDD>> variables;
             std::vector<Dd<DdType::CUDD>> variablesPrime;
-            variables.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {unprimed}));
+            variables.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {unprimed}));
-            variablesPrime.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.addVar(), {primed}));
+            variablesPrime.emplace_back(Dd<DdType::CUDD>(this->shared_from_this(), cuddManager.bddVar(), {primed}));
 
             // Now group the non-primed and primed variable.
-            this->getCuddManager().MakeTreeNode(variables.front().getCuddAdd().NodeReadIndex(), 2, MTR_FIXED);
+            this->getCuddManager().MakeTreeNode(variables.front().getIndex(), 2, MTR_FIXED);
             
             metaVariableMap.emplace(unprimed, DdMetaVariable<DdType::CUDD>(name, variables, this->shared_from_this()));
             metaVariableMap.emplace(primed, DdMetaVariable<DdType::CUDD>(name + "'", variablesPrime, this->shared_from_this()));
@@ -199,22 +211,22 @@ namespace storm {
         
         std::vector<std::string> DdManager<DdType::CUDD>::getDdVariableNames() const {
             // First, we initialize a list DD variables and their names.
-            std::vector<std::pair<ADD, std::string>> variablePairs;
+            std::vector<std::pair<uint_fast64_t, std::string>> variablePairs;
             for (auto const& variablePair : this->metaVariableMap) {
                 DdMetaVariable<DdType::CUDD> const& metaVariable = variablePair.second;
                 // If the meta variable is of type bool, we don't need to suffix it with the bit number.
                 if (metaVariable.getType() == DdMetaVariable<storm::dd::DdType::CUDD>::MetaVariableType::Bool) {
-                    variablePairs.emplace_back(metaVariable.getDdVariables().front().getCuddAdd(), variablePair.first.getName());
+                    variablePairs.emplace_back(metaVariable.getDdVariables().front().getIndex(), variablePair.first.getName());
                 } else {
                     // For integer-valued meta variables, we, however, have to add the suffix.
                     for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) {
-                        variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getCuddAdd(), variablePair.first.getName() + '.' + std::to_string(variableIndex));
+                        variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getIndex(), variablePair.first.getName() + '.' + std::to_string(variableIndex));
                     }
                 }
             }
             
             // Then, we sort this list according to the indices of the ADDs.
-            std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair<ADD, std::string> const& a, std::pair<ADD, std::string> const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); });
+            std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair<uint_fast64_t, std::string> const& a, std::pair<uint_fast64_t, std::string> const& b) { return a.first < b.first; });
             
             // Now, we project the sorted vector to its second component.
             std::vector<std::string> result;
@@ -227,22 +239,22 @@ namespace storm {
         
         std::vector<storm::expressions::Variable> DdManager<DdType::CUDD>::getDdVariables() const {
             // First, we initialize a list DD variables and their names.
-            std::vector<std::pair<ADD, storm::expressions::Variable>> variablePairs;
+            std::vector<std::pair<uint_fast64_t, storm::expressions::Variable>> variablePairs;
             for (auto const& variablePair : this->metaVariableMap) {
                 DdMetaVariable<DdType::CUDD> const& metaVariable = variablePair.second;
                 // If the meta variable is of type bool, we don't need to suffix it with the bit number.
                 if (metaVariable.getType() == DdMetaVariable<storm::dd::DdType::CUDD>::MetaVariableType::Bool) {
-                    variablePairs.emplace_back(metaVariable.getDdVariables().front().getCuddAdd(), variablePair.first);
+                    variablePairs.emplace_back(metaVariable.getDdVariables().front().getIndex(), variablePair.first);
                 } else {
                     // For integer-valued meta variables, we, however, have to add the suffix.
                     for (uint_fast64_t variableIndex = 0; variableIndex < metaVariable.getNumberOfDdVariables(); ++variableIndex) {
-                        variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getCuddAdd(), variablePair.first);
+                        variablePairs.emplace_back(metaVariable.getDdVariables()[variableIndex].getIndex(), variablePair.first);
                     }
                 }
             }
             
             // Then, we sort this list according to the indices of the ADDs.
-            std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair<ADD, storm::expressions::Variable> const& a, std::pair<ADD, storm::expressions::Variable> const& b) { return a.first.NodeReadIndex() < b.first.NodeReadIndex(); });
+            std::sort(variablePairs.begin(), variablePairs.end(), [](std::pair<uint_fast64_t, storm::expressions::Variable> const& a, std::pair<uint_fast64_t, storm::expressions::Variable> const& b) { return a.first < b.first; });
             
             // Now, we project the sorted vector to its second component.
             std::vector<storm::expressions::Variable> result;

src/storage/dd/CuddDdManager.h

@@ -36,18 +36,20 @@ namespace storm {
 #endif
             
             /*!
-             * Retrieves a DD representing the constant one function.
+             * Retrieves a DD representing the constant one function. If the flag is set, the result will be given in
+             * terms of an MTBDD rather than a BDD.
              *
              * @return A DD representing the constant one function.
              */
-            Dd<DdType::CUDD> getOne() const;
+            Dd<DdType::CUDD> getOne(bool asMtbdd = false) const;
             
             /*!
-             * Retrieves a DD representing the constant zero function.
+             * Retrieves a DD representing the constant zero function. If the flag is set, the result will be given in
+             * terms of an MTBDD rather than a BDD.
              *
              * @return A DD representing the constant zero function.
              */
-            Dd<DdType::CUDD> getZero() const;
+            Dd<DdType::CUDD> getZero(bool asMtbdd = false) const;
             
             /*!
              * Retrieves a DD representing the constant function with the given value.
@@ -62,19 +64,21 @@ namespace storm {
              *
              * @param variable The expression variable associated with the meta variable.
              * @param value The value the meta variable is supposed to have.
+             * @param asMtbdd If set to true, the result will be given in terms of an MTBDD.
              * @return The DD representing the function that maps all inputs which have the given meta variable equal
              * to the given value one.
              */
-            Dd<DdType::CUDD> getEncoding(storm::expressions::Variable const& variable, int_fast64_t value) const;
+            Dd<DdType::CUDD> getEncoding(storm::expressions::Variable const& variable, int_fast64_t value, bool asMtbdd = false) const;
             
             /*!
              * Retrieves the DD representing the range of the meta variable, i.e., a function that maps all legal values
              * of the range of the meta variable to one.
              *
              * @param variable The expression variable associated with the meta variable.
+             * @param asMtbdd If set to true, the result will be given in terms of an MTBDD.
              * @return The range of the meta variable.
              */
-            Dd<DdType::CUDD> getRange(storm::expressions::Variable const& variable) const;
+            Dd<DdType::CUDD> getRange(storm::expressions::Variable const& variable, bool asMtbdd = false) const;
 
             /*!
              * Retrieves the DD representing the identity of the meta variable, i.e., a function that maps all legal

src/storage/dd/CuddDdMetaVariable.cpp

@@ -3,18 +3,20 @@
 
 namespace storm {
     namespace dd {
-        DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
+        DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Int), low(low), high(high), ddVariables(ddVariables), cube(manager->getOne()), cubeAsMtbdd(manager->getOne(true)), manager(manager) {
             // Create the cube of all variables of this meta variable.
             for (auto const& ddVariable : this->ddVariables) {
-                this->cube *= ddVariable;
+                this->cube &= ddVariable;
             }
+            this->cubeAsMtbdd = this->cube.toMtbdd();
         }
         
-        DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Bool), low(0), high(1), ddVariables(ddVariables), cube(manager->getOne()), manager(manager) {
+        DdMetaVariable<DdType::CUDD>::DdMetaVariable(std::string const& name, std::vector<Dd<DdType::CUDD>> const& ddVariables, std::shared_ptr<DdManager<DdType::CUDD>> manager) : name(name), type(MetaVariableType::Bool), low(0), high(1), ddVariables(ddVariables), cube(manager->getOne()), cubeAsMtbdd(manager->getOne(true)), manager(manager) {
             // Create the cube of all variables of this meta variable.
             for (auto const& ddVariable : this->ddVariables) {
-                this->cube *= ddVariable;
+                this->cube &= ddVariable;
             }
+            this->cubeAsMtbdd = this->cube.toMtbdd();
         }
         
         std::string const& DdMetaVariable<DdType::CUDD>::getName() const {
@@ -48,5 +50,10 @@ namespace storm {
         Dd<DdType::CUDD> const& DdMetaVariable<DdType::CUDD>::getCube() const {
             return this->cube;
         }
+
+        Dd<DdType::CUDD> const& DdMetaVariable<DdType::CUDD>::getCubeAsMtbdd() const {
+            return this->cubeAsMtbdd;
+        }
+
     }
 }

src/storage/dd/CuddDdMetaVariable.h

@@ -113,6 +113,13 @@ namespace storm {
              */
             Dd<DdType::CUDD> const& getCube() const;
             
+            /*!
+             * Retrieves the cube of all variables that encode this meta variable represented as an MTBDD.
+             *
+             * @return The cube of all variables that encode this meta variable.
+             */
+            Dd<DdType::CUDD> const& getCubeAsMtbdd() const;
+            
             // The name of the meta variable.
             std::string name;
             
@@ -131,6 +138,10 @@ namespace storm {
             // The cube consisting of all variables that encode the meta variable.
             Dd<DdType::CUDD> cube;
             
+            // The cube consisting of all variables that encode the meta variable represented by an MTBDD. This is
+            // used as a shortcut mainly for the abstraction methods.
+            Dd<DdType::CUDD> cubeAsMtbdd;
+            
             // A pointer to the manager responsible for this meta variable.
             std::shared_ptr<DdManager<DdType::CUDD>> manager;
         };

src/storage/dd/CuddOdd.cpp

@@ -17,17 +17,17 @@ namespace storm {
             std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>> uniqueTableForLevels(ddVariableIndices.size() + 1);
             
             // Now construct the ODD structure.
-            std::shared_ptr<Odd<DdType::CUDD>> rootOdd = buildOddRec(dd.getCuddAdd().getNode(), manager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
+            // Currently, the DD needs to be an MTBDD, because complement edges are not supported.
+            std::shared_ptr<Odd<DdType::CUDD>> rootOdd = buildOddRec(dd.toMtbdd().getCuddDdNode(), manager->getCuddManager(), 0, ddVariableIndices.size(), ddVariableIndices, uniqueTableForLevels);
             
             // Finally, move the children of the root ODD into this ODD.
-            this->dd = rootOdd->dd;
             this->elseNode = std::move(rootOdd->elseNode);
             this->thenNode = std::move(rootOdd->thenNode);
             this->elseOffset = rootOdd->elseOffset;
             this->thenOffset = rootOdd->thenOffset;
         }
         
-        Odd<DdType::CUDD>::Odd(ADD dd, std::shared_ptr<Odd<DdType::CUDD>>&& elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd<DdType::CUDD>>&& thenNode, uint_fast64_t thenOffset) : dd(dd), elseNode(elseNode), thenNode(thenNode), elseOffset(elseOffset), thenOffset(thenOffset) {
+        Odd<DdType::CUDD>::Odd(std::shared_ptr<Odd<DdType::CUDD>> elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd<DdType::CUDD>> thenNode, uint_fast64_t thenOffset) : elseNode(elseNode), thenNode(thenNode), elseOffset(elseOffset), thenOffset(thenOffset) {
             // Intentionally left empty.
         }
         
@@ -92,18 +92,18 @@ namespace storm {
                         thenOffset = 1;
                     }
                     
-                    return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(ADD(manager, dd), nullptr, elseOffset, nullptr, thenOffset));
+                    return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(nullptr, elseOffset, nullptr, thenOffset));
                 } else if (ddVariableIndices[currentLevel] < static_cast<uint_fast64_t>(dd->index)) {
                     // If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
                     // node for the then-successor as well.
                     std::shared_ptr<Odd<DdType::CUDD>> elseNode = buildOddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
                     std::shared_ptr<Odd<DdType::CUDD>> thenNode = elseNode;
-                    return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(ADD(manager, dd), std::move(elseNode), elseNode->getElseOffset() + elseNode->getThenOffset(), std::move(thenNode), thenNode->getElseOffset() + thenNode->getThenOffset()));
+                    return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()));
                 } else {
                     // Otherwise, we compute the ODDs for both the then- and else successors.
                     std::shared_ptr<Odd<DdType::CUDD>> elseNode = buildOddRec(Cudd_E(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
                     std::shared_ptr<Odd<DdType::CUDD>> thenNode = buildOddRec(Cudd_T(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
-                    return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(ADD(manager, dd), std::move(elseNode), elseNode->getElseOffset() + elseNode->getThenOffset(), std::move(thenNode), thenNode->getElseOffset() + thenNode->getThenOffset()));
+                    return std::shared_ptr<Odd<DdType::CUDD>>(new Odd<DdType::CUDD>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()));
                 }
             }
         }

src/storage/dd/CuddOdd.h

@@ -92,13 +92,13 @@ namespace storm {
             /*!
              * Constructs an offset-labeled DD with the given topmost DD node, else- and then-successor.
              *
-             * @param dd The DD associated with this ODD node.
+             * @param dd The DD node associated with this ODD node.
              * @param elseNode The else-successor of thie ODD node.
              * @param elseOffset The offset of the else-successor.
              * @param thenNode The then-successor of thie ODD node.
              * @param thenOffset The offset of the then-successor.
              */
-            Odd(ADD dd, std::shared_ptr<Odd<DdType::CUDD>>&& elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd<DdType::CUDD>>&& thenNode, uint_fast64_t thenOffset);
+            Odd(std::shared_ptr<Odd<DdType::CUDD>> elseNode, uint_fast64_t elseOffset, std::shared_ptr<Odd<DdType::CUDD>> thenNode, uint_fast64_t thenOffset);
             
             /*!
              * Recursively builds the ODD.
@@ -114,9 +114,6 @@ namespace storm {
              */
             static std::shared_ptr<Odd<DdType::CUDD>> buildOddRec(DdNode* dd, Cudd const& manager, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<std::map<DdNode*, std::shared_ptr<Odd<DdType::CUDD>>>>& uniqueTableForLevels);
             
-            // The DD associated with this ODD node.
-            ADD dd;
-            
             // The then- and else-nodes.
             std::shared_ptr<Odd<DdType::CUDD>> elseNode;
             std::shared_ptr<Odd<DdType::CUDD>> thenNode;

src/utility/cli.h

@@ -70,6 +70,7 @@ log4cplus::Logger printer;
 #include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
 
 // Headers related to exception handling.
+#include "src/exceptions/InvalidStateException.h"
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/exceptions/InvalidSettingsException.h"
 #include "src/exceptions/InvalidTypeException.h"
@@ -276,22 +277,25 @@ namespace storm {
                 }
                 
                 // Customize model-building.
-//                typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options;
+                if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Sparse) {
-//                if (formula) {
+                    typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options;
-//                    options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(*formula.get());
+                    if (formula) {
-//                }
+                        options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(*formula.get());
-//                options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
+                    }
-//                
+                    options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
-//                // Then, build the model from the symbolic description.
+                    // Then, build the model from the symbolic description.
-//                result = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
+                    result = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
-                
+                } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd) {
-                typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
+                    typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
-                if (formula) {
+                    if (formula) {
-                    options = typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options(*formula.get());
+                        options = typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options(*formula.get());
+                    }
+                    options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
+                    
+                    storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
                 }
-                options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
                 
-                storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
                 return result;
             }
             
@@ -425,6 +429,8 @@ namespace storm {
                 STORM_LOG_THROW(program, storm::exceptions::InvalidStateException, "Program has not been successfully parsed.");
                 std::shared_ptr<storm::models::AbstractModel<ValueType>> model = buildSymbolicModel<ValueType>(program.get(), formula);
                 
+                STORM_LOG_THROW(model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
+                
                 // Preprocess the model if needed.
                 model = preprocessModel<ValueType>(model, formula);
 

test/functional/storage/CuddDdTest.cpp

@@ -62,8 +62,15 @@ TEST(CuddDdManager, EncodingTest) {
     ASSERT_THROW(encoding = manager->getEncoding(x.first, 10), storm::exceptions::InvalidArgumentException);
     ASSERT_NO_THROW(encoding = manager->getEncoding(x.first, 4));
     EXPECT_EQ(1, encoding.getNonZeroCount());
-    EXPECT_EQ(6, encoding.getNodeCount());
+    // As a BDD, this DD has one only leaf, because there does not exist a 0-leaf, and (consequently) one node less
-    EXPECT_EQ(2, encoding.getLeafCount());
+    // than the MTBDD.
+    EXPECT_EQ(5, encoding.getNodeCount());
+    EXPECT_EQ(1, encoding.getLeafCount());
+    
+    // As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6.
+    EXPECT_EQ(6, encoding.toMtbdd().getNodeCount());
+    EXPECT_EQ(2, encoding.toMtbdd().getLeafCount());
 }
 
 TEST(CuddDdManager, RangeTest) {
@@ -75,8 +82,8 @@ TEST(CuddDdManager, RangeTest) {
     ASSERT_NO_THROW(range = manager->getRange(x.first));
     
     EXPECT_EQ(9, range.getNonZeroCount());
-    EXPECT_EQ(2, range.getLeafCount());
+    EXPECT_EQ(1, range.getLeafCount());
-    EXPECT_EQ(6, range.getNodeCount());
+    EXPECT_EQ(5, range.getNodeCount());
 }
 
 TEST(CuddDdManager, IdentityTest) {
@@ -100,17 +107,14 @@ TEST(CuddDd, OperatorTest) {
     EXPECT_FALSE(manager->getZero() != manager->getZero());
     EXPECT_TRUE(manager->getZero() != manager->getOne());
     
-    storm::dd::Dd<storm::dd::DdType::CUDD> dd1 = manager->getOne();
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd1 = manager->getOne(true);
-    storm::dd::Dd<storm::dd::DdType::CUDD> dd2 = manager->getOne();
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd2 = manager->getOne(true);
     storm::dd::Dd<storm::dd::DdType::CUDD> dd3 = dd1 + dd2;
     EXPECT_TRUE(dd3 == manager->getConstant(2));
     
-    dd3 += manager->getZero();
+    dd3 += manager->getZero(true);
     EXPECT_TRUE(dd3 == manager->getConstant(2));
     
-    dd3 = dd1 && manager->getConstant(3);
-    EXPECT_TRUE(dd1 == manager->getOne());
-
     dd3 = dd1 * manager->getConstant(3);
     EXPECT_TRUE(dd3 == manager->getConstant(3));
 
@@ -118,22 +122,22 @@ TEST(CuddDd, OperatorTest) {
     EXPECT_TRUE(dd3 == manager->getConstant(6));
     
     dd3 = dd1 - dd2;
-    EXPECT_TRUE(dd3 == manager->getZero());
+    EXPECT_TRUE(dd3.isZero());
     
     dd3 -= manager->getConstant(-2);
     EXPECT_TRUE(dd3 == manager->getConstant(2));
     
     dd3 /= manager->getConstant(2);
-    EXPECT_TRUE(dd3 == manager->getOne());
+    EXPECT_TRUE(dd3.isOne());
     
-    dd3.complement();
+    dd3 = dd3.toBdd().complement();
-    EXPECT_TRUE(dd3 == manager->getZero());
+    EXPECT_TRUE(dd3.isZero());
     
     dd1 = !dd3;
-    EXPECT_TRUE(dd1 == manager->getOne());
+    EXPECT_TRUE(dd1.isOne());
 
-    dd3 = dd1 || dd2;
+    dd3 = dd1 || dd2.toBdd();
-    EXPECT_TRUE(dd3 == manager->getOne());
+    EXPECT_TRUE(dd3.isOne());
     
     dd1 = manager->getIdentity(x.first);
     dd2 = manager->getConstant(5);
@@ -142,7 +146,7 @@ TEST(CuddDd, OperatorTest) {
     EXPECT_EQ(1, dd3.getNonZeroCount());
     
     storm::dd::Dd<storm::dd::DdType::CUDD> dd4 = dd1.notEquals(dd2);
-    EXPECT_TRUE(dd4 == !dd3);
+    EXPECT_TRUE(dd4.toBdd() == !dd3.toBdd());
     
     dd3 = dd1.less(dd2);
     EXPECT_EQ(11, dd3.getNonZeroCount());
@@ -161,12 +165,12 @@ TEST(CuddDd, OperatorTest) {
     EXPECT_EQ(10, dd4.getNonZeroCount());
     
     dd4 = dd3.minimum(dd1);
-    dd4 *= manager->getEncoding(x.first, 2);
+    dd4 *= manager->getEncoding(x.first, 2, true);
     dd4 = dd4.sumAbstract({x.first});
     EXPECT_EQ(2, dd4.getValue());
 
     dd4 = dd3.maximum(dd1);
-    dd4 *= manager->getEncoding(x.first, 2);
+    dd4 *= manager->getEncoding(x.first, 2, true);
     dd4 = dd4.sumAbstract({x.first});
     EXPECT_EQ(5, dd4.getValue());
 
@@ -197,7 +201,7 @@ TEST(CuddDd, AbstractionTest) {
     EXPECT_EQ(1, dd3.getNonZeroCount());
     ASSERT_THROW(dd3 = dd3.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException);
     ASSERT_NO_THROW(dd3 = dd3.existsAbstract({x.first}));
-    EXPECT_TRUE(dd3 == manager->getZero());
+    EXPECT_TRUE(dd3.isOne());
 
     dd3 = dd1.equals(dd2);
     dd3 *= manager->getConstant(3);
@@ -253,7 +257,7 @@ TEST(CuddDd, GetSetValueTest) {
     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);
     
-    storm::dd::Dd<storm::dd::DdType::CUDD> dd1 = manager->getOne();
+    storm::dd::Dd<storm::dd::DdType::CUDD> dd1 = manager->getOne(true);
     ASSERT_NO_THROW(dd1.setValue(x.first, 4, 2));
     EXPECT_EQ(2, dd1.getLeafCount());