% <pre>  2-process Bakery, infinite-state case in PVS

bakery: THEORY
BEGIN

phase : TYPE = {idle, trying, critical}

state: TYPE = [# pc1, pc2: phase, t1, t2: nat #]

s, pre, post: VAR state

P1_transition(pre, post): boolean = 
    IF pre`pc1 = idle
      THEN post = pre WITH [`t1 := pre`t2 + 1, `pc1 := trying]
    ELSIF pre`pc1 = trying AND (pre`t2 = 0 OR pre`t1 < pre`t2)
      THEN post = pre WITH [`pc1 := critical]
    ELSIF pre`pc1 = critical
      THEN post = pre WITH [`t1 := 0, `pc1 := idle]
    ELSE post = pre
    ENDIF

% Could also be written as
%
%   CASES pre`pc1 OF
%      idle:     post = pre WITH [`t1 := pre`t2 + 1, `pc1 := trying],
%      trying:   IF  (pre`t2 = 0 OR pre`t1 < pre`t2)
%                 THEN post = pre WITH [`pc1 := critical]
%                ELSE post = pre ENDIF,
%      critical: post = pre WITH [`t1 := 0, `pc1 := idle]
%    ENDCASES
%


P2_transition(pre, post): boolean =  
    IF pre`pc2 = idle
      THEN post = pre WITH [`t2 := pre`t1 + 1, `pc2 := trying]
    ELSIF pre`pc2 = trying AND (pre`t1 = 0 OR pre`t1 > pre`t2)
      THEN post = pre WITH [`pc2 := critical]
    ELSIF pre`pc2 = critical
      THEN post = pre WITH [`t2 := 0, `pc2 := idle]
    ELSE post = pre
    ENDIF

transitions(pre, post): bool = 
   P1_transition(pre, post) OR P2_transition(pre, post)

init(s): boolean = s`pc1 = idle AND s`pc2 = idle AND s`t1 = 0 AND s`t2 = 0

safe(s): boolean = NOT (s`pc1 = critical AND s`pc2 = critical)

IMPORTING transitions[state, init, transitions]

% Intentionally not proved
first_try: LEMMA indinv(safe)

strong_safe(s): bool = safe(s) 
  AND (s`t1 = 0 => s`pc1 = idle)
  AND (s`t2 = 0 => s`pc2 = idle)

% Intentionally not proved
second_try: LEMMA indinv(strong_safe)

inductive_safe(s): bool = strong_safe(s)
  AND ((s`pc1 = critical AND s`pc2 = trying) => s`t1 < s`t2)
  AND ((s`pc2 = critical AND s`pc1 = trying) => s`t1 > s`t2)

third_try: LEMMA indinv(inductive_safe)

abstract_state: TYPE = 
  [# pc1, pc2: phase, t1_is_0, t2_is_0, t1_lt_t2: bool #]

a_s, a_pre, a_post: VAR abstract_state

abst(s): abstract_state =
  (# pc1 := s`pc1, 
     pc2 := s`pc2,
     t1_is_0 := s`t1 = 0, 
     t2_is_0 := s`t2 = 0,
     t1_lt_t2 := s`t1 < s`t2 #)

a_init(a_s): bool = 
   a_s`pc1 = idle AND a_s`pc2 = idle AND a_s`t1_is_0 AND a_s`t2_is_0

a_P1_transition(a_pre, a_post): bool = 
%   a_pre = a_post OR
   IF a_pre`pc1 = idle
     THEN a_post = a_pre WITH [`t1_is_0 := false,
                               `t1_lt_t2 := false,
                               `pc1 := trying]
   ELSIF a_pre`pc1 = trying AND (a_pre`t2_is_0 OR a_pre`t1_lt_t2)
     THEN a_post = a_pre WITH [`pc1 := critical]
   ELSIF a_pre`pc1 = critical
     THEN a_post = a_pre WITH [`t1_is_0 := true,
                               `t1_lt_t2 := NOT a_pre`t2_is_0,
                               `pc1 := idle]
   ELSE a_post = a_pre
   ENDIF

a_P2_transition(a_pre, a_post): bool =  
%   a_pre = a_post OR
   IF a_pre`pc2 = idle
     THEN a_post = a_pre WITH [`t2_is_0 := false,
                               `t1_lt_t2 := true,
                               `pc2 := trying]
   ELSIF a_pre`pc2 = trying AND (a_pre`t1_is_0 OR NOT a_pre`t1_lt_t2)
     THEN a_post = a_pre WITH [`pc2 := critical]
   ELSIF a_pre`pc2 = critical
     THEN a_post = a_pre WITH [`t2_is_0 := true,
                               `t1_lt_t2 := false,
                               `pc2 := idle]
   ELSE a_post = a_pre
   ENDIF

a_trans(a_pre, a_post): bool = a_P1_transition(a_pre, a_post)
                               OR a_P2_transition(a_pre, a_post)

a_safe(a_s): boolean = NOT (a_s`pc1 = critical AND a_s`pc2 = critical)

init_simulation: THEOREM
   init(s) IMPLIES a_init(abst(s))

% Intentionally not proved
trans_simulation: THEOREM
   transitions(pre, post) IMPLIES a_trans(abst(pre), abst(post))

safety_preserved: THEOREM a_safe(abst(s)) IMPLIES safe(s)

abs_invariant_ctl: THEOREM
   a_init(a_s) IMPLIES AG(a_trans, a_safe)(a_s)

not_eq(s): bool = s`t1 = s`t2 => s`t1=0

extra: LEMMA indinv(not_eq)

strong_trans_simulation: THEOREM
   indinv(not_eq) 
    AND not_eq(pre)
    AND not_eq(post)
    AND transitions(pre, post) 
     IMPLIES a_trans(abst(pre), abst(post))

auto_abstract: THEOREM init(s) IMPLIES AG(transitions, safe)(s)

END bakery