sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Added a few more example files.

main
gereon 13 years ago
parent
ac86932785
commit
966377ae32
7 changed files with 640 additions and 0 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 80
      examples/dtmc/crowds/crowds10_5.pm
  2. 95
      examples/dtmc/crowds/crowds15_5.pm
  3. 110
      examples/dtmc/crowds/crowds20_5.pm
  4. 85
      examples/dtmc/synchronous_leader/leader3_5.pm
  5. 89
      examples/dtmc/synchronous_leader/leader4_8.pm
  6. 90
      examples/dtmc/synchronous_leader/leader5_8.pm
  7. 91
      examples/dtmc/synchronous_leader/leader6_8.pm

80
examples/dtmc/crowds/crowds10_5.pm
View File

@ -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;

95
examples/dtmc/crowds/crowds15_5.pm
View File

@ -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 -> 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0);
// decide whether crowd member is good or bad according to given probabilities
[] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false);
// if the current member is a good member, update the last seen index (chosen uniformly)
[] phase=2 & good -> 1/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 -> 1: (observe0'=observe0+1) & (phase'=4);
[] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4);
[] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4);
[] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4);
[] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4);
[] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> 1: (observe5'=observe5+1) & (phase'=4);
[] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> 1: (observe6'=observe6+1) & (phase'=4);
[] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> 1: (observe7'=observe7+1) & (phase'=4);
[] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> 1: (observe8'=observe8+1) & (phase'=4);
[] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> 1: (observe9'=observe9+1) & (phase'=4);
[] phase=2 & !good & lastSeen=10 & observe10 < TotalRuns -> 1: (observe10'=observe10+1) & (phase'=4);
[] phase=2 & !good & lastSeen=11 & observe11 < TotalRuns -> 1: (observe11'=observe11+1) & (phase'=4);
[] phase=2 & !good & lastSeen=12 & observe12 < TotalRuns -> 1: (observe12'=observe12+1) & (phase'=4);
[] phase=2 & !good & lastSeen=13 & observe13 < TotalRuns -> 1: (observe13'=observe13+1) & (phase'=4);
[] phase=2 & !good & lastSeen=14 & observe14 < TotalRuns -> 1: (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 -> 1: (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;

110
examples/dtmc/crowds/crowds20_5.pm
View File

@ -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 -> 1:(phase'=1) & (runCount'=runCount+1) & (lastSeen'=0);
// decide whether crowd member is good or bad according to given probabilities
[] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false);
// if the current member is a good member, update the last seen index (chosen uniformly)
[] phase=2 & good -> 1/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 -> 1:(observe0'=observe0+1) & (phase'=4);
[] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1:(observe1'=observe1+1) & (phase'=4);
[] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1:(observe2'=observe2+1) & (phase'=4);
[] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1:(observe3'=observe3+1) & (phase'=4);
[] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1:(observe4'=observe4+1) & (phase'=4);
[] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> 1:(observe5'=observe5+1) & (phase'=4);
[] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> 1:(observe6'=observe6+1) & (phase'=4);
[] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> 1:(observe7'=observe7+1) & (phase'=4);
[] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> 1:(observe8'=observe8+1) & (phase'=4);
[] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> 1:(observe9'=observe9+1) & (phase'=4);
[] phase=2 & !good & lastSeen=10 & observe10 < TotalRuns -> 1:(observe10'=observe10+1) & (phase'=4);
[] phase=2 & !good & lastSeen=11 & observe11 < TotalRuns -> 1:(observe11'=observe11+1) & (phase'=4);
[] phase=2 & !good & lastSeen=12 & observe12 < TotalRuns -> 1:(observe12'=observe12+1) & (phase'=4);
[] phase=2 & !good & lastSeen=13 & observe13 < TotalRuns -> 1:(observe13'=observe13+1) & (phase'=4);
[] phase=2 & !good & lastSeen=14 & observe14 < TotalRuns -> 1:(observe14'=observe14+1) & (phase'=4);
[] phase=2 & !good & lastSeen=15 & observe15 < TotalRuns -> 1:(observe15'=observe15+1) & (phase'=4);
[] phase=2 & !good & lastSeen=16 & observe16 < TotalRuns -> 1:(observe16'=observe16+1) & (phase'=4);
[] phase=2 & !good & lastSeen=17 & observe17 < TotalRuns -> 1:(observe17'=observe17+1) & (phase'=4);
[] phase=2 & !good & lastSeen=18 & observe18 < TotalRuns -> 1:(observe18'=observe18+1) & (phase'=4);
[] phase=2 & !good & lastSeen=19 & observe19 < TotalRuns -> 1:(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 -> 1:(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;

85
examples/dtmc/synchronous_leader/leader3_5.pm
View File

@ -0,0 +1,85 @@
// synchronous leader election protocol (itai & Rodeh)
// dxp/gxn 25/01/01
dtmc
// CONSTANTS
const int N = 3; // number of processes
const int K = 5; // range of probabilistic choice
// counter module used to count the number of processes that have been read
// and to know when a process has decided
module counter
// counter (c=i means process j reading process (i-1)+j next)
c : [1..N-1];
// reading
[read] c<N-1 -> (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;

89
examples/dtmc/synchronous_leader/leader4_8.pm
View File

@ -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;

90
examples/dtmc/synchronous_leader/leader5_8.pm
View File

@ -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;

91
examples/dtmc/synchronous_leader/leader6_8.pm
View File

@ -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;
Write Preview
Loading…
Cancel
Save