51 lines
1.1 KiB
Text
51 lines
1.1 KiB
Text
|
MODULE main
|
||
|
|
VAR
|
||
|
|
turn : {p,q};
|
||
|
|
wantp : boolean;
|
||
|
|
wantq : boolean;
|
||
|
|
procp : process user(turn, wantp, wantq, p, q);
|
||
|
|
procq : process user(turn, wantq, wantp, q, p);
|
||
|
|
ASSIGN
|
||
|
|
init(turn) := p;
|
||
|
|
init(wantp) := FALSE;
|
||
|
|
init(wantq) := FALSE;
|
||
|
|
--SPEC
|
||
|
|
--AG (proc1.state = entering -> AF proc1.state = critical)
|
||
|
|
|
||
|
|
MODULE user(turn, wantp, wantq, myid, otherid)
|
||
|
|
VAR
|
||
|
|
state : {p1,p2,p3,p4,p5,p6,p7,p8,p9,p10};
|
||
|
|
ASSIGN
|
||
|
|
init(state) := p1;
|
||
|
|
next(state) :=
|
||
|
|
case
|
||
|
|
state = p1 : {p1,p2};
|
||
|
|
state = p2 : p3;
|
||
|
|
state = p3 & wantq = TRUE : p4;
|
||
|
|
state = p3 & wantq = FALSE : p8;
|
||
|
|
state = p4 & turn = otherid: p5;
|
||
|
|
state = p4 & turn = myid: p3;
|
||
|
|
state = p5 : p6;
|
||
|
|
state = p6 & turn = myid : p7;
|
||
|
|
state = p7 : p3;
|
||
|
|
state = p8 : p9;
|
||
|
|
state = p9 : p10;
|
||
|
|
state = p10 : p1;
|
||
|
|
TRUE : state;
|
||
|
|
esac;
|
||
|
|
|
||
|
|
next(turn) :=
|
||
|
|
case
|
||
|
|
next(state) = p10 : otherid;
|
||
|
|
TRUE : turn;
|
||
|
|
esac;
|
||
|
|
|
||
|
|
next(wantp) :=
|
||
|
|
case
|
||
|
|
next(state) = p3 & state != p4 : TRUE;
|
||
|
|
next(state) = p6 : FALSE;
|
||
|
|
next(state) = p1 & state = p10 : FALSE;
|
||
|
|
TRUE : wantp;
|
||
|
|
esac;
|
||
|
|
FAIRNESS
|
||
|
|
running
|