diff --git a/prism-examples/leader/asynchronous/.autopp b/prism-examples/leader/asynchronous/.autopp new file mode 100755 index 00000000..dd396d4e --- /dev/null +++ b/prism-examples/leader/asynchronous/.autopp @@ -0,0 +1,7 @@ +#!/bin/csh + +foreach N ( 3 4 5 6 7 8 9 10 ) + echo "Generating for N=$N" + prismpp .leaderN.nm.pp $N >! leader_"$N".nm + unix2dos leader"$N".nm +end diff --git a/prism-examples/leader/asynchronous/.leaderN.nm.pp b/prism-examples/leader/asynchronous/.leaderN.nm.pp new file mode 100644 index 00000000..ee353421 --- /dev/null +++ b/prism-examples/leader/asynchronous/.leaderN.nm.pp @@ -0,0 +1,98 @@ +// asynchronous leader election +// 4 processes +// gxn/dxp 29/01/01 + +mdp + +#const N# +const N= #N#; // number of processes + +//---------------------------------------------------------------------------------------------------------------------------- +module process1 + + // COUNTER + c1 : [0..#N#-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 + [p#N#1] (s1=1) & (receive1=0) & !( (p1=0) & (p#N#=1) ) -> (s1'=2) & (receive1'=1); + // become inactive + [p#N#1] (s1=1) & (receive1=0) & (p1=0) & (p#N#=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) + [c#N#1] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2); + // receive counter and sent counter + // only active process (decide) + [c#N#1] (s1=2) & (receive1=1) & (sent1=2) & (c#N#=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0); + // other active process (pick again) + [c#N#1] (s1=2) & (receive1=1) & (sent1=2) & (c#N# (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 + [p#N#1] (s1=3) & (receive1=0) -> (p1'=p#N#) & (receive1'=1); + // receive counter + [c#N#1] (s1=3) & (receive1=1) & (c#N# (c1'=c#N#+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 +#for i=2:N# +module process#i#=process1[s1=s#i#,p1=p#i#,c1=c#i#,sent1=sent#i#,receive1=receive#i#,p12=p#i##mod(i,N)+1#,p#N#1=p#mod(i-2,N)+1##i#,c12=c#i##mod(i,N)+1#,c#N#1=c#mod(i-2,N)+1##i#,p#N#=p#mod(i-2,N)+1#,c#N#=c#mod(i-2,N)+1#] endmodule +#end# + +//---------------------------------------------------------------------------------------------------------------------------- + +// reward - expected number of rounds (equals the number of times a process receives a counter) +rewards + [c12] true : 1; +endrewards + +//---------------------------------------------------------------------------------------------------------------------------- +formula leaders = #+ i=1:N#(s#i#=4?1:0)#end#; +label "elected" = #| i=1:N#s#i#=4#end#; + diff --git a/prism-examples/leader/asynchronous/auto b/prism-examples/leader/asynchronous/auto index 5d2fcd72..07dc96a3 100755 --- a/prism-examples/leader/asynchronous/auto +++ b/prism-examples/leader/asynchronous/auto @@ -1,10 +1,10 @@ #!/bin/csh -prism leader3.nm leader3.pctl -const K=1 -m -prism leader4.nm leader4.pctl -const K=1 -m -prism leader5.nm leader5.pctl -const K=1 -m -#prism leader6.nm leader6.pctl -const K=1 -m -#prism leader7.nm leader7.pctl -const K=1 -m -#prism leader8.nm leader8.pctl -const K=1 -m -#prism leader9.nm leader9.pctl -const K=1 -m -#prism leader10.nm leader10.pctl -const K=1 -m +prism leader3.nm leader.pctl -const K=1 -m +prism leader4.nm leader.pctl -const K=1 -m +prism leader5.nm leader.pctl -const K=1 -m +#prism leader6.nm leader.pctl -const K=1 -m +#prism leader7.nm leader.pctl -const K=1 -m +#prism leader8.nm leader.pctl -const K=1 -m +#prism leader9.nm leader.pctl -const K=1 -m +#prism leader10.nm leader.pctl -const K=1 -m diff --git a/prism-examples/leader/asynchronous/leader.pctl b/prism-examples/leader/asynchronous/leader.pctl new file mode 100644 index 00000000..0152e1a9 --- /dev/null +++ b/prism-examples/leader/asynchronous/leader.pctl @@ -0,0 +1,12 @@ +// only one leader is elected +leaders<=1 + +// with probability 1 eventually a leader is elected +P>=1 [ F "elected" ] +// min/max probability leader is elected within K steps +const int K; +Pmin=?[ F<=K "elected" ] +Pmax=?[ F<=K "elected" ] +// the min/max expected time to elect a leader +Rmin=?[ F "elected" ] +Rmax=?[ F "elected" ] diff --git a/prism-examples/leader/asynchronous/leader10.pctl b/prism-examples/leader/asynchronous/leader10.pctl deleted file mode 100644 index d7bd267a..00000000 --- a/prism-examples/leader/asynchronous/leader10.pctl +++ /dev/null @@ -1,11 +0,0 @@ -// only one leader is elected. -(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) + (s8=4?1:0) + (s9=4?1:0) + (s10=4?1:0)<=1 -// with probability 1 eventually a leader is elected -P>=1 [ true U (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4 | s9=4 | s10=4) ] -// min/max probability leader is elected within K steps -const int K; -Pmin=?[ true U<=K (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4 | s9=4 | s10=4) ] -Pmax=?[ true U<=K (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4 | s9=4 | s10=4) ] -// min/max expected time to elect a leader -Rmin=?[ F (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4 | s9=4 | s10=4) ] -Rmax=?[ F (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4 | s9=4 | s10=4) ] diff --git a/prism-examples/leader/asynchronous/leader3.pctl b/prism-examples/leader/asynchronous/leader3.pctl deleted file mode 100644 index 44fee886..00000000 --- a/prism-examples/leader/asynchronous/leader3.pctl +++ /dev/null @@ -1,11 +0,0 @@ -// only one leader is elected -(s1=4?1:0) + (s2=4?1:0) + (s3=4?1:0)<=1 -// with probability 1 eventually a leader is elected -P>=1 [ true U (s1=4 | s2=4 | s3=4) ] -// min/max probability leader is elected within K steps -const int K; -Pmin=?[ true U<=K (s1=4 | s2=4 | s3=4) ] -Pmax=?[ true U<=K (s1=4 | s2=4 | s3=4) ] -// the min/max expected time to elect a leader -Rmin=?[ F (s1=4 | s2=4 | s3=4) ] -Rmax=?[ F (s1=4 | s2=4 | s3=4) ] diff --git a/prism-examples/leader/asynchronous/leader4.pctl b/prism-examples/leader/asynchronous/leader4.pctl deleted file mode 100644 index 3110d06e..00000000 --- a/prism-examples/leader/asynchronous/leader4.pctl +++ /dev/null @@ -1,11 +0,0 @@ -// only one leader is elected. -(s1=4?1:0) + (s2=4?1:0) + (s3=4?1:0) + (s4=4?1:0)<=1 -// with probability 1 eventually a leader is elected -P>=1 [ true U (s1=4 | s2=4 | s3=4 | s4=4) ] -// min/max probability leader is elected within K steps -const int K; -Pmin=?[ true U<=K (s1=4 | s2=4 | s3=4 | s4=4) ] -Pmax=?[ true U<=K (s1=4 | s2=4 | s3=4 | s4=4) ] -// min/max expected time to elect a leader -Rmin=?[ F (s1=4 | s2=4 | s3=4 | s4=4) ] -Rmax=?[ F (s1=4 | s2=4 | s3=4 | s4=4) ] diff --git a/prism-examples/leader/asynchronous/leader5.pctl b/prism-examples/leader/asynchronous/leader5.pctl deleted file mode 100644 index 12b34b7d..00000000 --- a/prism-examples/leader/asynchronous/leader5.pctl +++ /dev/null @@ -1,11 +0,0 @@ -// only one leader is elected. -(s1=4?1:0) + (s2=4?1:0) + (s3=4?1:0) + (s4=4?1:0) + (s5=4?1:0)<=1 -// with probability 1 eventually a leader is elected -P>=1 [ true U (s1=4 | s2=4 | s3=4 | s4=4 | s5=4) ] -// min/max probability leader is elected within K steps -const int K; -Pmin=?[ true U<=K (s1=4 | s2=4 | s3=4 | s4=4 | s5=4) ] -Pmax=?[ true U<=K (s1=4 | s2=4 | s3=4 | s4=4 | s5=4) ] -// min/max expected time to elect a leader -Rmin=?[ F (s1=4 | s2=4 | s3=4 | s4=4 | s5=4) ] -Rmax=?[ F (s1=4 | s2=4 | s3=4 | s4=4 | s5=4) ] diff --git a/prism-examples/leader/asynchronous/leader6.pctl b/prism-examples/leader/asynchronous/leader6.pctl deleted file mode 100644 index 59506f05..00000000 --- a/prism-examples/leader/asynchronous/leader6.pctl +++ /dev/null @@ -1,11 +0,0 @@ -// only one leader is elected. -(s1=4?1:0) + (s2=4?1:0) + (s3=4?1:0) + (s4=4?1:0) + (s5=4?1:0) + (s6=4?1:0)<=1 -// with probability 1 eventually a leader is elected -P>=1 [ true U (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4) ] -// min/max probability leader is elected within K steps -const int K; -Pmin=?[ true U<=K (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4) ] -Pmax=?[ true U<=K (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4) ] -// min/max expected time to elect a leader -Rmin=?[ F (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4) ] -Rmax=?[ F (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4) ] diff --git a/prism-examples/leader/asynchronous/leader7.pctl b/prism-examples/leader/asynchronous/leader7.pctl deleted file mode 100644 index a0445821..00000000 --- a/prism-examples/leader/asynchronous/leader7.pctl +++ /dev/null @@ -1,11 +0,0 @@ -// only one leader is elected. -(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)<=1 -// with probability 1 eventually a leader is elected -P>=1 [ true U (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4) ] -// min/max probability leader is elected within K steps -const int K; -Pmin=?[ true U<=K (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4) ] -Pmax=?[ true U<=K (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4) ] -// min/max expected time to elect a leader -Rmin=?[ F (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4) ] -Rmax=?[ F (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4) ] diff --git a/prism-examples/leader/asynchronous/leader8.pctl b/prism-examples/leader/asynchronous/leader8.pctl deleted file mode 100644 index 1de47904..00000000 --- a/prism-examples/leader/asynchronous/leader8.pctl +++ /dev/null @@ -1,11 +0,0 @@ -// only one leader is elected. -(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) + (s8=4?1:0)<=1 -// with probability 1 eventually a leader is elected -P>=1 [ true U (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4) ] -// min/max probability leader is elected within K steps -const int K; -Pmin=?[ true U<=K (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4) ] -Pmax=?[ true U<=K (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4) ] -// min/max expected time to elect a leader -Rmin=?[ F (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4) ] -Rmax=?[ F (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4) ] diff --git a/prism-examples/leader/asynchronous/leader9.pctl b/prism-examples/leader/asynchronous/leader9.pctl deleted file mode 100644 index f7b2c555..00000000 --- a/prism-examples/leader/asynchronous/leader9.pctl +++ /dev/null @@ -1,11 +0,0 @@ -// only one leader is elected. -(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) + (s8=4?1:0) + (s9=4?1:0)<=1 -// with probability 1 eventually a leader is elected -P>=1 [ true U (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4 | s9=4) ] -// min/max probability leader is elected within K steps -const int K; -Pmin=?[ true U<=K (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4 | s9=4) ] -Pmax=?[ true U<=K (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4 | s9=4) ] -// min/max expected time to elect a leader -Rmin=?[ F (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4 | s9=4) ] -Rmax=?[ F (s1=4 | s2=4 | s3=4 | s4=4 | s5=4 | s6=4 | s7=4 | s8=4 | s9=4) ]