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

Tidy up mutual (and add pp files). 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@679 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
9e877df567
commit
c7585ab93f
14 changed files with 201 additions and 261 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. 7
      prism-examples/mutual/.autopp
  2. 66
      prism-examples/mutual/.mutualN.nm.pp
  3. 10
      prism-examples/mutual/auto
  4. 18
      prism-examples/mutual/mutual.pctl
  5. 39
      prism-examples/mutual/mutual10.nm
  6. 68
      prism-examples/mutual/mutual10.pctl
  7. 25
      prism-examples/mutual/mutual3.nm
  8. 25
      prism-examples/mutual/mutual3.pctl
  9. 27
      prism-examples/mutual/mutual4.nm
  10. 29
      prism-examples/mutual/mutual4.pctl
  11. 29
      prism-examples/mutual/mutual5.nm
  12. 33
      prism-examples/mutual/mutual5.pctl
  13. 35
      prism-examples/mutual/mutual8.nm
  14. 51
      prism-examples/mutual/mutual8.pctl

7
prism-examples/mutual/.autopp
View File

@ -0,0 +1,7 @@
#!/bin/csh
foreach N ( 3 4 5 8 10 )
echo "Generating for N=$N"
prismpp .mutualN.nm.pp $N >! mutual"$N".nm
unix2dos mutual"$N".nm
end

66
prism-examples/mutual/.mutualN.nm.pp
View File

