MODULE main
VAR
    wantP: boolean;
    wantQ: boolean;
    p: proc(wantP, wantQ);
    q: proc(wantQ, wantP);
ASSIGN
    init(wantP) := FALSE;
    init(wantQ) := FALSE;

    next(wantP) := case
                    p.state = setTrue: TRUE;
                    p.state = setFalse: FALSE;
                    TRUE: wantP;
                   esac;
    next(wantQ) := case
                    q.state = setTrue: TRUE;
                    q.state = setFalse: FALSE;
                    TRUE: wantQ;
                   esac;

CTLSPEC -- no 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 individual starvation
  AG (p.state = await -> AF p.state = critical)
CTLSPEC
  AG (q.state = await -> AF q.state = critical)

CTLSPEC -- prova: path senza starvation
  AG (q.state = await -> EF q.state = critical)


MODULE proc(mine, other)
VAR
    state: {local, await, critical, setTrue, setFalse};
ASSIGN
    init(state) := local;
    next(state) := case
                    state = local: {local, await};
                    state = await & other = FALSE: setTrue;
                    state = await: await;
                    state = setTrue: critical;
                    state = critical: setFalse;
                    state = setFalse: local;
                   esac;