Tidy up phil/nofair (and add pp files).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@684 bbc10eb1-c90d-0410-af57-cb519fbb1720

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

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#;
+
+

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

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} ]

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));
+
+

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));
+
+

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));
+
+

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));
+
+

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));
+
+

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));
+
+

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));
+
+

prism-examples/phil/nofair/phil3.pctl

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

prism-examples/phil/nofair/phil4.pctl

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

prism-examples/phil/nofair/phil5.pctl

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

prism-examples/phil/nofair/phil6.pctl

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

prism-examples/phil/nofair/phil7.pctl

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

prism-examples/phil/nofair/phil8.pctl

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

prism-examples/phil/nofair/phil9.pctl

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