MODULE main
VAR
  turn : {p,q};
  procp : process user(turn, p, q);
  procq : process user(turn, q, p);
ASSIGN
  init(turn) := p;
--SPEC
  --AG (proc1.state = entering -> AF proc1.state = critical)

MODULE user(turn, myid, otherid)
VAR
  state : {p1,p2,p3,p4};
ASSIGN
  init(state) := p1;
  next(state) := 
    case 
      state = p1 : {p1,p2};
      state = p2 & turn = myid : p3;
      state = p3 : p4;
      state = p4 : p1;
      TRUE : state;
    esac;
  next(turn) := 
    case
      next(state) = p4 : otherid;
      TRUE : turn;
    esac;
FAIRNESS
  running