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