38 lines
1 KiB
Text
38 lines
1 KiB
Text
|
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)
|
||
|
|
|
||
|
|
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;
|
||
|
|
state = done: begin;
|
||
|
|
TRUE: state;
|
||
|
|
esac;
|