Tidy up phil/original (and add pp files).

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

prism-examples/phil/original/.autopp

@@ -0,0 +1,7 @@
+#!/bin/csh
+
+foreach N ( 3 4 5 6 7 8 9 10 15 25 30 )
+  echo "Generating for N=$N"
+  prismpp .philN.nm.pp $N >! phil"$N".nm
+  unix2dos phil"$N".nm
+end

prism-examples/phil/original/.philN.nm.pp

@@ -0,0 +1,42 @@
+#const N#
+// randomized dining philosophers [LR81]
+// dxp/gxn 12/12/99
+// atomic formulae 
+// left fork free and right fork free resp.
+formula lfree = p2>=0&p2<=4|p2=6|p2=10;
+formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11;
+
+module phil1
+
+	p1: [0..11];
+
+	[] p1=0 -> (p1'=0); // stay thinking
+	[] 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=2 &  !lfree -> (p1'=2); // left not free
+	[] p1=3 &  rfree -> (p1'=5); // pick up right
+	[] p1=3 &  !rfree -> (p1'=3); // right not free
+	[] 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
+#for i=2:N#
+module phil#i# = phil1 [ p1=p#i#, p2=p#mod(i,N)+1#, p3=p#mod(i-2,N)+1# ] endmodule
+#end#
+
+// labels
+label "hungry" = #| i=1:N#((p#i#>0)&(p#i#<8))#end#;
+label "eat" = #| i=1:N#((p#i#>=8)&(p#i#<=9))#end#;
+

prism-examples/phil/original/auto

@@ -1,14 +1,14 @@
 #!/bin/csh
 
-prism phil3.nm  phil3.pctl  -fair -m
-prism phil4.nm  phil4.pctl  -fair -m
-prism phil5.nm  phil5.pctl  -fair -m
-prism phil6.nm  phil6.pctl  -fair -m
-prism phil7.nm  phil7.pctl  -fair -m
-prism phil8.nm  phil8.pctl  -fair -m
-prism phil9.nm  phil9.pctl  -fair -m
-prism phil10.nm phil10.pctl -fair -m
-prism phil15.nm phil15.pctl -fair -m
-prism phil20.nm phil20.pctl -fair -m
-prism phil25.nm phil25.pctl -fair -m
-prism phil30.nm phil30.pctl -fair -m
+prism phil3.nm  phil.pctl  -fair -m
+prism phil4.nm  phil.pctl  -fair -m
+prism phil5.nm  phil.pctl  -fair -m
+prism phil6.nm  phil.pctl  -fair -m
+prism phil7.nm  phil.pctl  -fair -m
+prism phil8.nm  phil.pctl  -fair -m
+prism phil9.nm  phil.pctl  -fair -m
+#prism phil10.nm phil.pctl -fair -m
+#prism phil15.nm phil.pctl -fair -m
+#prism phil20.nm phil.pctl -fair -m
+#prism phil25.nm phil.pctl -fair -m
+#prism phil30.nm phil.pctl -fair -m

prism-examples/phil/original/phil.pctl

@@ -0,0 +1,3 @@
+// Liveness (if a philosopher is hungry then eventually some philosopher eats)
+
+"hungry" => P>=1 [ true U "eat"]

prism-examples/phil/original/phil10.nm

@@ -2,8 +2,8 @@
 // dxp/gxn 12/12/99
 // 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;
+formula lfree = p2>=0&p2<=4|p2=6|p2=10;
+formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11;
 
 module phil1
 
@@ -31,12 +31,17 @@ module phil1
 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
+module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule
+module phil3 = phil1 [ p1=p3, p2=p4, p3=p2 ] endmodule
+module phil4 = phil1 [ p1=p4, p2=p5, p3=p3 ] endmodule
+module phil5 = phil1 [ p1=p5, p2=p6, p3=p4 ] endmodule
+module phil6 = phil1 [ p1=p6, p2=p7, p3=p5 ] endmodule
+module phil7 = phil1 [ p1=p7, p2=p8, p3=p6 ] endmodule
+module phil8 = phil1 [ p1=p8, p2=p9, p3=p7 ] endmodule
+module phil9 = phil1 [ p1=p9, p2=p10, p3=p8 ] endmodule
+module phil10 = phil1 [ p1=p10, p2=p1, p3=p9 ] endmodule
+
+// 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));
+

prism-examples/phil/original/phil10.pctl

@@ -1,4 +0,0 @@
-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..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9)  | (p6=8..9)  | (p7=8..9)  | (p8=8..9)  | (p9=8..9)  | (p10=8..9);
-// liveness (if a philosopher is hungry then eventually some philosopher eats)
-"hungry" => P>=1 [ true U "eat"]

prism-examples/phil/original/phil15.nm

@@ -2,8 +2,8 @@
 // dxp/gxn 12/12/99
 // atomic formulae 
 // left fork free and right fork free resp.
-formula lfree = p2=0..4,6,10;
-formula rfree = p15=0..3,5,7,11;
+formula lfree = p2>=0&p2<=4|p2=6|p2=10;
+formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11;
 
 module phil1
 
@@ -31,17 +31,22 @@ module phil1
 endmodule
 
 // construct further modules through renaming
-module phil2  = phil1 [p1=p2,  p2=p3,  p15=p1]  endmodule
-module phil3  = phil1 [p1=p3,  p2=p4,  p15=p2]  endmodule
-module phil4  = phil1 [p1=p4,  p2=p5,  p15=p3]  endmodule
-module phil5  = phil1 [p1=p5,  p2=p6,  p15=p4]  endmodule
-module phil6  = phil1 [p1=p6,  p2=p7,  p15=p5]  endmodule
-module phil7  = phil1 [p1=p7,  p2=p8,  p15=p6]  endmodule
-module phil8  = phil1 [p1=p8,  p2=p9,  p15=p7]  endmodule
-module phil9  = phil1 [p1=p9,  p2=p10, p15=p8]  endmodule
-module phil10 = phil1 [p1=p10, p2=p11, p15=p9]  endmodule
-module phil11 = phil1 [p1=p11, p2=p12, p15=p10] endmodule
-module phil12 = phil1 [p1=p12, p2=p13, p15=p11] endmodule
-module phil13 = phil1 [p1=p13, p2=p14, p15=p12] endmodule
-module phil14 = phil1 [p1=p14, p2=p15, p15=p13] endmodule
-module phil15 = phil1 [p1=p15, p2=p1,  p15=p14] endmodule
+module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule
+module phil3 = phil1 [ p1=p3, p2=p4, p3=p2 ] endmodule
+module phil4 = phil1 [ p1=p4, p2=p5, p3=p3 ] endmodule
+module phil5 = phil1 [ p1=p5, p2=p6, p3=p4 ] endmodule
+module phil6 = phil1 [ p1=p6, p2=p7, p3=p5 ] endmodule
+module phil7 = phil1 [ p1=p7, p2=p8, p3=p6 ] endmodule
+module phil8 = phil1 [ p1=p8, p2=p9, p3=p7 ] endmodule
+module phil9 = phil1 [ p1=p9, p2=p10, p3=p8 ] endmodule
+module phil10 = phil1 [ p1=p10, p2=p11, p3=p9 ] endmodule
+module phil11 = phil1 [ p1=p11, p2=p12, p3=p10 ] endmodule
+module phil12 = phil1 [ p1=p12, p2=p13, p3=p11 ] endmodule
+module phil13 = phil1 [ p1=p13, p2=p14, p3=p12 ] endmodule
+module phil14 = phil1 [ p1=p14, p2=p15, p3=p13 ] endmodule
+module phil15 = phil1 [ p1=p15, p2=p1, p3=p14 ] endmodule
+
+// 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))|((p11>0)&(p11<8))|((p12>0)&(p12<8))|((p13>0)&(p13<8))|((p14>0)&(p14<8))|((p15>0)&(p15<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))|((p11>=8)&(p11<=9))|((p12>=8)&(p12<=9))|((p13>=8)&(p13<=9))|((p14>=8)&(p14<=9))|((p15>=8)&(p15<=9));
+

prism-examples/phil/original/phil15.pctl

@@ -1,4 +0,0 @@
-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)) | ((p11>0) & (p11<8)) | ((p12>0) & (p12<8)) | ((p13>0) & (p13<8)) | ((p14>0) & (p14<8)) | ((p15>0) & (p15<8));
-label "eat"    = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9)  | (p6=8..9) | (p7=8..9)  | (p8=8..9)  | (p9=8..9)  | (p10=8..9) | (p11=8..9) | (p12=8..9) | (p13=8..9) | (p14=8..9) | (p15=8..9);
-// liveness (if a philosopher is hungry then eventually some philosopher eats)
-"hungry" => P>=1 [ true U "eat"]

