MODULE main
VAR
  wp : boolean;
  wq : boolean;
  turn : 1..2;
  p : process user(wp,wq, turn, 1, 2);
  q : process user(wq,wp, turn, 2, 1);
ASSIGN
  init(wp) := FALSE;
  init(wq) := FALSE;
  init(turn) := 1;

SPEC -- PROGRESS
  AG (p.state = local -> EF p.state = enter )
SPEC -- MUTUAL EXCLUSION
  AG !(p.state = critical & q.state = critical)
SPEC -- DEADLOCK
  AG (p.state = set -> AF (p.state = critical | q.state = critical))
SPEC -- INDIVIDUAL STARVATION
  AG (p.state = set -> AF p.state = critical)

MODULE user(wp, wq, turn, me, other)
VAR
  state : {local, set, enter, checkTurn, loopUnset, waitTurn, loopSet, critical, setTurn, exit};
ASSIGN
  init(state) := local;
  next(state) :=
    case
      state = local : {local, set};
      state = set : enter;

      state = enter & wq = FALSE : critical;     -- Go to CS

      state = enter & wq = TRUE : checkTurn;     -- Start waiting loop
      state = checkTurn & turn = me : enter;      -- Go back to loop check
      state = checkTurn & turn = other : loopUnset;  -- Descend in loop
      state = loopUnset : waitTurn;
      state = waitTurn & turn = me : loopSet;     -- Wait until turn == 1
      state = loopSet : enter;                   -- End of loop

      state = critical : exit;
      state = setTurn : exit;
      state = exit : local;
      TRUE : state;
    esac;

  next(wp) :=
    case
      state = set : TRUE;
      state = loopUnset : FALSE;
      state = loopSet : TRUE;
      state = exit : FALSE;
      TRUE : wp;
    esac;
  next(turn) :=
    case
      state = setTurn : other;
      TRUE : turn;
    esac;
FAIRNESS
  running