improvements to async leader

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@869 bbc10eb1-c90d-0410-af57-cb519fbb1720

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

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#<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
+	[p#N#1] (s1=3) & (receive1=0) -> (p1'=p#N#) & (receive1'=1);
+	// receive counter
+	[c#N#1] (s1=3) & (receive1=1) & (c#N#<N-1) -> (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#;
+

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

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" ]

prism-examples/leader/asynchronous/leader10.pctl

@@ -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) ]

prism-examples/leader/asynchronous/leader3.pctl

@@ -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) ]

prism-examples/leader/asynchronous/leader4.pctl

@@ -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) ]

prism-examples/leader/asynchronous/leader5.pctl

@@ -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) ]

prism-examples/leader/asynchronous/leader6.pctl

@@ -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) ]

prism-examples/leader/asynchronous/leader7.pctl

@@ -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) ]

prism-examples/leader/asynchronous/leader8.pctl

@@ -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) ]

prism-examples/leader/asynchronous/leader9.pctl

@@ -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) ]