prism-examples/phil/original/phil20.pctl

@@ -1,4 +0,0 @@
-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)) | ((p11>0) & (p11<8)) | ((p12>0) & (p12<8)) | ((p13>0) & (p13<8)) | ((p14>0) & (p14<8)) | ((p15>0) & (p15<8)) | ((p16>0) & (p16<8)) | ((p17>0) & (p17<8)) | ((p18>0) & (p18<8)) | ((p19>0) & (p19<8)) | ((p20>0) & (p20<8));
-label "eat"    = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9) | (p6=8..9) | (p7=8..9)  | (p8=8..9)  | (p9=8..9)  | (p10=8..9) | (p11=8..9) | (p12=8..9) | (p13=8..9) | (p14=8..9) | (p15=8..9) | (p16=8..9) | (p17=8..9)  | (p18=8..9)  | (p19=8..9)  | (p20=8..9);
-// liveness (if a philosopher is hungry then eventually some philosopher eats)
-"hungry" => P>=1 [ true U "eat"]

prism-examples/phil/original/phil25.nm

@@ -2,8 +2,8 @@
 // dxp/gxn 12/12/99
 // atomic formulae 
 // left fork free and right fork free resp.
-formula lfree = p2=0..4,6,10;
-formula rfree = p25=0..3,5,7,11;
+formula lfree = p2>=0&p2<=4|p2=6|p2=10;
+formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11;
 
 module phil1
 
