diff --git a/prism-examples/rabin/.autopp b/prism-examples/rabin/.autopp new file mode 100755 index 00000000..5ba73e4f --- /dev/null +++ b/prism-examples/rabin/.autopp @@ -0,0 +1,9 @@ +#!/bin/csh + +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 diff --git a/prism-examples/rabin/.rabinN.nm.pp b/prism-examples/rabin/.rabinN.nm.pp new file mode 100644 index 00000000..5dd46968 --- /dev/null +++ b/prism-examples/rabin/.rabinN.nm.pp @@ -0,0 +1,60 @@ +#const N# +#const K=4+func(ceil,func(log,N,2))# +// N-processor mutual exclusion [Rab82] +// with global variables to remove sychronization +// gxn/dxp 02/02/00 + +nondeterministic + +// size of shared counter +const int K = #K#; // 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 + +// atomic formula for process 1 drawing +formula draw = p1=1 & (b (p1'=0); + // enter trying + [] p1=0 -> (p1'=1); + // make a draw + [] draw ->#+ i=1:K-1# #1/func(floor,func(pow,2,i))# : (b1'=#i#) & (r1'=r) & (b'=max(b,#i#)) + #end#+ #1/func(floor,func(pow,2,K-1))# : (b1'=#K#) & (r1'=r) & (b'=max(b,#K#)); + // enter critical section and randomly set r to 1 or 2 + [] 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 + [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); + // leave crictical section + [] p1=2 -> (p1'=0) & (c'=0); + // stay in critical section + [] p1=2 -> (p1'=2); + +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# diff --git a/prism-examples/rabin/.rabinN.pctl.pp b/prism-examples/rabin/.rabinN.pctl.pp new file mode 100644 index 00000000..c3c02e3c --- /dev/null +++ b/prism-examples/rabin/.rabinN.pctl.pp @@ -0,0 +1,8 @@ +#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" ] diff --git a/prism-examples/rabin/rabin10.nm b/prism-examples/rabin/rabin10.nm index bcc2e942..08d26943 100644 --- a/prism-examples/rabin/rabin10.nm +++ b/prism-examples/rabin/rabin10.nm @@ -1,9 +1,12 @@ -// ten processor mutual exclusion [Rab82] +// N-processor mutual exclusion [Rab82] // with global variables to remove sychronization // gxn/dxp 02/02/00 nondeterministic +// 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 @@ -11,7 +14,7 @@ nondeterministic // r current round global c : [0..1]; -global b : [0..8]; +global b : [0..K]; global r : [1..2]; // local variables: process i @@ -28,25 +31,25 @@ formula draw = p1=1 & (b (p1'=0); // remain in remainder + [] p1=0 -> (p1'=0); + // enter trying [] p1=0 -> (p1'=1); // make a draw - [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) - + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) - + 0.0078125 : (b1'=7) & (r1'=r) & (b'=max(b,7)) - + 0.0078125 : (b1'=8) & (r1'=r) & (b'=max(b,8)); + [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) + + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) + + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) + + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) + + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) + + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) + + 0.0078125 : (b1'=7) & (r1'=r) & (b'=max(b,7)) + + 0.0078125 : (b1'=8) & (r1'=r) & (b'=max(b,8)); // enter critical section and randomly set r to 1 or 2 [] 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); + + 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 [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); // leave crictical section @@ -57,14 +60,12 @@ module process1 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 -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 -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 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 +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 +module process9 = process1 [p1=p9, b1=b9, r1=r9] endmodule module process10 = process1 [p1=p10, b1=b10, r1=r10] endmodule - diff --git a/prism-examples/rabin/rabin10.pctl b/prism-examples/rabin/rabin10.pctl index da433092..886db82f 100644 --- a/prism-examples/rabin/rabin10.pctl +++ b/prism-examples/rabin/rabin10.pctl @@ -1,58 +1,8 @@ -// mutual exclusion +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; -(!((p1=2) & (p2=2))) & -(!((p1=2) & (p3=2))) & -(!((p1=2) & (p4=2))) & -(!((p1=2) & (p5=2))) & -(!((p1=2) & (p6=2))) & -(!((p1=2) & (p7=2))) & -(!((p1=2) & (p8=2))) & -(!((p1=2) & (p9=2))) & -(!((p1=2) & (p10=2))) & -(!((p2=2) & (p3=2))) & -(!((p2=2) & (p4=2))) & -(!((p2=2) & (p5=2))) & -(!((p2=2) & (p6=2))) & -(!((p2=2) & (p7=2))) & -(!((p2=2) & (p8=2))) & -(!((p2=2) & (p9=2))) & -(!((p2=2) & (p10=2))) & -(!((p3=2) & (p4=2))) & -(!((p3=2) & (p5=2))) & -(!((p3=2) & (p6=2))) & -(!((p3=2) & (p7=2))) & -(!((p3=2) & (p8=2))) & -(!((p3=2) & (p9=2))) & -(!((p3=2) & (p10=2))) & -(!((p4=2) & (p5=2))) & -(!((p4=2) & (p6=2))) & -(!((p4=2) & (p7=2))) & -(!((p4=2) & (p8=2))) & -(!((p4=2) & (p9=2))) & -(!((p4=2) & (p10=2))) & -(!((p5=2) & (p6=2))) & -(!((p5=2) & (p7=2))) & -(!((p5=2) & (p8=2))) & -(!((p5=2) & (p9=2))) & -(!((p5=2) & (p10=2))) & -(!((p6=2) & (p7=2))) & -(!((p6=2) & (p8=2))) & -(!((p6=2) & (p9=2))) & -(!((p6=2) & (p10=2))) & -(!((p7=2) & (p8=2))) & -(!((p7=2) & (p9=2))) & -(!((p7=2) & (p10=2))) & -(!((p8=2) & (p9=2))) & -(!((p8=2) & (p10=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 - -((p1=1) | (p2=1) | (p3=1) | (p4=1) | (p5=1) | (p6=1) | (p7=1) | (p8=1) | (p9=1) | (p10=1)) => -P>=1 [ true U (p1=2) | (p2=2) | (p3=2) | (p4=2) | (p5=2) | (p6=2) | (p7=2) | (p8=2) | (p9=2) | (p10=2) ] - -// if all processes are trying process 1 enters the critical section first - -(p1=1) & (p2=1) & (p3=1) & (p4=1) & (p5=1) & (p6=1) & (p7=1) & (p8=1) & (p9=1) & (p10=1) => -P>=0.5 [ !(p2=2) & !(p3=2) & !(p4=2) & !(p5=2) & !(p6=2) & !(p7=2) & !(p8=2) & !(p9=2) & !(p10=2) U (p1=2) ] +// Liveness: If a process is trying, then eventually a process enters the critical section +"one_trying" => P>=1 [ true U "one_critical" ] diff --git a/prism-examples/rabin/rabin12.nm b/prism-examples/rabin/rabin12.nm index 29bc8135..9b09fa67 100644 --- a/prism-examples/rabin/rabin12.nm +++ b/prism-examples/rabin/rabin12.nm @@ -1,9 +1,12 @@ -// twelve processor mutual exclusion [Rab82] +// N-processor mutual exclusion [Rab82] // with global variables to remove sychronization // gxn/dxp 02/02/00 nondeterministic +// 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 @@ -11,7 +14,7 @@ nondeterministic // r current round global c : [0..1]; -global b : [0..8]; +global b : [0..K]; global r : [1..2]; // local variables: process i @@ -28,25 +31,25 @@ formula draw = p1=1 & (b (p1'=0); // remain in remainder + [] p1=0 -> (p1'=0); + // enter trying [] p1=0 -> (p1'=1); // make a draw - [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) - + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) - + 0.0078125 : (b1'=7) & (r1'=r) & (b'=max(b,7)) - + 0.0078125 : (b1'=8) & (r1'=r) & (b'=max(b,8)); + [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) + + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) + + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) + + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) + + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) + + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) + + 0.0078125 : (b1'=7) & (r1'=r) & (b'=max(b,7)) + + 0.0078125 : (b1'=8) & (r1'=r) & (b'=max(b,8)); // enter critical section and randomly set r to 1 or 2 [] 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); + + 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 [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); // leave crictical section @@ -57,16 +60,14 @@ module process1 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 -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 -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 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 +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 +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 - diff --git a/prism-examples/rabin/rabin12.pctl b/prism-examples/rabin/rabin12.pctl index a4a07444..eee23e74 100644 --- a/prism-examples/rabin/rabin12.pctl +++ b/prism-examples/rabin/rabin12.pctl @@ -1,79 +1,8 @@ -// mutual exclusion +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; -(!((p1=2) & (p2=2))) & -(!((p1=2) & (p3=2))) & -(!((p1=2) & (p4=2))) & -(!((p1=2) & (p5=2))) & -(!((p1=2) & (p6=2))) & -(!((p1=2) & (p7=2))) & -(!((p1=2) & (p8=2))) & -(!((p1=2) & (p9=2))) & -(!((p1=2) & (p10=2))) & -(!((p1=2) & (p11=2))) & -(!((p1=2) & (p12=2))) & -(!((p2=2) & (p3=2))) & -(!((p2=2) & (p4=2))) & -(!((p2=2) & (p5=2))) & -(!((p2=2) & (p6=2))) & -(!((p2=2) & (p7=2))) & -(!((p2=2) & (p8=2))) & -(!((p2=2) & (p9=2))) & -(!((p2=2) & (p10=2))) & -(!((p2=2) & (p11=2))) & -(!((p2=2) & (p12=2))) & -(!((p3=2) & (p4=2))) & -(!((p3=2) & (p5=2))) & -(!((p3=2) & (p6=2))) & -(!((p3=2) & (p7=2))) & -(!((p3=2) & (p8=2))) & -(!((p3=2) & (p9=2))) & -(!((p3=2) & (p10=2))) & -(!((p3=2) & (p11=2))) & -(!((p3=2) & (p12=2))) & -(!((p4=2) & (p5=2))) & -(!((p4=2) & (p6=2))) & -(!((p4=2) & (p7=2))) & -(!((p4=2) & (p8=2))) & -(!((p4=2) & (p9=2))) & -(!((p4=2) & (p10=2))) & -(!((p4=2) & (p11=2))) & -(!((p4=2) & (p12=2))) & -(!((p5=2) & (p6=2))) & -(!((p5=2) & (p7=2))) & -(!((p5=2) & (p8=2))) & -(!((p5=2) & (p9=2))) & -(!((p5=2) & (p10=2))) & -(!((p5=2) & (p11=2))) & -(!((p5=2) & (p12=2))) & -(!((p6=2) & (p7=2))) & -(!((p6=2) & (p8=2))) & -(!((p6=2) & (p9=2))) & -(!((p6=2) & (p10=2))) & -(!((p6=2) & (p11=2))) & -(!((p6=2) & (p12=2))) & -(!((p7=2) & (p8=2))) & -(!((p7=2) & (p9=2))) & -(!((p7=2) & (p10=2))) & -(!((p7=2) & (p11=2))) & -(!((p7=2) & (p12=2))) & -(!((p8=2) & (p9=2))) & -(!((p8=2) & (p10=2))) & -(!((p8=2) & (p11=2))) & -(!((p8=2) & (p12=2))) & -(!((p9=2) & (p10=2))) & -(!((p9=2) & (p11=2))) & -(!((p9=2) & (p12=2))) & -(!((p10=2) & (p11=2))) & -(!((p10=2) & (p12=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 - -((p1=1) | (p2=1) | (p3=1) | (p4=1) | (p5=1) | (p6=1) | (p7=1) | (p8=1) | (p9=1) | (p10=1) | (p11=1) | (p12=1)) => -P>=1 [ true U (p1=2) | (p2=2) | (p3=2) | (p4=2) | (p5=2) | (p6=2) | (p7=2) | (p8=2) | (p9=2) | (p10=2) | (p11=2) | (p12=2) ] - -// if all processes are trying process 1 enters the critical section first - -(p1=1) & (p2=1) & (p3=1) & (p4=1) & (p5=1) & (p6=1) & (p7=1) & (p8=1) & (p9=1) & (p10=1) & (p11=1) & (p12=1) => -P>=0.5 [ !(p2=2) & !(p3=2) & !(p4=2) & !(p5=2) & !(p6=2) & !(p7=2) & !(p8=2) & !(p9=2) & !(p10=2) & !(p11=2) & !(p12=2) U (p1=2) ] +// Liveness: If a process is trying, then eventually a process enters the critical section +"one_trying" => P>=1 [ true U "one_critical" ] diff --git a/prism-examples/rabin/rabin3.nm b/prism-examples/rabin/rabin3.nm index 9d5409a7..7f64b6ca 100644 --- a/prism-examples/rabin/rabin3.nm +++ b/prism-examples/rabin/rabin3.nm @@ -1,9 +1,12 @@ -// three processor mutual exclusion [Rab82] +// N-processor mutual exclusion [Rab82] // with global variables to remove sychronization // gxn/dxp 02/02/00 nondeterministic +// size of shared counter +const int K = 6; // 4+ceil(log_2 N) + // global variables (all modules can read and write) // c=0 critical section free // c=1 critical section not free @@ -11,7 +14,7 @@ nondeterministic // r current round global c : [0..1]; -global b : [0..6]; +global b : [0..K]; global r : [1..2]; // local variables: process i @@ -28,23 +31,23 @@ formula draw = p1=1 & (b (p1'=0); // remain in remainder + [] p1=0 -> (p1'=0); + // enter trying [] p1=0 -> (p1'=1); // make a draw - [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) - + 0.03125 : (b1'=6) & (r1'=r) & (b'=max(b,6)); + [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) + + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) + + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) + + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) + + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) + + 0.03125 : (b1'=6) & (r1'=r) & (b'=max(b,6)); // enter critical section and randomly set r to 1 or 2 [] 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); + + 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 [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); // leave crictical section @@ -55,7 +58,5 @@ module process1 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 - diff --git a/prism-examples/rabin/rabin3.pctl b/prism-examples/rabin/rabin3.pctl index 8867eb1b..e7065df7 100644 --- a/prism-examples/rabin/rabin3.pctl +++ b/prism-examples/rabin/rabin3.pctl @@ -1,16 +1,8 @@ -// mutual exclusion +label "one_trying" = p1=1|p2=1|p3=1; +label "one_critical" = p1=2|p2=2|p3=2; -(!((p1=2) & (p2=2))) & -(!((p1=2) & (p3=2))) & -(!((p2=2) & (p3=2))) +// Mutual exclusion +(p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0) <= 1 -// liveness -// if a process is trying then eventually a process enters the critical section - -((p1=1) | (p2=1) | (p3=1)) => -P>=1 [ true U (p1=2) | (p2=2) | (p3=2) ] - -// if all processes are trying process 1 enters the critical section first - -(p1=1) & (p2=1) & (p3=1) => -P>=0.5 [ !(p2=2) & !(p3=2) U (p1=2) ] +// Liveness: If a process is trying, then eventually a process enters the critical section +"one_trying" => P>=1 [ true U "one_critical" ] diff --git a/prism-examples/rabin/rabin4.nm b/prism-examples/rabin/rabin4.nm index 491c7c50..b949d354 100644 --- a/prism-examples/rabin/rabin4.nm +++ b/prism-examples/rabin/rabin4.nm @@ -1,9 +1,12 @@ -// four processor mutual exclusion [Rab82] +// N-processor mutual exclusion [Rab82] // with global variables to remove sychronization // gxn/dxp 02/02/00 nondeterministic +// size of shared counter +const int K = 6; // 4+ceil(log_2 N) + // global variables (all modules can read and write) // c=0 critical section free // c=1 critical section not free @@ -11,7 +14,7 @@ nondeterministic // r current round global c : [0..1]; -global b : [0..6]; +global b : [0..K]; global r : [1..2]; // local variables: process i @@ -28,23 +31,23 @@ formula draw = p1=1 & (b (p1'=0); // remain in remainder + [] p1=0 -> (p1'=0); + // enter trying [] p1=0 -> (p1'=1); // make a draw - [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) - + 0.03125 : (b1'=6) & (r1'=r) & (b'=max(b,6)); + [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) + + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) + + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) + + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) + + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) + + 0.03125 : (b1'=6) & (r1'=r) & (b'=max(b,6)); // enter critical section and randomly set r to 1 or 2 [] 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); + + 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 [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); // leave crictical section @@ -55,8 +58,6 @@ module process1 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 module process4 = process1 [p1=p4, b1=b4, r1=r4] endmodule - diff --git a/prism-examples/rabin/rabin4.pctl b/prism-examples/rabin/rabin4.pctl index b0b08363..ac26f07c 100644 --- a/prism-examples/rabin/rabin4.pctl +++ b/prism-examples/rabin/rabin4.pctl @@ -1,19 +1,8 @@ -// mutual exclusion +label "one_trying" = p1=1|p2=1|p3=1|p4=1; +label "one_critical" = p1=2|p2=2|p3=2|p4=2; -(!((p1=2) & (p2=2))) & -(!((p1=2) & (p3=2))) & -(!((p1=2) & (p4=2))) & -(!((p2=2) & (p3=2))) & -(!((p2=2) & (p4=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 - -((p1=1) | (p2=1) | (p3=1) | (p4=1)) => -P>=1 [ true U (p1=2) | (p2=2) | (p3=2) | (p4=2) ] - -// if all processes are trying process 1 enters the critical section first - -(p1=1) & (p2=1) & (p3=1) & (p4=1) => -P>=0.5 [ !(p2=2) & !(p3=2) & !(p4=2) U (p1=2) ] +// Liveness: If a process is trying, then eventually a process enters the critical section +"one_trying" => P>=1 [ true U "one_critical" ] diff --git a/prism-examples/rabin/rabin5.nm b/prism-examples/rabin/rabin5.nm index 52a7ea5a..1d9c9e44 100644 --- a/prism-examples/rabin/rabin5.nm +++ b/prism-examples/rabin/rabin5.nm @@ -1,9 +1,12 @@ -// five processor mutual exclusion [Rab82] +// N-processor mutual exclusion [Rab82] // with global variables to remove sychronization // gxn/dxp 02/02/00 nondeterministic +// size of shared counter +const int K = 7; // 4+ceil(log_2 N) + // global variables (all modules can read and write) // c=0 critical section free // c=1 critical section not free @@ -11,7 +14,7 @@ nondeterministic // r current round global c : [0..1]; -global b : [0..7]; +global b : [0..K]; global r : [1..2]; // local variables: process i @@ -28,24 +31,24 @@ formula draw = p1=1 & (b (p1'=0); // remain in remainder + [] p1=0 -> (p1'=0); + // enter trying [] p1=0 -> (p1'=1); // make a draw - [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) - + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) - + 0.015625 : (b1'=7) & (r1'=r) & (b'=max(b,7)); + [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) + + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) + + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) + + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) + + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) + + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) + + 0.015625 : (b1'=7) & (r1'=r) & (b'=max(b,7)); // enter critical section and randomly set r to 1 or 2 [] 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); + + 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 [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); // leave crictical section @@ -56,9 +59,7 @@ module process1 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 module process4 = process1 [p1=p4, b1=b4, r1=r4] endmodule module process5 = process1 [p1=p5, b1=b5, r1=r5] endmodule - diff --git a/prism-examples/rabin/rabin5.pctl b/prism-examples/rabin/rabin5.pctl index 9bac1412..6e78b1f4 100644 --- a/prism-examples/rabin/rabin5.pctl +++ b/prism-examples/rabin/rabin5.pctl @@ -1,23 +1,8 @@ -// mutual exclusion +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; -(!((p1=2) & (p2=2))) & -(!((p1=2) & (p3=2))) & -(!((p1=2) & (p4=2))) & -(!((p1=2) & (p5=2))) & -(!((p2=2) & (p3=2))) & -(!((p2=2) & (p4=2))) & -(!((p2=2) & (p5=2))) & -(!((p3=2) & (p4=2))) & -(!((p3=2) & (p5=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 - -((p1=1) | (p2=1) | (p3=1) | (p4=1) | (p5=1)) => -P>=1 [ true U (p1=2) | (p2=2) | (p3=2) | (p4=2) | (p5=2) ] - -// if all processes are trying process 1 enters the critical section first - -(p1=1) & (p2=1) & (p3=1) & (p4=1) & (p5=1) => -P>=0.5 [ !(p2=2) & !(p3=2) & !(p4=2) & !(p5=2) U (p1=2) ] +// Liveness: If a process is trying, then eventually a process enters the critical section +"one_trying" => P>=1 [ true U "one_critical" ] diff --git a/prism-examples/rabin/rabin6.nm b/prism-examples/rabin/rabin6.nm index a8227daa..28641f9a 100644 --- a/prism-examples/rabin/rabin6.nm +++ b/prism-examples/rabin/rabin6.nm @@ -1,9 +1,12 @@ -// six processor mutual exclusion [Rab82] +// N-processor mutual exclusion [Rab82] // with global variables to remove sychronization // gxn/dxp 02/02/00 nondeterministic +// size of shared counter +const int K = 7; // 4+ceil(log_2 N) + // global variables (all modules can read and write) // c=0 critical section free // c=1 critical section not free @@ -11,7 +14,7 @@ nondeterministic // r current round global c : [0..1]; -global b : [0..7]; +global b : [0..K]; global r : [1..2]; // local variables: process i @@ -28,24 +31,24 @@ formula draw = p1=1 & (b (p1'=0); // remain in remainder + [] p1=0 -> (p1'=0); + // enter trying [] p1=0 -> (p1'=1); // make a draw - [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) - + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) - + 0.015625 : (b1'=7) & (r1'=r) & (b'=max(b,7)); + [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) + + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) + + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) + + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) + + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) + + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) + + 0.015625 : (b1'=7) & (r1'=r) & (b'=max(b,7)); // enter critical section and randomly set r to 1 or 2 [] 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); + + 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 [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); // leave crictical section @@ -56,10 +59,8 @@ module process1 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 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 - diff --git a/prism-examples/rabin/rabin6.pctl b/prism-examples/rabin/rabin6.pctl index d76f0b55..6f51c121 100644 --- a/prism-examples/rabin/rabin6.pctl +++ b/prism-examples/rabin/rabin6.pctl @@ -1,28 +1,8 @@ -// mutual exclusion +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; -(!((p1=2) & (p2=2))) & -(!((p1=2) & (p3=2))) & -(!((p1=2) & (p4=2))) & -(!((p1=2) & (p5=2))) & -(!((p1=2) & (p6=2))) & -(!((p2=2) & (p3=2))) & -(!((p2=2) & (p4=2))) & -(!((p2=2) & (p5=2))) & -(!((p2=2) & (p6=2))) & -(!((p3=2) & (p4=2))) & -(!((p3=2) & (p5=2))) & -(!((p3=2) & (p6=2))) & -(!((p4=2) & (p5=2))) & -(!((p4=2) & (p6=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 - -((p1=1) | (p2=1) | (p3=1) | (p4=1) | (p5=1) | (p6=1)) => -P>=1 [ true U (p1=2) | (p2=2) | (p3=2) | (p4=2) | (p5=2) | (p6=2) ] - -// if all processes are trying process 1 enters the critical section first - -(p1=1) & (p2=1) & (p3=1) & (p4=1) & (p5=1) & (p6=1) => -P>=0.5 [ !(p2=2) & !(p3=2) & !(p4=2) & !(p5=2) & !(p6=2) U (p1=2) ] +// Liveness: If a process is trying, then eventually a process enters the critical section +"one_trying" => P>=1 [ true U "one_critical" ] diff --git a/prism-examples/rabin/rabin8.nm b/prism-examples/rabin/rabin8.nm index 9de21eed..51e9226f 100644 --- a/prism-examples/rabin/rabin8.nm +++ b/prism-examples/rabin/rabin8.nm @@ -1,9 +1,12 @@ -// eight processor mutual exclusion [Rab82] +// N-processor mutual exclusion [Rab82] // with global variables to remove sychronization // gxn/dxp 02/02/00 nondeterministic +// size of shared counter +const int K = 7; // 4+ceil(log_2 N) + // global variables (all modules can read and write) // c=0 critical section free // c=1 critical section not free @@ -11,7 +14,7 @@ nondeterministic // r current round global c : [0..1]; -global b : [0..7]; +global b : [0..K]; global r : [1..2]; // local variables: process i @@ -28,35 +31,34 @@ formula draw = p1=1 & (b ((p1'=0)); // remain in remainder - [] p1=0 -> ((p1'=1)); + [] p1=0 -> (p1'=0); + // enter trying + [] p1=0 -> (p1'=1); // make a draw - [] draw -> 0.5 : ((b1'=1)) & ((r1'=r)) & ((b'=max(b,1))) - + 0.25 : ((b1'=2)) & ((r1'=r)) & ((b'=max(b,2))) - + 0.125 : ((b1'=3)) & ((r1'=r)) & ((b'=max(b,3))) - + 0.0625 : ((b1'=4)) & ((r1'=r)) & ((b'=max(b,4))) - + 0.03125 : ((b1'=5)) & ((r1'=r)) & ((b'=max(b,5))) - + 0.015625 : ((b1'=6)) & ((r1'=r)) & ((b'=max(b,6))) - + 0.015625 : ((b1'=7)) & ((r1'=r)) & ((b'=max(b,7))); + [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) + + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) + + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) + + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) + + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) + + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) + + 0.015625 : (b1'=7) & (r1'=r) & (b'=max(b,7)); // enter critical section and randomly set r to 1 or 2 - [] 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)); + [] 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 - [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> ((p1'=p1)); + [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); // leave crictical section - [] p1=2 -> ((p1'=0)) & ((c'=0)); + [] p1=2 -> (p1'=0) & (c'=0); // stay in critical section - [] p1=2 -> ((p1'=2)); + [] p1=2 -> (p1'=2); 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 module process4 = process1 [p1=p4, b1=b4, r1=r4] endmodule @@ -64,4 +66,3 @@ 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 - diff --git a/prism-examples/rabin/rabin8.pctl b/prism-examples/rabin/rabin8.pctl index e991be4e..0be844cd 100644 --- a/prism-examples/rabin/rabin8.pctl +++ b/prism-examples/rabin/rabin8.pctl @@ -1,41 +1,8 @@ -// mutual exclusion +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; -(!((p1=2) & (p2=2))) & -(!((p1=2) & (p3=2))) & -(!((p1=2) & (p4=2))) & -(!((p1=2) & (p5=2))) & -(!((p1=2) & (p6=2))) & -(!((p1=2) & (p7=2))) & -(!((p1=2) & (p8=2))) & -(!((p2=2) & (p3=2))) & -(!((p2=2) & (p4=2))) & -(!((p2=2) & (p5=2))) & -(!((p2=2) & (p6=2))) & -(!((p2=2) & (p7=2))) & -(!((p2=2) & (p8=2))) & -(!((p3=2) & (p4=2))) & -(!((p3=2) & (p5=2))) & -(!((p3=2) & (p6=2))) & -(!((p3=2) & (p7=2))) & -(!((p3=2) & (p8=2))) & -(!((p4=2) & (p5=2))) & -(!((p4=2) & (p6=2))) & -(!((p4=2) & (p7=2))) & -(!((p4=2) & (p8=2))) & -(!((p5=2) & (p6=2))) & -(!((p5=2) & (p7=2))) & -(!((p5=2) & (p8=2))) & -(!((p6=2) & (p7=2))) & -(!((p6=2) & (p8=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 - -((p1=1) | (p2=1) | (p3=1) | (p4=1) | (p5=1) | (p6=1) | (p7=1) | (p8=1)) => -P>=1 [ true U (p1=2) | (p2=2) | (p3=2) | (p4=2) | (p5=2) | (p6=2) | (p7=2) | (p8=2) ] - -// if all processes are trying process 1 enters the critical section first - -(p1=1) & (p2=1) & (p3=1) & (p4=1) & (p5=1) & (p6=1) & (p7=1) & (p8=1) => -P>=0.5 [ !(p2=2) & !(p3=2) & !(p4=2) & !(p5=2) & !(p6=2) & !(p7=2) & !(p8=2) U (p1=2) ] +// Liveness: If a process is trying, then eventually a process enters the critical section +"one_trying" => P>=1 [ true U "one_critical" ]