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

absbakery : CONTEXT =  
BEGIN 
   phase : TYPE = {idle, trying, critical};

process : MODULE =
BEGIN
 INPUT other_t_IS_0: BOOLEAN
 OUTPUT my_t_IS_0: BOOLEAN
 OUTPUT pc: phase
 GLOBAL my_t_LT_other_t: BOOLEAN

 INITIALIZATION
  pc = idle;
  my_t_IS_0 = TRUE;
  my_t_LT_other_t = FALSE
 TRANSITION
    [pc = idle -->
          my_t_IS_0' = FALSE;
          my_t_LT_other_t' = FALSE;
          pc' = trying
     []                   
     pc = trying AND (other_t_IS_0 OR my_t_LT_other_t) --> 
          pc' = critical
     []
     pc = critical -->  
          my_t_IS_0' = TRUE;
	  my_t_LT_other_t' = NOT other_t_IS_0;
          pc' = idle
    ]
END;

P1 : MODULE = RENAME pc TO pc1 IN process;

P2 : MODULE = RENAME other_t_IS_0 TO my_t_IS_0, 
                          my_t_IS_0 TO other_t_IS_0, 
                          pc TO pc2 IN process;

system : MODULE = P1 [] P2;

% sal-path-finder -d 10 absbakery system

% sal-viewer absbakery system
%./a.out --max-depth=10

safety: THEOREM system |- G(NOT (pc1 = critical AND pc2 = critical));
% sal-model-checker absbakery safety
% ./a.out --verbose

% sal-smc -v 1 absbakery safety

END