diff --git a/prism-examples/brp/brp.pm b/prism-examples/brp/brp.pm
index 8f94d7ad..37bd600e 100644
--- a/prism-examples/brp/brp.pm
+++ b/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
diff --git a/prism-examples/cell/cell.sm b/prism-examples/cell/cell.sm
index 3f97cf7d..d177f094 100644
--- a/prism-examples/cell/cell.sm
+++ b/prism-examples/cell/cell.sm
@@ -22,8 +22,6 @@ module cell
 endmodule
 
 // rewards - number calls in the cell
-rewards
-	
+rewards "calls"
 	true : n;
-	
 endrewards
diff --git a/prism-examples/leader/synchronous/leader4_8.pm b/prism-examples/leader/synchronous/leader4_8.pm
index 55e45d84..b55e6679 100644
--- a/prism-examples/leader/synchronous/leader4_8.pm
+++ b/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
diff --git a/prism-examples/polling/poll.csl b/prism-examples/polling/poll.csl
index e799ec44..f9d39974 100644
--- a/prism-examples/polling/poll.csl
+++ b/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
 
 
diff --git a/prism-examples/polling/poll10.sm b/prism-examples/polling/poll10.sm
index 0dc25c54..f993821d 100644
--- a/prism-examples/polling/poll10.sm
+++ b/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
diff --git a/prism-examples/polling/poll11.sm b/prism-examples/polling/poll11.sm
index b223c88c..56c315e6 100644
--- a/prism-examples/polling/poll11.sm
+++ b/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
diff --git a/prism-examples/polling/poll12.sm b/prism-examples/polling/poll12.sm
index 461b607b..17ce7a69 100644
--- a/prism-examples/polling/poll12.sm
+++ b/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
diff --git a/prism-examples/polling/poll13.sm b/prism-examples/polling/poll13.sm
index 2d401b4c..4926ef12 100644
--- a/prism-examples/polling/poll13.sm
+++ b/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
diff --git a/prism-examples/polling/poll14.sm b/prism-examples/polling/poll14.sm
index 91501706..ac91e554 100644
--- a/prism-examples/polling/poll14.sm
+++ b/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
diff --git a/prism-examples/polling/poll15.sm b/prism-examples/polling/poll15.sm
index cef544ca..02245f5f 100644
--- a/prism-examples/polling/poll15.sm
+++ b/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
diff --git a/prism-examples/polling/poll16.sm b/prism-examples/polling/poll16.sm
index e04e5ad0..d66f9674 100644
--- a/prism-examples/polling/poll16.sm
+++ b/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
diff --git a/prism-examples/polling/poll17.sm b/prism-examples/polling/poll17.sm
index b91d2435..5da5c8cb 100644
--- a/prism-examples/polling/poll17.sm
+++ b/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
diff --git a/prism-examples/polling/poll18.sm b/prism-examples/polling/poll18.sm
index b030919d..f6541d99 100644
--- a/prism-examples/polling/poll18.sm
+++ b/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
diff --git a/prism-examples/polling/poll19.sm b/prism-examples/polling/poll19.sm
index dbf6924a..61d563e0 100644
--- a/prism-examples/polling/poll19.sm
+++ b/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
diff --git a/prism-examples/polling/poll2.sm b/prism-examples/polling/poll2.sm
index 7e8fe47a..ebd28000 100644
--- a/prism-examples/polling/poll2.sm
+++ b/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
diff --git a/prism-examples/polling/poll20.sm b/prism-examples/polling/poll20.sm
index 06e2c65f..5cbd5ae9 100644
--- a/prism-examples/polling/poll20.sm
+++ b/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
diff --git a/prism-examples/polling/poll3.sm b/prism-examples/polling/poll3.sm
index 444a1be6..2248e638 100644
--- a/prism-examples/polling/poll3.sm
+++ b/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
diff --git a/prism-examples/polling/poll4.sm b/prism-examples/polling/poll4.sm
index 2f27cfd8..e5a04ca6 100644
--- a/prism-examples/polling/poll4.sm
+++ b/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
diff --git a/prism-examples/polling/poll5.sm b/prism-examples/polling/poll5.sm
index 3ee2e7aa..259d159f 100644
--- a/prism-examples/polling/poll5.sm
+++ b/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
diff --git a/prism-examples/polling/poll6.sm b/prism-examples/polling/poll6.sm
index 68b9da60..f5ccb16e 100644
--- a/prism-examples/polling/poll6.sm
+++ b/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
diff --git a/prism-examples/polling/poll7.sm b/prism-examples/polling/poll7.sm
index 150f4f19..7b5381b0 100644
--- a/prism-examples/polling/poll7.sm
+++ b/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
diff --git a/prism-examples/polling/poll8.sm b/prism-examples/polling/poll8.sm
index b907de11..f96ec4ee 100644
--- a/prism-examples/polling/poll8.sm
+++ b/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
diff --git a/prism-examples/polling/poll9.sm b/prism-examples/polling/poll9.sm
index 95dfd4bb..61b5d7ff 100644
--- a/prism-examples/polling/poll9.sm
+++ b/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