MODULE main
VAR
  save : boolean;
  saved : boolean;
  turn_a_0 : boolean; --TYPE-- 1..2
  fork1_o_try___to___take___left : boolean;
  fork1_o_try___to___take___right : boolean;
  fork1_o_owner_a_1 : boolean; --TYPE-- 0..2
  fork1_o_owner_a_0 : boolean;
  fork1_o_loop_a_1 : boolean; --TYPE-- 0..2
  fork1_o_loop_a_0 : boolean;
  phil1_o_fair : boolean;
  phil1_o_state_a_0 : boolean; --TYPE-- eat think
  phil1_o_loop_a_0 : boolean; --TYPE-- eat think
  fork2_o_try___to___take___left : boolean;
  fork2_o_try___to___take___right : boolean;
  fork2_o_owner_a_1 : boolean; --TYPE-- 0..2
  fork2_o_owner_a_0 : boolean;
  fork2_o_loop_a_1 : boolean; --TYPE-- 0..2
  fork2_o_loop_a_0 : boolean;
  phil2_o_fair : boolean;
  phil2_o_state_a_0 : boolean; --TYPE-- eat think
  phil2_o_loop_a_0 : boolean; --TYPE-- eat think
  live : boolean;
DEFINE
  fork1_o_looped := saved & (fork1_o_loop_a_0 <-> fork1_o_owner_a_0) & (fork1_o_loop_a_1 <-> fork1_o_owner_a_1);
  phil1_o_looped := saved & (phil1_o_loop_a_0 <-> phil1_o_state_a_0);
  fork2_o_looped := saved & (fork2_o_loop_a_0 <-> fork2_o_owner_a_0) & (fork2_o_loop_a_1 <-> fork2_o_owner_a_1);
  phil2_o_looped := saved & (phil2_o_loop_a_0 <-> phil2_o_state_a_0);
  found := !phil1_o_state_a_0;
  looped := phil1_o_looped & phil2_o_looped;
  fair := phil1_o_fair & phil2_o_fair;
  _o_MACRO1 := fork1_o_owner_a_1 | fork1_o_owner_a_0;
  _o_MACRO0 := !phil2_o_state_a_0 | _o_MACRO1;
  _o_MACRO5 := fork1_o_owner_a_0 <-> turn_a_0;
  _o_MACRO6 := fork1_o_owner_a_1 <-> !turn_a_0;
  _o_MACRO4 := _o_MACRO5 | _o_MACRO6;
  _o_MACRO3 := phil2_o_state_a_0 | _o_MACRO4;
  _o_MACRO2 := !_o_MACRO0 | _o_MACRO3;
  _o_MACRO7 := !_o_MACRO0 | !_o_MACRO3;
  _o_MACRO8 := !fork1_o_try___to___take___left | !turn_a_0;
  _o_MACRO9 := !phil1_o_state_a_0 | _o_MACRO1;
  _o_MACRO11 := phil1_o_state_a_0 | _o_MACRO4;
  _o_MACRO10 := !_o_MACRO9 | _o_MACRO11;
  _o_MACRO12 := !_o_MACRO9 | !_o_MACRO11;
  _o_MACRO14 := !fork1_o_try___to___take___right | turn_a_0;
  _o_MACRO13 := !_o_MACRO8 | _o_MACRO14;
  _o_MACRO15 := !_o_MACRO8 | !_o_MACRO14;
  _o_MACRO16 := !save | saved;
  _o_MACRO17 := save | saved;
  _o_MACRO19 := fork2_o_owner_a_1 | fork2_o_owner_a_0;
  _o_MACRO18 := !phil1_o_state_a_0 | _o_MACRO19;
  _o_MACRO23 := fork2_o_owner_a_0 <-> turn_a_0;
  _o_MACRO24 := fork2_o_owner_a_1 <-> !turn_a_0;
  _o_MACRO22 := _o_MACRO23 | _o_MACRO24;
  _o_MACRO21 := phil1_o_state_a_0 | _o_MACRO22;
  _o_MACRO20 := !_o_MACRO18 | _o_MACRO21;
  _o_MACRO25 := !_o_MACRO18 | !_o_MACRO21;
  _o_MACRO26 := !fork2_o_try___to___take___left | turn_a_0;
  _o_MACRO27 := !phil2_o_state_a_0 | _o_MACRO19;
  _o_MACRO29 := phil2_o_state_a_0 | _o_MACRO22;
  _o_MACRO28 := !_o_MACRO27 | _o_MACRO29;
  _o_MACRO30 := !_o_MACRO27 | !_o_MACRO29;
  _o_MACRO32 := !fork2_o_try___to___take___right | !turn_a_0;
  _o_MACRO31 := !_o_MACRO26 | _o_MACRO32;
  _o_MACRO33 := !_o_MACRO26 | !_o_MACRO32;
