updated reward structures in phil_lss files

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

prism-examples/phil_lss/phil_lss3.nm

@@ -91,11 +91,9 @@ endmodule
 module phil2=phil1 [p1=p2, p2=p3, p3=p1, s1=s2] endmodule
 module phil3=phil1 [p1=p3, p2=p1, p3=p2, s1=s3] endmodule
 
-// rewards - expected number of steps
-rewards
-	
+// reward structure - number of steps
+rewards "steps"
 	[s1] true : 1;
 	[s2] true : 1;
 	[s3] true : 1;
-	
-endrewards
+endrewards

prism-examples/phil_lss/phil_lss3.pctl

@@ -1,12 +1,13 @@
-// philosopher in its trying region
-label "trying" =((p1>0) & (p1<8))  | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8));
-// philosopher in its critical section
-label "entered" =((p1>7) & (p1<13)) | ((p2>7) & (p2<13)) | ((p3>7) & (p3<13));
+const int L; // discrete time bound
+
+label "trying" =((p1>0) & (p1<8))  | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)); // philosopher in its trying region
+label "entered" =((p1>7) & (p1<13)) | ((p2>7) & (p2<13)) | ((p3>7) & (p3<13)); // philosopher in its critical section
 
 // lockout free
 "trying" =>  P>=1 [ true U "entered" ]
+
 // bounded until: minimum probability (from a state where a process is in its trying region) that some process enters its critical section within k steps
-const int L;
 Pmin=? [ true U<=L "entered" {"trying"}{min} ]
+
 // expected time: maximum expected time (from a state where a process is in its trying region) that some process enters its critical section
 Rmax=? [ F "entered" {"trying"}{max} ]

prism-examples/phil_lss/phil_lss4.nm

@@ -119,12 +119,10 @@ module phil2=phil1 [p1=p2, p2=p3, p3=p4, p4=p1, s1=s2] endmodule
 module phil3=phil1 [p1=p3, p2=p4, p3=p1, p4=p2, s1=s3] endmodule
 module phil4=phil1 [p1=p4, p2=p1, p3=p2, p4=p3, s1=s4] endmodule
 
-// rewards - expected number of steps
-rewards
-	
+// reward structure - number of steps
+rewards "steps"
 	[s1] true : 1;
 	[s2] true : 1;
 	[s3] true : 1;
 	[s4] true : 1;
-	
-endrewards
+endrewards

prism-examples/phil_lss/phil_lss4.pctl

@@ -1,12 +1,13 @@
-// philosopher in its trying region
-label "trying" =((p1>0) & (p1<8))  | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)) | ((p4>0) & (p4<8));
-// philosopher in its critical section
-label "entered" =((p1>7) & (p1<13)) | ((p2>7) & (p2<13)) | ((p3>7) & (p3<13)) | ((p4>7) & (p4<13));
+const int L; // discrete time bound
+
+label "trying" =((p1>0) & (p1<8))  | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)) | ((p4>0) & (p4<8)); // philosopher in its trying region
+label "entered" =((p1>7) & (p1<13)) | ((p2>7) & (p2<13)) | ((p3>7) & (p3<13)) | ((p4>7) & (p4<13)); // philosopher in its critical section
 
 // lockout free
 "trying" =>  P>=1 [ true U "entered" ]
+
 // bounded until: minimum probability (from a state where a process is in its trying region) that some process enters its critical section within k steps
-const int L;
 Pmin=? [ true U<=L "entered" {"trying"}{min} ]
+
 // expected time: maximum expected time (from a state where a process is in its trying region) that some process enters its critical section
 Rmax=? [ F "entered" {"trying"}{max} ]