Added pp files to Beauquier.

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

prism-examples/self-stabilisation/beauquier/.autopp

@@ -0,0 +1,7 @@
+#!/bin/csh
+
+foreach N ( 3 5 7 9 11 )
+	echo "Generating for N=$N"
+	prismpp .beauquierN.nm.pp $N >! beauquier$N.nm
+	unix2dos beauquier$N.nm
+end

prism-examples/self-stabilisation/beauquier/.beauquierN.nm.pp

@@ -0,0 +1,35 @@
+#const N#
+// self stabilisation algorithm Beauquier, Gradinariu and Johnen
+// gxn/dxp 18/07/02
+
+mdp
+
+// module of process 1
+module process1
+	
+	d1 : bool; // probabilistic variable
+	p1 : bool; // deterministic variable
+	
+	[] d1=d#N# &  p1=p#N# -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1);
+	[] d1=d#N# & !p1=p#N# -> (d1'=!d1);
+	
+endmodule
+
+// add further processes through renaming
+#for i=2:N#
+module process#i# = process1 [ p1=p#i#, p#N#=p#i-1#, d1=d#i#, d#N#=d#i-1# ] endmodule
+#end#
+
+// cost - 1 in each state (expected steps)
+rewards "steps"
+	true : 1;
+endrewards
+
+// initial states - any state with more than 1 token, that is all states
+init
+	true
+endinit
+
+// formula, for use in properties: number of tokens
+formula num_tokens = #+ i=1:N#(p#i#=p#func(mod, i, N)+1#?1:0)#end#;
+

prism-examples/self-stabilisation/beauquier/beauquier11.nm

@@ -1,8 +1,7 @@
 // self stabilisation algorithm Beauquier, Gradinariu and Johnen
 // gxn/dxp 18/07/02
 
-// model is an mdp
-nondeterministic
+mdp
 
 // module of process 1
 module process1
@@ -10,8 +9,8 @@ module process1
 	d1 : bool; // probabilistic variable
 	p1 : bool; // deterministic variable
 	