@ -0,0 +1,66 @@
#const N#
// mutual exclusion [PZ82]
// dxp/gxn 19/12/99
mdp
// atomic formula
// none in low, high, tie
formula none_lht = #& i=2:N#!(p#i#>=4&p#i#<=13)#end#;
// some in admit
formula some_a = #| i=2:N#(p#i#>=14&p#i#<=15)#end#;
// some in high, admit
formula some_ha = #| i=2:N#(p#i#>=4&p#i#<=5|p#i#>=10&p#i#<=15)#end#;
// none in high, tie, admit
formula none_hta = #& i=2:N#(p#i#>=0&p#i#<=3|p#i#>=7&p#i#<=8)#end#;
// none in enter
formula none_e = #& i=2:N#!(p#i#>=2&p#i#<=3)#end#;
module process1
p1: [0..15];
[] p1=0 -> (p1'=0);
[] p1=0 -> (p1'=1);
[] p1=1 -> (p1'=2);
[] p1=2 & (none_lht | some_a) -> (p1'=3);
[] p1=2 & !(none_lht | some_a) -> (p1'=2);
[] p1=3 -> (p1'=4);
[] p1=3 -> (p1'=7);
[] p1=4 & some_ha -> (p1'=5);
[] p1=4 & !some_ha -> (p1'=10);
[] p1=5 -> (p1'=6);
[] p1=6 & some_ha -> (p1'=6);
[] p1=6 & !some_ha -> (p1'=9);
[] p1=7 & none_hta -> (p1'=8);
[] p1=7 & !none_hta -> (p1'=7);
[] p1=8 -> (p1'=9);
[] p1=9 -> 0.5 : (p1'=4) + 0.5 : (p1'=7);
[] p1=10 -> (p1'=11);
[] p1=11 & none_lht -> (p1'=13);
[] p1=11 & !none_lht -> (p1'=12);
[] p1=12 -> (p1'=0);
[] p1=13 -> (p1'=14);
[] p1=14 & none_e -> (p1'=15);
[] p1=14 & !none_e -> (p1'=14);
[] p1=15 -> (p1'=0);
endmodule
// construct further modules through renaming
#for i=2:N#
module process#i# = process1 [ p1=p#i#, p#i#=p1 ] endmodule
#end#
// formulas/labels for properties
// number of procs in critical section
formula num_crit = #+ i=1:N#p#1#>9?1:0#end#;
// some process is between 4 and 13
label "some_4_13" = #| i=1:N#(p#i#>=4&p#i#<=13)#end#;
// some process is in 14
label "some_14" = #| i=1:N#(p#i#=14)#end#;

10
prism-examples/mutual/auto
View File

@ -1,7 +1,7 @@
#!/bin/csh
prism mutual3.nm mutual3.pctl -fair
prism mutual4.nm mutual4.pctl -fair
prism mutual5.nm mutual5.pctl -fair
prism mutual8.nm mutual8.pctl -fair
prism mutual10.nm mutual10.pctl -fair
prism mutual3.nm mutual.pctl -fair
prism mutual4.nm mutual.pctl -fair
prism mutual5.nm mutual.pctl -fair
prism mutual8.nm mutual.pctl -fair
prism mutual10.nm mutual.pctl -fair

18
prism-examples/mutual/mutual.pctl
View File

@ -0,0 +1,18 @@
// Theorem 1 (mutual exclusion)
num_crit <= 1
// Lemma C
// If the crical section is occupied then eventually it becomes clear
num_crit > 0 => P>=1 [ F num_crit = 0 ]
// Lemma D
// If a process is between 4 and 13 (in our version) then eventually some process gets to 14
"some_4_13" => P>=1 [ F "some_14" ]
// Theorem 2 (liveness)
// If process 1 tries then eventually it enters the critical section
p1=1 => P>=1 [ F p1=10 ]

39
prism-examples/mutual/mutual10.nm
View File

@ -5,15 +5,16 @@ mdp
// atomic formula
// none in low, high, tie
formula none_lht = p2!=4..13 & p3!=4..13 & p4!=4..13 & p5!=4..13 & p6!=4..13 & p7!=4..13 & p8!=4..13 & p9!=4..13 & p10!=4..13;
formula none_lht = !(p2>=4&p2<=13)&!(p3>=4&p3<=13)&!(p4>=4&p4<=13)&!(p5>=4&p5<=13)&!(p6>=4&p6<=13)&!(p7>=4&p7<=13)&!(p8>=4&p8<=13)&!(p9>=4&p9<=13)&!(p10>=4&p10<=13);
// some in admit
formula some_a = p2=14..15 | p3=14..15 | p4=14..15 | p5=14..15 | p6=14..15 | p7=14..15 | p8=14..15 | p9=14..15 | p10=14..15;
formula some_a = (p2>=14&p2<=15)|(p3>=14&p3<=15)|(p4>=14&p4<=15)|(p5>=14&p5<=15)|(p6>=14&p6<=15)|(p7>=14&p7<=15)|(p8>=14&p8<=15)|(p9>=14&p9<=15)|(p10>=14&p10<=15);
// some in high, admit
formula some_ha = p2=4..5,10..15 | p3=4..5,10..15 | p4=4..5,10..15 | p5=4..5,10..15 | p6=4..5,10..15 | p7=4..5,10..15 | p8=4..5,10..15 | p9=4..5,10..15 | p10=4..5,10..15;
formula some_ha = (p2>=4&p2<=5|p2>=10&p2<=15)|(p3>=4&p3<=5|p3>=10&p3<=15)|(p4>=4&p4<=5|p4>=10&p4<=15)|(p5>=4&p5<=5|p5>=10&p5<=15)|(p6>=4&p6<=5|p6>=10&p6<=15)|(p7>=4&p7<=5|p7>=10&p7<=15)|(p8>=4&p8<=5|p8>=10&p8<=15)|(p9>=4&p9<=5|p9>=10&p9<=15)|(p10>=4&p10<=5|p10>=10&p10<=15);
// none in high, tie, admit
formula none_hta = p2=0..3,7..8 & p3=0..3,7..8 & p4=0..3,7..8 & p5=0..3,7..8 & p6=0..3,7..8 & p7=0..3,7..8 & p8=0..3,7..8 & p9=0..3,7..8 & p10=0..3,7..8;
formula none_hta = (p2>=0&p2<=3|p2>=7&p2<=8)&(p3>=0&p3<=3|p3>=7&p3<=8)&(p4>=0&p4<=3|p4>=7&p4<=8)&(p5>=0&p5<=3|p5>=7&p5<=8)&(p6>=0&p6<=3|p6>=7&p6<=8)&(p7>=0&p7<=3|p7>=7&p7<=8)&(p8>=0&p8<=3|p8>=7&p8<=8)&(p9>=0&p9<=3|p9>=7&p9<=8)&(p10>=0&p10<=3|p10>=7&p10<=8);
// none in enter
formula none_e = p2!=2..3 & p3!=2..3 & p4!=2..3 & p5!=2..3 & p6!=2..3 & p7!=2..3 & p8!=2..3 & p9!=2..3 & p10!=2..3;
formula none_e = !(p2>=2&p2<=3)&!(p3>=2&p3<=3)&!(p4>=2&p4<=3)&!(p5>=2&p5<=3)&!(p6>=2&p6<=3)&!(p7>=2&p7<=3)&!(p8>=2&p8<=3)&!(p9>=2&p9<=3)&!(p10>=2&p10<=3);
module process1
@ -48,13 +49,23 @@ endmodule
// construct further modules through renaming
module process2 = process1 [p1=p2, p2=p1] endmodule
module process3 = process1 [p1=p3, p3=p1] endmodule
module process4 = process1 [p1=p4, p4=p1] endmodule
module process5 = process1 [p1=p5, p5=p1] endmodule
module process6 = process1 [p1=p6, p6=p1] endmodule
module process7 = process1 [p1=p7, p7=p1] endmodule
module process8 = process1 [p1=p8, p8=p1] endmodule
module process9 = process1 [p1=p9, p9=p1] endmodule
module process10 = process1 [p1=p10, p10=p1] endmodule
module process2 = process1 [ p1=p2, p2=p1 ] endmodule
module process3 = process1 [ p1=p3, p3=p1 ] endmodule
module process4 = process1 [ p1=p4, p4=p1 ] endmodule
module process5 = process1 [ p1=p5, p5=p1 ] endmodule
module process6 = process1 [ p1=p6, p6=p1 ] endmodule
module process7 = process1 [ p1=p7, p7=p1 ] endmodule
module process8 = process1 [ p1=p8, p8=p1 ] endmodule
module process9 = process1 [ p1=p9, p9=p1 ] endmodule
module process10 = process1 [ p1=p10, p10=p1 ] endmodule
// formulas/labels for properties
// number of procs in critical section
formula num_crit = p1>9?1:0+p1>9?1:0+p1>9?1:0+p1>9?1:0+p1>9?1:0+p1>9?1:0+p1>9?1:0+p1>9?1:0+p1>9?1:0+p1>9?1:0;
// some process is between 4 and 13
label "some_4_13" = (p1>=4&p1<=13)|(p2>=4&p2<=13)|(p3>=4&p3<=13)|(p4>=4&p4<=13)|(p5>=4&p5<=13)|(p6>=4&p6<=13)|(p7>=4&p7<=13)|(p8>=4&p8<=13)|(p9>=4&p9<=13)|(p10>=4&p10<=13);
// some process is in 14
label "some_14" = (p1=14)|(p2=14)|(p3=14)|(p4=14)|(p5=14)|(p6=14)|(p7=14)|(p8=14)|(p9=14)|(p10=14);

68
prism-examples/mutual/mutual10.pctl
View File

@ -1,68 +0,0 @@
// theorem 1 (mutual exclusion)
(!((p1>9) & (p2>9))) &
(!((p1>9) & (p3>9))) &
(!((p1>9) & (p4>9))) &
(!((p1>9) & (p5>9))) &
(!((p1>9) & (p6>9))) &
(!((p1>9) & (p7>9))) &
(!((p1>9) & (p8>9))) &
(!((p1>9) & (p9>9))) &
(!((p1>9) & (p10>9))) &
(!((p2>9) & (p3>9))) &
(!((p2>9) & (p4>9))) &
(!((p2>9) & (p5>9))) &
(!((p2>9) & (p6>9))) &
(!((p2>9) & (p7>9))) &
(!((p2>9) & (p8>9))) &
(!((p2>9) & (p9>9))) &
(!((p2>9) & (p10>9))) &
(!((p3>9) & (p4>9))) &
(!((p3>9) & (p5>9))) &
(!((p3>9) & (p6>9))) &
(!((p3>9) & (p7>9))) &
(!((p3>9) & (p8>9))) &
(!((p3>9) & (p9>9))) &
(!((p3>9) & (p10>9))) &
(!((p4>9) & (p5>9))) &
(!((p4>9) & (p6>9))) &
(!((p4>9) & (p7>9))) &
(!((p4>9) & (p8>9))) &
(!((p4>9) & (p9>9))) &
(!((p4>9) & (p10>9))) &
(!((p5>9) & (p6>9))) &
(!((p5>9) & (p7>9))) &
(!((p5>9) & (p8>9))) &
(!((p5>9) & (p9>9))) &
(!((p5>9) & (p10>9))) &
(!((p6>9) & (p7>9))) &
(!((p6>9) & (p8>9))) &
(!((p6>9) & (p9>9))) &
(!((p6>9) & (p10>9))) &
(!((p7>9) & (p8>9))) &
(!((p7>9) & (p9>9))) &
(!((p7>9) & (p10>9))) &
(!((p8>9) & (p9>9))) &
(!((p8>9) & (p10>9))) &
(!((p9>9) & (p10>9)))
// lemma c
// if the crical section is occupied then eventually it becomes clear
(p1>9) | (p2>9) | (p3>9) | (p4>9) | (p5>9) | (p6>9) | (p7>9) | (p8>9) | (p9>9) | (p10>9) =>
P>=1 [ true U (p1<10) & (p2<10) & (p3<10) & (p4<10) & (p5<10) & (p6<10) & (p7<10) & (p8<10) & (p9<10) & (p10<10) ]
// lemma d
// if a process is between 4 and 13 (in our version) then eventually some process gets to 14
((p1>3) & (p1<14)) | ((p2>3) & (p2<14)) | ((p3>3) & (p3<14)) | ((p4>3) & (p4<14)) | ((p5>3) & (p5<14)) | ((p6>3) & (p6<14)) | ((p7>3) & (p7<14)) | ((p8>3) & (p8<14)) | ((p9>3) & (p9<14)) | ((p10>3) & (p10<14)) =>
P>=1 [ true U (p1=14) | (p2=14) | (p3=14) | (p4=14) | (p5=14) | (p6=14) | (p7=14) | (p8=14) | (p9=14) | (p10=14) ]
// theorem 2 (liveness)
// if process 1 tries then eventually it enters the critical section
(p1=1) => P>=1 [ true U (p1=10) ]
// not probability 1
P<=0.5 [ (p2!=10 & p3!=10) U (p1=10) ]

25
prism-examples/mutual/mutual3.nm
View File

@ -5,15 +5,16 @@ mdp
// atomic formula
// none in low, high, tie
formula none_lht = p2!=4..13 & p3!=4..13;
formula none_lht = !(p2>=4&p2<=13)&!(p3>=4&p3<=13);
// some in admit
formula some_a = p2=14..15 | p3=14..15;
formula some_a = (p2>=14&p2<=15)|(p3>=14&p3<=15);
// some in high, admit
formula some_ha = p2=4..5,10..15 | p3=4..5,10..15;
formula some_ha = (p2>=4&p2<=5|p2>=10&p2<=15)|(p3>=4&p3<=5|p3>=10&p3<=15);
// none in high, tie, admit
formula none_hta = p2=0..3,7..8 & p3=0..3,7..8;
formula none_hta = (p2>=0&p2<=3|p2>=7&p2<=8)&(p3>=0&p3<=3|p3>=7&p3<=8);
// none in enter
formula none_e = p2!=2..3 & p3!=2..3;
formula none_e = !(p2>=2&p2<=3)&!(p3>=2&p3<=3);
module process1
@ -48,6 +49,16 @@ endmodule
// construct further modules through renaming
module process2 = process1 [p1=p2, p2=p1] endmodule
module process3 = process1 [p1=p3, p3=p1] endmodule
module process2 = process1 [ p1=p2, p2=p1 ] endmodule
module process3 = process1 [ p1=p3, p3=p1 ] endmodule
// formulas/labels for properties
// number of procs in critical section
formula num_crit = p1>9?1:0+p1>9?1:0+p1>9?1:0;
// some process is between 4 and 13
label "some_4_13" = (p1>=4&p1<=13)|(p2>=4&p2<=13)|(p3>=4&p3<=13);
// some process is in 14
label "some_14" = (p1=14)|(p2=14)|(p3=14);

25
prism-examples/mutual/mutual3.pctl
View File

@ -1,25 +0,0 @@
// theorem 1 (mutual exclusion)
!((p1>9) & (p2>9))
& !((p1>9) & (p3>9))
& !((p2>9) & (p3>9))
// lemma c
// if the crical section is occupied then eventually it becomes clear
(p1>9) | (p2>9) | (p3>9) => P>=1 [ true U (p1<10) & (p2<10) & (p3<10) ]
// lemma d
// if a process is between 4 and 13 (in our version) then eventually some process gets to 14
((p1>3) & (p1<14)) | ((p2>3) & (p2<14)) | ((p3>3) & (p3<14)) => P>=1 [ true U (p1=14) | (p2=14) | (p3=14) ]
// theorem 2 (liveness)
// if process 1 tries then eventually it enters the critical section
(p1=1) => P>=1 [ true U (p1=10) ]
// not probability 1
P<=0.5 [ (p2!=10 & p3!=10) U (p1=10) ]

27
prism-examples/mutual/mutual4.nm
View File

@ -5,15 +5,16 @@ mdp
// atomic formula
// none in low, high, tie
formula none_lht = p2!=4..13 & p3!=4..13 & p4!=4..13;
formula none_lht = !(p2>=4&p2<=13)&!(p3>=4&p3<=13)&!(p4>=4&p4<=13);
// some in admit
formula some_a = p2=14..15 | p3=14..15 | p4=14..15;
formula some_a = (p2>=14&p2<=15)|(p3>=14&p3<=15)|(p4>=14&p4<=15);
// some in high, admit
formula some_ha = p2=4..5,10..15 | p3=4..5,10..15 | p4=4..5,10..15;
formula some_ha = (p2>=4&p2<=5|p2>=10&p2<=15)|(p3>=4&p3<=5|p3>=10&p3<=15)|(p4>=4&p4<=5|p4>=10&p4<=15);
// none in high, tie, admit
formula none_hta = p2=0..3,7..8 & p3=0..3,7..8 & p4=0..3,7..8;
formula none_hta = (p2>=0&p2<=3|p2>=7&p2<=8)&(p3>=0&p3<=3|p3>=7&p3<=8)&(p4>=0&p4<=3|p4>=7&p4<=8);
// none in enter
formula none_e = p2!=2..3 & p3!=2..3 & p4!=2..3;
formula none_e = !(p2>=2&p2<=3)&!(p3>=2&p3<=3)&!(p4>=2&p4<=3);
module process1
@ -48,7 +49,17 @@ endmodule
// construct further modules through renaming
module process2 = process1 [p1=p2, p2=p1] endmodule
module process3 = process1 [p1=p3, p3=p1] endmodule
module process4 = process1 [p1=p4, p4=p1] endmodule
module process2 = process1 [ p1=p2, p2=p1 ] endmodule
module process3 = process1 [ p1=p3, p3=p1 ] endmodule
module process4 = process1 [ p1=p4, p4=p1 ] endmodule
// formulas/labels for properties
// number of procs in critical section
formula num_crit = p1>9?1:0+p1>9?1:0+p1>9?1:0+p1>9?1:0;
// some process is between 4 and 13
label "some_4_13" = (p1>=4&p1<=13)|(p2>=4&p2<=13)|(p3>=4&p3<=13)|(p4>=4&p4<=13);
// some process is in 14
label "some_14" = (p1=14)|(p2=14)|(p3=14)|(p4=14);

29
prism-examples/mutual/mutual4.pctl
View File

@ -1,29 +0,0 @@
// theorem 1 (mutual exclusion)
(!((p1>9) & (p2>9))) &
(!((p1>9) & (p3>9))) &
(!((p1>9) & (p4>9))) &
(!((p2>9) & (p3>9))) &
(!((p2>9) & (p4>9))) &
(!((p3>9) & (p4>9)))
// lemma c
// if the crical section is occupied then eventually it becomes clear
(p1>9) | (p2>9) | (p3>9) | (p4>9) =>
P>=1 [ true U (p1<10) & (p2<10) & (p3<10) & (p4<10) ]
// lemma d
// if a process is between 4 and 13 (in our version) then eventually some process gets to 14
((p1>3) & (p1<14)) | ((p2>3) & (p2<14)) | ((p3>3) & (p3<14)) | ((p4>3) & (p4<14)) =>
P>=1 [ true U (p1=14) | (p2=14) | (p3=14) | (p4=14) ]
// theorem 2 (liveness)
// if process 1 tries then eventually it enters the critical section
(p1=1) => P>=1 [ true U (p1=10) ]
// not probability 1
P<=0.5 [ (p2!=10 & p3!=10) U (p1=10) ]

29
prism-examples/mutual/mutual5.nm
View File

@ -5,15 +5,16 @@ mdp
// atomic formula
// none in low, high, tie
formula none_lht = p2!=4..13 & p3!=4..13 & p4!=4..13 & p5!=4..13;
formula none_lht = !(p2>=4&p2<=13)&!(p3>=4&p3<=13)&!(p4>=4&p4<=13)&!(p5>=4&p5<=13);
// some in admit
formula some_a = p2=14..15 | p3=14..15 | p4=14..15 | p5=14..15;
formula some_a = (p2>=14&p2<=15)|(p3>=14&p3<=15)|(p4>=14&p4<=15)|(p5>=14&p5<=15);
// some in high, admit
formula some_ha = p2=4..5,10..15 | p3=4..5,10..15 | p4=4..5,10..15 | p5=4..5,10..15;
formula some_ha = (p2>=4&p2<=5|p2>=10&p2<=15)|(p3>=4&p3<=5|p3>=10&p3<=15)|(p4>=4&p4<=5|p4>=10&p4<=15)|(p5>=4&p5<=5|p5>=10&p5<=15);
// none in high, tie, admit
formula none_hta = p2=0..3,7..8 & p3=0..3,7..8 & p4=0..3,7..8 & p5=0..3,7..8;
formula none_hta = (p2>=0&p2<=3|p2>=7&p2<=8)&(p3>=0&p3<=3|p3>=7&p3<=8)&(p4>=0&p4<=3|p4>=7&p4<=8)&(p5>=0&p5<=3|p5>=7&p5<=8);
// none in enter
formula none_e = p2!=2..3 & p3!=2..3 & p4!=2..3 & p5!=2..3;
formula none_e = !(p2>=2&p2<=3)&!(p3>=2&p3<=3)&!(p4>=2&p4<=3)&!(p5>=2&p5<=3);
module process1
@ -48,8 +49,18 @@ endmodule
// construct further modules through renaming
module process2 = process1 [p1=p2, p2=p1] endmodule
module process3 = process1 [p1=p3, p3=p1] endmodule
module process4 = process1 [p1=p4, p4=p1] endmodule
module process5 = process1 [p1=p5, p5=p1] endmodule
module process2 = process1 [ p1=p2, p2=p1 ] endmodule
module process3 = process1 [ p1=p3, p3=p1 ] endmodule
module process4 = process1 [ p1=p4, p4=p1 ] endmodule
module process5 = process1 [ p1=p5, p5=p1 ] endmodule
// formulas/labels for properties
// number of procs in critical section
formula num_crit = p1>9?1:0+p1>9?1:0+p1>9?1:0+p1>9?1:0+p1>9?1:0;
// some process is between 4 and 13
label "some_4_13" = (p1>=4&p1<=13)|(p2>=4&p2<=13)|(p3>=4&p3<=13)|(p4>=4&p4<=13)|(p5>=4&p5<=13);
// some process is in 14
label "some_14" = (p1=14)|(p2=14)|(p3=14)|(p4=14)|(p5=14);

33
prism-examples/mutual/mutual5.pctl
View File

@ -1,33 +0,0 @@
// theorem 1 (mutual exclusion)
(!((p1>9) & (p2>9))) &
(!((p1>9) & (p3>9))) &
(!((p1>9) & (p4>9))) &
(!((p1>9) & (p5>9))) &
(!((p2>9) & (p3>9))) &
(!((p2>9) & (p4>9))) &
(!((p2>9) & (p5>9))) &
(!((p3>9) & (p4>9))) &
(!((p3>9) & (p5>9))) &
(!((p4>9) & (p5>9)))
// lemma c
// if the crical section is occupied then eventually it becomes clear
(p1>9) | (p2>9) | (p3>9) | (p4>9) | (p5>9) =>
P>=1 [ true U (p1<10) & (p2<10) & (p3<10) & (p4<10) & (p5<10) ]
// lemma d
// if a process is between 4 and 13 (in our version) then eventually some process gets to 14
((p1>3) & (p1<14)) | ((p2>3) & (p2<14)) | ((p3>3) & (p3<14)) | ((p4>3) & (p4<14)) | ((p5>3) & (p5<14)) =>
P>=1 [ true U (p1=14) | (p2=14) | (p3=14) | (p4=14) | (p5=14) ]
// theorem 2 (liveness)
// if process 1 tries then eventually it enters the critical section
(p1=1) => P>=1 [ true U (p1=10) ]
// not probability 1
P<=0.5 [ (p2!=10 & p3!=10) U (p1=10) ]

35
prism-examples/mutual/mutual8.nm
View File

@ -5,15 +5,16 @@ mdp
// atomic formula
// none in low, high, tie
formula none_lht = p2!=4..13 & p3!=4..13 & p4!=4..13 & p5!=4..13 & p6!=4..13 & p7!=4..13 & p8!=4..13;
formula none_lht = !(p2>=4&p2<=13)&!(p3>=4&p3<=13)&!(p4>=4&p4<=13)&!(p5>=4&p5<=13)&!(p6>=4&p6<=13)&!(p7>=4&p7<=13)&!(p8>=4&p8<=13);
// some in admit
formula some_a = p2=14..15 | p3=14..15 | p4=14..15 | p5=14..15 | p6=14..15 | p7=14..15 | p8=14..15;
formula some_a = (p2>=14&p2<=15)|(p3>=14&p3<=15)|(p4>=14&p4<=15)|(p5>=14&p5<=15)|(p6>=14&p6<=15)|(p7>=14&p7<=15)|(p8>=14&p8<=15);
// some in high, admit
formula some_ha = p2=4..5,10..15 | p3=4..5,10..15 | p4=4..5,10..15 | p5=4..5,10..15 | p6=4..5,10..15 | p7=4..5,10..15 | p8=4..5,10..15;
formula some_ha = (p2>=4&p2<=5|p2>=10&p2<=15)|(p3>=4&p3<=5|p3>=10&p3<=15)|(p4>=4&p4<=5|p4>=10&p4<=15)|(p5>=4&p5<=5|p5>=10&p5<=15)|(p6>=4&p6<=5|p6>=10&p6<=15)|(p7>=4&p7<=5|p7>=10&p7<=15)|(p8>=4&p8<=5|p8>=10&p8<=15);
// none in high, tie, admit
formula none_hta = p2=0..3,7..8 & p3=0..3,7..8 & p4=0..3,7..8 & p5=0..3,7..8 & p6=0..3,7..8 & p7=0..3,7..8 & p8=0..3,7..8;
formula none_hta = (p2>=0&p2<=3|p2>=7&p2<=8)&(p3>=0&p3<=3|p3>=7&p3<=8)&(p4>=0&p4<=3|p4>=7&p4<=8)&(p5>=0&p5<=3|p5>=7&p5<=8)&(p6>=0&p6<=3|p6>=7&p6<=8)&(p7>=0&p7<=3|p7>=7&p7<=8)&(p8>=0&p8<=3|p8>=7&p8<=8);
// none in enter
formula none_e = p2!=2..3 & p3!=2..3 & p4!=2..3 & p5!=2..3 & p6!=2..3 & p7!=2..3 & p8!=2..3;
formula none_e = !(p2>=2&p2<=3)&!(p3>=2&p3<=3)&!(p4>=2&p4<=3)&!(p5>=2&p5<=3)&!(p6>=2&p6<=3)&!(p7>=2&p7<=3)&!(p8>=2&p8<=3);
module process1
@ -48,11 +49,21 @@ endmodule
// construct further modules through renaming
module process2 = process1 [p1=p2, p2=p1] endmodule
module process3 = process1 [p1=p3, p3=p1] endmodule
module process4 = process1 [p1=p4, p4=p1] endmodule
module process5 = process1 [p1=p5, p5=p1] endmodule
module process6 = process1 [p1=p6, p6=p1] endmodule
module process7 = process1 [p1=p7, p7=p1] endmodule
module process8 = process1 [p1=p8, p8=p1] endmodule
module process2 = process1 [ p1=p2, p2=p1 ] endmodule
module process3 = process1 [ p1=p3, p3=p1 ] endmodule
module process4 = process1 [ p1=p4, p4=p1 ] endmodule
module process5 = process1 [ p1=p5, p5=p1 ] endmodule
module process6 = process1 [ p1=p6, p6=p1 ] endmodule
module process7 = process1 [ p1=p7, p7=p1 ] endmodule
module process8 = process1 [ p1=p8, p8=p1 ] endmodule
// formulas/labels for properties
// number of procs in critical section
formula num_crit = p1>9?1:0+p1>9?1:0+p1>9?1:0+p1>9?1:0+p1>9?1:0+p1>9?1:0+p1>9?1:0+p1>9?1:0;
// some process is between 4 and 13
label "some_4_13" = (p1>=4&p1<=13)|(p2>=4&p2<=13)|(p3>=4&p3<=13)|(p4>=4&p4<=13)|(p5>=4&p5<=13)|(p6>=4&p6<=13)|(p7>=4&p7<=13)|(p8>=4&p8<=13);
// some process is in 14
label "some_14" = (p1=14)|(p2=14)|(p3=14)|(p4=14)|(p5=14)|(p6=14)|(p7=14)|(p8=14);

51
prism-examples/mutual/mutual8.pctl
View File

@ -1,51 +0,0 @@
// theorem 1 (mutual exclusion)
(!((p1>9) & (p2>9))) &
(!((p1>9) & (p3>9))) &
(!((p1>9) & (p4>9))) &
(!((p1>9) & (p5>9))) &
(!((p1>9) & (p6>9))) &
(!((p1>9) & (p7>9))) &
(!((p1>9) & (p8>9))) &
(!((p2>9) & (p3>9))) &
(!((p2>9) & (p4>9))) &
(!((p2>9) & (p5>9))) &
(!((p2>9) & (p6>9))) &
(!((p2>9) & (p7>9))) &
(!((p2>9) & (p8>9))) &
(!((p3>9) & (p4>9))) &
(!((p3>9) & (p5>9))) &
(!((p3>9) & (p6>9))) &
(!((p3>9) & (p7>9))) &
(!((p3>9) & (p8>9))) &
(!((p4>9) & (p5>9))) &
(!((p4>9) & (p6>9))) &
(!((p4>9) & (p7>9))) &
(!((p4>9) & (p8>9))) &
(!((p5>9) & (p6>9))) &
(!((p5>9) & (p7>9))) &
(!((p5>9) & (p8>9))) &
(!((p6>9) & (p7>9))) &
(!((p6>9) & (p8>9))) &
(!((p7>9) & (p8>9)))
// lemma c
// if the crical section is occupied then eventually it becomes clear
(p1>9) | (p2>9) | (p3>9) | (p4>9) | (p5>9) | (p6>9) | (p7>9) | (p8>9) =>
P>=1 [ true U (p1<10) & (p2<10) & (p3<10) & (p4<10) & (p5<10) & (p6<10) & (p7<10) & (p8<10) ]
// lemma d
// if a process is between 4 and 13 (in our version) then eventually some process gets to 14
((p1>3) & (p1<14)) | ((p2>3) & (p2<14)) | ((p3>3) & (p3<14)) | ((p4>3) & (p4<14)) | ((p5>3) & (p5<14)) | ((p6>3) & (p6<14)) | ((p7>3) & (p7<14)) | ((p8>3) & (p8<14)) =>
P>=1 [ true U (p1=14) | (p2=14) | (p3=14) | (p4=14) | (p5=14) | (p6=14) | (p7=14) | (p8=14) ]
// theorem 2 (liveness)
// if process 1 tries then eventually it enters the critical section
(p1=1) => P>=1 [ true U (p1=10) ]
// not probability 1
P<=0.5 [ (p2!=10 & p3!=10) U (p1=10) ]
Write Preview
Loading…
Cancel
Save