@@ -31,27 +31,32 @@ module phil1
 endmodule
 
 // construct further modules through renaming
-module phil2  = phil1 [p1=p2,  p2=p3,  p25=p1]  endmodule
-module phil3  = phil1 [p1=p3,  p2=p4,  p25=p2]  endmodule
-module phil4  = phil1 [p1=p4,  p2=p5,  p25=p3]  endmodule
-module phil5  = phil1 [p1=p5,  p2=p6,  p25=p4]  endmodule
-module phil6  = phil1 [p1=p6,  p2=p7,  p25=p5]  endmodule
-module phil7  = phil1 [p1=p7,  p2=p8,  p25=p6]  endmodule
-module phil8  = phil1 [p1=p8,  p2=p9,  p25=p7]  endmodule
-module phil9  = phil1 [p1=p9,  p2=p10, p25=p8]  endmodule
-module phil10 = phil1 [p1=p10, p2=p11, p25=p9]  endmodule
-module phil11 = phil1 [p1=p11, p2=p12, p25=p10] endmodule
-module phil12 = phil1 [p1=p12, p2=p13, p25=p11] endmodule
-module phil13 = phil1 [p1=p13, p2=p14, p25=p12] endmodule
-module phil14 = phil1 [p1=p14, p2=p15, p25=p13] endmodule
-module phil15 = phil1 [p1=p15, p2=p16, p25=p14] endmodule
-module phil16 = phil1 [p1=p16, p2=p17, p25=p15] endmodule
-module phil17 = phil1 [p1=p17, p2=p18, p25=p16] endmodule
-module phil18 = phil1 [p1=p18, p2=p19, p25=p17] endmodule
-module phil19 = phil1 [p1=p19, p2=p20, p25=p18] endmodule
-module phil20 = phil1 [p1=p20, p2=p21, p25=p19] endmodule
-module phil21 = phil1 [p1=p21, p2=p22, p25=p20] endmodule
-module phil22 = phil1 [p1=p22, p2=p23, p25=p21] endmodule
-module phil23 = phil1 [p1=p23, p2=p24, p25=p22] endmodule
-module phil24 = phil1 [p1=p24, p2=p25, p25=p23] endmodule
-module phil25 = phil1 [p1=p25, p2=p1,  p25=p24] endmodule
+module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule
+module phil3 = phil1 [ p1=p3, p2=p4, p3=p2 ] endmodule
+module phil4 = phil1 [ p1=p4, p2=p5, p3=p3 ] endmodule
+module phil5 = phil1 [ p1=p5, p2=p6, p3=p4 ] endmodule
+module phil6 = phil1 [ p1=p6, p2=p7, p3=p5 ] endmodule
+module phil7 = phil1 [ p1=p7, p2=p8, p3=p6 ] endmodule
+module phil8 = phil1 [ p1=p8, p2=p9, p3=p7 ] endmodule
+module phil9 = phil1 [ p1=p9, p2=p10, p3=p8 ] endmodule
+module phil10 = phil1 [ p1=p10, p2=p11, p3=p9 ] endmodule
+module phil11 = phil1 [ p1=p11, p2=p12, p3=p10 ] endmodule
+module phil12 = phil1 [ p1=p12, p2=p13, p3=p11 ] endmodule
+module phil13 = phil1 [ p1=p13, p2=p14, p3=p12 ] endmodule
+module phil14 = phil1 [ p1=p14, p2=p15, p3=p13 ] endmodule
+module phil15 = phil1 [ p1=p15, p2=p16, p3=p14 ] endmodule
+module phil16 = phil1 [ p1=p16, p2=p17, p3=p15 ] endmodule
+module phil17 = phil1 [ p1=p17, p2=p18, p3=p16 ] endmodule
+module phil18 = phil1 [ p1=p18, p2=p19, p3=p17 ] endmodule
+module phil19 = phil1 [ p1=p19, p2=p20, p3=p18 ] endmodule
+module phil20 = phil1 [ p1=p20, p2=p21, p3=p19 ] endmodule
+module phil21 = phil1 [ p1=p21, p2=p22, p3=p20 ] endmodule
+module phil22 = phil1 [ p1=p22, p2=p23, p3=p21 ] endmodule
+module phil23 = phil1 [ p1=p23, p2=p24, p3=p22 ] endmodule
+module phil24 = phil1 [ p1=p24, p2=p25, p3=p23 ] endmodule
+module phil25 = phil1 [ p1=p25, p2=p1, p3=p24 ] endmodule
+
+// 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))|((p11>0)&(p11<8))|((p12>0)&(p12<8))|((p13>0)&(p13<8))|((p14>0)&(p14<8))|((p15>0)&(p15<8))|((p16>0)&(p16<8))|((p17>0)&(p17<8))|((p18>0)&(p18<8))|((p19>0)&(p19<8))|((p20>0)&(p20<8))|((p21>0)&(p21<8))|((p22>0)&(p22<8))|((p23>0)&(p23<8))|((p24>0)&(p24<8))|((p25>0)&(p25<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))|((p11>=8)&(p11<=9))|((p12>=8)&(p12<=9))|((p13>=8)&(p13<=9))|((p14>=8)&(p14<=9))|((p15>=8)&(p15<=9))|((p16>=8)&(p16<=9))|((p17>=8)&(p17<=9))|((p18>=8)&(p18<=9))|((p19>=8)&(p19<=9))|((p20>=8)&(p20<=9))|((p21>=8)&(p21<=9))|((p22>=8)&(p22<=9))|((p23>=8)&(p23<=9))|((p24>=8)&(p24<=9))|((p25>=8)&(p25<=9));
+

