inf_bakery: CONTEXT =
BEGIN
PC: TYPE = {sleeping, trying, critical};
job: MODULE =
BEGIN
INPUT y2 : NATURAL
OUTPUT y1 : NATURAL
LOCAL pc : PC
INITIALIZATION
pc = sleeping;
y1 = 0
TRANSITION
[ pc = sleeping --> y1' = y2 + 1;
pc' = trying
[]
pc = trying AND (y2 = 0 OR y1 < y2) --> pc' = critical
[]
pc = critical --> y1' = 0;
pc' = sleeping
]
END;
system: MODULE =
job
[]
RENAME y2 TO y1, y1 TO y2
IN job;
mutex: THEOREM system
|- G(NOT(pc.1 = critical AND pc.2 = critical));
invalid: THEOREM system
|- G(NOT(pc.1 = trying AND pc.2 = critical));
aux1: THEOREM system |- G(pc.1 = trying => y1 > 0);
aux2: THEOREM system |- G(pc.2 = trying => y2 > 0);
END