updated rewards in polling files

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

prism-examples/brp/brp.pm

@@ -99,7 +99,7 @@ module checker
 
 	T : bool;
 	
-	//[NewFile] (T=false) -> (T'=false);
+//	[NewFile] (T=false) -> (T'=false);
 	[NewFile] (T=false) -> (T'=true);
 	
 endmodule

prism-examples/cell/cell.sm

@@ -22,8 +22,6 @@ module cell
 endmodule
 
 // rewards - number calls in the cell
-rewards
-	
+rewards "calls"
 	true : n;
-	
 endrewards

prism-examples/leader/synchronous/leader4_8.pm

@@ -1,4 +1,4 @@
-// synchronous leader election protocol  (itai & Rodeh)
+// synchronous leader election protocol (itai & Rodeh)
 // dxp/gxn 25/01/01
 // N=4 and K=8
 
@@ -83,7 +83,5 @@ module process4=process1[s1=s4,p1=p4,v1=v4,u1=u4,v2=v1] endmodule
 
 // REWARDS -expected number of rounds
 rewards
-	
 	[pick] true : 1;
-	
 endrewards

prism-examples/polling/poll.csl

@@ -1,3 +1,6 @@
+// time bound
+const double T;
+
 //Probability that in the long run station 1 is awaiting service 
 S=? [ s1=1 & !(s=1 & a=1) ]
 
@@ -11,12 +14,10 @@ P=? [ true U (s=1 & a=0) {s1=1}{min} ]
 P=? [ !(s=2 & a=1) U (s=1 & a=1) ]
 
 // once a station becomes full, probability it will be polled within T time units is ...
-const int T;
 P=?[ true U<=T (s=1 & a=0) ]
 
 // expected reward accumlated by time T
-// waiting=1 and served=0 for expected time station 1 spends awaiting service
-// waiting=0 and served=1 for expected number of times station 1 is served
-R=?[C<=T]
+R{"waiting"}=?[C<=T] // time the station 1 is waiting to be served
+R{"served"}=?[C<=T] // number of times station1 is served
 
 

prism-examples/polling/poll10.sm

@@ -78,12 +78,11 @@ module station9 = station1 [s1=s9, loop1a=loop9a, loop1b=loop9b, serve1=serve9]
 module station10 = station1 [s1=s10, loop1a=loop10a, loop1b=loop10b, serve1=serve10] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll11.sm

@@ -83,12 +83,11 @@ module station10 = station1 [s1=s10, loop1a=loop10a, loop1b=loop10b, serve1=serv
 module station11 = station1 [s1=s11, loop1a=loop11a, loop1b=loop11b, serve1=serve11] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll12.sm

@@ -88,12 +88,11 @@ module station11 = station1 [s1=s11, loop1a=loop11a, loop1b=loop11b, serve1=serv
 module station12 = station1 [s1=s12, loop1a=loop12a, loop1b=loop12b, serve1=serve12] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll13.sm

@@ -94,12 +94,11 @@ module station12 = station1 [s1=s12, loop1a=loop12a, loop1b=loop12b, serve1=serv
 module station13 = station1 [s1=s13, loop1a=loop13a, loop1b=loop13b, serve1=serve13] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll14.sm

@@ -98,12 +98,11 @@ module station13 = station1 [s1=s13, loop1a=loop13a, loop1b=loop13b, serve1=serv
 module station14 = station1 [s1=s14, loop1a=loop14a, loop1b=loop14b, serve1=serve14] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll15.sm

@@ -103,12 +103,11 @@ module station14 = station1 [s1=s14, loop1a=loop14a, loop1b=loop14b, serve1=serv
 module station15 = station1 [s1=s15, loop1a=loop15a, loop1b=loop15b, serve1=serve15] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll16.sm

@@ -108,12 +108,11 @@ module station15 = station1 [s1=s15, loop1a=loop15a, loop1b=loop15b, serve1=serv
 module station16 = station1 [s1=s16, loop1a=loop16a, loop1b=loop16b, serve1=serve16] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll17.sm

@@ -113,12 +113,11 @@ module station16 = station1 [s1=s16, loop1a=loop16a, loop1b=loop16b, serve1=serv
 module station17 = station1 [s1=s17, loop1a=loop17a, loop1b=loop17b, serve1=serve17] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll18.sm

@@ -118,12 +118,11 @@ module station17 = station1 [s1=s17, loop1a=loop17a, loop1b=loop17b, serve1=serv
 module station18 = station1 [s1=s18, loop1a=loop18a, loop1b=loop18b, serve1=serve18] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll19.sm

@@ -123,12 +123,11 @@ module station18 = station1 [s1=s18, loop1a=loop18a, loop1b=loop18b, serve1=serv
 module station19 = station1 [s1=s19, loop1a=loop19a, loop1b=loop19b, serve1=serve19] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll2.sm

@@ -38,12 +38,11 @@ endmodule
 module station2 = station1 [s1=s2, loop1a=loop2a, loop1b=loop2b, serve1=serve2] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll20.sm

@@ -128,12 +128,11 @@ module station19 = station1 [s1=s19, loop1a=loop19a, loop1b=loop19b, serve1=serv
 module station20 = station1 [s1=s20, loop1a=loop20a, loop1b=loop20b, serve1=serve20] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll3.sm

@@ -43,12 +43,11 @@ module station2 = station1 [s1=s2, loop1a=loop2a, loop1b=loop2b, serve1=serve2]
 module station3 = station1 [s1=s3, loop1a=loop3a, loop1b=loop3b, serve1=serve3] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll4.sm

@@ -48,12 +48,11 @@ module station3 = station1 [s1=s3, loop1a=loop3a, loop1b=loop3b, serve1=serve3]
 module station4 = station1 [s1=s4, loop1a=loop4a, loop1b=loop4b, serve1=serve4] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll5.sm

@@ -53,12 +53,11 @@ module station4 = station1 [s1=s4, loop1a=loop4a, loop1b=loop4b, serve1=serve4]
 module station5 = station1 [s1=s5, loop1a=loop5a, loop1b=loop5b, serve1=serve5] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll6.sm

@@ -58,12 +58,11 @@ module station5 = station1 [s1=s5, loop1a=loop5a, loop1b=loop5b, serve1=serve5]
 module station6 = station1 [s1=s6, loop1a=loop6a, loop1b=loop6b, serve1=serve6] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll7.sm

@@ -63,12 +63,11 @@ module station6 = station1 [s1=s6, loop1a=loop6a, loop1b=loop6b, serve1=serve6]
 module station7 = station1 [s1=s7, loop1a=loop7a, loop1b=loop7b, serve1=serve7] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll8.sm

@@ -68,12 +68,11 @@ module station7 = station1 [s1=s7, loop1a=loop7a, loop1b=loop7b, serve1=serve7]
 module station8 = station1 [s1=s8, loop1a=loop8a, loop1b=loop8b, serve1=serve8] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards

prism-examples/polling/poll9.sm

@@ -73,12 +73,11 @@ module station8 = station1 [s1=s8, loop1a=loop8a, loop1b=loop8b, serve1=serve8]
 module station9 = station1 [s1=s9, loop1a=loop9a, loop1b=loop9b, serve1=serve9] endmodule
 
 // cumulative rewards
-const int waiting = 1; // expected time the station 1 is waiting to be served
-const int served = 0; // expected number of times station1 is served 
 
-rewards
-	
-	s1=1 & !(s=1 & a=1) : waiting;
-	[serve1] true : served;
-	
+rewards "waiting" // expected time the station 1 is waiting to be served
+	s1=1 & !(s=1 & a=1) : 1;
+endrewards
+
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
 endrewards