% This is a corrected version of the naive solution to
% the dining philosophers problem for 3 philosophers.

sort Phil = struct p1 | p2 | p3;
     Fork = struct f1 | f2 | f3;

map lf, rf: Phil -> Fork;
eqn lf(p1) = f1;
    lf(p2) = f2;
    lf(p3) = f3;
    rf(p1) = f3;
    rf(p2) = f1;
    rf(p3) = f2;

act get, put, up, down, lock, free: Phil # Fork;
    eat: Phil;

proc P_Phil(p: Phil) =
       (p == p1) -> get(p,rf(p)) . get(p,lf(p)) . eat(p) .
                    put(p,rf(p)) . put(p,lf(p)) . P_Phil(p)
                 <> get(p,lf(p)) . get(p,rf(p)) . eat(p) .
                    put(p,lf(p)) . put(p,rf(p)) . P_Phil(p);
     P_Fork(f: Fork) = sum p:Phil. up(p,f) . down(p,f) . P_Fork(f);

init block( { get, put, up, down },
       comm( { get|up->lock, put|down->free },
         P_Fork(f1) || P_Fork(f2) || P_Fork(f3) ||
         P_Phil(p1) || P_Phil(p2) || P_Phil(p3)
     ));