ASSIGN
  init(fork1_o_owner_a_1) := FALSE;
  init(fork1_o_owner_a_0) := FALSE;
  next(fork1_o_owner_a_1) := ((turn_a_0 | _o_MACRO0) & _o_MACRO2 & (fork1_o_owner_a_1 | _o_MACRO7) | _o_MACRO8) & ((turn_a_0 | _o_MACRO9) & _o_MACRO10 & (fork1_o_owner_a_1 | _o_MACRO12) | _o_MACRO13) & (fork1_o_owner_a_1 | _o_MACRO15);
  next(fork1_o_owner_a_0) := (_o_MACRO8 | _o_MACRO2 & (!turn_a_0 | _o_MACRO0) & (fork1_o_owner_a_0 | _o_MACRO7)) & (_o_MACRO13 | _o_MACRO10 & (!turn_a_0 | _o_MACRO9) & (fork1_o_owner_a_0 | _o_MACRO12)) & (fork1_o_owner_a_0 | _o_MACRO15);
  init(fork1_o_loop_a_1) := FALSE;
  init(fork1_o_loop_a_0) := FALSE;
  next(fork1_o_loop_a_1) := (fork1_o_owner_a_1 | _o_MACRO16) & (fork1_o_loop_a_1 | !_o_MACRO16);
  next(fork1_o_loop_a_0) := (fork1_o_owner_a_0 | _o_MACRO16) & (fork1_o_loop_a_0 | !_o_MACRO16);
  init(phil1_o_state_a_0) := TRUE;
  next(phil1_o_state_a_0) := (!phil1_o_state_a_0 | turn_a_0 | fork1_o_owner_a_1 | !fork1_o_owner_a_0 | fork2_o_owner_a_1 | !fork2_o_owner_a_0) & (phil1_o_state_a_0 | !phil1_o_state_a_0 & !turn_a_0);
  init(phil1_o_loop_a_0) := TRUE;
  next(phil1_o_loop_a_0) := (phil1_o_state_a_0 | _o_MACRO16) & (phil1_o_loop_a_0 | !_o_MACRO16);
  init(phil1_o_fair) := FALSE;
  next(phil1_o_fair) := phil1_o_fair | !turn_a_0 & _o_MACRO17;
  init(fork2_o_owner_a_1) := FALSE;
  init(fork2_o_owner_a_0) := FALSE;
  next(fork2_o_owner_a_1) := ((turn_a_0 | _o_MACRO18) & _o_MACRO20 & (fork2_o_owner_a_1 | _o_MACRO25) | _o_MACRO26) & ((turn_a_0 | _o_MACRO27) & _o_MACRO28 & (fork2_o_owner_a_1 | _o_MACRO30) | _o_MACRO31) & (fork2_o_owner_a_1 | _o_MACRO33);
  next(fork2_o_owner_a_0) := (_o_MACRO26 | _o_MACRO20 & (!turn_a_0 | _o_MACRO18) & (fork2_o_owner_a_0 | _o_MACRO25)) & (_o_MACRO31 | _o_MACRO28 & (!turn_a_0 | _o_MACRO27) & (fork2_o_owner_a_0 | _o_MACRO30)) & (fork2_o_owner_a_0 | _o_MACRO33);
  init(fork2_o_loop_a_1) := FALSE;
  init(fork2_o_loop_a_0) := FALSE;
  next(fork2_o_loop_a_1) := (fork2_o_owner_a_1 | _o_MACRO16) & (fork2_o_loop_a_1 | !_o_MACRO16);
  next(fork2_o_loop_a_0) := (fork2_o_owner_a_0 | _o_MACRO16) & (fork2_o_loop_a_0 | !_o_MACRO16);
  init(phil2_o_state_a_0) := TRUE;
  next(phil2_o_state_a_0) := (!phil2_o_state_a_0 | !turn_a_0 | !fork2_o_owner_a_1 | fork2_o_owner_a_0 | !fork1_o_owner_a_1 | fork1_o_owner_a_0) & (phil2_o_state_a_0 | !phil2_o_state_a_0 & turn_a_0);
  init(phil2_o_loop_a_0) := TRUE;
  next(phil2_o_loop_a_0) := (phil2_o_state_a_0 | _o_MACRO16) & (phil2_o_loop_a_0 | !_o_MACRO16);
  init(phil2_o_fair) := FALSE;
  next(phil2_o_fair) := phil2_o_fair | turn_a_0 & _o_MACRO17;
  init(saved) := FALSE;
  next(saved) := _o_MACRO17;
  init(live) := FALSE;
  next(live) := found | live;
--INVAR
--  (!fork1_o_owner_a_1 | !fork1_o_owner_a_0) &
--  (!fork1_o_loop_a_1 | !fork1_o_loop_a_0) &
--  (!fork2_o_owner_a_1 | !fork2_o_owner_a_0) &
--  (!fork2_o_loop_a_1 | !fork2_o_loop_a_0)
SPEC
  AG (live | !fair | !looped)