%
2-process Bakery, infinite-state case in SAL bakery : CONTEXT = BEGIN phase : TYPE = {idle, trying, critical}; ticket: TYPE = NATURAL; process : MODULE = BEGIN INPUT other_t: ticket OUTPUT my_t: ticket OUTPUT pc: phase INITIALIZATION pc = idle; my_t = 0 TRANSITION [pc = idle --> my_t' = other_t + 1; % change to 0 for a bug pc' = trying [] pc = trying AND (other_t = 0 OR my_t < other_t) --> pc' = critical [] pc = critical --> my_t' = 0; pc' = idle ] END; P1 : MODULE = RENAME pc TO pc1 IN process; P2 : MODULE = RENAME other_t TO my_t, my_t TO other_t, pc TO pc2 IN process; system : MODULE = P1 [] P2; % following is equivalent to system alt_system : MODULE = (RENAME pc TO pc1 IN process) [] (RENAME pc TO pc2, my_t TO other_t, other_t TO my_t IN process); safety: THEOREM system |- G(NOT (pc1 = critical AND pc2 = critical)); % sal-model-checker bakery safety % ./a.out --max-depth=22222 --verbose % sal-inf-bmc -v 1 bakery safety % untrue unbounded: THEOREM system |- G(my_t < 8); % sal-model-checker bakery unbounded % ./a.out --max-depth=21 --verbose % sal-inf-bmc -v 1 -d 20 bakery unbounded % untrue liveness: THEOREM system |- F(pc1 = critical); % sal-inf-bmc -v 1 bakery liveness response: THEOREM system |- G(pc1 = trying => F(pc1 = critical)); % sal-inf-bmc -v 1 bakery response weak_fair: THEOREM system |- F(G(pc1 = trying)) => G(F(pc1 = critical)); % sal-inf-bmc -v 1 bakery weak_fair strong_fair: THEOREM system |- G(F(pc1 = trying)) => G(F(pc1 = critical)); % sal-inf-bmc -v 1 bakery strong_fair aux: LEMMA system |- G((my_t = 0 => pc1 = idle) AND (other_t = 0 => pc2 = idle)); % can prove by induction % sal-inf-bmc -v 1 -d 1 -i bakery aux strong_prop: THEOREM system |- G(((pc1 = critical AND pc2 = trying) => my_t < other_t) AND ((pc2 = critical AND pc1 = trying) => other_t < my_t)); % can prove by induction given aux % sal-inf-bmc -v 1 -d 1 -i -l aux bakery strong_prop % can then prove safety given aux and strong_prop % sal-inf-bmc -v 1 -d 1 -i -l aux -l strong_prop bakery safety % but can prove strong_prop alone with 3-induction % sal-inf-bmc -v 1 -d 3 -i bakery strong_prop % then prove safety given just strong_prop by 4-induction % sal-inf-bmc -v 1 -d 4 -i -l strong_prop bakery safety % and can prove safety alone with 7-induction % sal-inf-bmc -v 1 -d 7 -i bakery safety END