Rabin: tidy up.

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

prism-examples/rabin/.autopp

@@ -4,6 +4,4 @@ foreach N ( 3 4 5 6 8 10 12 )
 	echo "Generating for N=$N"
 	prismpp .rabinN.nm.pp $N >! rabin$N.nm
 	unix2dos rabin$N.nm
-	prismpp .rabinN.pctl.pp $N >! rabin$N.pctl
-	unix2dos rabin$N.pctl
 end

prism-examples/rabin/.rabinN.nm.pp

@@ -4,7 +4,7 @@
 // with global variables to remove sychronization 
 // gxn/dxp 02/02/00
 
-nondeterministic
+mdp
 
 // size of shared counter
 const int K = #K#; // 4+ceil(log_2 N)
@@ -58,3 +58,14 @@ endmodule
 // construct further modules through renaming
 #for i=2:N#
 module process#i# = process1 [p1=p#i#, b1=b#i#, r1=r#i#] endmodule
#end#
+
+// formulas/labels for use in properties:
+
+// number of processes in critical section
+formula num_procs_in_crit = #+ i=1:N#(p#i#=2?1:0)#end#;
+
+// one of the processes is trying
+label "one_trying" = #| i=1:N#p#i#=1#end#;
+
+// one of the processes is in the critical section
+label "one_critical" = #| i=1:N#p#i#=2#end#;

prism-examples/rabin/.rabinN.pctl.pp

@@ -1,8 +0,0 @@
-#const N#
-label "one_trying" = #| i=1:N#p#i#=1#end#;
label "one_critical" = #| i=1:N#p#i#=2#end#;
-
-// Mutual exclusion
-#+ i=1:N#(p#i#=2?1:0)#end# <= 1
-
-// Liveness: If a process is trying, then eventually a process enters the critical section
-"one_trying" => P>=1 [ true U "one_critical" ]

prism-examples/rabin/auto

@@ -1,9 +1,9 @@
 #!/bin/csh
 
-prism rabin3.nm rabin3.pctl -fair
-prism rabin4.nm rabin4.pctl -fair
-prism rabin5.nm rabin5.pctl -fair
-prism rabin6.nm rabin6.pctl -fair
-prism rabin8.nm rabin8.pctl -fair
-prism rabin10.nm rabin10.pctl -fair
-prism rabin12.nm rabin12.pctl -fair
+prism rabin3.nm rabin.pctl -fair
+prism rabin4.nm rabin.pctl -fair
+prism rabin5.nm rabin.pctl -fair
+prism rabin6.nm rabin.pctl -fair
+prism rabin8.nm rabin.pctl -fair
+prism rabin10.nm rabin.pctl -fair
+prism rabin12.nm rabin.pctl -fair

prism-examples/rabin/rabin3.pctl → prism-examples/rabin/rabin.pctl

@@ -1,8 +1,5 @@
-label "one_trying" = p1=1|p2=1|p3=1;
-label "one_critical" = p1=2|p2=2|p3=2;
-
 // Mutual exclusion
-(p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0) <= 1
+num_procs_in_crit <= 1
 
 // Liveness: If a process is trying, then eventually a process enters the critical section
 "one_trying" => P>=1 [ true U "one_critical" ]

prism-examples/rabin/rabin10.nm

@@ -2,7 +2,7 @@
 // with global variables to remove sychronization 
 // gxn/dxp 02/02/00
 
-nondeterministic
+mdp
 
 // size of shared counter
 const int K = 8; // 4+ceil(log_2 N)
@@ -69,3 +69,14 @@ module process7 = process1 [p1=p7, b1=b7, r1=r7] endmodule
 module process8 = process1 [p1=p8, b1=b8, r1=r8] endmodule
 module process9 = process1 [p1=p9, b1=b9, r1=r9] endmodule
 module process10 = process1 [p1=p10, b1=b10, r1=r10] endmodule