prism-examples/phil/original/phil25.pctl

@@ -1,4 +0,0 @@
-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)) | ((p11>0) & (p11<8)) | ((p12>0) & (p12<8)) | ((p13>0) & (p13<8)) | ((p14>0) & (p14<8)) | ((p15>0) & (p15<8)) | ((p16>0) & (p16<8)) | ((p17>0) & (p17<8)) | ((p18>0) & (p18<8)) | ((p19>0) & (p19<8)) | ((p20>0) & (p20<8)) | ((p21>0) & (p21<8)) | ((p22>0) & (p22<8)) | ((p23>0) & (p23<8)) | ((p24>0) & (p24<8)) | ((p25>0) & (p25<8));
-label "eat"    = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9) | (p6=8..9) | (p7=8..9)  | (p8=8..9)  | (p9=8..9)  | (p10=8..9) | (p11=8..9) | (p12=8..9) | (p13=8..9) | (p14=8..9) | (p15=8..9) | (p16=8..9) | (p17=8..9)  | (p18=8..9)  | (p19=8..9)  | (p20=8..9) | (p21=8..9) | (p22=8..9) | (p23=8..9) | (p24=8..9) | (p25=8..9);
-// liveness (if a philosopher is hungry then eventually some philosopher eats)
-"hungry" => P>=1 [ true U "eat"]

prism-examples/phil/original/phil3.nm

@@ -2,8 +2,8 @@
 // dxp/gxn 12/12/99
 // atomic formulae 
 // left fork free and right fork free resp.
-formula lfree = p2=0..4,6,10;
-formula rfree = p3=0..3,5,7,11;
+formula lfree = p2>=0&p2<=4|p2=6|p2=10;
+formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11;
 
 module phil1
 
@@ -31,5 +31,10 @@ module phil1
 endmodule
 
 // construct further modules through renaming
-module phil2 = phil1 [p1=p2, p2=p3, p3=p1] endmodule
-module phil3 = phil1 [p1=p3, p2=p1, p3=p2] endmodule
+module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule
+module phil3 = phil1 [ p1=p3, p2=p1, p3=p2 ] endmodule
+
+// labels
+label "hungry" = ((p1>0)&(p1<8))|((p2>0)&(p2<8))|((p3>0)&(p3<8));
+label "eat" = ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9));
+

prism-examples/phil/original/phil3.pctl

@@ -1,4 +0,0 @@
-label "hungry" = ((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8));
-label "eat"    = (p1=8..9) | (p2=8..9) | (p3=8..9);
-// liveness (if a philosopher is hungry then eventually some philosopher eats)
-"hungry" => P>=1 [ true U "eat"]

prism-examples/phil/original/phil30.nm

@@ -2,8 +2,8 @@
 // dxp/gxn 12/12/99
 // atomic formulae 
 // left fork free and right fork free resp.
-formula lfree = p2=0..4,6,10;
-formula rfree = p30=0..3,5,7,11;
+formula lfree = p2>=0&p2<=4|p2=6|p2=10;
+formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11;
 
 module phil1
 
@@ -31,32 +31,37 @@ module phil1
 endmodule
 
 // construct further modules through renaming
