From 8c1870eb549918de4ff2becf67b3c6c40efe9022 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 18 Feb 2015 17:08:33 +0100
Subject: [PATCH] Intermediate commit.

Former-commit-id: e5f251718f0f024c41d8268cf55d3eecc538f0ce
---
 src/builder/DdPrismModelBuilder.cpp           | 175 +++++++++++++-----
 src/builder/DdPrismModelBuilder.h             |  16 +-
 src/builder/ExplicitPrismModelBuilder.cpp     |   6 +
 src/parser/PrismParser.cpp                    |   2 +-
 src/storage/expressions/Expression.cpp        |   7 +
 src/storage/expressions/Expression.h          |   8 +
 src/storage/prism/Command.cpp                 |  15 ++
 src/storage/prism/Command.h                   |   9 +
 src/storage/prism/Module.cpp                  |  25 +++
 src/storage/prism/Module.h                    |   8 +
 src/storage/prism/Program.cpp                 |  84 ++++++++-
 src/storage/prism/Program.h                   |  20 ++
 src/storage/prism/RewardModel.cpp             |  14 ++
 src/storage/prism/RewardModel.h               |   9 +
 src/utility/cli.h                             |   3 +
 .../builder/DdPrismModelBuilderTest.cpp       |  27 +++
 .../builder/ExplicitPrismModelBuilderTest.cpp |  28 +++
 test/functional/builder/coin2-2.nm            |  60 ++++++
 test/functional/builder/csma2-2.nm            | 130 +++++++++++++
 test/functional/builder/firewire3-0.5.nm      | 170 +++++++++++++++++
 test/functional/builder/leader3.nm            |  91 +++++++++
 test/functional/builder/two_dice.nm           |  40 ++++
 wlan0_collide.nm                              |  13 ++
 23 files changed, 904 insertions(+), 56 deletions(-)
 create mode 100644 test/functional/builder/coin2-2.nm
 create mode 100644 test/functional/builder/csma2-2.nm
 create mode 100644 test/functional/builder/firewire3-0.5.nm
 create mode 100644 test/functional/builder/leader3.nm
 create mode 100644 test/functional/builder/two_dice.nm
 create mode 100644 wlan0_collide.nm

diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index acc7c5235..43f051eb5 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -82,23 +82,25 @@ namespace storm {
                 updateDd *= result;
             }
             
-            // FIXME: global boolean variables cause problems. They cannot be added here, because then synchronization goes wrong.
-//            for (uint_fast64_t i = 0; i < generationInfo.program.getGlobalBooleanVariables().size(); ++i) {
-//                storm::prism::BooleanVariable const& booleanVariable = generationInfo.program.getGlobalBooleanVariables().at(i);
-//                if (update.getAssignmentMapping().find(booleanVariable.getName()) == update.getAssignmentMapping().end()) {
-//                    // Multiply identity matrix
-//                    updateDd = updateDd * generationInfo.variableToIdentityDecisionDiagramMap.at(booleanVariable.getName());
-//                }
-//            }
-//            
-//            // All unused global integer variables do not change
-//            for (uint_fast64_t i = 0; i < generationInfo.program.getGlobalIntegerVariables().size(); ++i) {
-//                storm::prism::IntegerVariable const& integerVariable = generationInfo.program.getGlobalIntegerVariables().at(i);
-//                if (update.getAssignmentMapping().find(integerVariable.getName()) == update.getAssignmentMapping().end()) {
-//                    // Multiply identity matrix
-//                    updateDd = updateDd * generationInfo.variableToIdentityDecisionDiagramMap.at(integerVariable.getName());
-//                }
-//            }
+            // This works under the assumption that global variables are only written in non-synchronzing commands, but
+            // is not checked here.
+            for (auto const& booleanVariable : generationInfo.program.getGlobalBooleanVariables()) {
+                storm::expressions::Variable const& metaVariable = generationInfo.variableToRowMetaVariableMap.at(booleanVariable.getExpressionVariable());
+
+                if (assignedVariables.find(metaVariable) == assignedVariables.end()) {
+                    STORM_LOG_TRACE("Multiplying identity of variable " << booleanVariable.getName());
+                    updateDd *= generationInfo.variableToIdentityMap.at(booleanVariable.getExpressionVariable());
+                }
+            }
+            
+            // All unused global integer variables do not change
+            for (auto const& integerVariable : generationInfo.program.getGlobalIntegerVariables()) {
+                storm::expressions::Variable const& metaVariable = generationInfo.variableToRowMetaVariableMap.at(integerVariable.getExpressionVariable());
+                if (assignedVariables.find(metaVariable) == assignedVariables.end()) {
+                    STORM_LOG_TRACE("Multiplying identity of variable " << integerVariable.getName());
+                    updateDd *= generationInfo.variableToIdentityMap.at(integerVariable.getExpressionVariable());
+                }
+            }
             
             // All unassigned boolean variables need to keep their value.
             for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) {
@@ -140,6 +142,7 @@ namespace storm {
                     commandDd += updateDd;
                 }
                 
+                (guardDd * commandDd).exportToDot(module.getName() + "_" + command.getActionName() + ".dot");
                 return ActionDecisionDiagram(guardDd, guardDd * commandDd);
             } else {
                 return ActionDecisionDiagram(*generationInfo.manager);
@@ -152,16 +155,28 @@ namespace storm {
             for (storm::prism::Command const& command : module.getCommands()) {
                 
                 // Determine whether the command is relevant for the selected action.
-                bool relevant = (!synchronizationActionIndex && !command.isLabeled()) || (synchronizationActionIndex && command.getActionIndex() == synchronizationActionIndex.get());
+                bool relevant = (!synchronizationActionIndex && !command.isLabeled()) || (synchronizationActionIndex && command.isLabeled() && command.getActionIndex() == synchronizationActionIndex.get());
                 
                 if (!relevant) {
                     continue;
                 }
                 
+                if (synchronizationActionIndex) {
+                    std::cout << command << " is relevant for synch " << synchronizationActionIndex.get() << std::endl;
+                }
+                
                 // At this point, the command is known to be relevant for the action.
                 commandDds.push_back(createCommandDecisionDiagram(generationInfo, module, command));
             }
             
+            if (synchronizationActionIndex && synchronizationActionIndex.get() == 0) {
+                int i = 0;
+                for (auto const& commandDd : commandDds) {
+                    commandDd.transitionsDd.exportToDot("cmd_" + std::to_string(i) + ".dot");
+                    ++i;
+                }
+            }
+            
             ActionDecisionDiagram result(*generationInfo.manager);
             if (!commandDds.empty()) {
                 switch (generationInfo.program.getModelType()){
@@ -318,6 +333,9 @@ namespace storm {
             storm::dd::Dd<Type> action1Extended = action1.transitionsDd * identityDd2;
             storm::dd::Dd<Type> action2Extended = action2.transitionsDd * identityDd1;
 
+            action1.transitionsDd.exportToDot("act1.dot");
+            action2.transitionsDd.exportToDot("act2.dot");
+            
             if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) {
                 return ActionDecisionDiagram(action1.guardDd + action2.guardDd, action1Extended + action2Extended, 0);
             } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
@@ -329,24 +347,28 @@ 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);
+                std::cout << "max used nondet: " << numberOfUsedNondeterminismVariables << std::endl;
                 if (action1.numberOfUsedNondeterminismVariables > action2.numberOfUsedNondeterminismVariables) {
                     storm::dd::Dd<Type> nondeterminisimEncoding = generationInfo.manager->getOne();
                     
-                    for (uint_fast64_t i = action2.numberOfUsedNondeterminismVariables + 1; i <= action1.numberOfUsedNondeterminismVariables; ++i) {
+                    for (uint_fast64_t i = action2.numberOfUsedNondeterminismVariables; i < action1.numberOfUsedNondeterminismVariables; ++i) {
                         nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0);
                     }
                     action2Extended *= nondeterminisimEncoding;
                 } else if (action2.numberOfUsedNondeterminismVariables > action1.numberOfUsedNondeterminismVariables) {
                     storm::dd::Dd<Type> nondeterminisimEncoding = generationInfo.manager->getOne();
                     
-                    for (uint_fast64_t i = action1.numberOfUsedNondeterminismVariables + 1; i <= action2.numberOfUsedNondeterminismVariables; ++i) {
+                    for (uint_fast64_t i = action1.numberOfUsedNondeterminismVariables; i < action2.numberOfUsedNondeterminismVariables; ++i) {
                         nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0);
                     }
                     action1Extended *= nondeterminisimEncoding;
                 }
                 
+                action1Extended.exportToDot("act1ext.dot");
+                action2Extended.exportToDot("act2ext.dot");
+                
                 // Add a new variable that resolves the nondeterminism between the two choices.
-                storm::dd::Dd<Type> combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables + 1], 1).ite(action2Extended, action1Extended);
+                storm::dd::Dd<Type> combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1).ite(action2Extended, action1Extended);
                 
                 return ActionDecisionDiagram(action1.guardDd || action2.guardDd, combinedTransitions, numberOfUsedNondeterminismVariables + 1);
             } else {
@@ -358,15 +380,18 @@ namespace storm {
         typename DdPrismModelBuilder<Type>::ModuleDecisionDiagram DdPrismModelBuilder<Type>::createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map<uint_fast64_t, uint_fast64_t> const& synchronizingActionToOffsetMap) {
             // Start by creating the action DD for the independent action.
             ActionDecisionDiagram independentActionDd = createActionDecisionDiagram(generationInfo, module, boost::optional<uint_fast64_t>(), 0);
+            uint_fast64_t numberOfUsedNondeterminismVariables = independentActionDd.numberOfUsedNondeterminismVariables;
             
             // Create module DD for all synchronizing actions of the module.
             std::map<uint_fast64_t, ActionDecisionDiagram> actionIndexToDdMap;
             for (auto const& actionIndex : module.getActionIndices()) {
                 STORM_LOG_TRACE("Creating DD for action '" << actionIndex << "'.");
-                actionIndexToDdMap.emplace(actionIndex, createActionDecisionDiagram(generationInfo, module, actionIndex, synchronizingActionToOffsetMap.at(actionIndex)));
+                ActionDecisionDiagram tmp = createActionDecisionDiagram(generationInfo, module, actionIndex, synchronizingActionToOffsetMap.at(actionIndex));
+                numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, tmp.numberOfUsedNondeterminismVariables);
+                actionIndexToDdMap.emplace(actionIndex, tmp);
             }
             
-            return ModuleDecisionDiagram(independentActionDd, actionIndexToDdMap, generationInfo.moduleToIdentityMap.at(module.getName()));
+            return ModuleDecisionDiagram(independentActionDd, actionIndexToDdMap, generationInfo.moduleToIdentityMap.at(module.getName()), numberOfUsedNondeterminismVariables);
         }
         
         template <storm::dd::DdType Type>