+
+// formulas/labels for use in properties:
+
+// number of processes in critical section
+formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0)+(p7=2?1:0)+(p8=2?1:0)+(p9=2?1:0)+(p10=2?1:0);
+
+// one of the processes is trying
+label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1|p8=1|p9=1|p10=1;
+
+// one of the processes is in the critical section
+label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2;

prism-examples/rabin/rabin10.pctl

@@ -1,8 +0,0 @@
-label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1|p8=1|p9=1|p10=1;
-label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2;
-
-// Mutual exclusion
-(p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0)+(p7=2?1:0)+(p8=2?1:0)+(p9=2?1:0)+(p10=2?1:0) <= 1
-
-// Liveness: If a process is trying, then eventually a process enters the critical section
-"one_trying" => P>=1 [ true U "one_critical" ]

prism-examples/rabin/rabin12.nm

@@ -2,7 +2,7 @@
 // with global variables to remove sychronization 
 // gxn/dxp 02/02/00
 
-nondeterministic
+mdp
 
 // size of shared counter
 const int K = 8; // 4+ceil(log_2 N)
@@ -71,3 +71,14 @@ module process9 = process1 [p1=p9, b1=b9, r1=r9] endmodule
 module process10 = process1 [p1=p10, b1=b10, r1=r10] endmodule
 module process11 = process1 [p1=p11, b1=b11, r1=r11] endmodule
 module process12 = process1 [p1=p12, b1=b12, r1=r12] endmodule
+
+// formulas/labels for use in properties:
+
+// number of processes in critical section
+formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0)+(p7=2?1:0)+(p8=2?1:0)+(p9=2?1:0)+(p10=2?1:0)+(p11=2?1:0)+(p12=2?1:0);
+
+// one of the processes is trying
+label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1|p8=1|p9=1|p10=1|p11=1|p12=1;
+
+// one of the processes is in the critical section
+label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2|p11=2|p12=2;

prism-examples/rabin/rabin12.pctl

@@ -1,8 +0,0 @@
-label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1|p8=1|p9=1|p10=1|p11=1|p12=1;
-label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2|p11=2|p12=2;
-
-// Mutual exclusion
-(p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0)+(p7=2?1:0)+(p8=2?1:0)+(p9=2?1:0)+(p10=2?1:0)+(p11=2?1:0)+(p12=2?1:0) <= 1
-
-// Liveness: If a process is trying, then eventually a process enters the critical section
-"one_trying" => P>=1 [ true U "one_critical" ]

prism-examples/rabin/rabin3.nm

@@ -2,7 +2,7 @@
 // with global variables to remove sychronization 
 // gxn/dxp 02/02/00
 
-nondeterministic
+mdp
 
 // size of shared counter
 const int K = 6; // 4+ceil(log_2 N)
@@ -60,3 +60,14 @@ endmodule
 // construct further modules through renaming
 module process2 = process1 [p1=p2, b1=b2, r1=r2] endmodule
 module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule
+
+// formulas/labels for use in properties:
+
+// number of processes in critical section
+formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0);
+
+// one of the processes is trying
+label "one_trying" = p1=1|p2=1|p3=1;
+
+// one of the processes is in the critical section
+label "one_critical" = p1=2|p2=2|p3=2;

prism-examples/rabin/rabin4.nm

@@ -2,7 +2,7 @@
 // with global variables to remove sychronization 
 // gxn/dxp 02/02/00
 
-nondeterministic
+mdp
 
 // size of shared counter
 const int K = 6; // 4+ceil(log_2 N)
@@ -61,3 +61,14 @@ endmodule
 module process2 = process1 [p1=p2, b1=b2, r1=r2] endmodule
 module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule
 module process4 = process1 [p1=p4, b1=b4, r1=r4] endmodule
+
+// formulas/labels for use in properties:
+
+// number of processes in critical section
+formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0);
+
+// one of the processes is trying
+label "one_trying" = p1=1|p2=1|p3=1|p4=1;
+
+// one of the processes is in the critical section
+label "one_critical" = p1=2|p2=2|p3=2|p4=2;