-module phil2  = phil1 [p1=p2,  p2=p3,  p30=p1]  endmodule
-module phil3  = phil1 [p1=p3,  p2=p4,  p30=p2]  endmodule
-module phil4  = phil1 [p1=p4,  p2=p5,  p30=p3]  endmodule
-module phil5  = phil1 [p1=p5,  p2=p6,  p30=p4]  endmodule
-module phil6  = phil1 [p1=p6,  p2=p7,  p30=p5]  endmodule
-module phil7  = phil1 [p1=p7,  p2=p8,  p30=p6]  endmodule
-module phil8  = phil1 [p1=p8,  p2=p9,  p30=p7]  endmodule
-module phil9  = phil1 [p1=p9,  p2=p10, p30=p8]  endmodule
-module phil10 = phil1 [p1=p10, p2=p11, p30=p9]  endmodule
-module phil11 = phil1 [p1=p11, p2=p12, p30=p10] endmodule
-module phil12 = phil1 [p1=p12, p2=p13, p30=p11] endmodule
-module phil13 = phil1 [p1=p13, p2=p14, p30=p12] endmodule
-module phil14 = phil1 [p1=p14, p2=p15, p30=p13] endmodule
-module phil15 = phil1 [p1=p15, p2=p16, p30=p14] endmodule
-module phil16 = phil1 [p1=p16, p2=p17, p30=p15] endmodule
-module phil17 = phil1 [p1=p17, p2=p18, p30=p16] endmodule
-module phil18 = phil1 [p1=p18, p2=p19, p30=p17] endmodule
-module phil19 = phil1 [p1=p19, p2=p20, p30=p18] endmodule
-module phil20 = phil1 [p1=p20, p2=p21, p30=p19] endmodule
-module phil21 = phil1 [p1=p21, p2=p22, p30=p20] endmodule
-module phil22 = phil1 [p1=p22, p2=p23, p30=p21] endmodule
-module phil23 = phil1 [p1=p23, p2=p24, p30=p22] endmodule
-module phil24 = phil1 [p1=p24, p2=p25, p30=p23] endmodule
-module phil25 = phil1 [p1=p25, p2=p26, p30=p24] endmodule
-module phil26 = phil1 [p1=p26, p2=p27, p30=p25] endmodule
-module phil27 = phil1 [p1=p27, p2=p28, p30=p26] endmodule
-module phil28 = phil1 [p1=p28, p2=p29, p30=p27] endmodule
-module phil29 = phil1 [p1=p29, p2=p30, p30=p28] endmodule
-module phil30 = phil1 [p1=p30, p2=p1,  p30=p29] endmodule
+module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule
+module phil3 = phil1 [ p1=p3, p2=p4, p3=p2 ] endmodule
+module phil4 = phil1 [ p1=p4, p2=p5, p3=p3 ] endmodule
+module phil5 = phil1 [ p1=p5, p2=p6, p3=p4 ] endmodule
+module phil6 = phil1 [ p1=p6, p2=p7, p3=p5 ] endmodule
+module phil7 = phil1 [ p1=p7, p2=p8, p3=p6 ] endmodule
+module phil8 = phil1 [ p1=p8, p2=p9, p3=p7 ] endmodule
+module phil9 = phil1 [ p1=p9, p2=p10, p3=p8 ] endmodule
+module phil10 = phil1 [ p1=p10, p2=p11, p3=p9 ] endmodule
+module phil11 = phil1 [ p1=p11, p2=p12, p3=p10 ] endmodule
+module phil12 = phil1 [ p1=p12, p2=p13, p3=p11 ] endmodule
+module phil13 = phil1 [ p1=p13, p2=p14, p3=p12 ] endmodule
+module phil14 = phil1 [ p1=p14, p2=p15, p3=p13 ] endmodule
+module phil15 = phil1 [ p1=p15, p2=p16, p3=p14 ] endmodule
+module phil16 = phil1 [ p1=p16, p2=p17, p3=p15 ] endmodule
+module phil17 = phil1 [ p1=p17, p2=p18, p3=p16 ] endmodule
+module phil18 = phil1 [ p1=p18, p2=p19, p3=p17 ] endmodule
+module phil19 = phil1 [ p1=p19, p2=p20, p3=p18 ] endmodule
+module phil20 = phil1 [ p1=p20, p2=p21, p3=p19 ] endmodule
+module phil21 = phil1 [ p1=p21, p2=p22, p3=p20 ] endmodule
+module phil22 = phil1 [ p1=p22, p2=p23, p3=p21 ] endmodule
+module phil23 = phil1 [ p1=p23, p2=p24, p3=p22 ] endmodule
+module phil24 = phil1 [ p1=p24, p2=p25, p3=p23 ] endmodule
+module phil25 = phil1 [ p1=p25, p2=p26, p3=p24 ] endmodule
+module phil26 = phil1 [ p1=p26, p2=p27, p3=p25 ] endmodule
+module phil27 = phil1 [ p1=p27, p2=p28, p3=p26 ] endmodule
+module phil28 = phil1 [ p1=p28, p2=p29, p3=p27 ] endmodule
+module phil29 = phil1 [ p1=p29, p2=p30, p3=p28 ] endmodule
+module phil30 = phil1 [ p1=p30, p2=p1, p3=p29 ] endmodule
+
+// 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))|((p11>0)&(p11<8))|((p12>0)&(p12<8))|((p13>0)&(p13<8))|((p14>0)&(p14<8))|((p15>0)&(p15<8))|((p16>0)&(p16<8))|((p17>0)&(p17<8))|((p18>0)&(p18<8))|((p19>0)&(p19<8))|((p20>0)&(p20<8))|((p21>0)&(p21<8))|((p22>0)&(p22<8))|((p23>0)&(p23<8))|((p24>0)&(p24<8))|((p25>0)&(p25<8))|((p26>0)&(p26<8))|((p27>0)&(p27<8))|((p28>0)&(p28<8))|((p29>0)&(p29<8))|((p30>0)&(p30<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))|((p11>=8)&(p11<=9))|((p12>=8)&(p12<=9))|((p13>=8)&(p13<=9))|((p14>=8)&(p14<=9))|((p15>=8)&(p15<=9))|((p16>=8)&(p16<=9))|((p17>=8)&(p17<=9))|((p18>=8)&(p18<=9))|((p19>=8)&(p19<=9))|((p20>=8)&(p20<=9))|((p21>=8)&(p21<=9))|((p22>=8)&(p22<=9))|((p23>=8)&(p23<=9))|((p24>=8)&(p24<=9))|((p25>=8)&(p25<=9))|((p26>=8)&(p26<=9))|((p27>=8)&(p27<=9))|((p28>=8)&(p28<=9))|((p29>=8)&(p29<=9))|((p30>=8)&(p30<=9));
+

