updated properties and rewards in phil (no fair)

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

prism-examples/phil/nofair/phil-nofair10.nm

@@ -1,11 +1,11 @@
 // 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)
 
-// dxp/gxn 23/01/02
-
 nondeterministic
 
 // atomic formulae 

prism-examples/phil/nofair/phil-nofair3.nm

@@ -1,11 +1,11 @@
 // 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)
 
-// dxp/gxn 23/01/02
-
 nondeterministic
 
 // atomic formulae 
@@ -40,8 +40,6 @@ 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
-	
+rewards "steps"
 	[] true : 1;
-	
 endrewards

prism-examples/phil/nofair/phil-nofair4.nm

@@ -1,11 +1,11 @@
 // 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)
 
-// dxp/gxn 23/01/02
-
 nondeterministic
 
 // atomic formulae 

prism-examples/phil/nofair/phil-nofair5.nm

@@ -1,11 +1,11 @@
 // 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)
 
-// dxp/gxn 23/01/02
-
 nondeterministic
 
 // atomic formulae 

prism-examples/phil/nofair/phil-nofair6.nm

@@ -1,11 +1,11 @@
 // 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)
 
-// dxp/gxn 23/01/02
-
 nondeterministic
 
 // atomic formulae 

prism-examples/phil/nofair/phil-nofair7.nm

@@ -1,11 +1,11 @@
 // 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)
 
-// dxp/gxn 23/01/02
-
 nondeterministic
 
 // atomic formulae 

prism-examples/phil/nofair/phil-nofair8.nm

@@ -1,11 +1,11 @@
 // 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)
 
-// dxp/gxn 23/01/02
-
 nondeterministic
 
 // atomic formulae 

prism-examples/phil/nofair/phil-nofair9.nm

@@ -1,5 +1,10 @@
 // randomized dining philosophers [LR81]
-// dxp/gxn 12/12/99
+// 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)
  
 nondeterministic
 

prism-examples/phil/nofair/phil3.pctl

@@ -1,9 +1,13 @@
+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)
-const int K;
 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}]
+Rmax=?[F "eat" {"hungry"}{max}]

prism-examples/phil/nofair/phil4.pctl

@@ -1,9 +1,13 @@
+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)
-const int K;
 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,9 +1,13 @@
+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)
-const int K;
 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,9 +1,13 @@
+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)
-const int K;
 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,9 +1,13 @@
+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)
-const int K;
 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,9 +1,13 @@
+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)
-const int K;
 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,9 +1,13 @@
+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)
-const int K;
 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}]