DoFork1 = ( pick_right_1 -> put_right_1 -> DoFork1 | pick_left_2 -> put_left_2 -> DoFork1 ).
procedure do_fork1 { abstract { 1 , DoFork1 }; }
DoFork2 = ( pick_right_2 -> put_right_2 -> DoFork2 | pick_left_1 -> put_left_1 -> DoFork2 ).
procedure do_fork2 { abstract { 1 , DoFork2 }; }

program phil1,phil2,fork1,fork2 {
  specification abs_1,{P0::eating == 0,P1::eating == 0,1,1},DpSpec1;
  specification abs_2,{1,1,1,1},DefaultSpec;
}

ltl DpSpec1 { #G [(P0::eating == 0) || (P1::eating == 0)]; }