% This is a specification of a solution to the dining philosophers
% problem for 3 philosophers using a scheduler (sequential version).

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 ack_get, get, put, up, down, lock, free: Phil # Fork;
    eat: Phil;

proc P_Phil(p: Phil) =
       (get(p,lf(p)).get(p,rf(p)) + get(p,rf(p)).get(p,lf(p))) . eat(p) .
       (put(p,lf(p)).put(p,rf(p)) + put(p,rf(p)).put(p,lf(p))) . P_Phil(p);
     P_Fork(f: Fork) = sum p:Phil. up(p,f) . down(p,f) . P_Fork(f);
     Waiter = ack_get(p1, lf(p1)) . ack_get(p1, rf(p1)) .
              ack_get(p2, lf(p2)) . ack_get(p2, rf(p2)) .
              ack_get(p3, lf(p3)) . ack_get(p3, rf(p3)) . Waiter;

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