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

MODULE main
VAR
  turn: 1 .. 2;
  p: proc(turn, 1); 
  q: proc(turn, 2);
ASSIGN
    init(turn) := 1;
    next(turn) :=
               case
                    q.state = done: 1;
                    p.state = done: 2;
                    TRUE: turn;
               esac;

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

CTLSPEC -- no deadlock
  AG ((p.state = wait | q.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)


LTLSPEC -- no mutual exclusion
  G (p.state != critical | q.state != critical)
LTLSPEC -- no deadlock
  G ((p.state = wait | q.state = wait) -> F (p.state = critical | q.state = critical))
LTLSPEC -- no individual starvation
  G (p.state = wait -> F p.state = critical)
LTLSPEC
  G (q.state = wait -> F 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: done;
                    state = done: begin;
                    TRUE: state;
                esac;