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

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

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

CTLSPEC -- no starvation
    AG (p.state = await -> AF(p.state = critical));
CTLSPEC -- no starvation
    AG (q.state = await -> AF(q.state = critical));

LTLSPEC -- mutual exclusion
    G !(p.state = critical & q.state = critical)
LTLSPEC -- no deadlock
    G ((p.state = await | q.state = await) -> F(p.state = critical | q.state = critical));
LTLSPEC -- no starvation
    G (p.state = await -> F(p.state = critical));
LTLSPEC -- no starvation
    G (q.state = await -> F(q.state = critical));

MODULE proc(turn, ID, otherID, mine, other)
VAR
    state: {local, set_true, while, loop_set_false, await, loop_set_true, critical, switch_turn, set_false};

ASSIGN
    init(state) := local;
    next(state) := case
                     state = local: {local, set_true};
                     state = set_true: while;
                     state = while & other = FALSE: critical;
                     state = critical: switch_turn;
                     state = switch_turn: set_false;
                     state = set_false: local;
                     
                     -- while loop
                     state = while & other = TRUE & turn = ID: while;
                     state = while & other = TRUE & turn = otherID: loop_set_false;
                     state = loop_set_false: await;
                     state = await & turn = otherID: await;
                     state = await & turn = ID: loop_set_true;
                     state = loop_set_true: while;
                   esac;
     next(turn) := case
                     state = switch_turn: otherID;
                     TRUE: turn;
                   esac;
     next(mine) := case -- change want{P,Q}
                     state = set_true: TRUE;
                     state = loop_set_true: TRUE;
                     state = set_false: FALSE;
                     state = loop_set_false: FALSE;
                     TRUE: mine;
                   esac;

FAIRNESS running