Browse Source
Added PRISM files for all of our examples. Added missing reward models. Added result files that indicate the results of PRISM on our examples.
main
Added PRISM files for all of our examples. Added missing reward models. Added result files that indicate the results of PRISM on our examples.
main
dehnert
12 years ago
24 changed files with 1356 additions and 0 deletions
-
3examples/dtmc/crowds/crowds.pctl
-
19examples/dtmc/crowds/crowds.res
-
80examples/dtmc/crowds/crowds10_5.pm
-
95examples/dtmc/crowds/crowds15_5.pm
-
110examples/dtmc/crowds/crowds20_5.pm
-
65examples/dtmc/crowds/crowds5_5.pm
-
4examples/dtmc/die/die.pctl
-
31examples/dtmc/die/die.pm
-
4examples/dtmc/die/die.res
-
3examples/dtmc/synchronous_leader/leader.pctl
-
14examples/dtmc/synchronous_leader/leader.res
-
85examples/dtmc/synchronous_leader/leader3_5.pm
-
89examples/dtmc/synchronous_leader/leader4_8.pm
-
90examples/dtmc/synchronous_leader/leader5_8.pm
-
91examples/dtmc/synchronous_leader/leader6_8.pm
-
8examples/mdp/asynchronous_leader/leader.pctl
-
49examples/mdp/asynchronous_leader/leader.res
-
96examples/mdp/asynchronous_leader/leader3.nm
-
97examples/mdp/asynchronous_leader/leader4.nm
-
98examples/mdp/asynchronous_leader/leader5.nm
-
99examples/mdp/asynchronous_leader/leader6.nm
-
100examples/mdp/asynchronous_leader/leader7.nm
-
13examples/mdp/two_dice/two_dice.pctl
-
13examples/mdp/two_dice/two_dice.res
@ -0,0 +1,3 @@ |
|||
P=? [ F "observe0Greater1" ] |
|||
P=? [ F "observeIGreater1" ] |
|||
P=? [ F "observeOnlyTrueSender" ] |
|||
@ -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 |
|||
@ -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; |
|||
@ -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; |
|||
@ -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; |
|||
@ -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; |
|||
@ -0,0 +1,4 @@ |
|||
P=? [ F "one" ] |
|||
P=? [ F "two" ] |
|||
P=? [ F "three" ] |
|||
R=? [ F "done" ] |
|||
@ -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; |
|||
@ -0,0 +1,4 @@ |
|||
P=? [ F "one" ] // 0.16666650772094727 |
|||
P=? [ F "two" ] // 0.16666650772094727 |
|||
P=? [ F "three" ] // 0.16666650772094727 |
|||
R=? [ F "done" ] // 3.6666650772094727 |
|||
@ -0,0 +1,3 @@ |
|||
P=? [ F "elected" ] |
|||
P=? [ F<=(4*(N+1)) "elected" ] |
|||
R=? [ F "elected" ] |
|||
@ -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 |
|||
@ -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; |
|||
|
|||
@ -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; |
|||
|
|||
@ -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; |
|||
|
|||
@ -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; |
|||
|
|||
@ -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" ] |
|||
@ -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 |
|||
@ -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; |
|||
|
|||
@ -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; |
|||
|
|||
@ -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; |
|||
|
|||
@ -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; |
|||
|
|||
@ -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; |
|||
|
|||
@ -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" ] |
|||
@ -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 |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue