one can never have enough labels in prism files

Former-commit-id: ec1751b34a [formerly 7f1a1b2944]
Former-commit-id: af5e22c01e

examples/pctmc/polling6.sm

@@ -63,13 +63,17 @@ module station6 = station1 [s1=s6, loop1a=loop6a, loop1b=loop6b, serve1=serve6]
 
 // cumulative rewards
 
-//rewards "waiting" // expected time the station 1 is waiting to be served
-//	s1=1 & !(s=1 & a=1) : 1;
-//endrewards
+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
+rewards "served" // expected number of times station1 is served
+	[serve1] true : 1;
+endrewards
+
+label "server1serving" = s=1 & a=1;
+label "server5polling" = s=5 & a=0;
+label "server5serving" = s=5 & a=1;
 
 init
 s = 1 &

examples/pdtmc/brp/brp.pm

@@ -134,3 +134,5 @@ module  channelL
     
 endmodule
 
+label "fatal" = s=5 & T;
+label "false_neg" = srep=1 & rrep=3 & recv;

examples/pdtmc/brp_rewards2/brp_rewards2.pm

@@ -143,4 +143,5 @@ rewards
 	[TO_Ack] true : TOAck;
 endrewards
 
-
+label "fatal" = s=5 & T;
+label "false_neg" = srep=1 & rrep=3 & recv;

examples/pdtmc/brp_rewards4/brp_rewards4.pm

@@ -144,3 +144,6 @@ rewards
 endrewards
 
 
+
+label "fatal" = s=5 & T;
+label "false_neg" = srep=1 & rrep=3 & recv;

examples/pmdp/brp/brp.pm

@@ -136,5 +136,6 @@ module	channelL
 	
 endmodule
 
-
+label "error" = s=5;
 label "fatal" = s=5 & T;
+

examples/pmdp/coin2/coin2.pm

@@ -47,7 +47,10 @@ endmodule
 
 module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule
 label "finished" = pc1=3 &pc2=3 ;
-label "all_coins_equal_1" = coin1=1 &coin2=1 ;
+label "all_coins_equal_0" = coin1=0 & coin2=0;
+label "all_coins_equal_1" = coin1=1 & coin2=1;
+label "agree" = coin1 = coin2;
+
 rewards "steps"
 	true : 1;
 endrewards

examples/pmdp/coin4/coin4.pm

@@ -53,6 +53,9 @@ module process4 = process1[pc1=pc4,coin1=coin4,p1=p4] endmodule
 
 label "finished" = pc1=3 &pc2=3 &pc3=3 &pc4=3;
 label "all_coins_equal_1" = coin1=1 &coin2=1 &coin3=1 &coin4=1 ;
+label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3 = 0 & coin4 = 0;
+label "agree" = coin1=coin2 & coin2=coin3 & coin3 = coin4;
+
 rewards "steps"
 	true : 1;
 endrewards

examples/pmdp/zeroconf/zeroconf.pm

@@ -256,3 +256,14 @@ module host0
 	[] l=4 -> 1 : true;
 	
 endmodule
+
+// reward structure
+const double err; // cost associated with using a IP address already in use
+
+rewards
+	[time] true : 1;
+	[send] l=3 & mess=0 & y=CONSEC & probes=1 & ip=1 : err;
+endrewards
+
+label "selected_ip" = l = 4;
+label "selected_ip_in_use" = l = 4 & ip = 1;