MODULE main
VAR
  turn : 1..2;
  p : process user(turn, 1, 2); 
  q : process user(turn, 2, 1); 
ASSIGN
  init(turn) := 1;
SPEC -- MUTUAL EXCLUSION
  AG !(p.state = exit & q.state = exit)
SPEC -- DEADLOCK
  AG (p.state = enter -> AF (p.state = exit | q.state = exit))
SPEC -- INDIVIDUAL STARVATION
  AG (p.state = enter -> AF p.state = exit)

MODULE user(turnloc, myproc, otherproc)
VAR
  state : {enter,exit};
ASSIGN
  init(state) := enter;
  next(state) :=
    case
      state = enter & turnloc = myproc : {enter,exit};
      state = exit : enter;
      TRUE : state;
    esac;
  next(turnloc) :=
    case
      state = exit : otherproc;
      TRUE : turnloc;
    esac;
FAIRNESS
  running