* From a book by Cohen, Harwood and Jackson . "The Specification of 
* Complex Systems"  Something on that famous white rat -- the traffic light
* short green in one direction
agent T = r:r:r:a#r:g:a:r:r:T;
agent T1 = T[r1/r,g1/g,a1/a];
agent T2 = T[r2/r,g2/g,a2/a];
* short red in the other dirction
agent S = g:g:g:a:r:a#r:g:g:S;
agent S1 = S[r1/r,g1/g,a1/a];
agent S2 = S[r2/r,g2/g,a2/a];
* a light that prefers to be on green
agent G = g:G + a#k:r:r:r:r:r:a#r:g:G;
agent G1 = G[r1/r,g1/g,a1/a];
agent G2 = G[r2/r,g2/g,a2/a];
* a light that prefers to be on red
agent R = r:R + 'k#r:r:a#r:g:a:r:r:R;
agent R1 = R[r1/r,g1/g,a1/a];
agent R2 = R[r2/r,g2/g,a2/a];
* at an intersection
agent RG = (R1 | G2)\{r1,r2,g1,g2,a1,a2};
* The (syntactic) sort of two parallel agents is a subset of the cross
* products of the sorts of the two agents... doing better than this is
* quite hard. The sort of the RG agent, inferred by SCWB is as follows.
* (Says the author of this: not in v6 it wasn't, nor in v7! Hmph.)
set RGsort = {a1#a2#r1#r2,a1#a2#r2,a1#g2,a1#g2#r1,a1#r1#r2,a1#r2,a2#g1#r2,a2#r1,a2#r1#r2,g1#g2,g1#r2,g2#r1,r1#r2};

* As you can see, the greens may possible synchronise, but we can check
* prop GGSafe = max(Z.[g1#g2]F & [-]Z);
* prop  DLF = max(Z.<->T & [-]Z);

* checkprop (RG, GGSafe);
* checkprop (RG, DLF);

* and other properties using the model checker.

* Modelling a ring of traffic lights
agent C = r:C + d#r:r#a:g:a:r#e:C;
agent C1 = r1:C1 + d1#r1:r1#a1:g1:a1:r1#e1:C1;
agent C2 = r2:C2 + d2#r2:r2#a2:g2:a2:r2#e2:C2;
agent C3 = r3:C3 + d3#r3:r3#a3:g3:a3:r3#e3:C3;
set Sig3 = {r1,r2,r3,g1,g2,g3,a1,a2,a3};
agent CR = (C1['e3/d1] | C2['e1/d2] | C3['e2/d3])\Sig3;
* Unhappily that ring doesn'tau allow a lot of traffic flow.
agent CC = ((r1#e1:C1)['e3/d1] | C2['e1/d2] | C3['e2/d3])\Sig3;