finor fixes

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

prism-examples/rabin/modified/mod_rabin10.nm

@@ -0,0 +1,101 @@
+// N-processor mutual exclusion [Rab82]
+// with global variables to remove sychronization 
+// gxn/dxp 03/12/08
+
+// modified version to verify a variant of the bounded waiting property
+// namely the probability a process entries the critical sectiongiven it tries
+
+// note we have removed the self loops to allow the fairness constraints 
+// to be ignored during verification
+
+// split the drawing phase into two steps but is still atomic as no
+// other process can move one the first step has been made
+
+mdp
+
+// size of shared counter
+const int K = 8; // 4+ceil(log_2 N)
+
+// global variables (all modules can read and write)
+// c=0 critical section free
+// c=1 critical section not free
+// b current highest draw
+// r current round 
+
+global c : [0..1];
+global b : [0..K];
+global r : [1..2];
+
+// local variables: process i 
+// state: pi
+//  0 remainder
+//  1 trying
+//  2 critical section
+// current draw: bi
+// current round: ri
+
+// formula for process 1 drawing
+formula draw = p1=1 & (b<b1 | r!=r1);
+
+// formula to keep drawing phase atomic
+// (can onlymove if no process is drawing
+formula go = (draw2=0&draw3=0&draw4=0&draw5=0&draw6=0&draw7=0&draw8=0&draw9=0&draw10=0);
+
+module process1
+
+	p1 : [0..2];
+	b1 : [0..K];
+	r1 : [0..2];
+	draw1 : [0..1];
+
+	// remain in remainder
+	// [] go & p1=0 -> (p1'=0);
+	// enter trying
+	[] go & p1=0 -> (p1'=1);
+	// make a draw
+	[] go & draw & draw1=0 -> (draw1'=1);
+	[] draw1=1 -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) & (draw1'=0)
+	         + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) & (draw1'=0)
+	         + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) & (draw1'=0)
+	         + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) & (draw1'=0)
+	         + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) & (draw1'=0)
+	         + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) & (draw1'=0)
+	         + 0.0078125 : (b1'=7) & (r1'=r) & (b'=max(b,7)) & (draw1'=0)
+	         + 0.0078125 : (b1'=8) & (r1'=r) & (b'=max(b,8)) & (draw1'=0);
+	// enter critical section and randomly set r to 1 or 2
+	[] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2)
+	                             + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2);
+	// loop when trying and cannot make a draw or enter critical section
+	// [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1);
+	// leave crictical section
+	[] go & p1=2 -> (p1'=0) & (c'=0);
+	// stay in critical section
+	// [] go & p1=2 -> (p1'=2);
+	
+endmodule
+
+// construct further modules through renaming
+module process2 = process1 [p1=p2, b1=b2, r1=r2, draw1=draw2, draw2=draw1 ] endmodule
+module process3 = process1 [p1=p3, b1=b3, r1=r3, draw1=draw3, draw3=draw1 ] endmodule
+module process4 = process1 [p1=p4, b1=b4, r1=r4, draw1=draw4, draw4=draw1 ] endmodule
+module process5 = process1 [p1=p5, b1=b5, r1=r5, draw1=draw5, draw5=draw1 ] endmodule
+module process6 = process1 [p1=p6, b1=b6, r1=r6, draw1=draw6, draw6=draw1 ] endmodule
+module process7 = process1 [p1=p7, b1=b7, r1=r7, draw1=draw7, draw7=draw1 ] endmodule
+module process8 = process1 [p1=p8, b1=b8, r1=r8, draw1=draw8, draw8=draw1 ] endmodule
+module process9 = process1 [p1=p9, b1=b9, r1=r9, draw1=draw9, draw9=draw1 ] endmodule
+module process10 = process1 [p1=p10, b1=b10, r1=r10, draw1=draw10, draw10=draw1 ] 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;
+
+// maximum value of the bi's
+formula maxb = max(b1,b2,b3,b4,b5,b6,b7,b8,b9,b10);
+

prism-examples/rabin/modified/mod_rabin3.nm

@@ -88,5 +88,5 @@ label "one_trying" = p1=1|p2=1|p3=1;
 label "one_critical" = p1=2|p2=2|p3=2;
 
 // maximum value of the bi's
-formula maxb = max(b1,b2 ,b3 );
+formula maxb = max(b1,b2,b3);
 

prism-examples/rabin/modified/mod_rabin4.nm

@@ -89,5 +89,5 @@ label "one_trying" = p1=1|p2=1|p3=1|p4=1;
 label "one_critical" = p1=2|p2=2|p3=2|p4=2;
 
 // maximum value of the bi's
-formula maxb = max(b1,b2 ,b3 ,b4 );
+formula maxb = max(b1,b2,b3,b4);
 

prism-examples/rabin/modified/mod_rabin5.nm

@@ -91,5 +91,5 @@ 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;
 
 // maximum value of the bi's
