Merge branch 'master' of https://sselab.de/lab9/private/git/storm

13 years ago · 74ad17bc90
25 changed files with 1469 additions and 18 deletions
--- a/examples/dtmc/crowds/crowds.pctl
+++ b/examples/dtmc/crowds/crowds.pctl
@ -0,0 +1,3 @@
+P=? [ F "observe0Greater1" ]
+P=? [ F "observeIGreater1" ]
+P=? [ F "observeOnlyTrueSender" ]
--- a/examples/dtmc/crowds/crowds.res
+++ b/examples/dtmc/crowds/crowds.res
@ -0,0 +1,19 @@
+// 5/5 
+P=? [ F "observe0Greater1" ] // 0.3328777473921436
+P=? [ F "observeIGreater1" ] // 0.15221847380560186
+P=? [ F "observeOnlyTrueSender" ] // 0.3215351607995943
+
+// 10/5
+P=? [ F "observe0Greater1" ] // 0.26345583706046355
+P=? [ F "observeIGreater1" ] // 0.09236405558901994
+P=? [ F "observeOnlyTrueSender" ] // 0.25849872034453947
+
+// 15/5
+P=? [ F "observe0Greater1" ] // 0.2408422942249347
+P=? [ F "observeIGreater1" ] // 0.0655686905854717
+P=? [ F "observeOnlyTrueSender" ] // 0.2377298605519743
+
+// 20/5
+P=? [ F "observe0Greater1" ] // 0.22967858575985317
+P=? [ F "observeIGreater1" ] // 0.05073192927314383
+P=? [ F "observeOnlyTrueSender" ] // 0.22742031678667812
--- a/examples/dtmc/crowds/crowds10_5.pm
+++ b/examples/dtmc/crowds/crowds10_5.pm
@ -0,0 +1,80 @@
+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 = 10;
+
+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;
+
+	observe5: [0..TotalRuns] init 0;
+
+	observe6: [0..TotalRuns] init 0;
+
+	observe7: [0..TotalRuns] init 0;
+
+	observe8: [0..TotalRuns] init 0;
+
+	observe9: [0..TotalRuns] init 0;
+
+	// the last seen crowd member
+	lastSeen: [0..CrowdSize - 1] init 0;
+
+	// get the protocol started
+	[] phase=0 & runCount<TotalRuns -> (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/10 : (lastSeen'=0) & (phase'=3) + 1/10 : (lastSeen'=1) & (phase'=3) + 1/10 : (lastSeen'=2) & (phase'=3) + 1/10 : (lastSeen'=3) & (phase'=3) + 1/10 : (lastSeen'=4) & (phase'=3) + 1/10 : (lastSeen'=5) & (phase'=3) + 1/10 : (lastSeen'=6) & (phase'=3) + 1/10 : (lastSeen'=7) & (phase'=3) + 1/10 : (lastSeen'=8) & (phase'=3) + 1/10 : (lastSeen'=9) & (phase'=3);
+
+	// if the current member is a bad member, record the most recently seen index
+	[] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> (observe0'=observe0+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> (observe1'=observe1+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> (observe2'=observe2+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> (observe3'=observe3+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> (observe4'=observe4+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> (observe5'=observe5+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> (observe6'=observe6+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> (observe7'=observe7+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> (observe8'=observe8+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> (observe9'=observe9+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 -> (phase'=0);
+
+endmodule
+
+label "observe0Greater1" = observe0 > 1;
+label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1;
+label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1;
--- a/examples/dtmc/crowds/crowds15_5.pm
+++ b/examples/dtmc/crowds/crowds15_5.pm
@ -0,0 +1,95 @@
+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 = 15;
+
+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;
+
+	observe5: [0..TotalRuns] init 0;
+
+	observe6: [0..TotalRuns] init 0;
+
+	observe7: [0..TotalRuns] init 0;
+
+	observe8: [0..TotalRuns] init 0;
+
+	observe9: [0..TotalRuns] init 0;
+
+	observe10: [0..TotalRuns] init 0;
+
+	observe11: [0..TotalRuns] init 0;
+
+	observe12: [0..TotalRuns] init 0;
+
+	observe13: [0..TotalRuns] init 0;
+
+	observe14: [0..TotalRuns] init 0;
+
+	// the last seen crowd member
+	lastSeen: [0..CrowdSize - 1] init 0;
+
+	// get the protocol started
+	[] phase=0 & runCount<TotalRuns -> (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/15 : (lastSeen'=0) & (phase'=3) + 1/15 : (lastSeen'=1) & (phase'=3) + 1/15 : (lastSeen'=2) & (phase'=3) + 1/15 : (lastSeen'=3) & (phase'=3) + 1/15 : (lastSeen'=4) & (phase'=3) + 1/15 : (lastSeen'=5) & (phase'=3) + 1/15 : (lastSeen'=6) & (phase'=3) + 1/15 : (lastSeen'=7) & (phase'=3) + 1/15 : (lastSeen'=8) & (phase'=3) + 1/15 : (lastSeen'=9) & (phase'=3) + 1/15 : (lastSeen'=10) & (phase'=3) + 1/15 : (lastSeen'=11) & (phase'=3) + 1/15 : (lastSeen'=12) & (phase'=3) + 1/15 : (lastSeen'=13) & (phase'=3) + 1/15 : (lastSeen'=14) & (phase'=3);
+
+	// if the current member is a bad member, record the most recently seen index
+	[] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> (observe0'=observe0+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> (observe1'=observe1+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> (observe2'=observe2+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> (observe3'=observe3+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> (observe4'=observe4+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> (observe5'=observe5+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> (observe6'=observe6+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> (observe7'=observe7+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> (observe8'=observe8+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> (observe9'=observe9+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=10 & observe10 < TotalRuns -> (observe10'=observe10+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=11 & observe11 < TotalRuns -> (observe11'=observe11+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=12 & observe12 < TotalRuns -> (observe12'=observe12+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=13 & observe13 < TotalRuns -> (observe13'=observe13+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=14 & observe14 < TotalRuns -> (observe14'=observe14+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 -> (phase'=0);
+
+endmodule
+
+label "observe0Greater1" = observe0 > 1;
+label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1 | observe10 > 1 | observe11 > 1 | observe12 > 1 | observe13 > 1 | observe14 > 1;
+label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1 & observe10 <= 1 & observe11 <= 1 & observe12 <= 1 & observe13 <= 1 & observe14 <= 1;
--- a/examples/dtmc/crowds/crowds20_5.pm
+++ b/examples/dtmc/crowds/crowds20_5.pm
@ -0,0 +1,110 @@
+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 = 20;
+
+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;
+
+	observe5: [0..TotalRuns] init 0;
+
+	observe6: [0..TotalRuns] init 0;
+
+	observe7: [0..TotalRuns] init 0;
+
+	observe8: [0..TotalRuns] init 0;
+
+	observe9: [0..TotalRuns] init 0;
+
+	observe10: [0..TotalRuns] init 0;
+
+	observe11: [0..TotalRuns] init 0;
+
+	observe12: [0..TotalRuns] init 0;
+
+	observe13: [0..TotalRuns] init 0;
+
+	observe14: [0..TotalRuns] init 0;
+
+	observe15: [0..TotalRuns] init 0;
+
+	observe16: [0..TotalRuns] init 0;
+
+	observe17: [0..TotalRuns] init 0;
+
+	observe18: [0..TotalRuns] init 0;
+
+	observe19: [0..TotalRuns] init 0;
+
+	// the last seen crowd member
+	lastSeen: [0..CrowdSize - 1] init 0;
+
+	// get the protocol started
+	[] phase=0 & runCount<TotalRuns -> (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/20 : (lastSeen'=0) & (phase'=3) + 1/20 : (lastSeen'=1) & (phase'=3) + 1/20 : (lastSeen'=2) & (phase'=3) + 1/20 : (lastSeen'=3) & (phase'=3) + 1/20 : (lastSeen'=4) & (phase'=3) + 1/20 : (lastSeen'=5) & (phase'=3) + 1/20 : (lastSeen'=6) & (phase'=3) + 1/20 : (lastSeen'=7) & (phase'=3) + 1/20 : (lastSeen'=8) & (phase'=3) + 1/20 : (lastSeen'=9) & (phase'=3) + 1/20 : (lastSeen'=10) & (phase'=3) + 1/20 : (lastSeen'=11) & (phase'=3) + 1/20 : (lastSeen'=12) & (phase'=3) + 1/20 : (lastSeen'=13) & (phase'=3) + 1/20 : (lastSeen'=14) & (phase'=3) + 1/20 : (lastSeen'=15) & (phase'=3) + 1/20 : (lastSeen'=16) & (phase'=3) + 1/20 : (lastSeen'=17) & (phase'=3) + 1/20 : (lastSeen'=18) & (phase'=3) + 1/20 : (lastSeen'=19) & (phase'=3);
+
+	// if the current member is a bad member, record the most recently seen index
+	[] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> (observe0'=observe0+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> (observe1'=observe1+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> (observe2'=observe2+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> (observe3'=observe3+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> (observe4'=observe4+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> (observe5'=observe5+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> (observe6'=observe6+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> (observe7'=observe7+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> (observe8'=observe8+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> (observe9'=observe9+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=10 & observe10 < TotalRuns -> (observe10'=observe10+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=11 & observe11 < TotalRuns -> (observe11'=observe11+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=12 & observe12 < TotalRuns -> (observe12'=observe12+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=13 & observe13 < TotalRuns -> (observe13'=observe13+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=14 & observe14 < TotalRuns -> (observe14'=observe14+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=15 & observe15 < TotalRuns -> (observe15'=observe15+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=16 & observe16 < TotalRuns -> (observe16'=observe16+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=17 & observe17 < TotalRuns -> (observe17'=observe17+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=18 & observe18 < TotalRuns -> (observe18'=observe18+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=19 & observe19 < TotalRuns -> (observe19'=observe19+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 -> (phase'=0);
+
+endmodule
+
+label "observe0Greater1" = observe0 > 1;
+label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1 | observe10 > 1 | observe11 > 1 | observe12 > 1 | observe13 > 1 | observe14 > 1 | observe15 > 1 | observe16 > 1 | observe17 > 1 | observe18 > 1 | observe19 > 1;
+label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1 & observe10 <= 1 & observe11 <= 1 & observe12 <= 1 & observe13 <= 1 & observe14 <= 1 & observe15 <= 1 & observe16 <= 1 & observe17 <= 1 & observe18 <= 1 & observe19 <= 1;
--- a/examples/dtmc/crowds/crowds5_5.pm
+++ b/examples/dtmc/crowds/crowds5_5.pm
@ -0,0 +1,65 @@
+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 -> (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 -> (observe0'=observe0+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> (observe1'=observe1+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> (observe2'=observe2+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> (observe3'=observe3+1) & (phase'=4);
+	[] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> (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 -> (phase'=0);
+
+endmodule
+
+label "observe0Greater1" = observe0 > 1;
+label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1;
+label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1;
--- a/examples/dtmc/die/die.pctl
+++ b/examples/dtmc/die/die.pctl
@ -0,0 +1,4 @@
+P=? [ F "one" ]
+P=? [ F "two" ]
+P=? [ F "three" ]
+R=? [ F "done" ]
--- a/examples/dtmc/die/die.pm
+++ b/examples/dtmc/die/die.pm
@ -0,0 +1,31 @@
+dtmc
+
+module die
+
+	// local state
+	s : [0..7] init 0;
+	// value of the die
+	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 -> (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;
+label "done" = s=7;
--- a/examples/dtmc/die/die.res
+++ b/examples/dtmc/die/die.res
@ -0,0 +1,4 @@
+P=? [ F "one" ] // 0.16666650772094727
+P=? [ F "two" ] // 0.16666650772094727
+P=? [ F "three" ] // 0.16666650772094727
+R=? [ F "done" ] // 3.6666650772094727
--- a/examples/dtmc/synchronous_leader/leader.pctl
+++ b/examples/dtmc/synchronous_leader/leader.pctl
@ -0,0 +1,3 @@
+P=? [ F "elected" ]
+P=? [ F<=(4*(N+1)) "elected" ]
+R=? [ F "elected" ]
--- a/examples/dtmc/synchronous_leader/leader.res
+++ b/examples/dtmc/synchronous_leader/leader.res
@ -0,0 +1,14 @@
+// 3/5
+P=? [ F "elected" ] // 1.0
+P=? [ F<=(4*(N+1)) "elected" ] // 0.999997440000001
+R=? [ F "elected" ] // 1.0416666623999995
+
+// 4/8
+P=? [ F "elected" ] // 1.0
+P=? [ F<=(4*(N+1)) "elected" ] // 0.9999965911265463
+R=? [ F "elected" ] // 1.0448979526072435
+
+// 5/8
+P=? [ F "elected" ] // 1.0
+P=? [ F<=(4*(N+1)) "elected" ] // 0.9999999097195733
+R=? [ F "elected" ] // 1.0176397499602707
--- a/examples/dtmc/synchronous_leader/leader3_5.pm
+++ b/examples/dtmc/synchronous_leader/leader3_5.pm
@ -0,0 +1,85 @@
+// synchronous leader election protocol  (itai & Rodeh)
+// dxp/gxn 25/01/01
+
+dtmc
+
+// CONSTANTS
+const N = 3; // number of processes
+const 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 -> (c'=c+1);
+	// finished reading
+	[read] c=N-1 -> (c'=c);
+	//decide
+	[done] u1|u2|u3 -> (c'=c);
+	// pick again reset counter 
+	[retry] !(u1|u2|u3) -> (c'=1);
+	// loop (when finished to avoid deadlocks)
+	[loop] s1=3 -> (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 -> (u1'=(p1!=v2)) & (v1'=v2);
+	[read] s1=1 & !u1 & c<N-1 -> (u1'=false) & (v1'=v2) & (p1'=0);
+	// read and move to decide
+	[read] s1=1 &  u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0);
+	[read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0);
+	// deciding
+	// done
+	[done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0);
+	//retry
+	[retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0);
+	// loop (when finished to avoid deadlocks)
+	[loop] s1=3 -> (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;
+
--- a/examples/dtmc/synchronous_leader/leader4_8.pm
+++ b/examples/dtmc/synchronous_leader/leader4_8.pm
@ -0,0 +1,89 @@
+// synchronous leader election protocol  (itai & Rodeh)
+// dxp/gxn 25/01/01
+
+dtmc
+
+// CONSTANTS
+const N = 4; // number of processes
+const K = 8; // 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 -> (c'=c+1);
+	// finished reading
+	[read] c=N-1 -> (c'=c);
+	//decide
+	[done] u1|u2|u3|u4 -> (c'=c);
+	// pick again reset counter 
+	[retry] !(u1|u2|u3|u4) -> (c'=1);
+	// loop (when finished to avoid deadlocks)
+	[loop] s1=3 -> (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)
+	             + 1/K : (s1'=1) & (p1'=5) & (v1'=5) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=6) & (v1'=6) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=7) & (v1'=7) & (u1'=true);
+	// read
+	[read] s1=1 &  u1 & c<N-1 -> (u1'=(p1!=v2)) & (v1'=v2);
+	[read] s1=1 & !u1 & c<N-1 -> (u1'=false) & (v1'=v2) & (p1'=0);
+	// read and move to decide
+	[read] s1=1 &  u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0);
+	[read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0);
+	// deciding
+	// done
+	[done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0);
+	//retry
+	[retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0);
+	// loop (when finished to avoid deadlocks)
+	[loop] s1=3 -> (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=v4 ] endmodule
+module process4 = process1 [ s1=s4,p1=p4,v1=v4,u1=u4,v2=v1 ] endmodule
+
+// expected number of rounds
+rewards "num_rounds"
+	[pick] true : 1;
+endrewards
+
+// labels
+label "elected" = s1=3&s2=3&s3=3&s4=3;
+
--- a/examples/dtmc/synchronous_leader/leader5_8.pm
+++ b/examples/dtmc/synchronous_leader/leader5_8.pm
@ -0,0 +1,90 @@
+// synchronous leader election protocol  (itai & Rodeh)
+// dxp/gxn 25/01/01
+
+dtmc
+
+// CONSTANTS
+const N = 5; // number of processes
+const K = 8; // 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 -> (c'=c+1);
+	// finished reading
+	[read] c=N-1 -> (c'=c);
+	//decide
+	[done] u1|u2|u3|u4|u5 -> (c'=c);
+	// pick again reset counter 
+	[retry] !(u1|u2|u3|u4|u5) -> (c'=1);
+	// loop (when finished to avoid deadlocks)
+	[loop] s1=3 -> (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)
+	             + 1/K : (s1'=1) & (p1'=5) & (v1'=5) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=6) & (v1'=6) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=7) & (v1'=7) & (u1'=true);
+	// read
+	[read] s1=1 &  u1 & c<N-1 -> (u1'=(p1!=v2)) & (v1'=v2);
+	[read] s1=1 & !u1 & c<N-1 -> (u1'=false) & (v1'=v2) & (p1'=0);
+	// read and move to decide
+	[read] s1=1 &  u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0);
+	[read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0);
+	// deciding
+	// done
+	[done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0);
+	//retry
+	[retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0);
+	// loop (when finished to avoid deadlocks)
+	[loop] s1=3 -> (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=v4 ] endmodule
+module process4 = process1 [ s1=s4,p1=p4,v1=v4,u1=u4,v2=v5 ] endmodule
+module process5 = process1 [ s1=s5,p1=p5,v1=v5,u1=u5,v2=v1 ] endmodule
+
+// expected number of rounds
+rewards "num_rounds"
+	[pick] true : 1;
+endrewards
+
+// labels
+label "elected" = s1=3&s2=3&s3=3&s4=3&s5=3;
+
--- a/examples/dtmc/synchronous_leader/leader6_8.pm
+++ b/examples/dtmc/synchronous_leader/leader6_8.pm
@ -0,0 +1,91 @@
+// synchronous leader election protocol  (itai & Rodeh)
+// dxp/gxn 25/01/01
+
+dtmc
+
+// CONSTANTS
+const N = 6; // number of processes
+const K = 8; // 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 -> (c'=c+1);
+	// finished reading
+	[read] c=N-1 -> (c'=c);
+	//decide
+	[done] u1|u2|u3|u4|u5|u6 -> (c'=c);
+	// pick again reset counter 
+	[retry] !(u1|u2|u3|u4|u5|u6) -> (c'=1);
+	// loop (when finished to avoid deadlocks)
+	[loop] s1=3 -> (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)
+	             + 1/K : (s1'=1) & (p1'=5) & (v1'=5) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=6) & (v1'=6) & (u1'=true)
+	             + 1/K : (s1'=1) & (p1'=7) & (v1'=7) & (u1'=true);
+	// read
+	[read] s1=1 &  u1 & c<N-1 -> (u1'=(p1!=v2)) & (v1'=v2);
+	[read] s1=1 & !u1 & c<N-1 -> (u1'=false) & (v1'=v2) & (p1'=0);
+	// read and move to decide
+	[read] s1=1 &  u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0);
+	[read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0);
+	// deciding
+	// done
+	[done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0);
+	//retry
+	[retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0);
+	// loop (when finished to avoid deadlocks)
+	[loop] s1=3 -> (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=v4 ] endmodule
+module process4 = process1 [ s1=s4,p1=p4,v1=v4,u1=u4,v2=v5 ] endmodule
+module process5 = process1 [ s1=s5,p1=p5,v1=v5,u1=u5,v2=v6 ] endmodule
+module process6 = process1 [ s1=s6,p1=p6,v1=v6,u1=u6,v2=v1 ] endmodule
+
+// expected number of rounds
+rewards "num_rounds"
+	[pick] true : 1;
+endrewards
+
+// labels
+label "elected" = s1=3&s2=3&s3=3&s4=3&s5=3&s6=3;
+
--- a/examples/mdp/asynchronous_leader/leader.pctl
+++ b/examples/mdp/asynchronous_leader/leader.pctl
@ -0,0 +1,8 @@
+Pmin=? [ F "elected" ]
+
+const int K = 25;
+Pmin=? [ F<=K "elected" ]
+Pmax=? [ F<=K "elected" ]
+
+Rmin=? [ F "elected" ]
+Rmax=? [ F "elected" ]
--- a/examples/mdp/asynchronous_leader/leader.res
+++ b/examples/mdp/asynchronous_leader/leader.res
@ -0,0 +1,49 @@
+// 3
+Pmin=? [ F "elected" ] // 1.0
+
+const int K = 25;
+Pmin=? [ F<=K "elected" ] // 0.5625
+Pmax=? [ F<=K "elected" ] // 0.5625
+
+Rmin=? [ F "elected" ] // 3.3333212586585432
+Rmax=? [ F "elected" ] // 3.3333206579554826
+
+// 4
+Pmin=? [ F "elected" ] // 1.0
+
+const int K = 25;
+Pmin=? [ F<=K "elected" ] // 0.0625
+Pmax=? [ F<=K "elected" ] // 0.0625
+
+Rmin=? [ F "elected" ] // 4.2856896106114934
+Rmax=? [ F "elected" ] // 4.28569043544414
+
+// 5
+Pmin=? [ F "elected" ] // 1.0
+
+const int K = 25;
+Pmin=? [ F<=K "elected" ] // 0.0
+Pmax=? [ F<=K "elected" ] // 0.0
+
+Rmin=? [ F "elected" ] // 5.034886386278894
+Rmax=? [ F "elected" ] // 5.034881859133309
+
+// 6
+Pmin=? [ F "elected" ] // 1.0
+
+const int K = 25;
+Pmin=? [ F<=K "elected" ] // 0.0
+Pmax=? [ F<=K "elected" ] // 0.0
+
+Rmin=? [ F "elected" ] // 5.649720120334257
+Rmax=? [ F "elected" ] // 5.649719114527437
+
+// 7
+Pmin=? [ F "elected" ] // 1.0
+
+const int K = 25;
+Pmin=? [ F<=K "elected" ] // 0.0
+Pmax=? [ F<=K "elected" ] // 0.0
+
+Rmin=? [ F "elected" ] // 6.172433512043686
+Rmax=? [ F "elected" ] // 6.172434400085756
--- a/examples/mdp/asynchronous_leader/leader3.nm
+++ b/examples/mdp/asynchronous_leader/leader3.nm
@ -0,0 +1,96 @@
+// asynchronous leader election
+// 4 processes
+// gxn/dxp 29/01/01
+
+mdp
+
+const 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
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// reward - expected number of rounds (equals the number of times a process receives a counter)
+rewards
+	[c12] true : 1;
+endrewards
+
+//----------------------------------------------------------------------------------------------------------------------------
+formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0);
+label "elected" = s1=4|s2=4|s3=4;
+
--- a/examples/mdp/asynchronous_leader/leader4.nm
+++ b/examples/mdp/asynchronous_leader/leader4.nm
@ -0,0 +1,97 @@
+// asynchronous leader election
+// 4 processes
+// gxn/dxp 29/01/01
+
+mdp
+
+const N= 4; // number of processes
+
+//----------------------------------------------------------------------------------------------------------------------------
+module process1
+	
+	// COUNTER
+	c1 : [0..4-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
+	[p41] (s1=1) & (receive1=0) & !( (p1=0) & (p4=1) ) -> (s1'=2) & (receive1'=1);
+	// become inactive
+	[p41] (s1=1) & (receive1=0) & (p1=0) & (p4=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)
+	[c41] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2);
+	// receive counter and sent counter
+	// only active process (decide)
+	[c41] (s1=2) & (receive1=1) & (sent1=2) & (c4=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
+	// other active process (pick again)
+	[c41] (s1=2) & (receive1=1) & (sent1=2) & (c4<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
+	[p41] (s1=3) & (receive1=0) -> (p1'=p4) & (receive1'=1);
+	// receive counter
+	[c41] (s1=3) & (receive1=1) & (c4<N-1) -> (c1'=c4+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,p41=p12,c12=c23,c41=c12,p4=p1,c4=c1] endmodule
+module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p41=p23,c12=c34,c41=c23,p4=p2,c4=c2] endmodule
+module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p41,p41=p34,c12=c41,c41=c34,p4=p3,c4=c3] endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// reward - expected number of rounds (equals the number of times a process receives a counter)
+rewards
+	[c12] true : 1;
+endrewards
+
+//----------------------------------------------------------------------------------------------------------------------------
+formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0);
+label "elected" = s1=4|s2=4|s3=4|s4=4;
+
--- a/examples/mdp/asynchronous_leader/leader5.nm
+++ b/examples/mdp/asynchronous_leader/leader5.nm
@ -0,0 +1,98 @@
+// asynchronous leader election
+// 4 processes
+// gxn/dxp 29/01/01
+
+mdp
+
+const N= 5; // number of processes
+
+//----------------------------------------------------------------------------------------------------------------------------
+module process1
+	
+	// COUNTER
+	c1 : [0..5-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
+	[p51] (s1=1) & (receive1=0) & !( (p1=0) & (p5=1) ) -> (s1'=2) & (receive1'=1);
+	// become inactive
+	[p51] (s1=1) & (receive1=0) & (p1=0) & (p5=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)
+	[c51] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2);
+	// receive counter and sent counter
+	// only active process (decide)
+	[c51] (s1=2) & (receive1=1) & (sent1=2) & (c5=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
+	// other active process (pick again)
+	[c51] (s1=2) & (receive1=1) & (sent1=2) & (c5<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
+	[p51] (s1=3) & (receive1=0) -> (p1'=p5) & (receive1'=1);
+	// receive counter
+	[c51] (s1=3) & (receive1=1) & (c5<N-1) -> (c1'=c5+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,p51=p12,c12=c23,c51=c12,p5=p1,c5=c1] endmodule
+module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p51=p23,c12=c34,c51=c23,p5=p2,c5=c2] endmodule
+module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p51=p34,c12=c45,c51=c34,p5=p3,c5=c3] endmodule
+module process5=process1[s1=s5,p1=p5,c1=c5,sent1=sent5,receive1=receive5,p12=p51,p51=p45,c12=c51,c51=c45,p5=p4,c5=c4] endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// reward - expected number of rounds (equals the number of times a process receives a counter)
+rewards
+	[c12] true : 1;
+endrewards
+
+//----------------------------------------------------------------------------------------------------------------------------
+formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0);
+label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4;
+
--- a/examples/mdp/asynchronous_leader/leader6.nm
+++ b/examples/mdp/asynchronous_leader/leader6.nm
@ -0,0 +1,99 @@
+// asynchronous leader election
+// 4 processes
+// gxn/dxp 29/01/01
+
+mdp
+
+const N= 6; // number of processes
+
+//----------------------------------------------------------------------------------------------------------------------------
+module process1
+	
+	// COUNTER
+	c1 : [0..6-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
+	[p61] (s1=1) & (receive1=0) & !( (p1=0) & (p6=1) ) -> (s1'=2) & (receive1'=1);
+	// become inactive
+	[p61] (s1=1) & (receive1=0) & (p1=0) & (p6=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)
+	[c61] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2);
+	// receive counter and sent counter
+	// only active process (decide)
+	[c61] (s1=2) & (receive1=1) & (sent1=2) & (c6=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
+	// other active process (pick again)
+	[c61] (s1=2) & (receive1=1) & (sent1=2) & (c6<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
+	[p61] (s1=3) & (receive1=0) -> (p1'=p6) & (receive1'=1);
+	// receive counter
+	[c61] (s1=3) & (receive1=1) & (c6<N-1) -> (c1'=c6+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,p61=p12,c12=c23,c61=c12,p6=p1,c6=c1] endmodule
+module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p61=p23,c12=c34,c61=c23,p6=p2,c6=c2] endmodule
+module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p61=p34,c12=c45,c61=c34,p6=p3,c6=c3] endmodule
+module process5=process1[s1=s5,p1=p5,c1=c5,sent1=sent5,receive1=receive5,p12=p56,p61=p45,c12=c56,c61=c45,p6=p4,c6=c4] endmodule
+module process6=process1[s1=s6,p1=p6,c1=c6,sent1=sent6,receive1=receive6,p12=p61,p61=p56,c12=c61,c61=c56,p6=p5,c6=c5] endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// reward - expected number of rounds (equals the number of times a process receives a counter)
+rewards
+	[c12] true : 1;
+endrewards
+
+//----------------------------------------------------------------------------------------------------------------------------
+formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0)+(s6=4?1:0);
+label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4|s6=4;
+
--- a/examples/mdp/asynchronous_leader/leader7.nm
+++ b/examples/mdp/asynchronous_leader/leader7.nm
@ -0,0 +1,100 @@
+// asynchronous leader election
+// 4 processes
+// gxn/dxp 29/01/01
+
+mdp
+
+const N= 7; // number of processes
+
+//----------------------------------------------------------------------------------------------------------------------------
+module process1
+	
+	// COUNTER
+	c1 : [0..7-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
+	[p71] (s1=1) & (receive1=0) & !( (p1=0) & (p7=1) ) -> (s1'=2) & (receive1'=1);
+	// become inactive
+	[p71] (s1=1) & (receive1=0) & (p1=0) & (p7=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)
+	[c71] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2);
+	// receive counter and sent counter
+	// only active process (decide)
+	[c71] (s1=2) & (receive1=1) & (sent1=2) & (c7=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
+	// other active process (pick again)
+	[c71] (s1=2) & (receive1=1) & (sent1=2) & (c7<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
+	[p71] (s1=3) & (receive1=0) -> (p1'=p7) & (receive1'=1);
+	// receive counter
+	[c71] (s1=3) & (receive1=1) & (c7<N-1) -> (c1'=c7+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,p71=p12,c12=c23,c71=c12,p7=p1,c7=c1] endmodule
+module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p71=p23,c12=c34,c71=c23,p7=p2,c7=c2] endmodule
+module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p71=p34,c12=c45,c71=c34,p7=p3,c7=c3] endmodule
+module process5=process1[s1=s5,p1=p5,c1=c5,sent1=sent5,receive1=receive5,p12=p56,p71=p45,c12=c56,c71=c45,p7=p4,c7=c4] endmodule
+module process6=process1[s1=s6,p1=p6,c1=c6,sent1=sent6,receive1=receive6,p12=p67,p71=p56,c12=c67,c71=c56,p7=p5,c7=c5] endmodule
+module process7=process1[s1=s7,p1=p7,c1=c7,sent1=sent7,receive1=receive7,p12=p71,p71=p67,c12=c71,c71=c67,p7=p6,c7=c6] endmodule
+
+//----------------------------------------------------------------------------------------------------------------------------
+
+// reward - expected number of rounds (equals the number of times a process receives a counter)
+rewards
+	[c12] true : 1;
+endrewards
+
+//----------------------------------------------------------------------------------------------------------------------------
+formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0)+(s6=4?1:0)+(s7=4?1:0);
+label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4|s6=4|s7=4;
+
--- a/examples/mdp/two_dice/two_dice.pctl
+++ b/examples/mdp/two_dice/two_dice.pctl
@ -0,0 +1,13 @@
+Pmin=? [ F "two" ]
+Pmax=? [ F "two" ]
+Pmin=? [ F "three" ]
+Pmax=? [ F "three" ]
+Pmin=? [ F "four" ]
+Pmax=? [ F "four" ]
+Pmin=? [ F "five" ]
+Pmax=? [ F "five" ]
+Pmin=? [ F "six" ]
+Pmax=? [ F "six" ]
+
+Rmin=? [ F "done" ]
+Rmax=? [ F "done" ]
--- a/examples/mdp/two_dice/two_dice.res
+++ b/examples/mdp/two_dice/two_dice.res
@ -0,0 +1,13 @@
+Pmin=? [ F "two" ] // 0.027777761220932007
+Pmax=? [ F "two" ] // 0.027777761220932007
+Pmin=? [ F "three" ] // 0.055555522441864014
+Pmax=? [ F "three" ] // 0.055555522441864014
+Pmin=? [ F "four" ] // 0.08333328366279602
+Pmax=? [ F "four" ] // 0.08333328366279602
+Pmin=? [ F "five" ] // 0.11111104488372803
+Pmax=? [ F "five" ] // 0.11111104488372803
+Pmin=? [ F "six" ] // 0.13888880610466003
+Pmax=? [ F "six" ] // 0.13888880610466003
+
+Rmin=? [ F "done" ] // 7.333329498767853
+Rmax=? [ F "done" ] // 7.333329498767853
--- a/src/storm.cpp
+++ b/src/storm.cpp
@ -138,21 +138,36 @@ void cleanUp() {
 }

 void testCheckingDie(storm::models::Dtmc<double>& dtmc) {
+	storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
+
 	storm::formula::Ap<double>* oneFormula = new storm::formula::Ap<double>("one");
 	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(oneFormula);
 	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);

+	mc->check(*probFormula);
+	delete probFormula;
+
+	oneFormula = new storm::formula::Ap<double>("two");
+	eventuallyFormula = new storm::formula::Eventually<double>(oneFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	oneFormula = new storm::formula::Ap<double>("three");
+	eventuallyFormula = new storm::formula::Eventually<double>(oneFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
 	storm::formula::Ap<double>* done = new storm::formula::Ap<double>("done");
 	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(done);
 	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula);

-	storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
-	mc->check(*probFormula);
 	mc->check(*rewardFormula);
-
-	delete mc;
-	delete probFormula;
 	delete rewardFormula;
+	delete mc;
 }

 void testCheckingCrowds(storm::models::Dtmc<double>& dtmc) {
@ -191,13 +206,10 @@ void testCheckingSynchronousLeader(storm::models::Dtmc<double>& dtmc, uint_fast6
 	delete probFormula;

 	electedFormula = new storm::formula::Ap<double>("elected");
-	storm::formula::BoundedUntil<double>* boundedUntilFormula = new storm::formula::BoundedUntil<double>(new storm::formula::Ap<double>("true"), electedFormula, 1);
+	storm::formula::BoundedUntil<double>* boundedUntilFormula = new storm::formula::BoundedUntil<double>(new storm::formula::Ap<double>("true"), electedFormula, n * 4);
 	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedUntilFormula);

-	for (uint_fast64_t L = 1; L < 5; ++L) {
-		boundedUntilFormula->setBound(L*(n + 1));
-		mc->check(*probFormula);
-	}
+	mc->check(*probFormula);
 	delete probFormula;

 	electedFormula = new storm::formula::Ap<double>("elected");
@ -211,23 +223,92 @@ void testCheckingSynchronousLeader(storm::models::Dtmc<double>& dtmc, uint_fast6
 }

 void testCheckingDice(storm::models::Mdp<double>& mdp) {
-	storm::formula::Ap<double>* threeFormula = new storm::formula::Ap<double>("three");
-	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(threeFormula);
-	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+	storm::formula::Ap<double>* twoFormula = new storm::formula::Ap<double>("two");
+	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
+	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);

 	storm::modelChecker::GmmxxMdpPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxMdpPrctlModelChecker<double>(mdp);

 	mc->check(*probFormula);
 	delete probFormula;

+	twoFormula = new storm::formula::Ap<double>("two");
+	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	twoFormula = new storm::formula::Ap<double>("three");
+	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	twoFormula = new storm::formula::Ap<double>("three");
+	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	twoFormula = new storm::formula::Ap<double>("four");
+	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	twoFormula = new storm::formula::Ap<double>("four");
+	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	twoFormula = new storm::formula::Ap<double>("five");
+	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	twoFormula = new storm::formula::Ap<double>("five");
+	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	twoFormula = new storm::formula::Ap<double>("six");
+	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	twoFormula = new storm::formula::Ap<double>("six");
+	eventuallyFormula = new storm::formula::Eventually<double>(twoFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
 	storm::formula::Ap<double>* doneFormula = new storm::formula::Ap<double>("done");
-	//storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(doneFormula);
-	storm::formula::InstantaneousReward<double>* reachabilityRewardFormula = new storm::formula::InstantaneousReward<double>(8);
+	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(doneFormula);
 	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);

 	mc->check(*rewardFormula);
 	delete rewardFormula;

+	doneFormula = new storm::formula::Ap<double>("done");
+	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(doneFormula);
+	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+
+	mc->check(*rewardFormula);
+	delete rewardFormula;
+
 	delete mc;
 }

@ -249,19 +330,33 @@ void testCheckingAsynchLeader(storm::models::Mdp<double>& mdp) {
 	delete probMaxFormula;

 	electedFormula = new storm::formula::Ap<double>("elected");
-	storm::formula::BoundedEventually<double>* boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(electedFormula, 50);
+	storm::formula::BoundedEventually<double>* boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(electedFormula, 25);
 	probMinFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);

 	mc->check(*probMinFormula);
 	delete probMinFormula;

 	electedFormula = new storm::formula::Ap<double>("elected");
-	boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(electedFormula, 50);
+	boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(electedFormula, 25);
 	probMaxFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);

 	mc->check(*probMaxFormula);
 	delete probMaxFormula;

+	electedFormula = new storm::formula::Ap<double>("elected");
+	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(electedFormula);
+	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
+
+	mc->check(*rewardFormula);
+	delete rewardFormula;
+
+	electedFormula = new storm::formula::Ap<double>("elected");
+	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(electedFormula);
+	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+
+	mc->check(*rewardFormula);
+	delete rewardFormula;
+
 	delete mc;
 }

@ -278,7 +373,7 @@ void testChecking() {

 		// testCheckingDie(*dtmc);
 		// testCheckingCrowds(*dtmc);
-		// testCheckingSynchronousLeader(*dtmc, 4);
+		// testCheckingSynchronousLeader(*dtmc, 6);
 	} else if (parser.getType() == storm::models::MDP) {
 		std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
 		mdp->printModelInformationToStream(std::cout);