s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Tidy up and addition of .pp files to rabin. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@381 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 19 years ago
parent
597427f1e4
commit
d21e1b2a29
17 changed files with 252 additions and 376 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 9
      prism-examples/rabin/.autopp
  2. 60
      prism-examples/rabin/.rabinN.nm.pp
  3. 8
      prism-examples/rabin/.rabinN.pctl.pp
  4. 49
      prism-examples/rabin/rabin10.nm
  5. 62
      prism-examples/rabin/rabin10.pctl
  6. 49
      prism-examples/rabin/rabin12.nm
  7. 83
      prism-examples/rabin/rabin12.pctl
  8. 29
      prism-examples/rabin/rabin3.nm
  9. 20
      prism-examples/rabin/rabin3.pctl
  10. 29
      prism-examples/rabin/rabin4.nm
  11. 23
      prism-examples/rabin/rabin4.pctl
  12. 31
      prism-examples/rabin/rabin5.nm
  13. 27
      prism-examples/rabin/rabin5.pctl
  14. 31
      prism-examples/rabin/rabin6.nm
  15. 32
      prism-examples/rabin/rabin6.pctl
  16. 41
      prism-examples/rabin/rabin8.nm
  17. 45
      prism-examples/rabin/rabin8.pctl

9
prism-examples/rabin/.autopp
View File

@ -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

60
prism-examples/rabin/.rabinN.nm.pp
View File

@ -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<b1 | r!=r1);
module process1
p1 : [0..2];
b1 : [0..K];
r1 : [0..2];
// remain in remainder
[] p1=0 -> (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#

8
prism-examples/rabin/.rabinN.pctl.pp
View File

@ -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" ]

49
prism-examples/rabin/rabin10.nm
View File

@ -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<b1 | r!=r1);
module process1
p1 : [0..2];
b1 : [0..8];
b1 : [0..K];
r1 : [0..2];
// enter trying
[] p1=0 -> (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

62
prism-examples/rabin/rabin10.pctl
View File

@ -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" ]

49
prism-examples/rabin/rabin12.nm
View File

@ -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<b1 | r!=r1);
module process1
p1 : [0..2];
b1 : [0..8];
b1 : [0..K];
r1 : [0..2];
// enter trying
[] p1=0 -> (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

83
prism-examples/rabin/rabin12.pctl
View File

@ -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" ]

29
prism-examples/rabin/rabin3.nm
View File

@ -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<b1 | r!=r1);
module process1
p1 : [0..2];
b1 : [0..6];
b1 : [0..K];
r1 : [0..2];
// enter trying
[] p1=0 -> (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

20
prism-examples/rabin/rabin3.pctl
View File

@ -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" ]

29
prism-examples/rabin/rabin4.nm
View File

@ -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<b1 | r!=r1);
module process1
p1 : [0..2];
b1 : [0..6];
b1 : [0..K];
r1 : [0..2];
// enter trying
[] p1=0 -> (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

23
prism-examples/rabin/rabin4.pctl
View File

@ -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" ]

31
prism-examples/rabin/rabin5.nm
View File

@ -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<b1 | r!=r1);
module process1
p1 : [0..2];
b1 : [0..7];
b1 : [0..K];
r1 : [0..2];
// enter trying
[] p1=0 -> (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

27
prism-examples/rabin/rabin5.pctl
View File

@ -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" ]

31
prism-examples/rabin/rabin6.nm
View File

@ -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<b1 | r!=r1);
module process1
p1 : [0..2];
b1 : [0..7];
b1 : [0..K];
r1 : [0..2];
// enter trying
[] p1=0 -> (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

32
prism-examples/rabin/rabin6.pctl
View File

@ -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" ]

41
prism-examples/rabin/rabin8.nm
View File

@ -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<b1 | r!=r1);
module process1
p1 : [0..2];
b1 : [0..7];
b1 : [0..K];
r1 : [0..2];
// enter trying
[] p1=0 -> ((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

45
prism-examples/rabin/rabin8.pctl
View File

@ -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" ]
Write Preview
Loading…
Cancel
Save