From 3977cafe73eaa8cfe59a45822d1f6d9ef85fb991 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 18 Feb 2015 22:11:00 +0100
Subject: [PATCH] Extended DD-based model building to also build the MDP models
of our benchmark suite. Added (MDP) tests for DD-based model building and
explicit model building.
Former-commit-id: 4e18f98ee6921d4bb6a82b1c78017970e8e4f270
---
src/builder/DdPrismModelBuilder.cpp | 90 +++----
.../builder/DdPrismModelBuilderTest.cpp | 5 +
.../builder/ExplicitPrismModelBuilderTest.cpp | 5 +
test/functional/builder/brp-16-2.pm | 136 +++++++++++
test/functional/builder/crowds-5-5.pm | 69 ++++++
test/functional/builder/die.pm | 31 +++
test/functional/builder/leader-3-5.pm | 85 +++++++
test/functional/builder/nand-5-2.pm | 76 ++++++
test/functional/builder/wlan0-2-2.nm | 219 ++++++++++++++++++
wlan0_collide.nm | 13 --
10 files changed, 652 insertions(+), 77 deletions(-)
create mode 100644 test/functional/builder/brp-16-2.pm
create mode 100644 test/functional/builder/crowds-5-5.pm
create mode 100644 test/functional/builder/die.pm
create mode 100644 test/functional/builder/leader-3-5.pm
create mode 100644 test/functional/builder/nand-5-2.pm
create mode 100644 test/functional/builder/wlan0-2-2.nm
delete mode 100644 wlan0_collide.nm
diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 43f051eb5..ef165a877 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -142,7 +142,6 @@ namespace storm {
commandDd += updateDd;
}
- (guardDd * commandDd).exportToDot(module.getName() + "_" + command.getActionName() + ".dot");
return ActionDecisionDiagram(guardDd, guardDd * commandDd);
} else {
return ActionDecisionDiagram(*generationInfo.manager);
@@ -161,22 +160,10 @@ namespace storm {
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()){
@@ -214,14 +201,15 @@ namespace storm {
template <storm::dd::DdType Type>
storm::dd::Dd<Type> DdPrismModelBuilder<Type>::encodeChoice(GenerationInformation& generationInfo, uint_fast64_t nondeterminismVariableOffset, uint_fast64_t numberOfBinaryVariables, int_fast64_t value) {
- storm::dd::Dd<Type> result = generationInfo.manager->getOne();
+ storm::dd::Dd<Type> result = generationInfo.manager->getZero();
+
+ STORM_LOG_TRACE("Encoding " << value << " with " << numberOfBinaryVariables << " binary variable(s) starting from offset " << nondeterminismVariableOffset << ".");
std::map<storm::expressions::Variable, int_fast64_t> metaVariableNameToValueMap;
for (uint_fast64_t i = nondeterminismVariableOffset; i < nondeterminismVariableOffset + numberOfBinaryVariables; ++i) {
if (value & (1ull << (numberOfBinaryVariables - i - 1))) {
metaVariableNameToValueMap.emplace(generationInfo.nondeterminismMetaVariables[i], 1);
- }
- else {
+ } else {
metaVariableNameToValueMap.emplace(generationInfo.nondeterminismMetaVariables[i], 0);
}
}
@@ -243,6 +231,8 @@ namespace storm {
}
uint_fast64_t maxChoices = static_cast<uint_fast64_t>(sumOfGuards.getMax());
+ STORM_LOG_TRACE("Found " << maxChoices << " local choices.");
+
// Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism.
if (maxChoices == 0) {
return ActionDecisionDiagram(*generationInfo.manager);
@@ -291,7 +281,7 @@ namespace storm {
// Calculate the overlapping part of command guard and the remaining DD.
storm::dd::Dd<Type> remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k];
- // Check if we can add some overlapping parts to the current index
+ // Check if we can add some overlapping parts to the current index.
if (!remainingGuardChoicesIntersection.isZero()) {
// Remove overlapping parts from the remaining DD.
remainingDds[k] = remainingDds[k] && !remainingGuardChoicesIntersection;
@@ -333,9 +323,6 @@ 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) {
@@ -347,7 +334,6 @@ 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();
@@ -364,9 +350,6 @@ namespace storm {
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).ite(action2Extended, action1Extended);
@@ -403,12 +386,10 @@ namespace storm {
// 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;
// Add variables to independent action DD.
storm::dd::Dd<Type> nondeterminismEncoding = generationInfo.manager->getOne();
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;
@@ -446,7 +427,6 @@ namespace storm {
// Now, we can simply add all synchronizing actions to the result.
for (auto const& synchronizingAction : synchronizingActionToDdMap) {
- synchronizingAction.second.exportToDot("synch" + std::to_string(synchronizingAction.first) + ".dot");
result += synchronizingAction.second;
}
@@ -516,7 +496,6 @@ namespace storm {
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);
}
@@ -528,9 +507,7 @@ namespace storm {
} 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);
@@ -566,7 +543,7 @@ namespace storm {
}
preparedProgram = preparedProgram.substituteConstants();
- std::cout << "translated prog: " << preparedProgram << std::endl;
+// 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.
@@ -575,51 +552,38 @@ 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 = 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()) {
-// 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;
+ 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.");
+
+ 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;
+ }
+ } 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.");
+ }
}
std::cout << reachableStates.getNonZeroCount() << " states and " << transitionMatrix.getNonZeroCount() << " transitions." << std::endl;
@@ -647,8 +611,6 @@ namespace storm {
transitionBdd = transitionBdd.existsAbstract(generationInfo.allNondeterminismVariables);
}
- transitionBdd.exportToDot("trans01.dot");
-
// Perform the BFS to discover all reachable states.
bool changed = true;
uint_fast64_t iteration = 0;
diff --git a/test/functional/builder/DdPrismModelBuilderTest.cpp b/test/functional/builder/DdPrismModelBuilderTest.cpp
index c81e46103..67ae4d1ac 100644
--- a/test/functional/builder/DdPrismModelBuilderTest.cpp
+++ b/test/functional/builder/DdPrismModelBuilderTest.cpp
@@ -60,4 +60,9 @@ TEST(DdPrismModelBuilderTest, Mdp) {
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
EXPECT_EQ(4093, model.first.getNonZeroCount());
EXPECT_EQ(5585, model.second.getNonZeroCount());
+
+ program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
+ model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ EXPECT_EQ(37, model.first.getNonZeroCount());
+ EXPECT_EQ(59, model.second.getNonZeroCount());
}
\ No newline at end of file
diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
index b2861f33d..88996a549 100644
--- a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
+++ b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp
@@ -58,4 +58,9 @@ TEST(ExplicitPrismModelBuilderTest, Mdp) {
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
EXPECT_EQ(4093, model->getNumberOfStates());
EXPECT_EQ(5585, model->getNumberOfTransitions());
+
+ program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
+ model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
+ EXPECT_EQ(37, model->getNumberOfStates());
+ EXPECT_EQ(59, model->getNumberOfTransitions());
}
\ No newline at end of file
diff --git a/test/functional/builder/brp-16-2.pm b/test/functional/builder/brp-16-2.pm
new file mode 100644
index 000000000..e3c30cb98
--- /dev/null
+++ b/test/functional/builder/brp-16-2.pm
@@ -0,0 +1,136 @@
+// bounded retransmission protocol [D'AJJL01]
+// gxn/dxp 23/05/2001
+
+dtmc
+
+// number of chunks
+const int N = 16;
+// maximum number of retransmissions
+const int MAX = 2;
+
+module sender
+
+ s : [0..6];
+ // 0 idle
+ // 1 next_frame
+ // 2 wait_ack
+ // 3 retransmit
+ // 4 success
+ // 5 error
+ // 6 wait sync
+ srep : [0..3];
+ // 0 bottom
+ // 1 not ok (nok)
+ // 2 do not know (dk)
+ // 3 ok (ok)
+ nrtr : [0..MAX];
+ i : [0..N];
+ bs : bool;
+ s_ab : bool;
+ fs : bool;
+ ls : bool;
+
+ // idle
+ [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
+ // next_frame
+ [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0);
+ // wait_ack
+ [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
+ [TO_Msg] (s=2) -> (s'=3);
+ [TO_Ack] (s=2) -> (s'=3);
+ // retransmit
+ [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
+ [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
+ [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
+ // success
+ [] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
+ [] (s=4) & (i=N) -> (s'=0) & (srep'=3);
+ // error
+ [SyncWait] (s=5) -> (s'=6);
+ // wait sync
+ [SyncWait] (s=6) -> (s'=0) & (s_ab'=false);
+
+endmodule
+
+module receiver
+
+ r : [0..5];
+ // 0 new_file
+ // 1 fst_safe
+ // 2 frame_received
+ // 3 frame_reported
+ // 4 idle
+ // 5 resync
+ rrep : [0..4];
+ // 0 bottom
+ // 1 fst
+ // 2 inc
+ // 3 ok
+ // 4 nok
+ fr : bool;
+ lr : bool;
+ br : bool;
+ r_ab : bool;
+ recv : bool;
+
+
+ // new_file
+ [SyncWait] (r=0) -> (r'=0);
+ [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
+ // fst_safe_frame
+ [] (r=1) -> (r'=2) & (r_ab'=br);
+ // frame_received
+ [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1);
+ [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
+ [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3);
+ [aA] (r=2) & !(r_ab=br) -> (r'=4);
+ // frame_reported
+ [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
+ // idle
+ [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
+ [SyncWait] (r=4) & (ls=true) -> (r'=5);
+ [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
+ // resync
+ [SyncWait] (r=5) -> (r'=0) & (rrep'=0);
+
+endmodule
+
+module checker // prevents more than one frame being set
+
+ T : bool;
+
+ [NewFile] (T=false) -> (T'=true);
+
+endmodule
+
+module channelK
+
+ k : [0..2];
+
+ // idle
+ [aF] (k=0) -> 0.98 : (k'=1) + 0.02 : (k'=2);
+ // sending
+ [aG] (k=1) -> (k'=0);
+ // lost
+ [TO_Msg] (k=2) -> (k'=0);
+
+endmodule
+
+module channelL
+
+ l : [0..2];
+
+ // idle
+ [aA] (l=0) -> 0.99 : (l'=1) + 0.01 : (l'=2);
+ // sending
+ [aB] (l=1) -> (l'=0);
+ // lost
+ [TO_Ack] (l=2) -> (l'=0);
+
+endmodule
+
+rewards
+ [aF] i=1 : 1;
+endrewards
+
+label "target" = s=5;
diff --git a/test/functional/builder/crowds-5-5.pm b/test/functional/builder/crowds-5-5.pm
new file mode 100644
index 000000000..60bdaa7ea
--- /dev/null
+++ b/test/functional/builder/crowds-5-5.pm
@@ -0,0 +1,69 @@
+dtmc
+
+// probability of forwarding
+const double PF = 0.8;
+const double notPF = .2; // must be 1-PF
+// probability that a crowd member is bad
+const double badC = .167;
+ // probability that a crowd member is good
+const double goodC = 0.833;
+// Total number of protocol runs to analyze
+const int TotalRuns = 5;
+// size of the crowd
+const int CrowdSize = 5;
+
+module crowds
+ // protocol phase
+ phase: [0..4] init 0;
+
+ // crowd member good (or bad)
+ good: bool init false;
+
+ // number of protocol runs
+ runCount: [0..TotalRuns] init 0;
+
+ // observe_i is the number of times the attacker observed crowd member i
+ observe0: [0..TotalRuns] init 0;
+
+ observe1: [0..TotalRuns] init 0;
+
+ observe2: [0..TotalRuns] init 0;
+
+ observe3: [0..TotalRuns] init 0;
+
+ observe4: [0..TotalRuns] init 0;
+
+ // the last seen crowd member
+ lastSeen: [0..CrowdSize - 1] init 0;
+
+ // get the protocol started
+ [] phase=0 & runCount<TotalRuns -> 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0);
+
+ // decide whether crowd member is good or bad according to given probabilities
+ [] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false);
+
+ // if the current member is a good member, update the last seen index (chosen uniformly)
+ [] phase=2 & good -> 1/5 : (lastSeen'=0) & (phase'=3) + 1/5 : (lastSeen'=1) & (phase'=3) + 1/5 : (lastSeen'=2) & (phase'=3) + 1/5 : (lastSeen'=3) & (phase'=3) + 1/5 : (lastSeen'=4) & (phase'=3);
+
+ // if the current member is a bad member, record the most recently seen index
+ [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4);
+ [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4);
+ [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4);
+ [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4);
+ [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4);
+
+ // good crowd members forward with probability PF and deliver otherwise
+ [] phase=3 -> PF : (phase'=1) + notPF : (phase'=4);
+
+ // deliver the message and start over
+ [] phase=4 -> 1: (phase'=0);
+
+endmodule
+
+label "observe0Greater1" = observe0>1;
+label "observe1Greater1" = observe1>1;
+label "observe2Greater1" = observe2>1;
+label "observe3Greater1" = observe3>1;
+label "observe4Greater1" = observe4>1;
+label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1;
+label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1 & observe3<=1 & observe4<=1;
diff --git a/test/functional/builder/die.pm b/test/functional/builder/die.pm
new file mode 100644
index 000000000..dacde8a79
--- /dev/null
+++ b/test/functional/builder/die.pm
@@ -0,0 +1,31 @@
+// Knuth's model of a fair die using only fair coins
+dtmc
+
+module die
+
+ // local state
+ s : [0..7] init 0;
+ // value of the dice
+ d : [0..6] init 0;
+
+ [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
+ [] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
+ [] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
+ [] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
+ [] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
+ [] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
+ [] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
+ [] s=7 -> 1: (s'=7);
+
+endmodule
+
+rewards "coin_flips"
+ [] s<7 : 1;
+endrewards
+
+label "one" = s=7&d=1;
+label "two" = s=7&d=2;
+label "three" = s=7&d=3;
+label "four" = s=7&d=4;
+label "five" = s=7&d=5;
+label "six" = s=7&d=6;
diff --git a/test/functional/builder/leader-3-5.pm b/test/functional/builder/leader-3-5.pm
new file mode 100644
index 000000000..0703e733d
--- /dev/null
+++ b/test/functional/builder/leader-3-5.pm
@@ -0,0 +1,85 @@
+// synchronous leader election protocol (itai & Rodeh)
+// dxp/gxn 25/01/01
+
+dtmc
+
+// CONSTANTS
+const int N = 3; // number of processes
+const int K = 5; // range of probabilistic choice
+
+// counter module used to count the number of processes that have been read
+// and to know when a process has decided
+module counter
+
+ // counter (c=i means process j reading process (i-1)+j next)
+ c : [1..N-1];
+
+ // reading
+ [read] c<N-1 -> 1:(c'=c+1);
+ // finished reading
+ [read] c=N-1 -> 1:(c'=c);
+ //decide
+ [done] u1|u2|u3 -> 1:(c'=c);
+ // pick again reset counter
+ [retry] !(u1|u2|u3) -> 1:(c'=1);
+ // loop (when finished to avoid deadlocks)
+ [loop] s1=3 -> 1:(c'=c);
+
+endmodule
+
+// processes form a ring and suppose:
+// process 1 reads process 2
+// process 2 reads process 3
+// process 3 reads process 1
+module process1
+
+ // local state
+ s1 : [0..3];
+ // s1=0 make random choice
+ // s1=1 reading
+ // s1=2 deciding
+ // s1=3 finished
+
+ // has a unique id so far (initially true)
+ u1 : bool;
+
+ // value to be sent to next process in the ring (initially sets this to its own value)
+ v1 : [0..K-1];
+
+ // random choice
+ p1 : [0..K-1];
+
+ // pick value
+ [pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true)
+ + 1/K : (s1'=1) & (p1'=1) & (v1'=1) & (u1'=true)
+ + 1/K : (s1'=1) & (p1'=2) & (v1'=2) & (u1'=true)
+ + 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true)
+ + 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true);
+ // read
+ [read] s1=1 & u1 & c<N-1 -> 1:(u1'=(p1!=v2)) & (v1'=v2);
+ [read] s1=1 & !u1 & c<N-1 -> 1:(u1'=false) & (v1'=v2) & (p1'=0);
+ // read and move to decide
+ [read] s1=1 & u1 & c=N-1 -> 1:(s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0);
+ [read] s1=1 & !u1 & c=N-1 -> 1:(s1'=2) & (u1'=false) & (v1'=0);
+ // deciding
+ // done
+ [done] s1=2 -> 1:(s1'=3) & (u1'=false) & (v1'=0) & (p1'=0);
+ //retry
+ [retry] s1=2 -> 1:(s1'=0) & (u1'=false) & (v1'=0) & (p1'=0);
+ // loop (when finished to avoid deadlocks)
+ [loop] s1=3 -> 1:(s1'=3);
+
+endmodule
+
+// construct remaining processes through renaming
+module process2 = process1 [ s1=s2,p1=p2,v1=v2,u1=u2,v2=v3 ] endmodule
+module process3 = process1 [ s1=s3,p1=p3,v1=v3,u1=u3,v2=v1 ] endmodule
+
+// expected number of rounds
+rewards "num_rounds"
+ [pick] true : 1;
+endrewards
+
+// labels
+label "elected" = s1=3&s2=3&s3=3;
+
diff --git a/test/functional/builder/nand-5-2.pm b/test/functional/builder/nand-5-2.pm
new file mode 100644
index 000000000..e3f2f4dee
--- /dev/null
+++ b/test/functional/builder/nand-5-2.pm
@@ -0,0 +1,76 @@
+// nand multiplex system
+// gxn/dxp 20/03/03
+
+// U (correctly) performs a random permutation of the outputs of the previous stage
+
+dtmc
+
+const int N = 5; // number of inputs in each bundle
+const int K = 2; // number of restorative stages
+
+const int M = 2*K+1; // total number of multiplexing units
+
+// parameters taken from the following paper
+// A system architecture solution for unreliable nanoelectric devices
+// J. Han & P. Jonker
+// IEEEE trans. on nanotechnology vol 1(4) 2002
+
+const double perr = 0.02; // probability nand works correctly
+const double prob1 = 0.9; // probability initial inputs are stimulated
+
+// model whole system as a single module by resuing variables
+// to decrease the state space
+module multiplex
+
+ u : [1..M]; // number of stages
+ c : [0..N]; // counter (number of copies of the nand done)
+
+ s : [0..4]; // local state
+ // 0 - initial state
+ // 1 - set x inputs
+ // 2 - set y inputs
+ // 3 - set outputs
+ // 4 - done
+
+ z : [0..N]; // number of new outputs equal to 1
+ zx : [0..N]; // number of old outputs equal to 1
+ zy : [0..N]; // need second copy for y
+ // initially 9 since initially probability of stimulated state is 0.9
+
+ x : [0..1]; // value of first input
+ y : [0..1]; // value of second input
+
+ [] s=0 & (c<N) -> (s'=1); // do next nand if have not done N yet
+ [] s=0 & (c=N) & (u<M) -> (s'=1) & (zx'=z) & (zy'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished
+ [] s=0 & (c=N) & (u=M) -> (s'=4) & (zx'=0) & (zy'=0) & (x'=0) & (y'=0); // finished (so reset variables not needed to reduce state space)
+
+ // choose x permute selection (have zx stimulated inputs)
+ // note only need y to be random
+ [] s=1 & u=1 -> prob1 : (x'=1) & (s'=2) + (1-prob1) : (x'=0) & (s'=2); // initially random
+ [] s=1 & u>1 & zx>0 -> (x'=1) & (s'=2) & (zx'=zx-1);
+ [] s=1 & u>1 & zx=0 -> (x'=0) & (s'=2);
+
+ // choose x randomly from selection (have zy stimulated inputs)
+ [] s=2 & u=1 -> prob1 : (y'=1) & (s'=3) + (1-prob1) : (y'=0) & (s'=3); // initially random
+ [] s=2 & u>1 & zy<(N-c) & zy>0 -> zy/(N-c) : (y'=1) & (s'=3) & (zy'=zy-1) + 1-(zy/(N-c)) : (y'=0) & (s'=3);
+ [] s=2 & u>1 & zy=(N-c) & c<N -> 1 : (y'=1) & (s'=3) & (zy'=zy-1);
+ [] s=2 & u>1 & zy=0 -> 1 : (y'=0) & (s'=3);
+
+ // use nand gate
+ [] s=3 & z<N & c<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
+ + perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
+ // [] s=3 & z<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
+ // + perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
+
+ [] s=4 -> (s'=s);
+
+endmodule
+
+// rewards: final value of gate
+rewards
+ // [] s=0 & (c=N) & (u=M) : z/N;
+ s=0 & (c=N) & (u=M) : z/N;
+endrewards
+
+label "target" = s=4 & z/N<0.1;
+label "end" = s=4;
diff --git a/test/functional/builder/wlan0-2-2.nm b/test/functional/builder/wlan0-2-2.nm
new file mode 100644
index 000000000..a8ae9df7e
--- /dev/null
+++ b/test/functional/builder/wlan0-2-2.nm
@@ -0,0 +1,219 @@
+// WLAN PROTOCOL (two stations)
+// discrete time model
+// gxn/jzs 20/02/02
+
+mdp
+
+// COLLISIONS
+const int COL = 2; // maximum number of collisions
+
+// TIMING CONSTRAINTS
+// we have used the FHSS parameters
+// then scaled by the value of ASLOTTIME
+const int ASLOTTIME = 1;
+const int DIFS = 3; // due to scaling can be either 2 or 3 which is modelled by a non-deterministic choice
+const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice
+const int TRANS_TIME_MAX = 2; // scaling up
+const int TRANS_TIME_MIN = 4; // scaling down
+const int ACK_TO = 6;
+const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice
+const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice
+// maximum constant used in timing constraints + 1
+const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1;
+
+// CONTENTION WINDOW
+// CWMIN =15 & CWMAX =16
+// this means that MAX_BACKOFF IS 2
+const int MAX_BACKOFF = 0;
+
+//-----------------------------------------------------------------//
+// THE MEDIUM/CHANNEL
+
+// FORMULAE FOR THE CHANNEL
+// channel is busy
+formula busy = c1>0 | c2>0;
+// channel is free
+formula free = c1=0 & c2=0;
+
+module medium
+
+ // number of collisions
+ col : [0..COL];
+
+ // medium status
+ c1 : [0..2];
+ c2 : [0..2];
+ // ci corresponds to messages associated with station i
+ // 0 nothing being sent
+ // 1 being sent correctly
+ // 2 being sent garbled
+
+ // begin sending message and nothing else currently being sent
+ [send1] c1=0 & c2=0 -> (c1'=1);
+ [send2] c2=0 & c1=0 -> (c2'=1);
+
+ // begin sending message and something is already being sent
+ // in this case both messages become garbled
+ [send1] c1=0 & c2>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL));
+ [send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL));
+
+ // finish sending message
+ [finish1] c1>0 -> (c1'=0);
+ [finish2] c2>0 -> (c2'=0);
+
+endmodule
+
+//-----------------------------------------------------------------//
+// STATION 1
+module station1
+ // clock for station 1
+ x1 : [0..TIME_MAX];
+
+ // local state
+ s1 : [1..12];
+ // 1 sense
+ // 2 wait until free before setting backoff
+ // 3 wait for DIFS then set slot
+ // 4 set backoff
+ // 5 backoff
+ // 6 wait until free in backoff
+ // 7 wait for DIFS then resume backoff
+ // 8 vulnerable
+ // 9 transmit
+ // 11 wait for SIFS and then ACK
+ // 10 wait for ACT_TO
+ // 12 done
+ // BACKOFF
+ // separate into slots
+ slot1 : [0..1];
+ backoff1 : [0..15];
+
+ // BACKOFF COUNTER
+ bc1 : [0..1];
+ // SENSE
+ // let time pass
+ [time] s1=1 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
+ // ready to transmit
+ [] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0);
+ // found channel busy so wait until free
+ [] s1=1 & busy -> (s1'=2) & (x1'=0);
+ // WAIT UNTIL FREE BEFORE SETTING BACKOFF
+ // let time pass (no need for the clock x1 to change)
+ [time] s1=2 & busy -> (s1'=2);
+ // find that channel is free so check its free for DIFS before setting backoff
+ [] s1=2 & free -> (s1'=3);
+ // WAIT FOR DIFS THEN SET BACKOFF
+ // let time pass
+ [time] s1=3 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
+ // found channel busy so wait until free
+ [] s1=3 & busy -> (s1'=2) & (x1'=0);
+ // start backoff first uniformly choose slot
+ // backoff counter 0
+ [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF));
+ // SET BACKOFF (no time can pass)
+ // chosen slot now set backoff
+ [] s1=4 -> 1/16 : (s1'=5) & (backoff1'=0 )
+ + 1/16 : (s1'=5) & (backoff1'=1 )
+ + 1/16 : (s1'=5) & (backoff1'=2 )
+ + 1/16 : (s1'=5) & (backoff1'=3 )
+ + 1/16 : (s1'=5) & (backoff1'=4 )
+ + 1/16 : (s1'=5) & (backoff1'=5 )
+ + 1/16 : (s1'=5) & (backoff1'=6 )
+ + 1/16 : (s1'=5) & (backoff1'=7 )
+ + 1/16 : (s1'=5) & (backoff1'=8 )
+ + 1/16 : (s1'=5) & (backoff1'=9 )
+ + 1/16 : (s1'=5) & (backoff1'=10)
+ + 1/16 : (s1'=5) & (backoff1'=11)
+ + 1/16 : (s1'=5) & (backoff1'=12)
+ + 1/16 : (s1'=5) & (backoff1'=13)
+ + 1/16 : (s1'=5) & (backoff1'=14)
+ + 1/16 : (s1'=5) & (backoff1'=15);
+ // BACKOFF
+ // let time pass
+ [time] s1=5 & x1<ASLOTTIME & free -> (x1'=min(x1+1,TIME_MAX));
+ // decrement backoff
+ [] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1);
+ [] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1);
+ // finish backoff
+ [] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0);
+ // found channel busy
+ [] s1=5 & busy -> (s1'=6) & (x1'=0);
+ // WAIT UNTIL FREE IN BACKOFF
+ // let time pass (no need for the clock x1 to change)
+ [time] s1=6 & busy -> (s1'=6);
+ // find that channel is free
+ [] s1=6 & free -> (s1'=7);
+
+ // WAIT FOR DIFS THEN RESUME BACKOFF
+ // let time pass
+ [time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
+ // resume backoff (start again from previous backoff)
+ [] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0);
+ // found channel busy
+ [] s1=7 & busy -> (s1'=6) & (x1'=0);
+
+ // VULNERABLE
+ // let time pass
+ [time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX));
+ // move to transmit
+ [send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0);
+ // TRANSMIT
+ // let time pass
+ [time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX));
+ // finish transmission successful
+ [finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0);
+ // finish transmission garbled
+ [finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0);
+ // WAIT FOR SIFS THEN WAIT FOR ACK
+
+ // WAIT FOR SIFS i.e. c1=0
+ // check channel and busy: go into backoff
+ [] s1=10 & c1=0 & x1=0 & busy -> (s1'=2);
+ // check channel and free: let time pass
+ [time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
+ // let time pass
+ // following guard is always false as SIFS=1
+ // [time] s1=10 & c1=0 & x1>0 & x1<SIFS -> (x1'=min(x1+1,TIME_MAX));
+ // ack is sent after SIFS (since SIFS-1=0 add condition that channel is free)
+ [send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0);
+
+ // WAIT FOR ACK i.e. c1=1
+ // let time pass
+ [time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX));
+ // get acknowledgement so packet sent correctly and move to done
+ [finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0);
+
+ // WAIT FOR ACK_TO
+ // check channel and busy: go into backoff
+ [] s1=11 & x1=0 & busy -> (s1'=2);
+ // check channel and free: let time pass
+ [time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
+ // let time pass
+ [time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX));
+ // no acknowledgement (go to backoff waiting DIFS first)
+ [] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0);
+
+ // DONE
+ [time] s1=12 -> (s1'=12);
+
+endmodule
+
+// ---------------------------------------------------------------------------- //
+// STATION 2 (rename STATION 1)
+module
+station2=station1[x1=x2,
+ s1=s2,
+ s2=s1,
+ c1=c2,
+ c2=c1,
+ slot1=slot2,
+ backoff1=backoff2,
+ bc1=bc2,
+ send1=send2,
+ finish1=finish2]
+endmodule
+// ---------------------------------------------------------------------------- //
+
+label "twoCollisions" = col=2;
+label "fourCollisions" = col=4;
+label "sixCollisions" = col=6;
diff --git a/wlan0_collide.nm b/wlan0_collide.nm
deleted file mode 100644
index 5d94e23de..000000000
--- a/wlan0_collide.nm
+++ /dev/null
@@ -1,13 +0,0 @@
-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