MODULE main
VAR
  turn: 1..2;
  p: process proc(turn, 1); 
  q: process proc(turn, 2); 
ASSIGN
  init(turn) := 1;

CTLSPEC -- no mutual exclusion
  AG (p.state != critical | q.state != critical)

CTLSPEC -- no deadlock
  AG (p.state = wait -> AF (p.state = critical | q.state = critical))

CTLSPEC -- no individual starvation
  AG (p.state = wait -> AF p.state = critical)
CTLSPEC
  AG (q.state = wait -> AF q.state = critical)
CTLSPEC
  AG (q.state = wait -> EF q.state = critical)

MODULE proc(turn, id) -- Model a process taking turn
VAR
    state: {begin, wait, critical, done};
ASSIGN
    init(state) := begin;
    next(state) :=
                case
                    state = begin: {begin, wait};
                    state = wait & turn = id: critical;
                    state = critical: {critical, done};
                    state = done: begin;
                    TRUE: state;
                esac;
    next(turn) :=
               case
                    state = done: (turn mod 2)+1;
                    TRUE: turn;
               esac;
FAIRNESS
    running