-formula maxb = max(b1,b2 ,b3 ,b4 ,b5 );
+formula maxb = max(b1,b2,b3,b4,b5);
 

prism-examples/rabin/modified/mod_rabin6.nm

@@ -92,5 +92,5 @@ 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;
 
 // maximum value of the bi's
-formula maxb = max(b1,b2 ,b3 ,b4 ,b5 ,b6 );
+formula maxb = max(b1,b2,b3,b4,b5,b6);
 

prism-examples/rabin/modified/mod_rabin7.nm

@@ -93,5 +93,5 @@ label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1;
 label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2;
 
 // maximum value of the bi's
-formula maxb = max(b1,b2 ,b3 ,b4 ,b5 ,b6 ,b7 );
+formula maxb = max(b1,b2,b3,b4,b5,b6,b7);
 

prism-examples/rabin/modified/mod_rabin8.nm

@@ -94,5 +94,5 @@ 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;
 
 // maximum value of the bi's
-formula maxb = max(b1,b2 ,b3 ,b4 ,b5 ,b6 ,b7 ,b8 );
+formula maxb = max(b1,b2,b3,b4,b5,b6,b7,b8);
 

prism-examples/rabin/modified/mod_rabin9.nm

@@ -0,0 +1,100 @@
+// N-processor mutual exclusion [Rab82]
+// with global variables to remove sychronization 
+// gxn/dxp 03/12/08
+
+// modified version to verify a variant of the bounded waiting property
+// namely the probability a process entries the critical sectiongiven it tries
+
+// note we have removed the self loops to allow the fairness constraints 
+// to be ignored during verification
+
+// split the drawing phase into two steps but is still atomic as no
+// other process can move one the first step has been made
+
+mdp
+
+// size of shared counter
+const int K = 8; // 4+ceil(log_2 N)
+
+// global variables (all modules can read and write)
+// c=0 critical section free
+// c=1 critical section not free
+// b current highest draw
+// r current round 
+
+global c : [0..1];
+global b : [0..K];
+global r : [1..2];
+
+// local variables: process i 
+// state: pi
+//  0 remainder
+//  1 trying
+//  2 critical section
+// current draw: bi
+// current round: ri
+
+// formula for process 1 drawing
+formula draw = p1=1 & (b<b1 | r!=r1);
+
+// formula to keep drawing phase atomic
+// (can onlymove if no process is drawing
+formula go = (draw2=0&draw3=0&draw4=0&draw5=0&draw6=0&draw7=0&draw8=0&draw9=0);
+
+module process1
+
+	p1 : [0..2];
+	b1 : [0..K];
+	r1 : [0..2];
+	draw1 : [0..1];
+
+	// remain in remainder
+	// [] go & p1=0 -> (p1'=0);
+	// enter trying
+	[] go & p1=0 -> (p1'=1);
+	// make a draw
+	[] go & draw & draw1=0 -> (draw1'=1);
+	[] draw1=1 -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) & (draw1'=0)
+	         + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) & (draw1'=0)
+	         + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) & (draw1'=0)
+	         + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) & (draw1'=0)
+	         + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) & (draw1'=0)
+	         + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) & (draw1'=0)
+	         + 0.0078125 : (b1'=7) & (r1'=r) & (b'=max(b,7)) & (draw1'=0)
+	         + 0.0078125 : (b1'=8) & (r1'=r) & (b'=max(b,8)) & (draw1'=0);
+	// enter critical section and randomly set r to 1 or 2
+	[] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2)
+	                             + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2);
+	// loop when trying and cannot make a draw or enter critical section
+	// [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1);
+	// leave crictical section
+	[] go & p1=2 -> (p1'=0) & (c'=0);
+	// stay in critical section
+	// [] go & p1=2 -> (p1'=2);
+	
+endmodule
+
+// construct further modules through renaming
+module process2 = process1 [p1=p2, b1=b2, r1=r2, draw1=draw2, draw2=draw1 ] endmodule
+module process3 = process1 [p1=p3, b1=b3, r1=r3, draw1=draw3, draw3=draw1 ] endmodule
+module process4 = process1 [p1=p4, b1=b4, r1=r4, draw1=draw4, draw4=draw1 ] endmodule
+module process5 = process1 [p1=p5, b1=b5, r1=r5, draw1=draw5, draw5=draw1 ] endmodule
+module process6 = process1 [p1=p6, b1=b6, r1=r6, draw1=draw6, draw6=draw1 ] endmodule
+module process7 = process1 [p1=p7, b1=b7, r1=r7, draw1=draw7, draw7=draw1 ] endmodule
+module process8 = process1 [p1=p8, b1=b8, r1=r8, draw1=draw8, draw8=draw1 ] endmodule
+module process9 = process1 [p1=p9, b1=b9, r1=r9, draw1=draw9, draw9=draw1 ] 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);
+
+// 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;
+
+// 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;
+
+// maximum value of the bi's
+formula maxb = max(b1,b2,b3,b4,b5,b6,b7,b8,b9);
+