Added consensus to examples.

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

prism-examples/consensus/.autopp

@@ -0,0 +1,8 @@
+#!/bin/csh
+
+foreach N ( 2 4 6 8 10 )
+  echo "Generating for N=$N"
+  prismpp .coinN.nm.pp $N >! coin"$N".nm
+  unix2dos coin"$N".nm
+end
+

prism-examples/consensus/.coinN.nm.pp

@@ -0,0 +1,63 @@
+#const N#
+// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] 
+// gxn/dxp 20/11/00
+
+mdp
+
+// constants
+const int N=#N#;
+const int K;
+const int range = 2*(K+1)*N;
+const int counter_init = (K+1)*N;
+const int left = N;
+const int right = 2*(K+1)*N - N;
+
+// shared coin
+global counter : [0..range] init counter_init;
+
+module process1
+	
+	// program counter
+	pc1 : [0..3];
+	// 0 - flip
+	// 1 - write 
+	// 2 - check
+	// 3 - finished
+	
+	// local coin
+	coin1 : [0..1];	
+
+	// flip coin
+	[] (pc1=0)  -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1);
+	// write tails -1  (reset coin to add regularity)
+	[] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0);
+	// write heads +1 (reset coin to add regularity)
+	[] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0);
+	// check
+	// decide tails
+	[] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0);
+	// decide heads
+	[] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1);
+	// flip again
+	[] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0);
+	// loop (all loop together when done)
+	[done] (pc1=3) -> (pc1'=3);
+
+endmodule
+
+// construct remaining processes through renaming
+#for i=2:N#
+module process#i# = process1[pc1=pc#i#,coin1=coin#i#] endmodule
+#end#
+
+// labels
+label "finished" =#& i=1:N# pc#i#=3 #end#;
+label "all_coins_equal_0" =#& i=1:N# coin#i#=0 #end#;
+label "all_coins_equal_1" =#& i=1:N# coin#i#=1 #end#;
+label "agree" =#& i=1:N-1# coin#i#=coin#i+1# #end#;
+
+// rewards
+rewards "steps"
+	true : 1;
+endrewards
+

prism-examples/consensus/README

@@ -0,0 +1,11 @@
+This case study is based on the shared coin protocol from the randomised consensus algorithm of Aspnes and Herlihy [AH90].
+
+For more information, see: http://www.prismmodelchecker.org/casestudies/consensus_prism.php
+
+=====================================================================================
+
+[AH90]
+J. Aspnes and M. Herlihy.
+Fast randomized consensus using shared memory.
+Journal of Algorithms, 15(1):441-460, 1990.
+

prism-examples/consensus/auto

@@ -0,0 +1,16 @@
+#!/bin/csh
+
+prism coin2.nm coin.pctl -const K=2,k=10 -m
+prism coin2.nm coin.pctl -const K=4,k=10 -m
+#prism coin2.nm coin.pctl -const K=8,k=10 -m -maxiters 100000
+#prism coin2.nm coin.pctl -const K=16,k=10 -m -maxiters 100000
+
+prism coin4.nm coin.pctl -const K=2,k=10 -m
+prism coin4.nm coin.pctl -const K=4,k=10 -m
+
+#prism coin6.nm coin.pctl -const K=2,k=10 -m
+
+#prism coin8.nm coin.pctl -const K=2,k=10 -m
+
+#prism coin10.nm coin.pctl -const K=2,k=10 -m
+

prism-examples/consensus/coin.pctl

@@ -0,0 +1,25 @@
+const int k;
+
+// C1 (with probability 1, all N processes finish the protocol)
+// (needs fairness)
+P>=1 [ F "finished" ]
+
+// C2 (minimum probability that the protocol finishes with all coins equal to v) (v=1,2)
+// (needs fairness)
+// Results are same for v=1 and v=2 by symmetry
+// Analytic bound is (K-1)/(2*K)
+Pmin=? [ F "finished"&"all_coins_equal_0" ]
+Pmin=? [ F "finished"&"all_coins_equal_1" ]
+
+// Max probability of finishing protocol with coins not all equal
+// (no fairness needed since max. probabilities)
+Pmax=? [ F "finished"&!"agree" ]
+
+// Min/max probability of finishing within k steps
+Pmin=? [ F<=k "finished" ]
+Pmax=? [ F<=k "finished" ]
+
+// Min/max expected steps to finish
+R{"steps"}min=? [ F "finished" ]
+R{"steps"}max=? [ F "finished" ]
+

prism-examples/consensus/coin10.nm

@@ -0,0 +1,68 @@
+// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] 
+// gxn/dxp 20/11/00
+
+mdp
+
+// constants
+const int N=10;
+const int K;
+const int range = 2*(K+1)*N;
+const int counter_init = (K+1)*N;
+const int left = N;
+const int right = 2*(K+1)*N - N;
+
+// shared coin
+global counter : [0..range] init counter_init;
+
+module process1
+	
+	// program counter
+	pc1 : [0..3];
+	// 0 - flip
+	// 1 - write 
+	// 2 - check
+	// 3 - finished
+	
+	// local coin
+	coin1 : [0..1];	
+
+	// flip coin
+	[] (pc1=0)  -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1);
+	// write tails -1  (reset coin to add regularity)
+	[] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0);
+	// write heads +1 (reset coin to add regularity)
+	[] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0);
+	// check
+	// decide tails
+	[] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0);
+	// decide heads
+	[] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1);
+	// flip again
+	[] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0);
+	// loop (all loop together when done)
+	[done] (pc1=3) -> (pc1'=3);
+
+endmodule
+
+// construct remaining processes through renaming
+module process2 = process1[pc1=pc2,coin1=coin2] endmodule
+module process3 = process1[pc1=pc3,coin1=coin3] endmodule
+module process4 = process1[pc1=pc4,coin1=coin4] endmodule
+module process5 = process1[pc1=pc5,coin1=coin5] endmodule
+module process6 = process1[pc1=pc6,coin1=coin6] endmodule
+module process7 = process1[pc1=pc7,coin1=coin7] endmodule
+module process8 = process1[pc1=pc8,coin1=coin8] endmodule
+module process9 = process1[pc1=pc9,coin1=coin9] endmodule
+module process10 = process1[pc1=pc10,coin1=coin10] endmodule
+
+// labels
+label "finished" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & pc5=3 & pc6=3 & pc7=3 & pc8=3 & pc9=3 & pc10=3 ;
+label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 & coin5=0 & coin6=0 & coin7=0 & coin8=0 & coin9=0 & coin10=0 ;
+label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1 & coin7=1 & coin8=1 & coin9=1 & coin10=1 ;
+label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 & coin4=coin5 & coin5=coin6 & coin6=coin7 & coin7=coin8 & coin8=coin9 & coin9=coin10 ;
+
+// rewards
+rewards "steps"
+	true : 1;
+endrewards
+

prism-examples/consensus/coin2.nm

@@ -0,0 +1,60 @@
+// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] 
+// gxn/dxp 20/11/00
+
+mdp
+
+// constants
+const int N=2;
+const int K;
+const int range = 2*(K+1)*N;
+const int counter_init = (K+1)*N;
+const int left = N;
+const int right = 2*(K+1)*N - N;
+
+// shared coin
+global counter : [0..range] init counter_init;
+
+module process1
+	
+	// program counter
+	pc1 : [0..3];
+	// 0 - flip
+	// 1 - write 
+	// 2 - check
+	// 3 - finished
+	
+	// local coin
+	coin1 : [0..1];	
+
+	// flip coin
+	[] (pc1=0)  -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1);
+	// write tails -1  (reset coin to add regularity)
+	[] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0);
+	// write heads +1 (reset coin to add regularity)
+	[] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0);
+	// check
+	// decide tails
+	[] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0);
+	// decide heads
+	[] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1);
+	// flip again
+	[] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0);
+	// loop (all loop together when done)
+	[done] (pc1=3) -> (pc1'=3);
+
+endmodule
+
+// construct remaining processes through renaming
+module process2 = process1[pc1=pc2,coin1=coin2] endmodule
+
+// labels
+label "finished" = pc1=3 & pc2=3 ;
+label "all_coins_equal_0" = coin1=0 & coin2=0 ;
+label "all_coins_equal_1" = coin1=1 & coin2=1 ;
+label "agree" = coin1=coin2 ;
+
+// rewards
+rewards "steps"
+	true : 1;
+endrewards
+

prism-examples/consensus/coin4.nm

@@ -0,0 +1,62 @@
+// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] 
+// gxn/dxp 20/11/00
+
+mdp
+
+// constants
+const int N=4;
+const int K;
+const int range = 2*(K+1)*N;
+const int counter_init = (K+1)*N;
+const int left = N;
+const int right = 2*(K+1)*N - N;
+
+// shared coin
+global counter : [0..range] init counter_init;
+
+module process1
+	
+	// program counter
+	pc1 : [0..3];
+	// 0 - flip
+	// 1 - write 
+	// 2 - check
+	// 3 - finished
+	
+	// local coin
+	coin1 : [0..1];	
+
+	// flip coin
+	[] (pc1=0)  -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1);
+	// write tails -1  (reset coin to add regularity)
+	[] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0);
+	// write heads +1 (reset coin to add regularity)
+	[] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0);
+	// check
+	// decide tails
+	[] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0);
+	// decide heads
+	[] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1);
+	// flip again
+	[] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0);
+	// loop (all loop together when done)
+	[done] (pc1=3) -> (pc1'=3);
+
+endmodule
+
+// construct remaining processes through renaming
+module process2 = process1[pc1=pc2,coin1=coin2] endmodule
+module process3 = process1[pc1=pc3,coin1=coin3] endmodule
+module process4 = process1[pc1=pc4,coin1=coin4] endmodule
+
+// labels
+label "finished" = pc1=3 & pc2=3 & pc3=3 & pc4=3 ;
+label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 ;
+label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 ;
+label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 ;
+
+// rewards
+rewards "steps"
+	true : 1;
+endrewards
+

prism-examples/consensus/coin6.nm

@@ -0,0 +1,64 @@
+// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] 
+// gxn/dxp 20/11/00
+
+mdp
+
+// constants
+const int N=6;
+const int K;
+const int range = 2*(K+1)*N;
+const int counter_init = (K+1)*N;
+const int left = N;
+const int right = 2*(K+1)*N - N;
+
+// shared coin
+global counter : [0..range] init counter_init;
+
+module process1
+	
+	// program counter
+	pc1 : [0..3];
+	// 0 - flip
+	// 1 - write 
+	// 2 - check
+	// 3 - finished
+	
+	// local coin
+	coin1 : [0..1];	
+
+	// flip coin
+	[] (pc1=0)  -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1);
+	// write tails -1  (reset coin to add regularity)
+	[] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0);
+	// write heads +1 (reset coin to add regularity)
+	[] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0);
+	// check
+	// decide tails
+	[] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0);
+	// decide heads
+	[] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1);
+	// flip again
+	[] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0);
+	// loop (all loop together when done)
+	[done] (pc1=3) -> (pc1'=3);
+
+endmodule
+
+// construct remaining processes through renaming
+module process2 = process1[pc1=pc2,coin1=coin2] endmodule
+module process3 = process1[pc1=pc3,coin1=coin3] endmodule
+module process4 = process1[pc1=pc4,coin1=coin4] endmodule
+module process5 = process1[pc1=pc5,coin1=coin5] endmodule
+module process6 = process1[pc1=pc6,coin1=coin6] endmodule
+
+// labels
+label "finished" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & pc5=3 & pc6=3 ;
+label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 & coin5=0 & coin6=0 ;
+label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1 ;
+label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 & coin4=coin5 & coin5=coin6 ;
+
+// rewards
+rewards "steps"
+	true : 1;
+endrewards
+

prism-examples/consensus/coin8.nm

@@ -0,0 +1,66 @@
+// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] 
+// gxn/dxp 20/11/00
+
+mdp
+
+// constants
+const int N=8;
+const int K;
+const int range = 2*(K+1)*N;
+const int counter_init = (K+1)*N;
+const int left = N;
+const int right = 2*(K+1)*N - N;
+
+// shared coin
+global counter : [0..range] init counter_init;
+
+module process1
+	
+	// program counter
+	pc1 : [0..3];
+	// 0 - flip
+	// 1 - write 
+	// 2 - check
+	// 3 - finished
+	
+	// local coin
+	coin1 : [0..1];	
+
+	// flip coin
+	[] (pc1=0)  -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1);
+	// write tails -1  (reset coin to add regularity)
+	[] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0);
+	// write heads +1 (reset coin to add regularity)
+	[] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0);
+	// check
+	// decide tails
+	[] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0);
+	// decide heads
+	[] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1);
+	// flip again
+	[] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0);
+	// loop (all loop together when done)
+	[done] (pc1=3) -> (pc1'=3);
+
+endmodule
+
+// construct remaining processes through renaming
+module process2 = process1[pc1=pc2,coin1=coin2] endmodule
+module process3 = process1[pc1=pc3,coin1=coin3] endmodule
+module process4 = process1[pc1=pc4,coin1=coin4] endmodule
+module process5 = process1[pc1=pc5,coin1=coin5] endmodule
+module process6 = process1[pc1=pc6,coin1=coin6] endmodule
+module process7 = process1[pc1=pc7,coin1=coin7] endmodule
+module process8 = process1[pc1=pc8,coin1=coin8] endmodule
+
+// labels
+label "finished" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & pc5=3 & pc6=3 & pc7=3 & pc8=3 ;
+label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 & coin5=0 & coin6=0 & coin7=0 & coin8=0 ;
+label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1 & coin7=1 & coin8=1 ;
+label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 & coin4=coin5 & coin5=coin6 & coin6=coin7 & coin7=coin8 ;
+
+// rewards
+rewards "steps"
+	true : 1;
+endrewards
+

prism-examples/wlan/auto

@@ -4,9 +4,9 @@ prism wlan0.nm wlan.pctl -const TRANS_TIME_MAX=10,k=2
 prism wlan1.nm wlan.pctl -const TRANS_TIME_MAX=10,k=2
 prism wlan2.nm wlan.pctl -const TRANS_TIME_MAX=10,k=2
 prism wlan3.nm wlan.pctl -const TRANS_TIME_MAX=10,k=2
-prism wlan4.nm wlan.pctl -const TRANS_TIME_MAX=10,k=2
-prism wlan5.nm wlan.pctl -const TRANS_TIME_MAX=10,k=2
-prism wlan6.nm wlan.pctl -const TRANS_TIME_MAX=10,k=2
+#prism wlan4.nm wlan.pctl -const TRANS_TIME_MAX=10,k=2
+#prism wlan5.nm wlan.pctl -const TRANS_TIME_MAX=10,k=2
+#prism wlan6.nm wlan.pctl -const TRANS_TIME_MAX=10,k=2
 
 
 # probability collide
@@ -14,16 +14,16 @@ prism wlan0_collide.nm wlan_collide.pctl -const COL=2,TRANS_TIME_MAX=10,k=2
 prism wlan1_collide.nm wlan_collide.pctl -const COL=2,TRANS_TIME_MAX=10,k=2
 prism wlan2_collide.nm wlan_collide.pctl -const COL=2,TRANS_TIME_MAX=10,k=2
 prism wlan3_collide.nm wlan_collide.pctl -const COL=2,TRANS_TIME_MAX=10,k=2
-prism wlan4_collide.nm wlan_collide.pctl -const COL=2,TRANS_TIME_MAX=10,k=2
-prism wlan5_collide.nm wlan_collide.pctl -const COL=2,TRANS_TIME_MAX=10,k=2
-prism wlan6_collide.nm wlan_collide.pctl -const COL=2,TRANS_TIME_MAX=10,k=2
+#prism wlan4_collide.nm wlan_collide.pctl -const COL=2,TRANS_TIME_MAX=10,k=2
+#prism wlan5_collide.nm wlan_collide.pctl -const COL=2,TRANS_TIME_MAX=10,k=2
+#prism wlan6_collide.nm wlan_collide.pctl -const COL=2,TRANS_TIME_MAX=10,k=2
 
 # time bounded
 prism wlan0_time_bounded.nm wlan_time_bounded.pctl -const TRANS_TIME_MAX=10,DEADLINE=100 -nopre -m -prop 3
 prism wlan1_time_bounded.nm wlan_time_bounded.pctl -const TRANS_TIME_MAX=10,DEADLINE=100 -nopre -m -prop 3
 prism wlan2_time_bounded.nm wlan_time_bounded.pctl -const TRANS_TIME_MAX=10,DEADLINE=100 -nopre -m -prop 3
 prism wlan3_time_bounded.nm wlan_time_bounded.pctl -const TRANS_TIME_MAX=10,DEADLINE=100 -nopre -m -prop 3
-prism wlan4_time_bounded.nm wlan_time_bounded.pctl -const TRANS_TIME_MAX=10,DEADLINE=100 -nopre -m -prop 3
-prism wlan5_time_bounded.nm wlan_time_bounded.pctl -const TRANS_TIME_MAX=10,DEADLINE=100 -nopre -m -prop 3
-prism wlan6_time_bounded.nm wlan_time_bounded.pctl -const TRANS_TIME_MAX=10,DEADLINE=100 -nopre -m -prop 3
+#prism wlan4_time_bounded.nm wlan_time_bounded.pctl -const TRANS_TIME_MAX=10,DEADLINE=100 -nopre -m -prop 3
+#prism wlan5_time_bounded.nm wlan_time_bounded.pctl -const TRANS_TIME_MAX=10,DEADLINE=100 -nopre -m -prop 3
+#prism wlan6_time_bounded.nm wlan_time_bounded.pctl -const TRANS_TIME_MAX=10,DEADLINE=100 -nopre -m -prop 3