prism-examples/phil/original/phil30.pctl

@@ -1,4 +0,0 @@
-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)) | ((p11>0) & (p11<8)) | ((p12>0) & (p12<8)) | ((p13>0) & (p13<8)) | ((p14>0) & (p14<8)) | ((p15>0) & (p15<8)) | ((p16>0) & (p16<8)) | ((p17>0) & (p17<8)) | ((p18>0) & (p18<8)) | ((p19>0) & (p19<8)) | ((p20>0) & (p20<8)) | ((p21>0) & (p21<8)) | ((p22>0) & (p22<8)) | ((p23>0) & (p23<8)) | ((p24>0) & (p24<8)) | ((p25>0) & (p25<8)) | ((p26>0) & (p26<8)) | ((p27>0) & (p27<8)) | ((p28>0) & (p28<8)) | ((p29>0) & (p29<8)) | ((p30>0) & (p30<8));
-label "eat"    = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9) | (p6=8..9) | (p7=8..9)  | (p8=8..9)  | (p9=8..9)  | (p10=8..9) | (p11=8..9) | (p12=8..9) | (p13=8..9) | (p14=8..9) | (p15=8..9) | (p16=8..9) | (p17=8..9)  | (p18=8..9)  | (p19=8..9)  | (p20=8..9) | (p21=8..9) | (p22=8..9) | (p23=8..9) | (p24=8..9) | (p25=8..9) | (p26=8..9) | (p27=8..9)  | (p28=8..9)  | (p29=8..9)  | (p30=8..9);
-// liveness (if a philosopher is hungry then eventually some philosopher eats)
-"hungry" => P>=1 [ true U "eat"]

prism-examples/phil/original/phil4.nm

@@ -2,8 +2,8 @@
 // dxp/gxn 12/12/99
 // atomic formulae 
 // left fork free and right fork free resp.
-formula lfree = p2=0..4,6,10;
-formula rfree = p4=0..3,5,7,11;
+formula lfree = p2>=0&p2<=4|p2=6|p2=10;
+formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11;
 
 module phil1
 
@@ -31,6 +31,11 @@ module phil1
 endmodule
 
 // construct further modules through renaming
-module phil2 = phil1 [p1=p2, p2=p3, p4=p1] endmodule
-module phil3 = phil1 [p1=p3, p2=p4, p4=p2] endmodule
-module phil4 = phil1 [p1=p4, p2=p1, p4=p3] endmodule
+module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule
+module phil3 = phil1 [ p1=p3, p2=p4, p3=p2 ] endmodule
+module phil4 = phil1 [ p1=p4, p2=p1, p3=p3 ] endmodule
+
+// labels
+label "hungry" = ((p1>0)&(p1<8))|((p2>0)&(p2<8))|((p3>0)&(p3<8))|((p4>0)&(p4<8));
+label "eat" = ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9))|((p4>=8)&(p4<=9));
+

prism-examples/phil/original/phil4.pctl

@@ -1,4 +0,0 @@
-label "hungry" = ((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)) | ((p4>0) & (p4<8));
-label "eat"    = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9);
-// liveness (if a philosopher is hungry then eventually some philosopher eats)
-"hungry" => P>=1 [ true U "eat"]

prism-examples/phil/original/phil5.nm

@@ -2,8 +2,8 @@
 // dxp/gxn 12/12/99
 // atomic formulae 
 // left fork free and right fork free resp.