prism-examples/rabin/rabin4.pctl

@@ -1,8 +0,0 @@
-label "one_trying" = p1=1|p2=1|p3=1|p4=1;
-label "one_critical" = p1=2|p2=2|p3=2|p4=2;
-
-// Mutual exclusion
-(p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0) <= 1
-
-// Liveness: If a process is trying, then eventually a process enters the critical section
-"one_trying" => P>=1 [ true U "one_critical" ]

prism-examples/rabin/rabin5.nm

@@ -2,7 +2,7 @@
 // with global variables to remove sychronization 
 // gxn/dxp 02/02/00
 
-nondeterministic
+mdp
 
 // size of shared counter
 const int K = 7; // 4+ceil(log_2 N)
@@ -63,3 +63,14 @@ module process2 = process1 [p1=p2, b1=b2, r1=r2] endmodule
 module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule
 module process4 = process1 [p1=p4, b1=b4, r1=r4] endmodule
 module process5 = process1 [p1=p5, b1=b5, r1=r5] endmodule
+
+// formulas/labels for use in properties:
+
+// number of processes in critical section
+formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0);
+
+// one of the processes is trying
+label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1;
+
+// one of the processes is in the critical section
+label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2;

prism-examples/rabin/rabin5.pctl

@@ -1,8 +0,0 @@
-label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1;
-label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2;
-
-// Mutual exclusion
-(p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0) <= 1
-
-// Liveness: If a process is trying, then eventually a process enters the critical section
-"one_trying" => P>=1 [ true U "one_critical" ]

prism-examples/rabin/rabin6.nm

@@ -2,7 +2,7 @@
 // with global variables to remove sychronization 
 // gxn/dxp 02/02/00
 
-nondeterministic
+mdp
 
 // size of shared counter
 const int K = 7; // 4+ceil(log_2 N)
@@ -64,3 +64,14 @@ module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule
 module process4 = process1 [p1=p4, b1=b4, r1=r4] endmodule
 module process5 = process1 [p1=p5, b1=b5, r1=r5] endmodule
 module process6 = process1 [p1=p6, b1=b6, r1=r6] endmodule
+
+// formulas/labels for use in properties:
+
+// number of processes in critical section
+formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0);
+
+// one of the processes is trying
+label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1;
+
+// one of the processes is in the critical section
+label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2;

prism-examples/rabin/rabin6.pctl

@@ -1,8 +0,0 @@
-label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1;
-label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2;
-
-// Mutual exclusion
-(p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0) <= 1
-
-// Liveness: If a process is trying, then eventually a process enters the critical section
-"one_trying" => P>=1 [ true U "one_critical" ]

prism-examples/rabin/rabin8.nm

@@ -2,7 +2,7 @@
 // with global variables to remove sychronization 
 // gxn/dxp 02/02/00
 
-nondeterministic
+mdp
 
 // size of shared counter
 const int K = 7; // 4+ceil(log_2 N)
@@ -66,3 +66,14 @@ module process5 = process1 [p1=p5, b1=b5, r1=r5] endmodule
 module process6 = process1 [p1=p6, b1=b6, r1=r6] endmodule
 module process7 = process1 [p1=p7, b1=b7, r1=r7] endmodule
 module process8 = process1 [p1=p8, b1=b8, r1=r8] endmodule
+
+// formulas/labels for use in properties:
+
+// number of processes in critical section
+formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0)+(p7=2?1:0)+(p8=2?1:0);
+
+// one of the processes is trying
+label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1|p8=1;
+
+// one of the processes is in the critical section
+label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2;

prism-examples/rabin/rabin8.pctl

@@ -1,8 +0,0 @@
-label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1|p8=1;
-label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2;
-
-// Mutual exclusion
-(p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0)+(p7=2?1:0)+(p8=2?1:0) <= 1
-
-// Liveness: If a process is trying, then eventually a process enters the critical section
-"one_trying" => P>=1 [ true U "one_critical" ]