//specifying procedures
PickLeft = ( pick_left -> return {} -> STOP ). 
procedure pick_left { abstract { 1, PickLeft}; }
PutRight = ( put_right -> return {} -> STOP ).
procedure put_right { abstract { 1, PutRight}; }

//LTS claims
PhilSpec1 = ( pick_left -> put_left -> PhilSpec1 ).
PhilSpec2 = ( pick_left -> put_left -> PhilSpec2 ) + { pick_right }.
PhilSpec3 = ( pick_left -> pick_left -> ERROR3 ) + { put_left }.

/* LTL claims */
ltl PhilSpec4 { #G ( [P0::eating == 1] =>  #F put_left ); }
ltl PhilSpec5 { #G ( pick_left =>  ( #X ( #F pick_left ) ) ); }

program philosopher {
        specification abs_1, {1}, PhilSpec1;
        specification abs_2, {1}, PhilSpec2;
        specification abs_3, {1}, PhilSpec3;
        specification abs_4, {1}, PhilSpec4;
        specification abs_5, {1}, PhilSpec5;
}

/* dummy claim for assertion violation */
program philosopher {
        specification abs_6, {1}, DefaultSpec;
}