-formula lfree = p2=0..4,6,10;
-formula rfree = p5=0..3,5,7,11;
+formula lfree = p2>=0&p2<=4|p2=6|p2=10;
+formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11;
 
 module phil1
 
@@ -31,7 +31,12 @@ module phil1
 endmodule
 
 // construct further modules through renaming
-module phil2 = phil1 [p1=p2, p2=p3, p5=p1] endmodule
-module phil3 = phil1 [p1=p3, p2=p4, p5=p2] endmodule
-module phil4 = phil1 [p1=p4, p2=p5, p5=p3] endmodule
-module phil5 = phil1 [p1=p5, p2=p1, p5=p4] endmodule
+module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule
+module phil3 = phil1 [ p1=p3, p2=p4, p3=p2 ] endmodule
+module phil4 = phil1 [ p1=p4, p2=p5, p3=p3 ] endmodule
+module phil5 = phil1 [ p1=p5, p2=p1, p3=p4 ] endmodule
+
+// labels
+label "hungry" = ((p1>0)&(p1<8))|((p2>0)&(p2<8))|((p3>0)&(p3<8))|((p4>0)&(p4<8))|((p5>0)&(p5<8));
+label "eat" = ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9))|((p4>=8)&(p4<=9))|((p5>=8)&(p5<=9));
+

prism-examples/phil/original/phil5.pctl

@@ -1,4 +0,0 @@
-label "hungry" = ((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)) | ((p4>0) & (p4<8)) | ((p5>0) & (p5<8));
-label "eat"    = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9);
-// liveness (if a philosopher is hungry then eventually some philosopher eats)
-"hungry" => P>=1 [ true U "eat"]

prism-examples/phil/original/phil6.nm

@@ -2,8 +2,8 @@
 // dxp/gxn 12/12/99
 // atomic formulae 
 // left fork free and right fork free resp.
-formula lfree = p2=0..4,6,10;
-formula rfree = p6=0..3,5,7,11;
+formula lfree = p2>=0&p2<=4|p2=6|p2=10;
+formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11;
 
 module phil1
 
@@ -31,8 +31,13 @@ module phil1
 endmodule
 
 // construct further modules through renaming
-module phil2 = phil1 [p1=p2, p2=p3, p6=p1] endmodule
-module phil3 = phil1 [p1=p3, p2=p4, p6=p2] endmodule
-module phil4 = phil1 [p1=p4, p2=p5, p6=p3] endmodule
-module phil5 = phil1 [p1=p5, p2=p6, p6=p4] endmodule
-module phil6 = phil1 [p1=p6, p2=p1, p6=p5] endmodule
+module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule
+module phil3 = phil1 [ p1=p3, p2=p4, p3=p2 ] endmodule
+module phil4 = phil1 [ p1=p4, p2=p5, p3=p3 ] endmodule
+module phil5 = phil1 [ p1=p5, p2=p6, p3=p4 ] endmodule
+module phil6 = phil1 [ p1=p6, p2=p1, p3=p5 ] endmodule
+
+// 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));
+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));
+

prism-examples/phil/original/phil6.pctl

@@ -1,4 +0,0 @@
-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));
-label "eat"    = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9) | (p6=8..9);
-// liveness (if a philosopher is hungry then eventually some philosopher eats)
-"hungry" => P>=1 [ true U "eat"]

prism-examples/phil/original/phil7.nm

@@ -2,8 +2,8 @@
 // dxp/gxn 12/12/99
 // atomic formulae 
 // left fork free and right fork free resp.
-formula lfree = p2=0..4,6,10;
-formula rfree = p7=0..3,5,7,11;
+formula lfree = p2>=0&p2<=4|p2=6|p2=10;
+formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11;
 
 module phil1
 
@@ -31,9 +31,14 @@ module phil1
 endmodule
 
 // construct further modules through renaming
-module phil2 = phil1 [p1=p2, p2=p3, p7=p1] endmodule
-module phil3 = phil1 [p1=p3, p2=p4, p7=p2] endmodule
-module phil4 = phil1 [p1=p4, p2=p5, p7=p3] endmodule
-module phil5 = phil1 [p1=p5, p2=p6, p7=p4] endmodule
-module phil6 = phil1 [p1=p6, p2=p7, p7=p5] endmodule
-module phil7 = phil1 [p1=p7, p2=p1, p7=p6] endmodule
+module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule
+module phil3 = phil1 [ p1=p3, p2=p4, p3=p2 ] endmodule
+module phil4 = phil1 [ p1=p4, p2=p5, p3=p3 ] endmodule
+module phil5 = phil1 [ p1=p5, p2=p6, p3=p4 ] endmodule
+module phil6 = phil1 [ p1=p6, p2=p7, p3=p5 ] endmodule
+module phil7 = phil1 [ p1=p7, p2=p1, p3=p6 ] endmodule
+
+// 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));
+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));
+

