%
  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