-	[] (d1=d11) &  (p1=p11) -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1);
-	[] (d1=d11) & !(p1=p11) -> (d1'=!d1);
+	[] d1=d11 &  p1=p11 -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1);
+	[] d1=d11 & !p1=p11 -> (d1'=!d1);
 	
 endmodule
 
@@ -28,7 +27,7 @@ module process10=process1[p1=p10,p11=p9, d1=d10,d11=d9] endmodule
 module process11 = process1 [ p1=p11, p11=p10, d1=d11, d11=d10 ] endmodule
 
 // cost - 1 in each state (expected steps)
-rewards
+rewards "steps"
 	true : 1;
 endrewards
 
@@ -38,4 +37,5 @@ init
 endinit
 
 // formula, for use in properties: number of tokens
-formula num_tokens = (p11=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)+(p9=p10?1:0)+(p10=p11?1:0);
+formula num_tokens = (p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)+(p9=p10?1:0)+(p10=p11?1:0)+(p11=p1?1:0);
+

prism-examples/self-stabilisation/beauquier/beauquier3.nm

@@ -1,8 +1,7 @@
 // self stabilisation algorithm Beauquier, Gradinariu and Johnen
 // gxn/dxp 18/07/02
 
-// model is an mdp
-nondeterministic
+mdp
 
 // module of process 1
 module process1
@@ -20,7 +19,7 @@ module process2 =process1[p1=p2 ,p3=p1, d1=d2 ,d3=d1] endmodule
 module process3 = process1 [ p1=p3, p3=p2, d1=d3, d3=d2 ] endmodule
 
 // cost - 1 in each state (expected steps)
-rewards
+rewards "steps"
 	true : 1;
 endrewards
 
@@ -29,5 +28,6 @@ init
 	true
 endinit
 
-// formula for use in properties: number of tokens
-formula num_tokens = (p3=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0);
+// formula, for use in properties: number of tokens
+formula num_tokens = (p1=p2?1:0)+(p2=p3?1:0)+(p3=p1?1:0);
+

prism-examples/self-stabilisation/beauquier/beauquier5.nm

@@ -1,8 +1,7 @@
 // self stabilisation algorithm Beauquier, Gradinariu and Johnen
 // gxn/dxp 18/07/02
 
-// model is an mdp
-nondeterministic
+mdp
 
 // module of process 1
 module process1
@@ -10,8 +9,8 @@ module process1
 	d1 : bool; // probabilistic variable
 	p1 : bool; // deterministic variable
 	
-	[] (d1=d5) &  (p1=p5) -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1);
-	[] (d1=d5) & !(p1=p5) -> (d1'=!d1);
+	[] d1=d5 &  p1=p5 -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1);
+	[] d1=d5 & !p1=p5 -> (d1'=!d1);
 	
 endmodule
 
@@ -22,7 +21,7 @@ module process4 =process1[p1=p4 ,p5=p3, d1=d4 ,d5=d3] endmodule
 module process5 = process1 [ p1=p5, p5=p4, d1=d5, d5=d4 ] endmodule
 
 // cost - 1 in each state (expected steps)
-rewards
+rewards "steps"
 	true : 1;
 endrewards
 
@@ -32,4 +31,5 @@ init
 endinit
 
 // formula, for use in properties: number of tokens
-formula num_tokens = (p5=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0);
+formula num_tokens = (p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p1?1:0);
+

prism-examples/self-stabilisation/beauquier/beauquier7.nm

@@ -1,8 +1,7 @@
 // self stabilisation algorithm Beauquier, Gradinariu and Johnen
 // gxn/dxp 18/07/02
 
-// model is an mdp
-nondeterministic
+mdp
 
 // module of process 1
 module process1
@@ -10,8 +9,8 @@ module process1
 	d1 : bool; // probabilistic variable
 	p1 : bool; // deterministic variable
 	
-	[] (d1=d7) &  (p1=p7) -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1);
-	[] (d1=d7) & !(p1=p7) -> (d1'=!d1);
+	[] d1=d7 &  p1=p7 -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1);
+	[] d1=d7 & !p1=p7 -> (d1'=!d1);
 	
 endmodule
 
@@ -24,7 +23,7 @@ module process6 =process1[p1=p6 ,p7=p5, d1=d6 ,d7=d5] endmodule
 module process7 = process1 [ p1=p7, p7=p6, d1=d7, d7=d6 ] endmodule
 
 // cost - 1 in each state (expected steps)
-rewards
+rewards "steps"
 	true : 1;
 endrewards
 
@@ -34,4 +33,5 @@ init
 endinit
 
 // formula, for use in properties: number of tokens
-formula num_tokens = (p7=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0);
+formula num_tokens = (p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p1?1:0);
+

prism-examples/self-stabilisation/beauquier/beauquier9.nm

@@ -1,8 +1,7 @@
 // self stabilisation algorithm Beauquier, Gradinariu and Johnen
 // gxn/dxp 18/07/02
 
-// model is an mdp
-nondeterministic
+mdp
 
 // module of process 1
 module process1
@@ -10,8 +9,8 @@ module process1
 	d1 : bool; // probabilistic variable
 	p1 : bool; // deterministic variable
 	
-	[] (d1=d9) &  (p1=p9) -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1);
-	[] (d1=d9) & !(p1=p9) -> (d1'=!d1);
+	[] d1=d9 &  p1=p9 -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1);
+	[] d1=d9 & !p1=p9 -> (d1'=!d1);
 	
 endmodule
 
@@ -26,7 +25,7 @@ module process8 =process1[p1=p8 ,p9=p7, d1=d8 ,d9=d7] endmodule
 module process9 = process1 [ p1=p9, p9=p8, d1=d9, d9=d8 ] endmodule
 
 // cost - 1 in each state (expected steps)
-rewards
+rewards "steps"
 	true : 1;
 endrewards
 
@@ -36,4 +35,5 @@ init
 endinit
 
 // formula, for use in properties: number of tokens
-formula num_tokens = (p9=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0);
+formula num_tokens = (p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)+(p9=p1?1:0);
+