prism-examples/phil/original/phil7.pctl

@@ -1,4 +0,0 @@
-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));
-label "eat"    = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9) | (p6=8..9) | (p7=8..9);
-// liveness (if a philosopher is hungry then eventually some philosopher eats)
-"hungry" => P>=1 [ true U "eat"]

prism-examples/phil/original/phil8.nm

@@ -2,8 +2,8 @@
 // dxp/gxn 12/12/99
 // atomic formulae 
 // left fork free and right fork free resp.
-formula lfree = p2=0..4,6,10;
-formula rfree = p8=0..3,5,7,11;
+formula lfree = p2>=0&p2<=4|p2=6|p2=10;
+formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11;
 
 module phil1
 
@@ -31,10 +31,15 @@ module phil1
 endmodule
 
 // construct further modules through renaming
-module phil2 = phil1 [p1=p2, p2=p3, p8=p1] endmodule
-module phil3 = phil1 [p1=p3, p2=p4, p8=p2] endmodule
-module phil4 = phil1 [p1=p4, p2=p5, p8=p3] endmodule
-module phil5 = phil1 [p1=p5, p2=p6, p8=p4] endmodule
-module phil6 = phil1 [p1=p6, p2=p7, p8=p5] endmodule
-module phil7 = phil1 [p1=p7, p2=p8, p8=p6] endmodule
-module phil8 = phil1 [p1=p8, p2=p1, p8=p7] endmodule
+module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule
+module phil3 = phil1 [ p1=p3, p2=p4, p3=p2 ] endmodule
+module phil4 = phil1 [ p1=p4, p2=p5, p3=p3 ] endmodule
+module phil5 = phil1 [ p1=p5, p2=p6, p3=p4 ] endmodule
+module phil6 = phil1 [ p1=p6, p2=p7, p3=p5 ] endmodule
+module phil7 = phil1 [ p1=p7, p2=p8, p3=p6 ] endmodule
+module phil8 = phil1 [ p1=p8, p2=p1, p3=p7 ] endmodule
+
+// 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));
+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));
+

prism-examples/phil/original/phil8.pctl

@@ -1,4 +0,0 @@
-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));
-label "eat"    = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9) | (p6=8..9) | (p7=8..9) | (p8=8..9);
-// liveness (if a philosopher is hungry then eventually some philosopher eats)
-"hungry" => P>=1 [ true U "eat"]

prism-examples/phil/original/phil9.nm

@@ -1,12 +1,9 @@
 // randomized dining philosophers [LR81]
 // dxp/gxn 12/12/99
-
-mdp
-
 // atomic formulae 
 // left fork free and right fork free resp.
-formula lfree = p2=0..4,6,10;
-formula rfree = p9=0..3,5,7,11;
+formula lfree = p2>=0&p2<=4|p2=6|p2=10;
+formula rfree = p3>=0&p3<=3|p3=5|p3=7|p3=11;
 
 module phil1
 
@@ -34,11 +31,16 @@ module phil1
 endmodule
 
 // construct further modules through renaming
-module phil2 = phil1 [p1=p2, p2=p3, p9=p1] endmodule
-module phil3 = phil1 [p1=p3, p2=p4, p9=p2] endmodule
-module phil4 = phil1 [p1=p4, p2=p5, p9=p3] endmodule
-module phil5 = phil1 [p1=p5, p2=p6, p9=p4] endmodule
-module phil6 = phil1 [p1=p6, p2=p7, p9=p5] endmodule
-module phil7 = phil1 [p1=p7, p2=p8, p9=p6] endmodule
-module phil8 = phil1 [p1=p8, p2=p9, p9=p7] endmodule
-module phil9 = phil1 [p1=p9, p2=p1, p9=p8] endmodule
+module phil2 = phil1 [ p1=p2, p2=p3, p3=p1 ] endmodule
+module phil3 = phil1 [ p1=p3, p2=p4, p3=p2 ] endmodule
+module phil4 = phil1 [ p1=p4, p2=p5, p3=p3 ] endmodule
+module phil5 = phil1 [ p1=p5, p2=p6, p3=p4 ] endmodule
+module phil6 = phil1 [ p1=p6, p2=p7, p3=p5 ] endmodule
+module phil7 = phil1 [ p1=p7, p2=p8, p3=p6 ] endmodule
+module phil8 = phil1 [ p1=p8, p2=p9, p3=p7 ] endmodule
+module phil9 = phil1 [ p1=p9, p2=p1, p3=p8 ] endmodule
+
+// 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));
+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));
+

prism-examples/phil/original/phil9.pctl

@@ -1,4 +0,0 @@
-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));
-label "eat"    = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9) | (p6=8..9) | (p7=8..9) | (p8=8..9) | (p9=8..9);
-// liveness (if a philosopher is hungry then eventually some philosopher eats)
-"hungry" => P>=1 [ true U "eat"]