% <pre>  2-process Bakery, downscaled to finite-state

smallbakery : CONTEXT =  
BEGIN 
   phase : TYPE = {idle, trying, critical};
   max: NATURAL = 8;
   ticket: TYPE = [0..max];

process : MODULE =
BEGIN
 INPUT other_t: ticket
 OUTPUT my_t: ticket
 OUTPUT pc: phase

 INITIALIZATION
  pc = idle;
  my_t = 0

 TRANSITION
    [pc = idle AND other_t < max --> 
          my_t'  = other_t + 1;
          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;

% sal-path-finder -d 5 smallbakery system

% sal-viewer smallbakery system
%./a.out --max-depth=5


% 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 --verbose smallbakery safety
% ./a.out --verbose

% sal-smc -v 1 smallbakery safety

% untrue
unbounded: THEOREM system |- G(my_t < 8);
% sal-model-checker --verbose smallbakery unbounded
% ./a.out --verbose

% sal-smc -v 1 smallbakery unbounded
% sal-bmc -v 1 -d 20 smallbakery unbounded

% untrue
liveness: THEOREM system |- F(pc1 = critical);
% sal-model-checker --verbose smallbakery liveness
% ./a.out --verbose

% sal-smc -v 1 smallbakery liveness
% sal-bmc -v 1 smallbakery liveness

response: THEOREM system |- G(pc1 = trying => F(pc1 = critical));
% sal-model-checker smallbakery response
% ./a.out --verbose

% sal-smc -v 1 smallbakery response

weak_fair: THEOREM system |- F(G(pc1 = trying)) => G(F(pc1 = critical));
% sal-model-checker smallbakery weak_fair
% ./a.out --verbose

% sal-smc -v 1 smallbakery weak_fair

strong_fair: THEOREM system |- G(F(pc1 = trying)) => G(F(pc1 = critical));
% sal-model-checker smallbakery strong_fair
% ./a.out --verbose

% sal-smc -v 1 smallbakery strong_fair

aux: LEMMA system |- G((my_t = 0 => pc1 = idle) AND (other_t = 0 => pc2 = idle));
% sal-smc -v 1 smallbakery aux
% can also prove by induction
% sal-bmc -v 1 -d 1 -i smallbakery 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));
% sal-smc -v 1 smallbakery strong_prop
% can also prove by induction given aux
% sal-bmc -v 1 -d 1 -i -l aux smallbakery strong_prop
% can then prove safety given aux and strong_prop
% sal-bmc -v 1 -d 1 -i -l aux -l strong_prop smallbakery safety

% but can prove strong_prop alone with 3-induction
% sal-bmc -v 1 -d 3 -i smallbakery strong_prop
% then prove safety given just strong_prop by 4-induction
% sal-bmc -v 1 -d 4 -i -l strong_prop smallbakery safety

% and can prove safety alone with 7-induction
% sal-bmc -v 1 -d 7 -i smallbakery safety

END