diff --git a/prism-examples/phil/nofair/phil-nofair10.nm b/prism-examples/phil/nofair/phil-nofair10.nm
index 8b95e182..1479ae96 100644
--- a/prism-examples/phil/nofair/phil-nofair10.nm
+++ b/prism-examples/phil/nofair/phil-nofair10.nm
@@ -1,54 +1,57 @@
-// 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)
-
-mdp
-
-// atomic formulae 
-// left fork free and right fork free resp.
-formula lfree = p2=0..4,6,10;
-formula rfree = p10=0..3,5,7,11;
-
-module phil1
-
-	p1: [0..11];
-
-	[] p1=0 -> (p1'=1); // trying
-	[] p1=1 -> 0.5 : (p1'=2) + 0.5 : (p1'=3); // draw randomly
-	[] p1=2 &  lfree -> (p1'=4); // pick up left
-	[] p1=3 &  rfree -> (p1'=5); // pick up right
-	[] p1=4 &  rfree -> (p1'=8); // pick up right (got left)
-	[] p1=4 & !rfree -> (p1'=6); // right not free (got left)
-	[] p1=5 &  lfree -> (p1'=8); // pick up left (got right)
-	[] p1=5 & !lfree -> (p1'=7); // left not free (got right)
-	[] p1=6  -> (p1'=1); // put down left
-	[] p1=7  -> (p1'=1); // put down right
-	[] p1=8  -> (p1'=9); // move to eating (got forks)
-	[] p1=9  -> (p1'=10); // finished eating and put down left 
-	[] p1=9  -> (p1'=11); // finished eating and put down right
-	[] p1=10 -> (p1'=0); // put down right and return to think
-	[] p1=11 -> (p1'=0); // put down left and return to think
-
-endmodule
-
-// construct further modules through renaming
-module phil2  = phil1 [p1=p2,  p2=p3,  p10=p1] endmodule
-module phil3  = phil1 [p1=p3,  p2=p4,  p10=p2] endmodule
-module phil4  = phil1 [p1=p4,  p2=p5,  p10=p3] endmodule
-module phil5  = phil1 [p1=p5,  p2=p6,  p10=p4] endmodule
-module phil6  = phil1 [p1=p6,  p2=p7,  p10=p5] endmodule
-module phil7  = phil1 [p1=p7,  p2=p8,  p10=p6] endmodule
-module phil8  = phil1 [p1=p8,  p2=p9,  p10=p7] endmodule
-module phil9  = phil1 [p1=p9,  p2=p10, p10=p8] endmodule
-module phil10 = phil1 [p1=p10, p2=p1,  p10=p9] endmodule
-
-// rewards (number of steps)
-rewards
-	
-	[] true : 1;
-	
-endrewards
+// 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)
+
+mdp
+
+// atomic formulae 
+// left fork free and right fork free resp.
+formula lfree = (p2>=0&p2<=4)|p2=6|p2=10;
+formula rfree = (p10>=0&p10<=3)|p10=5|p10=7|p10=11;
+
+module phil1
+
+	p1: [0..11];
+
+	[] p1=0 -> (p1'=1); // trying
+	[] p1=1 -> 0.5 : (p1'=2) + 0.5 : (p1'=3); // draw randomly
+	[] p1=2 &  lfree -> (p1'=4); // pick up left
+	[] p1=3 &  rfree -> (p1'=5); // pick up right
+	[] p1=4 &  rfree -> (p1'=8); // pick up right (got left)
+	[] p1=4 & !rfree -> (p1'=6); // right not free (got left)
+	[] p1=5 &  lfree -> (p1'=8); // pick up left (got right)
+	[] p1=5 & !lfree -> (p1'=7); // left not free (got right)
+	[] p1=6  -> (p1'=1); // put down left
+	[] p1=7  -> (p1'=1); // put down right
+	[] p1=8  -> (p1'=9); // move to eating (got forks)
+	[] p1=9  -> (p1'=10); // finished eating and put down left 
+	[] p1=9  -> (p1'=11); // finished eating and put down right
+	[] p1=10 -> (p1'=0); // put down right and return to think
+	[] p1=11 -> (p1'=0); // put down left and return to think
+
+endmodule
+
+// construct further modules through renaming
+module phil2 = phil1 [ p1=p2, p2=p3, p10=p1 ] endmodule
+module phil3 = phil1 [ p1=p3, p2=p4, p10=p2 ] endmodule
+module phil4 = phil1 [ p1=p4, p2=p5, p10=p3 ] endmodule
+module phil5 = phil1 [ p1=p5, p2=p6, p10=p4 ] endmodule
+module phil6 = phil1 [ p1=p6, p2=p7, p10=p5 ] endmodule
+module phil7 = phil1 [ p1=p7, p2=p8, p10=p6 ] endmodule
+module phil8 = phil1 [ p1=p8, p2=p9, p10=p7 ] endmodule
+module phil9 = phil1 [ p1=p9, p2=p10, p10=p8 ] endmodule
+module phil10 = phil1 [ p1=p10, p2=p1, p10=p9 ] endmodule
+
+// rewards (number of steps)
+rewards "num_steps"
+	[] true : 1;
+endrewards
+// labels
+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))|((p10>0)&(p10<8));
+label "eat" = ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9))|((p4>=8)&(p4<=9))|((p5>=8)&(p5<=9))|((p6>=8)&(p6<=9))|((p7>=8)&(p7<=9))|((p8>=8)&(p8<=9))|((p9>=8)&(p9<=9))|((p10>=8)&(p10<=9));
+
+