1 MODULE phil(leftfork, rightfork)
3 state: {none, left, both};
12 rightfork=inuse: left;
20 f: array 0..6 of {free, inuse};
21 ph0: phil(f[6], f[1]);
22 ph1: phil(f[0], f[2]);
23 ph2: phil(f[1], f[3]);
24 ph3: phil(f[2], f[4]);
25 ph4: phil(f[3], f[5]);
26 ph5: phil(f[4], f[6]);
27 ph6: phil(f[5], f[0]);
38 ph6.state=both | ph1.state=left | ph0.state=both: inuse;
42 ph0.state=both | ph2.state=left | ph2.state=both: inuse;
46 ph1.state=both | ph3.state=left | ph3.state=both: inuse;
50 ph2.state=both | ph4.state=left | ph4.state=both: inuse;
54 ph3.state=both | ph5.state=left | ph5.state=both: inuse;
58 ph4.state=both | ph6.state=left | ph6.state=both: inuse;
62 ph5.state=both | ph0.state=left | ph0.state=both: inuse;
74 -- (F (ph0.state=both)) & (F (ph1.state=both)) & (F (ph2.state=both)) &
75 -- (F (ph3.state=both)) & (F (ph4.state=both)) & (F (ph5.state=both)) &
76 -- (F (ph6.state=both)))