UniTO/anno3/vpc/consegne/3/3.6.b.smv

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

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)


LTLSPEC -- no 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 individual starvation
  G (p.state = await -> F p.state = critical)
LTLSPEC
  G (q.state = await -> F 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;
    next(mine) := case
                    state = setTrue: TRUE;
                    state = setFalse: FALSE;
                    TRUE: mine;
                   esac;

FAIRNESS
    running