@@ -375,17 +400,15 @@ namespace storm {
             if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
                 storm::dd::Dd<Type> result = generationInfo.manager->getZero();
                 
-                // First, determine the maximal variable index that is used.
-                uint_fast64_t numberOfUsedNondeterminismVariables = module.independentAction.numberOfUsedNondeterminismVariables;
-                for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) {
-                    numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, synchronizingAction.second.numberOfUsedNondeterminismVariables);
-                }
+                // 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;
+                std::cout << "pumping number of used nondet variables to " << numberOfUsedNondeterminismVariables << std::endl;
 
-                // Now make all actions use the same amount of nondeterminism variables.
-                
                 // Add variables to independent action DD.
                 storm::dd::Dd<Type> nondeterminismEncoding = generationInfo.manager->getOne();
-                for (uint_fast64_t i = module.independentAction.numberOfUsedNondeterminismVariables + 1; i <= numberOfUsedNondeterminismVariables; ++i) {
+                for (uint_fast64_t i = module.independentAction.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) {
+                    std::cout << "adding " << i << " to independent" << std::endl;
                     nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0);
                 }
                 result = module.independentAction.transitionsDd * nondeterminismEncoding;
@@ -394,7 +417,7 @@ namespace storm {
                 std::map<uint_fast64_t, storm::dd::Dd<Type>> synchronizingActionToDdMap;
                 for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) {
                     nondeterminismEncoding = generationInfo.manager->getOne();
-                    for (uint_fast64_t i = synchronizingAction.second.numberOfUsedNondeterminismVariables + 1; i <= numberOfUsedNondeterminismVariables; ++i) {
+                    for (uint_fast64_t i = synchronizingAction.second.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) {
                         nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0);
                     }
                     synchronizingActionToDdMap.emplace(synchronizingAction.first, synchronizingAction.second.transitionsDd * nondeterminismEncoding);
@@ -422,8 +445,9 @@ namespace storm {
                 }
                 
                 // Now, we can simply add all synchronizing actions to the result.
-                for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) {
-                    result += synchronizingAction.second.transitionsDd;
+                for (auto const& synchronizingAction : synchronizingActionToDdMap) {
+                    synchronizingAction.second.exportToDot("synch" + std::to_string(synchronizingAction.first) + ".dot");
+                    result += synchronizingAction.second;
                 }
 
                 return result;
@@ -466,7 +490,9 @@ namespace storm {
                 ModuleDecisionDiagram nextModule = createModuleDecisionDiagram(generationInfo, currentModule, synchronizingActionToOffsetMap);
                 
                 // Combine the non-synchronizing action.
+                uint_fast64_t numberOfUsedNondeterminismVariables = nextModule.numberOfUsedNondeterminismVariables;
                 system.independentAction = combineUnsynchronizedActions(generationInfo, system.independentAction, nextModule.independentAction, system.identity, nextModule.identity);
+                numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, system.independentAction.numberOfUsedNondeterminismVariables);
                 
                 // For all synchronizing actions that the next module does not have, we need to multiply the identity of the next module.
                 for (auto& action : system.synchronizingActionToDecisionDiagramMap) {
@@ -479,13 +505,19 @@ namespace storm {
                 for (auto const& actionIndex : currentModule.getActionIndices()) {
                     if (system.hasSynchronizingAction(actionIndex)) {
                         system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineSynchronizingActions(generationInfo, system.synchronizingActionToDecisionDiagramMap[actionIndex], nextModule.synchronizingActionToDecisionDiagramMap[actionIndex]);
+                        numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables);
                     } else {
                         system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineUnsynchronizedActions(generationInfo, ActionDecisionDiagram(*generationInfo.manager), nextModule.synchronizingActionToDecisionDiagramMap[actionIndex], system.identity, nextModule.identity);
+                        numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables);
                     }
                 }
                 
                 // Combine identity matrices.
                 system.identity = system.identity * nextModule.identity;
+                
+                // Keep track of the number of nondeterminism variables used.
+                std::cout << "num used: " << numberOfUsedNondeterminismVariables << std::endl;
+                system.numberOfUsedNondeterminismVariables = std::max(system.numberOfUsedNondeterminismVariables, numberOfUsedNondeterminismVariables);
             }
             
             storm::dd::Dd<Type> result = createSystemFromModule(generationInfo, system);
