s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Out of date file in phil-original. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1920 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 16 years ago
parent
211be9eb3c
commit
19dc966bea
1 changed files with 57 additions and 52 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 109
      prism-examples/phil/original/phil20.nm

109
prism-examples/phil/original/phil20.nm
View File

@ -1,52 +1,57 @@
// randomized dining philosophers [LR81]
// dxp/gxn 12/12/99
// atomic formulae
// left fork free and right fork free resp.
formula lfree = p2=0..4,6,10;
formula rfree = p20=0..3,5,7,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
module phil2 = phil1 [p1=p2, p2=p3, p20=p1] endmodule
module phil3 = phil1 [p1=p3, p2=p4, p20=p2] endmodule
module phil4 = phil1 [p1=p4, p2=p5, p20=p3] endmodule
module phil5 = phil1 [p1=p5, p2=p6, p20=p4] endmodule
module phil6 = phil1 [p1=p6, p2=p7, p20=p5] endmodule
module phil7 = phil1 [p1=p7, p2=p8, p20=p6] endmodule
module phil8 = phil1 [p1=p8, p2=p9, p20=p7] endmodule
module phil9 = phil1 [p1=p9, p2=p10, p20=p8] endmodule
module phil10 = phil1 [p1=p10, p2=p11, p20=p9] endmodule
module phil11 = phil1 [p1=p11, p2=p12, p20=p10] endmodule
module phil12 = phil1 [p1=p12, p2=p13, p20=p11] endmodule
module phil13 = phil1 [p1=p13, p2=p14, p20=p12] endmodule
module phil14 = phil1 [p1=p14, p2=p15, p20=p13] endmodule
module phil15 = phil1 [p1=p15, p2=p16, p20=p14] endmodule
module phil16 = phil1 [p1=p16, p2=p17, p20=p15] endmodule
module phil17 = phil1 [p1=p17, p2=p18, p20=p16] endmodule
module phil18 = phil1 [p1=p18, p2=p19, p20=p17] endmodule
module phil19 = phil1 [p1=p19, p2=p20, p20=p18] endmodule
module phil20 = phil1 [p1=p20, p2=p1, p20=p19] endmodule
// 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 = (p20>=0&p20<=3)|p20=5|p20=7|p20=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
module phil2 = phil1 [ p1=p2, p2=p3, p20=p1 ] endmodule
module phil3 = phil1 [ p1=p3, p2=p4, p20=p2 ] endmodule
module phil4 = phil1 [ p1=p4, p2=p5, p20=p3 ] endmodule
module phil5 = phil1 [ p1=p5, p2=p6, p20=p4 ] endmodule
module phil6 = phil1 [ p1=p6, p2=p7, p20=p5 ] endmodule
module phil7 = phil1 [ p1=p7, p2=p8, p20=p6 ] endmodule
module phil8 = phil1 [ p1=p8, p2=p9, p20=p7 ] endmodule
module phil9 = phil1 [ p1=p9, p2=p10, p20=p8 ] endmodule
module phil10 = phil1 [ p1=p10, p2=p11, p20=p9 ] endmodule
module phil11 = phil1 [ p1=p11, p2=p12, p20=p10 ] endmodule
module phil12 = phil1 [ p1=p12, p2=p13, p20=p11 ] endmodule
module phil13 = phil1 [ p1=p13, p2=p14, p20=p12 ] endmodule
module phil14 = phil1 [ p1=p14, p2=p15, p20=p13 ] endmodule
module phil15 = phil1 [ p1=p15, p2=p16, p20=p14 ] endmodule
module phil16 = phil1 [ p1=p16, p2=p17, p20=p15 ] endmodule
module phil17 = phil1 [ p1=p17, p2=p18, p20=p16 ] endmodule
module phil18 = phil1 [ p1=p18, p2=p19, p20=p17 ] endmodule
module phil19 = phil1 [ p1=p19, p2=p20, p20=p18 ] endmodule
module phil20 = phil1 [ p1=p20, p2=p1, p20=p19 ] 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));
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));
Write Preview
Loading…
Cancel
Save