diff --git a/test/performance/builder/leader5.nm b/test/performance/builder/leader5.nm index 21eb227e9..c48a255bb 100644 --- a/test/performance/builder/leader5.nm +++ b/test/performance/builder/leader5.nm @@ -1,3 +1,4 @@ +<<<<<<< HEAD // asynchronous leader election // 4 processes // gxn/dxp 29/01/01 @@ -96,3 +97,103 @@ 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; +======= +// asynchronous leader election +// 4 processes +// gxn/dxp 29/01/01 + +mdp + +const int 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 (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 (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 "rounds" + [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; + +>>>>>>> 90d2b218a044edca8062084ee89d171695149c1e diff --git a/test/performance/builder/leader5_8.pm b/test/performance/builder/leader5_8.pm index 951898b8d..e6cfc2106 100644 --- a/test/performance/builder/leader5_8.pm +++ b/test/performance/builder/leader5_8.pm @@ -1,3 +1,4 @@ +<<<<<<< HEAD // synchronous leader election protocol (itai & Rodeh) // dxp/gxn 25/01/01 @@ -88,3 +89,95 @@ endrewards // labels label "elected" = s1=3&s2=3&s3=3&s4=3&s5=3; +======= +// synchronous leader election protocol (itai & Rodeh) +// dxp/gxn 25/01/01 + +dtmc + +// CONSTANTS +const int N = 5; // number of processes +const int 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 (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 (u1'=(p1!=v2)) & (v1'=v2); + [read] s1=1 & !u1 & c (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; + +>>>>>>> 90d2b218a044edca8062084ee89d171695149c1e