diff --git a/prism-examples/mutual/.autopp b/prism-examples/mutual/.autopp new file mode 100755 index 00000000..d23a35b2 --- /dev/null +++ b/prism-examples/mutual/.autopp @@ -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 diff --git a/prism-examples/mutual/.mutualN.nm.pp b/prism-examples/mutual/.mutualN.nm.pp new file mode 100644 index 00000000..6b39966d --- /dev/null +++ b/prism-examples/mutual/.mutualN.nm.pp @@ -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#; + + diff --git a/prism-examples/mutual/auto b/prism-examples/mutual/auto index a4fda4f8..576fb8e0 100755 --- a/prism-examples/mutual/auto +++ b/prism-examples/mutual/auto @@ -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 diff --git a/prism-examples/mutual/mutual.pctl b/prism-examples/mutual/mutual.pctl new file mode 100644 index 00000000..5baa9265 --- /dev/null +++ b/prism-examples/mutual/mutual.pctl @@ -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 ] diff --git a/prism-examples/mutual/mutual10.nm b/prism-examples/mutual/mutual10.nm index a51a40d7..41c13ff4 100644 --- a/prism-examples/mutual/mutual10.nm +++ b/prism-examples/mutual/mutual10.nm @@ -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); + diff --git a/prism-examples/mutual/mutual10.pctl b/prism-examples/mutual/mutual10.pctl deleted file mode 100644 index 4ed39da8..00000000 --- a/prism-examples/mutual/mutual10.pctl +++ /dev/null @@ -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) ] diff --git a/prism-examples/mutual/mutual3.nm b/prism-examples/mutual/mutual3.nm index fe212e89..8724ac66 100644 --- a/prism-examples/mutual/mutual3.nm +++ b/prism-examples/mutual/mutual3.nm @@ -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); + diff --git a/prism-examples/mutual/mutual3.pctl b/prism-examples/mutual/mutual3.pctl deleted file mode 100644 index e8c3bbad..00000000 --- a/prism-examples/mutual/mutual3.pctl +++ /dev/null @@ -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) ] diff --git a/prism-examples/mutual/mutual4.nm b/prism-examples/mutual/mutual4.nm index 1d468802..ece23046 100644 --- a/prism-examples/mutual/mutual4.nm +++ b/prism-examples/mutual/mutual4.nm @@ -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); + diff --git a/prism-examples/mutual/mutual4.pctl b/prism-examples/mutual/mutual4.pctl deleted file mode 100644 index 97ea3616..00000000 --- a/prism-examples/mutual/mutual4.pctl +++ /dev/null @@ -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) ] diff --git a/prism-examples/mutual/mutual5.nm b/prism-examples/mutual/mutual5.nm index b3f10119..3008c596 100644 --- a/prism-examples/mutual/mutual5.nm +++ b/prism-examples/mutual/mutual5.nm @@ -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); + diff --git a/prism-examples/mutual/mutual5.pctl b/prism-examples/mutual/mutual5.pctl deleted file mode 100644 index c5783194..00000000 --- a/prism-examples/mutual/mutual5.pctl +++ /dev/null @@ -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) ] diff --git a/prism-examples/mutual/mutual8.nm b/prism-examples/mutual/mutual8.nm index d834812a..b2bb6ac8 100644 --- a/prism-examples/mutual/mutual8.nm +++ b/prism-examples/mutual/mutual8.nm @@ -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); + diff --git a/prism-examples/mutual/mutual8.pctl b/prism-examples/mutual/mutual8.pctl deleted file mode 100644 index 02228669..00000000 --- a/prism-examples/mutual/mutual8.pctl +++ /dev/null @@ -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) ]