--- /dev/null
+MODULE proc(i, s, yme, yother)
+VAR
+ line: {l2, l3, l4, l7, l8};
+ASSIGN
+ init(line):=l2;
+ next(line):=case
+ line=l2: l3;
+ line=l3: l4;
+ line=l4: case
+ !(yother=0 | s!=i) : l4;
+ TRUE: l7;
+ esac;
+ line=l7: l8;
+ line=l8: l2;
+ esac;
+
+MODULE main
+VAR
+ y0: 0..1;
+ y1: 0..1;
+ s: 0..1;
+ proc0: proc(0, s, y0, y1);
+ proc1: proc(1, s, y1, y0);
+ASSIGN
+ next(y0):=case
+ proc0.line=l3: 1;
+ proc0.line=l8: 0;
+ TRUE: y0;
+ esac;
+ next(y1):=case
+ proc1.line=l3: 1;
+ proc1.line=l8: 0;
+ TRUE: y1;
+ esac;
+ next(s):=case
+ proc0.line=l3 & proc1.line=l3: {0,1};
+ proc0.line=l3: 0;
+ proc1.line=l3: 1;
+ TRUE: s;
+ esac;
+
+--Mutual exclusion
+LTLSPEC G(!(proc0.line=l7 & proc1.line=l7))
+
+--Absence of starvation
+LTLSPEC G (F(proc0.line=l7) & F(proc1.line=l7))
--- /dev/null
+MODULE phil(leftfork, rightfork)
+VAR
+ state: {none, left, both};
+ASSIGN
+ init(state) := none;
+ next(state) := case
+ state=none: case
+ leftfork=inuse: none;
+ TRUE: left;
+ esac;
+ state=left: case
+ rightfork=inuse: left;
+ TRUE: both;
+ esac;
+ TRUE: none;
+ esac;
+
+MODULE main
+VAR
+ f: array 0..6 of {free, inuse};
+ ph0: phil(f[6], f[1]);
+ ph1: phil(f[0], f[2]);
+ ph2: phil(f[1], f[3]);
+ ph3: phil(f[2], f[4]);
+ ph4: phil(f[3], f[5]);
+ ph5: phil(f[4], f[6]);
+ ph6: phil(f[5], f[0]);
+ASSIGN
+ init(f[0]):=free;
+ init(f[1]):=free;
+ init(f[2]):=free;
+ init(f[3]):=free;
+ init(f[4]):=free;
+ init(f[5]):=free;
+ init(f[6]):=free;
+
+ next(f[0]) := case
+ ph6.state=both | ph1.state=left | ph0.state=both: inuse;
+ TRUE: free;
+ esac;
+ next(f[1]) := case
+ ph0.state=both | ph2.state=left | ph2.state=both: inuse;
+ TRUE: free;
+ esac;
+ next(f[2]) := case
+ ph1.state=both | ph3.state=left | ph3.state=both: inuse;
+ TRUE: free;
+ esac;
+ next(f[3]) := case
+ ph2.state=both | ph4.state=left | ph4.state=both: inuse;
+ TRUE: free;
+ esac;
+ next(f[4]) := case
+ ph3.state=both | ph5.state=left | ph5.state=both: inuse;
+ TRUE: free;
+ esac;
+ next(f[5]) := case
+ ph4.state=both | ph6.state=left | ph6.state=both: inuse;
+ TRUE: free;
+ esac;
+ next(f[6]) := case
+ ph5.state=both | ph0.state=left | ph0.state=both: inuse;
+ TRUE: free;
+ esac;
+LTLSPEC F(
+ G(ph0.state=left) |
+ G(ph1.state=left) |
+ G(ph2.state=left) |
+ G(ph3.state=left) |
+ G(ph4.state=left) |
+ G(ph5.state=left) |
+ G(ph6.state=left))
+--LTLSPEC G(
+-- (F (ph0.state=both)) & (F (ph1.state=both)) & (F (ph2.state=both)) &
+-- (F (ph3.state=both)) & (F (ph4.state=both)) & (F (ph5.state=both)) &
+-- (F (ph6.state=both)))