diff --git a/prism-examples/phil/nofair/.autopp b/prism-examples/phil/nofair/.autopp new file mode 100755 index 00000000..82a46aba --- /dev/null +++ b/prism-examples/phil/nofair/.autopp @@ -0,0 +1,7 @@ +#!/bin/csh + +foreach N ( 3 4 5 6 7 8 9 ) + echo "Generating for N=$N" + prismpp .phil-nofairN.nm.pp $N >! phil-nofair"$N".nm + unix2dos phil-nofair"$N".nm +end diff --git a/prism-examples/phil/nofair/.phil-nofairN.nm.pp b/prism-examples/phil/nofair/.phil-nofairN.nm.pp new file mode 100644 index 00000000..24548bf6 --- /dev/null +++ b/prism-examples/phil/nofair/.phil-nofairN.nm.pp @@ -0,0 +1,52 @@ +#const N# +// randomized dining philosophers [LR81] +// dxp/gxn 23/01/02 + +// model which does not require fairness +// remove the possibility of loops: +// (1) cannot stay in thinking +// (2) if first fork not free then cannot move (another philosopher must more) + +mdp + +// atomic formulae +// left fork free and right fork free resp. +formula lfree = p2>=0&p2<=4|p2=6|p2=10; +formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11; + +module phil1 + + p1: [0..11]; + + [] p1=0 -> (p1'=1); // trying + [] p1=1 -> 0.5 : (p1'=2) + 0.5 : (p1'=3); // draw randomly + [] p1=2 & lfree -> (p1'=4); // pick up left + [] p1=3 & rfree -> (p1'=5); // pick up right + [] p1=4 & rfree -> (p1'=8); // pick up right (got left) + [] p1=4 & !rfree -> (p1'=6); // right not free (got left) + [] p1=5 & lfree -> (p1'=8); // pick up left (got right) + [] p1=5 & !lfree -> (p1'=7); // left not free (got right) + [] p1=6 -> (p1'=1); // put down left + [] p1=7 -> (p1'=1); // put down right + [] p1=8 -> (p1'=9); // move to eating (got forks) + [] p1=9 -> (p1'=10); // finished eating and put down left + [] p1=9 -> (p1'=11); // finished eating and put down right + [] p1=10 -> (p1'=0); // put down right and return to think + [] p1=11 -> (p1'=0); // put down left and return to think + +endmodule + +// construct further modules through renaming +#for i=2:N# +module phil#i# = phil1 [ p1=p#i#, p2=p#mod(i,N)+1#, p3=p#mod(i-2,N)+1# ] endmodule +#end# + +// rewards (number of steps) +rewards "num_steps" + [] true : 1; +endrewards +// labels +label "hungry" = #| i=1:N#((p#i#>0)&(p#i#<8))#end#; +label "eat" = #| i=1:N#((p#i#>=8)&(p#i#<=9))#end#; + + diff --git a/prism-examples/phil/nofair/auto b/prism-examples/phil/nofair/auto index 7a08923f..b50fe81b 100755 --- a/prism-examples/phil/nofair/auto +++ b/prism-examples/phil/nofair/auto @@ -1,10 +1,10 @@ #!/bin/csh -prism phil-nofair3.nm phil3.pctl -const K=1 -m -prism phil-nofair4.nm phil4.pctl -const K=1 -m -prism phil-nofair5.nm phil5.pctl -const K=1 -m -prism phil-nofair6.nm phil6.pctl -const K=1 -m -prism phil-nofair7.nm phil7.pctl -const K=1 -m -prism phil-nofair8.nm phil8.pctl -const K=1 -m -prism phil-nofair9.nm phil9.pctl -const K=1 -m -prism phil-nofair10.nm phil10.pctl -const K=1 -m +prism phil-nofair3.nm phil.pctl -const K=1 -m +prism phil-nofair4.nm phil.pctl -const K=1 -m +prism phil-nofair5.nm phil.pctl -const K=1 -m +prism phil-nofair6.nm phil.pctl -const K=1 -m +#prism phil-nofair7.nm phil.pctl -const K=1 -m +#prism phil-nofair8.nm phil.pctl -const K=1 -m +#prism phil-nofair9.nm phil.pctl -const K=1 -m +#prism phil-nofair10.nm phil.pctl -const K=1 -m diff --git a/prism-examples/phil/nofair/leader.pctl b/prism-examples/phil/nofair/leader.pctl new file mode 100644 index 00000000..0ad052c0 --- /dev/null +++ b/prism-examples/phil/nofair/leader.pctl @@ -0,0 +1,12 @@ +const int K; + +// Liveness (if a philosopher is hungry then eventually some philosopher eats) +"hungry" => P>=1 [ F "eat"] + +// Bounded until (minimum probability, from a state where someone +// is hungry, that a philosopher will eat within K steps) +Pmin=? [ F<=K "eat" {"hungry"}{min} ] + +// Expected time (from a state where someone is hungry, the maximum +// expected number of steps until a philosopher eats) +R{"num_steps"}max=? [F "eat" {"hungry"}{max} ] diff --git a/prism-examples/phil/nofair/phil-nofair3.nm b/prism-examples/phil/nofair/phil-nofair3.nm index 9b46aaad..6bb34a61 100644 --- a/prism-examples/phil/nofair/phil-nofair3.nm +++ b/prism-examples/phil/nofair/phil-nofair3.nm @@ -10,8 +10,8 @@ mdp // atomic formulae // left fork free and right fork free resp. -formula lfree = p2=0..4,6,10; -formula rfree = p3=0..3,5,7,11; +formula lfree = p2>=0&p2<=4|p2=6|p2=10; +formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11; module phil1 @@ -36,10 +36,15 @@ module phil1 endmodule // construct further modules through renaming -module phil2 = phil1 [p1=p2, p2=p3, p3=p1] endmodule -module phil3 = phil1 [p1=p3, p2=p1, p3=p2] endmodule +module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule +module phil3 = phil1 [ p1=p3, p2=p1, p3=p2 ] endmodule // rewards (number of steps) -rewards "steps" +rewards "num_steps" [] true : 1; endrewards +// labels +label "hungry" = ((p1>0)&(p1<8))|((p2>0)&(p2<8))|((p3>0)&(p3<8)); +label "eat" = ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9)); + + diff --git a/prism-examples/phil/nofair/phil-nofair4.nm b/prism-examples/phil/nofair/phil-nofair4.nm index 6ea7f254..ee0b8d78 100644 --- a/prism-examples/phil/nofair/phil-nofair4.nm +++ b/prism-examples/phil/nofair/phil-nofair4.nm @@ -10,8 +10,8 @@ mdp // atomic formulae // left fork free and right fork free resp. -formula lfree = p2=0..4,6,10; -formula rfree = p4=0..3,5,7,11; +formula lfree = p2>=0&p2<=4|p2=6|p2=10; +formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11; module phil1 @@ -36,13 +36,16 @@ module phil1 endmodule // construct further modules through renaming -module phil2 = phil1 [p1=p2, p2=p3, p4=p1] endmodule -module phil3 = phil1 [p1=p3, p2=p4, p4=p2] endmodule -module phil4 = phil1 [p1=p4, p2=p1, p4=p3] endmodule +module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule +module phil3 = phil1 [ p1=p3, p2=p4, p3=p2 ] endmodule +module phil4 = phil1 [ p1=p4, p2=p1, p3=p3 ] endmodule // rewards (number of steps) -rewards - +rewards "num_steps" [] true : 1; - endrewards +// labels +label "hungry" = ((p1>0)&(p1<8))|((p2>0)&(p2<8))|((p3>0)&(p3<8))|((p4>0)&(p4<8)); +label "eat" = ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9))|((p4>=8)&(p4<=9)); + + diff --git a/prism-examples/phil/nofair/phil-nofair5.nm b/prism-examples/phil/nofair/phil-nofair5.nm index a12e9b69..e77a586f 100644 --- a/prism-examples/phil/nofair/phil-nofair5.nm +++ b/prism-examples/phil/nofair/phil-nofair5.nm @@ -10,8 +10,8 @@ mdp // atomic formulae // left fork free and right fork free resp. -formula lfree = p2=0..4,6,10; -formula rfree = p5=0..3,5,7,11; +formula lfree = p2>=0&p2<=4|p2=6|p2=10; +formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11; module phil1 @@ -36,14 +36,17 @@ module phil1 endmodule // construct further modules through renaming -module phil2 = phil1 [p1=p2, p2=p3, p5=p1] endmodule -module phil3 = phil1 [p1=p3, p2=p4, p5=p2] endmodule -module phil4 = phil1 [p1=p4, p2=p5, p5=p3] endmodule -module phil5 = phil1 [p1=p5, p2=p1, p5=p4] endmodule +module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule +module phil3 = phil1 [ p1=p3, p2=p4, p3=p2 ] endmodule +module phil4 = phil1 [ p1=p4, p2=p5, p3=p3 ] endmodule +module phil5 = phil1 [ p1=p5, p2=p1, p3=p4 ] endmodule // rewards (number of steps) -rewards - +rewards "num_steps" [] true : 1; - endrewards +// labels +label "hungry" = ((p1>0)&(p1<8))|((p2>0)&(p2<8))|((p3>0)&(p3<8))|((p4>0)&(p4<8))|((p5>0)&(p5<8)); +label "eat" = ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9))|((p4>=8)&(p4<=9))|((p5>=8)&(p5<=9)); + + diff --git a/prism-examples/phil/nofair/phil-nofair6.nm b/prism-examples/phil/nofair/phil-nofair6.nm index 58588e9a..4936f9ea 100644 --- a/prism-examples/phil/nofair/phil-nofair6.nm +++ b/prism-examples/phil/nofair/phil-nofair6.nm @@ -10,8 +10,8 @@ mdp // atomic formulae // left fork free and right fork free resp. -formula lfree = p2=0..4,6,10; -formula rfree = p6=0..3,5,7,11; +formula lfree = p2>=0&p2<=4|p2=6|p2=10; +formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11; module phil1 @@ -36,15 +36,18 @@ module phil1 endmodule // construct further modules through renaming -module phil2 = phil1 [p1=p2, p2=p3, p6=p1] endmodule -module phil3 = phil1 [p1=p3, p2=p4, p6=p2] endmodule -module phil4 = phil1 [p1=p4, p2=p5, p6=p3] endmodule -module phil5 = phil1 [p1=p5, p2=p6, p6=p4] endmodule -module phil6 = phil1 [p1=p6, p2=p1, p6=p5] endmodule +module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule +module phil3 = phil1 [ p1=p3, p2=p4, p3=p2 ] endmodule +module phil4 = phil1 [ p1=p4, p2=p5, p3=p3 ] endmodule +module phil5 = phil1 [ p1=p5, p2=p6, p3=p4 ] endmodule +module phil6 = phil1 [ p1=p6, p2=p1, p3=p5 ] endmodule // rewards (number of steps) -rewards - +rewards "num_steps" [] true : 1; - endrewards +// labels +label "hungry" = ((p1>0)&(p1<8))|((p2>0)&(p2<8))|((p3>0)&(p3<8))|((p4>0)&(p4<8))|((p5>0)&(p5<8))|((p6>0)&(p6<8)); +label "eat" = ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9))|((p4>=8)&(p4<=9))|((p5>=8)&(p5<=9))|((p6>=8)&(p6<=9)); + + diff --git a/prism-examples/phil/nofair/phil-nofair7.nm b/prism-examples/phil/nofair/phil-nofair7.nm index 95c1dc82..b33d0786 100644 --- a/prism-examples/phil/nofair/phil-nofair7.nm +++ b/prism-examples/phil/nofair/phil-nofair7.nm @@ -10,8 +10,8 @@ mdp // atomic formulae // left fork free and right fork free resp. -formula lfree = p2=0..4,6,10; -formula rfree = p7=0..3,5,7,11; +formula lfree = p2>=0&p2<=4|p2=6|p2=10; +formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11; module phil1 @@ -36,16 +36,19 @@ module phil1 endmodule // construct further modules through renaming -module phil2 = phil1 [p1=p2, p2=p3, p7=p1] endmodule -module phil3 = phil1 [p1=p3, p2=p4, p7=p2] endmodule -module phil4 = phil1 [p1=p4, p2=p5, p7=p3] endmodule -module phil5 = phil1 [p1=p5, p2=p6, p7=p4] endmodule -module phil6 = phil1 [p1=p6, p2=p7, p7=p5] endmodule -module phil7 = phil1 [p1=p7, p2=p1, p7=p6] endmodule +module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule +module phil3 = phil1 [ p1=p3, p2=p4, p3=p2 ] endmodule +module phil4 = phil1 [ p1=p4, p2=p5, p3=p3 ] endmodule +module phil5 = phil1 [ p1=p5, p2=p6, p3=p4 ] endmodule +module phil6 = phil1 [ p1=p6, p2=p7, p3=p5 ] endmodule +module phil7 = phil1 [ p1=p7, p2=p1, p3=p6 ] endmodule // rewards (number of steps) -rewards - +rewards "num_steps" [] true : 1; - endrewards +// labels +label "hungry" = ((p1>0)&(p1<8))|((p2>0)&(p2<8))|((p3>0)&(p3<8))|((p4>0)&(p4<8))|((p5>0)&(p5<8))|((p6>0)&(p6<8))|((p7>0)&(p7<8)); +label "eat" = ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9))|((p4>=8)&(p4<=9))|((p5>=8)&(p5<=9))|((p6>=8)&(p6<=9))|((p7>=8)&(p7<=9)); + + diff --git a/prism-examples/phil/nofair/phil-nofair8.nm b/prism-examples/phil/nofair/phil-nofair8.nm index cf7d2d2a..558612c4 100644 --- a/prism-examples/phil/nofair/phil-nofair8.nm +++ b/prism-examples/phil/nofair/phil-nofair8.nm @@ -10,8 +10,8 @@ mdp // atomic formulae // left fork free and right fork free resp. -formula lfree = p2=0..4,6,10; -formula rfree = p8=0..3,5,7,11; +formula lfree = p2>=0&p2<=4|p2=6|p2=10; +formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11; module phil1 @@ -36,17 +36,20 @@ module phil1 endmodule // construct further modules through renaming -module phil2 = phil1 [p1=p2, p2=p3, p8=p1] endmodule -module phil3 = phil1 [p1=p3, p2=p4, p8=p2] endmodule -module phil4 = phil1 [p1=p4, p2=p5, p8=p3] endmodule -module phil5 = phil1 [p1=p5, p2=p6, p8=p4] endmodule -module phil6 = phil1 [p1=p6, p2=p7, p8=p5] endmodule -module phil7 = phil1 [p1=p7, p2=p8, p8=p6] endmodule -module phil8 = phil1 [p1=p8, p2=p1, p8=p7] endmodule +module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule +module phil3 = phil1 [ p1=p3, p2=p4, p3=p2 ] endmodule +module phil4 = phil1 [ p1=p4, p2=p5, p3=p3 ] endmodule +module phil5 = phil1 [ p1=p5, p2=p6, p3=p4 ] endmodule +module phil6 = phil1 [ p1=p6, p2=p7, p3=p5 ] endmodule +module phil7 = phil1 [ p1=p7, p2=p8, p3=p6 ] endmodule +module phil8 = phil1 [ p1=p8, p2=p1, p3=p7 ] endmodule // rewards (number of steps) -rewards - +rewards "num_steps" [] true : 1; - endrewards +// labels +label "hungry" = ((p1>0)&(p1<8))|((p2>0)&(p2<8))|((p3>0)&(p3<8))|((p4>0)&(p4<8))|((p5>0)&(p5<8))|((p6>0)&(p6<8))|((p7>0)&(p7<8))|((p8>0)&(p8<8)); +label "eat" = ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9))|((p4>=8)&(p4<=9))|((p5>=8)&(p5<=9))|((p6>=8)&(p6<=9))|((p7>=8)&(p7<=9))|((p8>=8)&(p8<=9)); + + diff --git a/prism-examples/phil/nofair/phil-nofair9.nm b/prism-examples/phil/nofair/phil-nofair9.nm index f6c68452..c7b0226f 100644 --- a/prism-examples/phil/nofair/phil-nofair9.nm +++ b/prism-examples/phil/nofair/phil-nofair9.nm @@ -10,8 +10,8 @@ mdp // atomic formulae // left fork free and right fork free resp. -formula lfree = p2=0..4,6,10; -formula rfree = p9=0..3,5,7,11; +formula lfree = p2>=0&p2<=4|p2=6|p2=10; +formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11; module phil1 @@ -36,18 +36,21 @@ module phil1 endmodule // construct further modules through renaming -module phil2 = phil1 [p1=p2, p2=p3, p9=p1] endmodule -module phil3 = phil1 [p1=p3, p2=p4, p9=p2] endmodule -module phil4 = phil1 [p1=p4, p2=p5, p9=p3] endmodule -module phil5 = phil1 [p1=p5, p2=p6, p9=p4] endmodule -module phil6 = phil1 [p1=p6, p2=p7, p9=p5] endmodule -module phil7 = phil1 [p1=p7, p2=p8, p9=p6] endmodule -module phil8 = phil1 [p1=p8, p2=p9, p9=p7] endmodule -module phil9 = phil1 [p1=p9, p2=p1, p9=p8] endmodule +module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule +module phil3 = phil1 [ p1=p3, p2=p4, p3=p2 ] endmodule +module phil4 = phil1 [ p1=p4, p2=p5, p3=p3 ] endmodule +module phil5 = phil1 [ p1=p5, p2=p6, p3=p4 ] endmodule +module phil6 = phil1 [ p1=p6, p2=p7, p3=p5 ] endmodule +module phil7 = phil1 [ p1=p7, p2=p8, p3=p6 ] endmodule +module phil8 = phil1 [ p1=p8, p2=p9, p3=p7 ] endmodule +module phil9 = phil1 [ p1=p9, p2=p1, p3=p8 ] endmodule // rewards (number of steps) -rewards - +rewards "num_steps" [] true : 1; - endrewards +// labels +label "hungry" = ((p1>0)&(p1<8))|((p2>0)&(p2<8))|((p3>0)&(p3<8))|((p4>0)&(p4<8))|((p5>0)&(p5<8))|((p6>0)&(p6<8))|((p7>0)&(p7<8))|((p8>0)&(p8<8))|((p9>0)&(p9<8)); +label "eat" = ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9))|((p4>=8)&(p4<=9))|((p5>=8)&(p5<=9))|((p6>=8)&(p6<=9))|((p7>=8)&(p7<=9))|((p8>=8)&(p8<=9))|((p9>=8)&(p9<=9)); + + diff --git a/prism-examples/phil/nofair/phil3.pctl b/prism-examples/phil/nofair/phil3.pctl deleted file mode 100644 index 2bd8e2f6..00000000 --- a/prism-examples/phil/nofair/phil3.pctl +++ /dev/null @@ -1,13 +0,0 @@ -const int K; // discrete time bound - -label "hungry" = ((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)); -label "eat" = (p1=8..9) | (p2=8..9) | (p3=8..9); - -// liveness (if a philosopher is hungry then eventually some philosopher eats) -"hungry" => P>=1 [ true U "eat"] - -// bounded until (minimum probability, from a state where someone is hungry, that a philosopher will eat within K steps) -Pmin=?[true U<=K "eat" {"hungry"}{min}] - -// expected time (from a state where someone is hungry the maximum exapected number of steps until a philosopher eats) -Rmax=?[F "eat" {"hungry"}{max}] diff --git a/prism-examples/phil/nofair/phil4.pctl b/prism-examples/phil/nofair/phil4.pctl deleted file mode 100644 index 6bd3cfdd..00000000 --- a/prism-examples/phil/nofair/phil4.pctl +++ /dev/null @@ -1,13 +0,0 @@ -const int K; // discrete time bound - -label "hungry" = ((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)) | ((p4>0) & (p4<8)); -label "eat" = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9); - -// liveness (if a philosopher is hungry then eventually some philosopher eats) -"hungry" => P>=1 [ true U "eat"] - -// bounded until (minimum probability, from a state where someone is hungry, that a philosopher will eat within K steps) -Pmin=?[true U<=K "eat" {"hungry"}{min}] - -// expected time (from a state where someone is hungry the maximum exapected number of steps until a philosopher eats) -Rmax=?[F "eat" {"hungry"}{max}] diff --git a/prism-examples/phil/nofair/phil5.pctl b/prism-examples/phil/nofair/phil5.pctl deleted file mode 100644 index 9e9c134a..00000000 --- a/prism-examples/phil/nofair/phil5.pctl +++ /dev/null @@ -1,13 +0,0 @@ -const int K; // discrete time bound - -label "hungry" = ((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)) | ((p4>0) & (p4<8)) | ((p5>0) & (p5<8)); -label "eat" = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9); - -// liveness (if a philosopher is hungry then eventually some philosopher eats) -"hungry" => P>=1 [ true U "eat"] - -// bounded until (minimum probability, from a state where someone is hungry, that a philosopher will eat within K steps) -Pmin=?[true U<=K "eat" {"hungry"}{min}] - -// expected time (from a state where someone is hungry the maximum exapected number of steps until a philosopher eats) -Rmax=?[F "eat" {"hungry"}{max}] diff --git a/prism-examples/phil/nofair/phil6.pctl b/prism-examples/phil/nofair/phil6.pctl deleted file mode 100644 index f490a4d0..00000000 --- a/prism-examples/phil/nofair/phil6.pctl +++ /dev/null @@ -1,13 +0,0 @@ -const int K; // discrete time bound - -label "hungry" = ((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)) | ((p4>0) & (p4<8)) | ((p5>0) & (p5<8)) | ((p6>0) & (p6<8)); -label "eat" = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9) | (p6=8..9); - -// liveness (if a philosopher is hungry then eventually some philosopher eats) -"hungry" => P>=1 [ true U "eat"] - -// bounded until (minimum probability, from a state where someone is hungry, that a philosopher will eat within K steps) -Pmin=?[true U<=K "eat" {"hungry"}{min}] - -// expected time (from a state where someone is hungry the maximum exapected number of steps until a philosopher eats) -Rmax=?[F "eat" {"hungry"}{max}] diff --git a/prism-examples/phil/nofair/phil7.pctl b/prism-examples/phil/nofair/phil7.pctl deleted file mode 100644 index 3697d135..00000000 --- a/prism-examples/phil/nofair/phil7.pctl +++ /dev/null @@ -1,13 +0,0 @@ -const int K; // discrete time bound - -label "hungry" = ((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)) | ((p4>0) & (p4<8)) | ((p5>0) & (p5<8)) | ((p6>0) & (p6<8)) | ((p7>0) & (p7<8)); -label "eat" = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9) | (p6=8..9) | (p7=8..9); - -// liveness (if a philosopher is hungry then eventually some philosopher eats) -"hungry" => P>=1 [ true U "eat"] - -// bounded until (minimum probability, from a state where someone is hungry, that a philosopher will eat within K steps) -Pmin=?[true U<=K "eat" {"hungry"}{min}] - -// expected time (from a state where someone is hungry the maximum exapected number of steps until a philosopher eats) -Rmax=?[F "eat" {"hungry"}{max}] diff --git a/prism-examples/phil/nofair/phil8.pctl b/prism-examples/phil/nofair/phil8.pctl deleted file mode 100644 index 1c0eee27..00000000 --- a/prism-examples/phil/nofair/phil8.pctl +++ /dev/null @@ -1,13 +0,0 @@ -const int K; // discrete time bound - -label "hungry" = ((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)) | ((p4>0) & (p4<8)) | ((p5>0) & (p5<8)) | ((p6>0) & (p6<8)) | ((p7>0) & (p7<8)) | ((p8>0) & (p8<8)); -label "eat" = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9) | (p6=8..9) | (p7=8..9) | (p8=8..9); - -// liveness (if a philosopher is hungry then eventually some philosopher eats) -"hungry" => P>=1 [ true U "eat"] - -// bounded until (minimum probability, from a state where someone is hungry, that a philosopher will eat within K steps) -Pmin=?[true U<=K "eat" {"hungry"}{min}] - -// expected time (from a state where someone is hungry the maximum exapected number of steps until a philosopher eats) -Rmax=?[F "eat" {"hungry"}{max}] diff --git a/prism-examples/phil/nofair/phil9.pctl b/prism-examples/phil/nofair/phil9.pctl deleted file mode 100644 index 6190fb92..00000000 --- a/prism-examples/phil/nofair/phil9.pctl +++ /dev/null @@ -1,13 +0,0 @@ -const int K; // discrete time bound - -label "hungry" = ((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)) | ((p4>0) & (p4<8)) | ((p5>0) & (p5<8)) | ((p6>0) & (p6<8)) | ((p7>0) & (p7<8)) | ((p8>0) & (p8<8)) | ((p9>0) & (p9<8)); -label "eat" = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9) | (p6=8..9) | (p7=8..9) | (p8=8..9) | (p9=8..9); - -// liveness (if a philosopher is hungry then eventually some philosopher eats) -"hungry" => P>=1 [ true U "eat"] - -// bounded until (minimum probability, from a state where someone is hungry, that a philosopher will eat within K steps) -Pmin=?[true U<=K "eat" {"hungry"}{min}] - -// expected time (from a state where someone is hungry the maximum exapected number of steps until a philosopher eats) -Rmax=?[F "eat" {"hungry"}{max}]