@@ -493,6 +525,15 @@ namespace storm {
             // For DTMCs, we normalize each row to 1 (to account for non-determinism).
             if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) {
                 result = result / result.sumAbstract(generationInfo.columnMetaVariables);
+            } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
+                // For MDPs, we need to throw away the nondeterminism variables from the generation information that
+                // were never used.
+                std::cout << "System uses " << system.numberOfUsedNondeterminismVariables << "nd vars" << std::endl;
+                for (uint_fast64_t index = system.numberOfUsedNondeterminismVariables; index < generationInfo.nondeterminismMetaVariables.size(); ++index) {
+                    std::cout << "removing " << generationInfo.nondeterminismMetaVariables[index].getName() << std::endl;
+                    generationInfo.allNondeterminismVariables.erase(generationInfo.nondeterminismMetaVariables[index]);
+                }
+                generationInfo.nondeterminismMetaVariables.resize(system.numberOfUsedNondeterminismVariables);
             }
             
             return std::make_pair(result, system);
@@ -508,9 +549,24 @@ namespace storm {
                 preparedProgram = program;
             }
             
-            preparedProgram = preparedProgram.substituteConstants();
+            if (preparedProgram.hasUndefinedConstants()) {
+                std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram.getUndefinedConstants();
+                std::stringstream stream;
+                bool printComma = false;
+                for (auto const& constant : undefinedConstants) {
+                    if (printComma) {
+                        stream << ", ";
+                    } else {
+                        printComma = true;
+                    }
+                    stream << constant.get().getName() << " (" << constant.get().getType() << ")";
+                }
+                stream << ".";
+                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
+            }
             
-//            std::cout << "translated prog: " << preparedProgram << std::endl;
+            preparedProgram = preparedProgram.substituteConstants();
+            std::cout << "translated prog: " << preparedProgram << std::endl;
             
             // Start by initializing the structure used for storing all information needed during the model generation.
             // In particular, this creates the meta variables used to encode the model.
@@ -519,33 +575,55 @@ namespace storm {
             auto clock = std::chrono::high_resolution_clock::now();
             std::pair<storm::dd::Dd<Type>, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo);
             storm::dd::Dd<Type> transitionMatrix = transitionMatrixModulePair.first;
+            transitionMatrix.exportToDot("trans.dot");
             ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second;
             
             // Cut the transition matrix to the reachable fragment of the state space.
             storm::dd::Dd<Type> reachableStates = computeReachableStates(generationInfo, createInitialStatesDecisionDiagram(generationInfo), transitionMatrix);
             transitionMatrix *= reachableStates;
+            reachableStates.exportToDot("reach.dot");
 
             // Detect deadlocks and 1) fix them if requested 2) throw an error otherwise.
             storm::dd::Dd<Type> statesWithTransition = transitionMatrix.notZero();
             if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
-                statesWithTransition.existsAbstract(generationInfo.allNondeterminismVariables);
+                statesWithTransition = statesWithTransition.existsAbstract(generationInfo.allNondeterminismVariables);
+                statesWithTransition.exportToDot("after_exists.dot");
             }
             statesWithTransition = statesWithTransition.existsAbstract(generationInfo.columnMetaVariables);
             storm::dd::Dd<Type> deadlockStates = reachableStates * !statesWithTransition;
+            deadlockStates.exportToDot("deadlocks.dot");
 
-            if (!deadlockStates.isZero()) {
-                // If we need to fix deadlocks, we do so now.
-                if (!storm::settings::generalSettings().isDontFixDeadlocksSet()) {
-                    STORM_LOG_WARN("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states.");
-                    
-                    // FIXME: For MDPs, we need to use an action encoding if we do not want to attach a lot of self-loops.
-                    transitionMatrix += deadlockStates * globalModule.identity;
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically.");
-                }
+//            if (!deadlockStates.isZero()) {
+//                // If we need to fix deadlocks, we do so now.
+//                if (!storm::settings::generalSettings().isDontFixDeadlocksSet()) {
+//                    std::cout << "fixing " << deadlockStates.getNonZeroCount() << std::endl;
+//                    STORM_LOG_WARN("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states.");
+//
+//                    if (program.getModelType() == storm::prism::Program::ModelType::DTMC) {
+//                        // For DTMCs, we can simply add the identity of the global module for all deadlock states.
+//                        transitionMatrix += deadlockStates * globalModule.identity;
+//                    } 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();
+//                        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;
+//                        (deadlockStates * globalModule.identity * action).exportToDot("selfloops.dot");
+//                    }
+//                } else {
+//                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically.");
+//                }
+//            } else {
+//                std::cout << "no deadlocks" << std::endl;
+//            }
+            
+            transitionMatrix.exportToDot("trans_reach.dot");
+            for (auto const& var : transitionMatrix.getContainedMetaVariables()) {
+                std::cout << "var: " << var.getName() << std::endl;
             }
             
-            return std::make_pair(reachableStates, transitionMatrix * reachableStates);
+            std::cout << reachableStates.getNonZeroCount() << " states and " << transitionMatrix.getNonZeroCount() << " transitions." << std::endl;
+            return std::make_pair(reachableStates, transitionMatrix);
         }
         
         template <storm::dd::DdType Type>
@@ -569,6 +647,7 @@ namespace storm {
                 transitionBdd = transitionBdd.existsAbstract(generationInfo.allNondeterminismVariables);
             }
             
+            transitionBdd.exportToDot("trans01.dot");
             
             // Perform the BFS to discover all reachable states.
             bool changed = true;
diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h
index 05f380060..20d94cf45 100644
--- a/src/builder/DdPrismModelBuilder.h
+++ b/src/builder/DdPrismModelBuilder.h
@@ -91,15 +91,15 @@ namespace storm {
             
             // This structure holds all decision diagrams related to a module.
             struct ModuleDecisionDiagram {
-                ModuleDecisionDiagram() : independentAction(), synchronizingActionToDecisionDiagramMap(), identity() {
+                ModuleDecisionDiagram() : independentAction(), synchronizingActionToDecisionDiagramMap(), identity(), numberOfUsedNondeterminismVariables(0) {
                     // Intentionally left empty.
                 }
                 
-                ModuleDecisionDiagram(storm::dd::DdManager<Type> const& manager) : independentAction(manager), synchronizingActionToDecisionDiagramMap(), identity(manager.getZero()) {
+                ModuleDecisionDiagram(storm::dd::DdManager<Type> const& manager) : independentAction(manager), synchronizingActionToDecisionDiagramMap(), identity(manager.getZero()), numberOfUsedNondeterminismVariables(0) {
                     // Intentionally left empty.
                 }
 
-                ModuleDecisionDiagram(ActionDecisionDiagram const& independentAction, std::map<uint_fast64_t, ActionDecisionDiagram> const& synchronizingActionToDecisionDiagramMap, storm::dd::Dd<Type> const& identity) : independentAction(independentAction), synchronizingActionToDecisionDiagramMap(synchronizingActionToDecisionDiagramMap), identity(identity) {
+                ModuleDecisionDiagram(ActionDecisionDiagram const& independentAction, std::map<uint_fast64_t, ActionDecisionDiagram> const& synchronizingActionToDecisionDiagramMap, storm::dd::Dd<Type> const& identity, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : independentAction(independentAction), synchronizingActionToDecisionDiagramMap(synchronizingActionToDecisionDiagramMap), identity(identity), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) {
                     // Intentionally left empty.
                 }
                 
@@ -118,6 +118,9 @@ namespace storm {
                 
                 // A decision diagram that represents the identity of this module.
                 storm::dd::Dd<Type> identity;
+                
+                // The number of variables encoding the nondeterminism that were actually used.
+                uint_fast64_t numberOfUsedNondeterminismVariables;
             };
             
             /*!
@@ -177,8 +180,8 @@ namespace storm {
                  */
                 void createMetaVariablesAndIdentities() {
                     // Add synchronization variables.
-                    for (uint_fast64_t i = 0; i < program.getActionIndices().size(); ++i) {
-                        std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable("sync" + std::to_string(i));
+                    for (auto const& actionIndex : program.getActionIndices()) {
+                        std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable(program.getActionName(actionIndex));
                         synchronizationMetaVariables.push_back(variablePair.first);
                         allNondeterminismVariables.insert(variablePair.first);
                     }
@@ -209,7 +212,8 @@ namespace storm {
                         storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first);
                         variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity);
                         rowColumnMetaVariablePairs.push_back(variablePair);
-                    }                    for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) {
+                    }
+                    for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) {
                         std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable(booleanVariable.getName());
                         
                         rowMetaVariables.insert(variablePair.first);
diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index 974d9d306..153ab0afe 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -103,6 +103,8 @@ namespace storm {
             
             // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.
 #ifdef STORM_HAVE_CARL
+            // If the program either has undefined constants or we are building a parametric model, but the parameters
+            // not only appear in the probabilities, we re
             if (!std::is_same<ValueType, storm::RationalFunction>::value && preparedProgram.hasUndefinedConstants()) {
 #else
             if (preparedProgram.hasUndefinedConstants()) {
@@ -120,6 +122,10 @@ namespace storm {
                 }
                 stream << ".";
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
+#ifdef STORM_HAVE_CARL
+            } else if (std::is_same<ValueType, storm::RationalFunction>::value && !preparedProgram.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted.");
+#endif
             }
             
             // Now that we have defined all the constants in the program, we need to substitute their appearances in
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index 3db49eb16..a96a5cd66 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -142,7 +142,7 @@ namespace storm {
             commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > +(qi::char_ - qi::lit(";")) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_r1)];
             commandDefinition.name("command definition");
             
-            moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > +commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_2, qi::_r1)];
+            moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > *commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_2, qi::_r1)];
             moduleDefinition.name("module definition");
             
             moduleRenaming = ((qi::lit("module") >> identifier >> qi::lit("=")) > identifier > qi::lit("[")
diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp
index 3b79861d5..630e17a8a 100644
--- a/src/storage/expressions/Expression.cpp
+++ b/src/storage/expressions/Expression.cpp
@@ -100,6 +100,13 @@ namespace storm {
             return result;
 		}
         
+        bool Expression::containsVariable(std::set<storm::expressions::Variable> const& variables) const {
+            std::set<storm::expressions::Variable> appearingVariables = this->getVariables();
+            std::set<storm::expressions::Variable> intersection;
+            std::set_intersection(variables.begin(), variables.end(), appearingVariables.begin(), appearingVariables.end(), std::inserter(intersection, intersection.begin()));
+            return !intersection.empty();
+        }
+        
         bool Expression::isRelationalExpression() const {
             if (!this->isFunctionApplication()) {
                 return false;
diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h
index 205012331..afc04bf56 100644
--- a/src/storage/expressions/Expression.h
+++ b/src/storage/expressions/Expression.h
@@ -213,6 +213,14 @@ namespace storm {
              */
             std::set<storm::expressions::Variable> getVariables() const;
 
+            /*!
+             * Retrieves whether the expression contains any of the given variables.
+             *
+             * @param variables The variables to search for.
+             * @return True iff any of the variables appear in the expression.
+             */
+            bool containsVariable(std::set<storm::expressions::Variable> const& variables) const;
+            
             /*!
              * Retrieves the base expression underlying this expression object. Note that prior to calling this, the
              * expression object must be properly initialized.
diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp
index a476e2fd9..7141ed455 100644
--- a/src/storage/prism/Command.cpp
+++ b/src/storage/prism/Command.cpp
@@ -48,6 +48,21 @@ namespace storm {
             return labeled;
         }
         
+        bool Command::containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const {
+            if (this->getGuardExpression().containsVariable(undefinedConstantVariables)) {
+                return false;
+            }
+            for (auto const& update : this->getUpdates()) {
+                for (auto const& assignment : update.getAssignments()) {
+                    if (assignment.getExpression().containsVariable(undefinedConstantVariables)) {
+                        return false;
+                    }
+                }
+            }
+            
+            return true;
+        }
+        
         std::ostream& operator<<(std::ostream& stream, Command const& command) {
             stream << "[" << command.getActionName() << "] " << command.getGuardExpression() << " -> ";
             for (uint_fast64_t i = 0; i < command.getUpdates().size(); ++i) {
diff --git a/src/storage/prism/Command.h b/src/storage/prism/Command.h
index e0dac47f9..b983a1ca9 100644
--- a/src/storage/prism/Command.h
+++ b/src/storage/prism/Command.h
@@ -99,6 +99,15 @@ namespace storm {
              */
             bool isLabeled() const;
             
+            /*!
+             * Checks whether the given set of variables only appears in the update probabilities of the command.
+             *
+             * @param undefinedConstantVariables The set of variables that may only appear in the update probabilities
+             * of the command.
+             * @return True iff the given set of variables only appears in the update probabilities of the command.
+             */
+            bool containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Command const& command);
             
         private:
diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp
index e6adf07b1..00b3e2828 100644
--- a/src/storage/prism/Module.cpp
+++ b/src/storage/prism/Module.cpp
@@ -170,6 +170,31 @@ namespace storm {
             return Module(this->getName(), newBooleanVariables, newIntegerVariables, newCommands, this->getFilename(), this->getLineNumber());
         }
         
+        bool Module::containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const {
+            for (auto const& booleanVariable : this->getBooleanVariables()) {
+                if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
+                    return false;
+                }
+            }
+            for (auto const& integerVariable : this->getIntegerVariables()) {
+                if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
+                    return false;
+                }
+                if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {
+                    return false;
+                }
+                if (integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) {
+                    return false;
+                }
+            }
+            
+            for (auto const& command : this->getCommands()) {
+                command.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables);
+            }
+            
+            return true;
+        }
+        
         std::ostream& operator<<(std::ostream& stream, Module const& module) {
             stream << "module " << module.getName() << std::endl;
             for (auto const& booleanVariable : module.getBooleanVariables()) {
diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h
index e8686cce5..0dc1f4dde 100644
--- a/src/storage/prism/Module.h
+++ b/src/storage/prism/Module.h
@@ -196,6 +196,14 @@ namespace storm {
              */
             Module substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
             
+            /*!
+             * Checks whether the given variables only appear in the update probabilities of the module and nowhere else.
+             *
+             * @param undefinedConstantVariables A set of variables that may only appear in the update probabilities.
+             * @return True iff the given variables only appear in the update probabilities of the module and nowhere else.
+             */
+            bool containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Module const& module);
 
         private:
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 5b2068a22..fc746ab00 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -11,7 +11,7 @@
 
 namespace storm {
     namespace prism {
-        Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool checkValidity) : LocatedInformation(filename, lineNumber), manager(manager), modelType(modelType), constants(constants), constantToIndexMap(), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), labels(labels), actionToIndexMap(actionToIndexMap), actions(), actionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap() {
+        Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool checkValidity) : LocatedInformation(filename, lineNumber), manager(manager), modelType(modelType), constants(constants), constantToIndexMap(), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), labels(labels), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(), actionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap() {
             this->createMappings();
             
             // Create a new initial construct if the corresponding flag was set.
@@ -53,6 +53,81 @@ namespace storm {
             return false;
         }
         
+        bool Program::hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards() const {
+            if (!this->hasUndefinedConstants()) {
+                return true;
+            }
+            
+            // Gather the variables of all undefined constants.
+            std::set<storm::expressions::Variable> undefinedConstantVariables;
+            for (auto const& constant : this->getConstants()) {
+                if (!constant.isDefined()) {
+                    undefinedConstantVariables.insert(constant.getExpressionVariable());
+                }
+            }
+            
+            // Now it remains to check that the intersection of the variables used in the program with the undefined
+            // constants' variables is empty (except for the update probabilities).
+            
+            // Start by checking the defining expressions of all defined constants.
+            for (auto const& constant : this->getConstants()) {
+                if (constant.isDefined()) {
+                    if (constant.getExpression().containsVariable(undefinedConstantVariables)) {
+                        return false;
+                    }
+                }
+            }
+            
+            // Now check initial value expressions of global variables.
+            for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
+                if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
+                    return false;
+                }
+            }
+            for (auto const& integerVariable : this->getGlobalIntegerVariables()) {
+                if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
+                    return false;
+                }
+                if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {
+                    return false;
+                }
+                if (integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) {
+                    return false;
+                }
+            }
+            
+            // Then check the formulas.
+            for (auto const& formula : this->getFormulas()) {
+                if (formula.getExpression().containsVariable(undefinedConstantVariables)) {
+                    return false;
+                }
+            }
+            
+            // Proceed by checking each of the modules.
+            for (auto const& module : this->getModules()) {
+                module.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables);
+            }
+
+            // Check the reward models.
+            for (auto const& rewardModel : this->getRewardModels()) {
+                rewardModel.containsVariablesOnlyInRewardValueExpressions(undefinedConstantVariables);
+            }
+                     
+            // Initial construct.
+            if (this->getInitialConstruct().getInitialStatesExpression().containsVariable(undefinedConstantVariables)) {
+                return false;
+            }
+            
+            // Labels.
+            for (auto const& label : this->getLabels()) {
+                if (label.getStatePredicateExpression().containsVariable(undefinedConstantVariables)) {
+                    return false;
+                }
+            }
+            
+            return true;
+        }
+        
         std::vector<std::reference_wrapper<storm::prism::Constant const>> Program::getUndefinedConstants() const {
             std::vector<std::reference_wrapper<storm::prism::Constant const>> result;
             for (auto const& constant : this->getConstants()) {
@@ -150,6 +225,12 @@ namespace storm {
             return this->actionIndices;
         }
         
+        std::string const& Program::getActionName(uint_fast64_t actionIndex) const {
+            auto const& indexNamePair = this->indexToActionMap.find(actionIndex);
+            STORM_LOG_THROW(indexNamePair != this->indexToActionMap.end(), storm::exceptions::InvalidArgumentException, "Unknown action index " << actionIndex << ".");
+            return indexNamePair->second;
+        }
+        
         std::set<uint_fast64_t> const& Program::getModuleIndicesByAction(std::string const& action) const {
             auto const& nameIndexPair = this->actionToIndexMap.find(action);
             STORM_LOG_THROW(nameIndexPair != this->actionToIndexMap.end(), storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist.");
@@ -272,6 +353,7 @@ namespace storm {
             for (auto const& actionIndexPair : this->getActionNameToIndexMapping()) {
                 this->actions.insert(actionIndexPair.first);
                 this->actionIndices.insert(actionIndexPair.second);
+                this->indexToActionMap.emplace(actionIndexPair.second, actionIndexPair.first);
             }
             
             // Build the mapping from action names to module indices so that the lookup can later be performed quickly.
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
index 2f6466109..5bb241a24 100644
--- a/src/storage/prism/Program.h
+++ b/src/storage/prism/Program.h
@@ -72,6 +72,15 @@ namespace storm {
              */
             bool hasUndefinedConstants() const;
 
+            /*!
+             * Retrieves whether there are undefined constants appearing in any place other than the update probabilities
+             * of the commands and the reward expressions. This is to be used for parametric model checking where the
+             * parameters are only allowed to govern the probabilities, not the underlying graph of the model.
+             *
+             * @return True iff all undefined constants of the model only appear in update probabilities.
+             */
+            bool hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards() const;
+            
             /*!
              * Retrieves the undefined constants in the program.
              *
@@ -225,6 +234,14 @@ namespace storm {
              */
             std::set<uint_fast64_t> const& getActionIndices() const;
             
+            /*!
+             * Retrieves the action name of the given action index.
+             *
+             * @param actionIndex The index of the action whose name to retrieve.
+             * @return The name of the action.
+             */
+            std::string const& getActionName(uint_fast64_t actionIndex) const;
+            
             /*!
              * Retrieves the indices of all modules within this program that contain commands that are labelled with the
              * given action.
@@ -442,6 +459,9 @@ namespace storm {
             
             // A mapping from action names to their indices.
             std::map<std::string, uint_fast64_t> actionToIndexMap;
+
+            // A mapping from action indices to their names.
+            std::map<uint_fast64_t, std::string> indexToActionMap;
             
             // The set of actions present in this program.
             std::set<std::string> actions;
diff --git a/src/storage/prism/RewardModel.cpp b/src/storage/prism/RewardModel.cpp
index 2c1b49ae7..6e13cb695 100644
--- a/src/storage/prism/RewardModel.cpp
+++ b/src/storage/prism/RewardModel.cpp
@@ -45,6 +45,20 @@ namespace storm {
             return RewardModel(this->getName(), newStateRewards, newTransitionRewards, this->getFilename(), this->getLineNumber());
         }
         
+        bool RewardModel::containsVariablesOnlyInRewardValueExpressions(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const {
+            for (auto const& stateReward : this->getStateRewards()) {
+                if (stateReward.getStatePredicateExpression().containsVariable(undefinedConstantVariables)) {
+                    return false;
+                }
+            }
+            for (auto const& transitionReward : this->getTransitionRewards()) {
+                if (transitionReward.getStatePredicateExpression().containsVariable(undefinedConstantVariables)) {
+                    return false;
+                }
+            }
+            return true;
+        }
+        
         std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel) {
             stream << "rewards";
             if (rewardModel.getName() != "") {
diff --git a/src/storage/prism/RewardModel.h b/src/storage/prism/RewardModel.h
index 2a2b0ab97..f8586b9a9 100644
--- a/src/storage/prism/RewardModel.h
+++ b/src/storage/prism/RewardModel.h
@@ -83,6 +83,15 @@ namespace storm {
              */
             RewardModel substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
             
+            /*!
+             * Checks whether any of the given variables only appear in the expressions defining the reward value.
+             *
+             * @param undefinedConstantVariables A set of variables that may only appear in the expressions defining the
+             * reward values.
+             * @return True iff the given variables only appear in the expressions defining the reward value.
+             */
+            bool containsVariablesOnlyInRewardValueExpressions(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const;
+            
             friend std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel);
 
         private:
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 2d6c48536..6cde40151 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -53,6 +53,9 @@ log4cplus::Logger printer;
 #include "src/builder/ExplicitPrismModelBuilder.h"
 #include "src/builder/DdPrismModelBuilder.h"
 
+// Headers for DD-related classes.
+#include "src/storage/dd/CuddDd.h"
+
 // Headers for model processing.
 #include "src/storage/NaiveDeterministicModelBisimulationDecomposition.h"
 #include "src/storage/DeterministicModelBisimulationDecomposition.h"
diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp
index 34edc67fd..c81e46103 100644
--- a/test/functional/builder/DdPrismModelBuilderTest.cpp
+++ b/test/functional/builder/DdPrismModelBuilderTest.cpp
@@ -34,3 +34,30 @@ TEST(DdPrismModelBuilderTest, Dtmc) {
     EXPECT_EQ(1728, model.first.getNonZeroCount());
     EXPECT_EQ(2505, model.second.getNonZeroCount());
 }
+
+TEST(DdPrismModelBuilderTest, Mdp) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    std::pair<storm::dd::Dd<storm::dd::DdType::CUDD>, storm::dd::Dd<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+    EXPECT_EQ(169, model.first.getNonZeroCount());
+    EXPECT_EQ(436, model.second.getNonZeroCount());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+    EXPECT_EQ(364, model.first.getNonZeroCount());
+    EXPECT_EQ(654, model.second.getNonZeroCount());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+    EXPECT_EQ(272, model.first.getNonZeroCount());
+    EXPECT_EQ(492, model.second.getNonZeroCount());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+    EXPECT_EQ(1038, model.first.getNonZeroCount());
+    EXPECT_EQ(1282, model.second.getNonZeroCount());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
+    model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+    EXPECT_EQ(4093, model.first.getNonZeroCount());
+    EXPECT_EQ(5585, model.second.getNonZeroCount());
+}
\ No newline at end of file
diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
index 4d3126997..b2861f33d 100644
--- a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
+++ b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
@@ -31,3 +31,31 @@ TEST(ExplicitPrismModelBuilderTest, Dtmc) {
     EXPECT_EQ(1728, model->getNumberOfStates());
     EXPECT_EQ(2505, model->getNumberOfTransitions());
 }
+
+TEST(ExplicitPrismModelBuilderTest, Mdp) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    
+    std::unique_ptr<storm::models::AbstractModel<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
+    EXPECT_EQ(169, model->getNumberOfStates());
+    EXPECT_EQ(436, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
+    model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
+    EXPECT_EQ(364, model->getNumberOfStates());
+    EXPECT_EQ(654, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
+    model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
+    EXPECT_EQ(272, model->getNumberOfStates());
+    EXPECT_EQ(492, model->getNumberOfTransitions());
+
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
+    model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
+    EXPECT_EQ(1038, model->getNumberOfStates());
+    EXPECT_EQ(1282, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
+    model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
+    EXPECT_EQ(4093, model->getNumberOfStates());
+    EXPECT_EQ(5585, model->getNumberOfTransitions());
+}
\ No newline at end of file
diff --git a/test/functional/builder/coin2-2.nm b/test/functional/builder/coin2-2.nm
new file mode 100644
index 000000000..17a222972
--- /dev/null
+++ b/test/functional/builder/coin2-2.nm
@@ -0,0 +1,60 @@
+// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] 
+// gxn/dxp 20/11/00
+
+mdp
+
+// constants
+const int N=2;
+const int K=2;
+const int range = 2*(K+1)*N;
+const int counter_init = (K+1)*N;
+const int left = N;
+const int right = 2*(K+1)*N - N;
+
+// shared coin
+global counter : [0..range] init counter_init;
+
+module process1
+	
+	// program counter
+	pc1 : [0..3];
+	// 0 - flip
+	// 1 - write 
+	// 2 - check
+	// 3 - finished
+	
+	// local coin
+	coin1 : [0..1];	
+
+	// flip coin
+	[] (pc1=0)  -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1);
+	// write tails -1  (reset coin to add regularity)
+	[] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0);
+	// write heads +1 (reset coin to add regularity)
+	[] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0);
+	// check
+	// decide tails
+	[] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0);
+	// decide heads
+	[] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1);
+	// flip again
+	[] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0);
+	// loop (all loop together when done)
+	[done] (pc1=3) -> 1 : (pc1'=3);
+
+endmodule
+
+// construct remaining processes through renaming
+module process2 = process1[pc1=pc2,coin1=coin2] endmodule
+
+// labels
+label "finished" = pc1=3 & pc2=3 ;
+label "all_coins_equal_0" = coin1=0 & coin2=0 ;
+label "all_coins_equal_1" = coin1=1 & coin2=1 ;
+label "agree" = coin1=coin2 ;
+
+// rewards
+rewards "steps"
+	true : 1;
+endrewards
+
diff --git a/test/functional/builder/csma2-2.nm b/test/functional/builder/csma2-2.nm
new file mode 100644
index 000000000..18ec5c897
--- /dev/null
+++ b/test/functional/builder/csma2-2.nm
@@ -0,0 +1,130 @@
+// CSMA/CD protocol - probabilistic version of kronos model (3 stations)
+// gxn/dxp 04/12/01
+
+mdp
+
+// note made changes since cannot have strict inequalities
+// in digital clocks approach and suppose a station only sends one message
+
+// simplified parameters scaled
+const int sigma=1; // time for messages to propagate along the bus
+const int lambda=30; // time to send a message
+
+// actual parameters
+const int N = 2; // number of processes
+const int K = 2; // exponential backoff limit
+const int slot = 2*sigma; // length of slot
+// const int M = floor(pow(2, K))-1 ; // max number of slots to wait
+const int M = 3 ; // max number of slots to wait
+//const int lambda=782;
+//const int sigma=26;
+
+// formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1);
+// formula min_collisions = min(cd1,cd2);
+// formula max_collisions = max(cd1,cd2);
+
+//----------------------------------------------------------------------------------------------------------------------------
+// the bus
+module bus
+	
+	b : [0..2];
+	// b=0 - idle
+	// b=1 - active
+	// b=2 - collision
+	
+	// clocks of bus
+	y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy)
+	y2 : [0..sigma+1]; // time since second send (used to find time until collision detected)
+	
+	// a sender sends (ok - no other message being sent)
+	[send1] (b=0) -> (b'=1);
+	[send2] (b=0) -> (b'=1);
+	
+	// a sender sends (bus busy - collision)
+	[send1] (b=1|b=2) & (y1<sigma) -> (b'=2);
+	[send2] (b=1|b=2) & (y1<sigma) -> (b'=2);
+	
+	// finish sending
+	[end1] (b=1) -> (b'=0) & (y1'=0);
+	[end2] (b=1) -> (b'=0) & (y1'=0);
+	
+	// bus busy
+	[busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b);  
+	[busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b);  
+	
+	// collision detected
+	[cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0);
+	
+	// time passage
+	[time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0
+	[time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1
+	[time] (b=2) & (y2<sigma) -> (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected)
+	
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+// model of first sender
+module station1
+	
+	// LOCAL STATE
+	s1 : [0..5];
+	// s1=0 - initial state
+	// s1=1 - transmit
+	// s1=2 - collision (set backoff)
+	// s1=3 - wait (bus busy)
+	// s1=4 - successfully sent
+	
+	// LOCAL CLOCK
+	x1 : [0..max(lambda,slot)];
+	
+	// BACKOFF COUNTER (number of slots to wait)
+	bc1 : [0..M];
+	
+	// COLLISION COUNTER
+	cd1 : [0..K];
+	
+	// start sending
+	[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending
+	[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff
+	
+	// transmitting
+	[time] (s1=1) & (x1<lambda) -> (x1'=min(x1+1,lambda)); // let time pass
+	[end1]  (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished
+	[cd]   (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter)
+	[cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important
+	
+	// set backoff (no time can pass in this state)
+	// probability depends on which transmission this is (cd1)
+	[] s1=2 & cd1=1 ->  1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ;
+	[] s1=2 & cd1=2 ->  1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ;
+	
+	// wait until backoff counter reaches 0 then send again
+	[time] (s1=3) & (x1<slot) -> (x1'=x1+1); // let time pass (in slot)
+	[time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots)
+	[send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free)
+	[busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy)
+	
+	// once finished nothing matters
+	[time] (s1>=4) -> (x1'=0);
+
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// construct further stations through renaming
+module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// reward structure for expected time
+rewards "time"
+	[time] true : 1;
+endrewards
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// labels/formulae
+label "all_delivered" = s1=4&s2=4;
+label "one_delivered" = s1=4|s2=4;
+label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2);
+
diff --git a/test/functional/builder/firewire3-0.5.nm b/test/functional/builder/firewire3-0.5.nm
new file mode 100644
index 000000000..a941e623b
--- /dev/null
+++ b/test/functional/builder/firewire3-0.5.nm
@@ -0,0 +1,170 @@
+// firewire protocol with integer semantics
+// dxp/gxn 14/06/01
+
+// CLOCKS
+// x1 (x2) clock for node1 (node2)
+// y1 and y2 (z1 and z2) clocks for wire12 (wire21)
+mdp
+
+// maximum and minimum delays
+// fast
+const int rc_fast_max = 85;
+const int rc_fast_min = 76;
+// slow
+const int rc_slow_max = 167;
+const int rc_slow_min = 159;
+// delay caused by the wire length
+const int delay = 3;
+// probability of choosing fast
+const double fast = 0.5;
+const double slow=1-fast;
+
+module wire12
+	
+	// local state
+	w12 : [0..9];
+	// 0 - empty
+	// 1 -	rec_req
+	// 2 -  rec_req_ack
+	// 3 -	rec_ack
+	// 4 -	rec_ack_idle
+	// 5 -	rec_idle
+	// 6 -	rec_idle_req
+	// 7 -	rec_ack_req
+	// 8 -	rec_req_idle
+	// 9 -	rec_idle_ack
+	
+	// clock for wire12
+	y1 : [0..delay+1];
+	y2 : [0..delay+1];
+
+	// empty
+	// do not need y1 and y2 to increase as always reset when this state is left
+	// similarly can reset y1 and y2 when we re-enter this state
+	[snd_req12]  w12=0 -> (w12'=1) & (y1'=0) & (y2'=0);
+	[snd_ack12]  w12=0 -> (w12'=3) & (y1'=0) & (y2'=0);
+	[snd_idle12] w12=0 -> (w12'=5) & (y1'=0) & (y2'=0);
+	[time]       w12=0 -> (w12'=w12);	
+	// rec_req
+	[snd_req12]  w12=1 -> (w12'=1);
+	[rec_req12]  w12=1 -> (w12'=0) & (y1'=0) & (y2'=0);
+	[snd_ack12]  w12=1 -> (w12'=2) & (y2'=0);
+	[snd_idle12] w12=1 -> (w12'=8) & (y2'=0);
+	[time]       w12=1 & y2<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_req_ack
+	[snd_ack12] w12=2 -> (w12'=2);
+	[rec_req12] w12=2 -> (w12'=3);
+	[time]      w12=2 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_ack
+	[snd_ack12]  w12=3 -> (w12'=3);
+	[rec_ack12]  w12=3 -> (w12'=0) & (y1'=0) & (y2'=0);
+	[snd_idle12] w12=3 -> (w12'=4) & (y2'=0);
+	[snd_req12]  w12=3 -> (w12'=7) & (y2'=0);
+	[time]       w12=3 & y2<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_ack_idle
+	[snd_idle12] w12=4 -> (w12'=4);
+	[rec_ack12]  w12=4 -> (w12'=5);
+	[time]       w12=4 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_idle
+	[snd_idle12] w12=5 -> (w12'=5);
+	[rec_idle12] w12=5 -> (w12'=0) & (y1'=0) & (y2'=0);
+	[snd_req12]  w12=5 -> (w12'=6) & (y2'=0);
+	[snd_ack12]  w12=5 -> (w12'=9) & (y2'=0);
+	[time]       w12=5 & y2<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_idle_req
+	[snd_req12]  w12=6 -> (w12'=6);
+	[rec_idle12] w12=6 -> (w12'=1);
+	[time]       w12=6 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_ack_req
+	[snd_req12] w12=7 -> (w12'=7);
+	[rec_ack12] w12=7 -> (w12'=1);
+	[time]      w12=7 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_req_idle
+	[snd_idle12] w12=8 -> (w12'=8);
+	[rec_req12]  w12=8 -> (w12'=5);
+	[time]       w12=8 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	// rec_idle_ack
+	[snd_ack12]  w12=9 -> (w12'=9);
+	[rec_idle12] w12=9 -> (w12'=3);
+	[time]       w12=9 & y1<delay ->  (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
+	
+endmodule
+
+module node1
+	
+	// clock for node1
+	x1 : [0..168];
+	
+	// local state
+	s1 : [0..8];
+	// 0 - root contention
+	// 1 - rec_idle
+	// 2 - rec_req_fast
+	// 3 - rec_req_slow
+	// 4 - rec_idle_fast
+	// 5 - rec_idle_slow
+	// 6 - snd_req
+	// 7- almost_root
+	// 8 - almost_child
+	
+	// added resets to x1 when not considered again until after rest
+	// removed root and child (using almost root and almost child)
+	
+	// root contention immediate state)
+	[snd_idle12] s1=0 -> fast : (s1'=2) & (x1'=0) +  slow : (s1'=3) & (x1'=0);
+	[rec_idle21] s1=0 -> (s1'=1);
+	// rec_idle immediate state)
+	[snd_idle12] s1=1 -> fast : (s1'=4) & (x1'=0) +  slow : (s1'=5) & (x1'=0);
+	[rec_req21]  s1=1 -> (s1'=0);
+	// rec_req_fast
+	[rec_idle21] s1=2 -> (s1'=4);	
+	[snd_ack12]  s1=2 & x1>=rc_fast_min -> (s1'=7) & (x1'=0);
+	[time]       s1=2 & x1<rc_fast_max -> (x1'=min(x1+1,168));
+	// rec_req_slow
+	[rec_idle21] s1=3 -> (s1'=5);
+	[snd_ack12]  s1=3 & x1>=rc_slow_min -> (s1'=7) & (x1'=0);
+	[time]       s1=3 & x1<rc_slow_max -> (x1'=min(x1+1,168));
+	// rec_idle_fast
+	[rec_req21] s1=4 -> (s1'=2);
+	[snd_req12] s1=4 & x1>=rc_fast_min -> (s1'=6) & (x1'=0);
+	[time]      s1=4 & x1<rc_fast_max -> (x1'=min(x1+1,168));
+	// rec_idle_slow
+	[rec_req21] s1=5 -> (s1'=3);
+	[snd_req12] s1=5 & x1>=rc_slow_min -> (s1'=6) & (x1'=0);
+	[time]      s1=5 & x1<rc_slow_max -> (x1'=min(x1+1,168));
+	// snd_req 
+	// do not use x1 until reset (in state 0 or in state 1) so do not need to increase x1
+	// also can set x1 to 0 upon entering this state
+	[rec_req21] s1=6 -> (s1'=0);
+	[rec_ack21] s1=6 -> (s1'=8);
+	[time]      s1=6 -> (s1'=s1);
+	// almost root (immediate) 
+	// loop in final states to remove deadlock
+	[] s1=7 & s2=8 -> (s1'=s1);
+	[] s1=8 & s2=7 -> (s1'=s1);
+	[time] s1=7 -> (s1'=s1);
+	[time] s1=8 -> (s1'=s1);
+	
+endmodule
+
+// construct remaining automata through renaming
+module wire21=wire12[w12=w21, y1=z1, y2=z2, 
+	snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21,
+	rec_req12=rec_req21, rec_idle12=rec_idle21, rec_ack12=rec_ack21]
+endmodule
+module node2=node1[s1=s2, s2=s1, x1=x2, 
+	rec_req21=rec_req12, rec_idle21=rec_idle12, rec_ack21=rec_ack12,
+	snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21]
+endmodule
+
+// reward structures
+// time
+rewards "time"	
+	[time] true : 1;
+endrewards
+// time nodes sending
+rewards "time_sending"
+	[time] (w12>0 | w21>0) : 1;
+endrewards
+
+label "elected" = ((s1=8) & (s2=7)) | ((s1=7) & (s2=8));
diff --git a/test/functional/builder/leader3.nm b/test/functional/builder/leader3.nm
new file mode 100644
index 000000000..96339dd96
--- /dev/null
+++ b/test/functional/builder/leader3.nm
@@ -0,0 +1,91 @@
+// asynchronous leader election
+// 4 processes
+// gxn/dxp 29/01/01
+
+mdp
+
+const int N = 3; // number of processes
+
+//----------------------------------------------------------------------------------------------------------------------------
+module process1
+	
+	// COUNTER
+	c1 : [0..3-1];
+	
+	// STATES
+	s1 : [0..4];
+	// 0  make choice
+	// 1 have not received neighbours choice
+	// 2 active
+	// 3 inactive
+	// 4 leader
+	
+	// PREFERENCE
+	p1 : [0..1];
+	
+	// VARIABLES FOR SENDING AND RECEIVING
+	receive1 : [0..2];
+	// not received anything
+	// received choice
+	// received counter
+	sent1 : [0..2];
+	// not send anything
+	// sent choice
+	// sent counter
+	
+	// pick value
+	[] (s1=0) -> 0.5 : (s1'=1) & (p1'=0) + 0.5 : (s1'=1) & (p1'=1);
+
+	// send preference
+	[p12] (s1=1) & (sent1=0) -> (sent1'=1);
+	// receive preference
+	// stay active
+	[p31] (s1=1) & (receive1=0) & !( (p1=0) & (p3=1) ) -> (s1'=2) & (receive1'=1);
+	// become inactive
+	[p31] (s1=1) & (receive1=0) & (p1=0) & (p3=1) -> (s1'=3) & (receive1'=1);
+	
+	// send preference (can now reset preference)
+	[p12] (s1=2) & (sent1=0) -> (sent1'=1) & (p1'=0);
+	// send counter (already sent preference)
+	// not received counter yet
+	[c12] (s1=2) & (sent1=1) & (receive1=1) -> (sent1'=2);
+	// received counter (pick again)
+	[c12] (s1=2) & (sent1=1) & (receive1=2) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
+	
+	// receive counter and not sent yet (note in this case do not pass it on as will send own counter)
+	[c31] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2);
+	// receive counter and sent counter
+	// only active process (decide)
+	[c31] (s1=2) & (receive1=1) & (sent1=2) & (c3=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
+	// other active process (pick again)
+	[c31] (s1=2) & (receive1=1) & (sent1=2) & (c3<N-1) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
+	
+	// send preference (must have received preference) and can now reset
+	[p12] (s1=3) & (receive1>0) & (sent1=0) -> (sent1'=1) & (p1'=0);
+	// send counter (must have received counter first) and can now reset
+	[c12] (s1=3) & (receive1=2) & (sent1=1) ->  (s1'=3) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
+	
+	// receive preference
+	[p31] (s1=3) & (receive1=0) -> (p1'=p3) & (receive1'=1);
+	// receive counter
+	[c31] (s1=3) & (receive1=1) & (c3<N-1) -> (c1'=c3+1) & (receive1'=2);
+		
+	// done
+	[done] (s1=4) -> (s1'=s1);
+	// add loop for processes who are inactive
+	[done] (s1=3) -> (s1'=s1);
+
+endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// construct further stations through renaming
+module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p31=p12,c12=c23,c31=c12,p3=p1,c3=c1] endmodule
+module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p31,p31=p23,c12=c31,c31=c23,p3=p2,c3=c2] endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+//----------------------------------------------------------------------------------------------------------------------------
+formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0);
+label "elected" = s1=4|s2=4|s3=4;
+
diff --git a/test/functional/builder/two_dice.nm b/test/functional/builder/two_dice.nm
new file mode 100644
index 000000000..778153138
--- /dev/null
+++ b/test/functional/builder/two_dice.nm
@@ -0,0 +1,40 @@
+// sum of two dice as the asynchronous parallel composition of
+// two copies of Knuth's model of a fair die using only fair coins
+
+mdp
+
+module die1
+
+	// local state
+	s1 : [0..7] init 0;
+	// value of the dice
+	d1 : [0..6] init 0;
+
+	[] s1=0 -> 0.5 : (s1'=1) + 0.5 : (s1'=2);
+	[] s1=1 -> 0.5 : (s1'=3) + 0.5 : (s1'=4);
+	[] s1=2 -> 0.5 : (s1'=5) + 0.5 : (s1'=6);
+	[] s1=3 -> 0.5 : (s1'=1) + 0.5 : (s1'=7) & (d1'=1);
+	[] s1=4 -> 0.5 : (s1'=7) & (d1'=2) + 0.5 : (s1'=7) & (d1'=3);
+	[] s1=5 -> 0.5 : (s1'=7) & (d1'=4) + 0.5 : (s1'=7) & (d1'=5);
+	[] s1=6 -> 0.5 : (s1'=2) + 0.5 : (s1'=7) & (d1'=6);
+	[] s1=7 & s2=7 -> 1: (s1'=7);
+endmodule
+
+module die2 = die1 [ s1=s2, s2=s1, d1=d2 ] endmodule
+
+rewards "coinflips"
+	[] s1<7 | s2<7 : 1;
+endrewards
+
+label "done" = s1=7 & s2=7;
+label "two" = s1=7 & s2=7 & d1+d2=2;
+label "three" = s1=7 & s2=7 & d1+d2=3;
+label "four" = s1=7 & s2=7 & d1+d2=4;
+label "five" = s1=7 & s2=7 & d1+d2=5;
+label "six" = s1=7 & s2=7 & d1+d2=6;
+label "seven" = s1=7 & s2=7 & d1+d2=7;
+label "eight" = s1=7 & s2=7 & d1+d2=8;
+label "nine" = s1=7 & s2=7 & d1+d2=9;
+label "ten" = s1=7 & s2=7 & d1+d2=10;
+label "eleven" = s1=7 & s2=7 & d1+d2=11;
+label "twelve" = s1=7 & s2=7 & d1+d2=12;
diff --git a/wlan0_collide.nm b/wlan0_collide.nm
new file mode 100644
index 000000000..5d94e23de
--- /dev/null
+++ b/wlan0_collide.nm
@@ -0,0 +1,13 @@
+mdp
+
+module station1
+    s1 : [0..12] init 0;
+
+//	[] s1=0 -> (s1'=8) ;
+
+	[] s1=1 -> (s1'=1);
+	[] s1=1 -> (s1'=1);
+	
+//[] s1=8 -> (s1'=8);
+
+endmodule