COPPER version 2.0 ... Command Line: copper --default --specification abs_2 dp-2.pp dp-2.spec --deadlock Simplify process started ... parsing preprocessed C file dp-2.pp ... parsing specification file dp-2.spec ... control locations created ... skip locations eliminated ... useless branch locations eliminated ... procedures inlined ... number of locations before parallelization = 10 ... number of locations after parallelization = 9 ... proc manager for phil1 created ... component for phil1 created ... number of locations before parallelization = 10 ... number of locations after parallelization = 9 ... proc manager for phil2 created ... component for phil2 created ... number of locations before parallelization = 3 ... number of locations after parallelization = 3 ... proc manager for fork1 created ... component for fork1 created ... number of locations before parallelization = 3 ... number of locations after parallelization = 3 ... proc manager for fork2 created ... component for fork2 created ... relevant propositions computed ... inputs processed ... checking DefaultSpec {Deadlock} temp_var_7 starting iteration number 1 ... model extracted in 3.7 milliseconds ... implementation machine extracted in 4.0 milliseconds ... global states : ( 11 11 4 4 ) = 1936 number of reachable states = 13 ... [<<-1>> {P0::eating = 0} <<[]>>:65535:255] [<<-1>> {P1::eating = 0} <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:65535:255] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:65535:255] ################################################# ================================================= +++++++++++++++++++++++++++++++++++++++++++++++++ P0::epsilon +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> branch ( 1 ) <<[]>>:65535:255] [<<-1>> {P1::eating = 0} <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:65535:255] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:65535:255] ################################################# ================================================= +++++++++++++++++++++++++++++++++++++++++++++++++ P0::epsilon +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_10 = __COPPER_HANDSHAKE__ ( "pick_left_1" ) <<[]>>:65535:255] [<<-1>> {P1::eating = 0} <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:65535:255] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:65535:255] ################################################# ================================================= +++++++++++++++++++++++++++++++++++++++++++++++++ P1::epsilon +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_10 = __COPPER_HANDSHAKE__ ( "pick_left_1" ) <<[]>>:65535:255] [<<-1>> branch ( 1 ) <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:65535:255] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:65535:255] ################################################# ================================================= +++++++++++++++++++++++++++++++++++++++++++++++++ P1::epsilon +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_10 = __COPPER_HANDSHAKE__ ( "pick_left_1" ) <<[]>>:65535:255] [<<-1>> P1::temp_var_15 = __COPPER_HANDSHAKE__ ( "pick_left_2" ) <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:65535:255] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:65535:255] ################################################# ================================================= +++++++++++++++++++++++++++++++++++++++++++++++++ P2::epsilon +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_10 = __COPPER_HANDSHAKE__ ( "pick_left_1" ) <<[]>>:65535:255] [<<-1>> P1::temp_var_15 = __COPPER_HANDSHAKE__ ( "pick_left_2" ) <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:0:0] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:65535:255] ################################################# ================================================= +++++++++++++++++++++++++++++++++++++++++++++++++ P3::epsilon +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_10 = __COPPER_HANDSHAKE__ ( "pick_left_1" ) <<[]>>:65535:255] [<<-1>> P1::temp_var_15 = __COPPER_HANDSHAKE__ ( "pick_left_2" ) <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:0:0] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:1:0] ################################################# ================================================= +++++++++++++++++++++++++++++++++++++++++++++++++ pick_left_2 +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_10 = __COPPER_HANDSHAKE__ ( "pick_left_1" ) <<[]>>:65535:255] [<<-1>> P1::temp_var_15 = __COPPER_HANDSHAKE__ ( "pick_left_2" ) <<[]>>:0:0] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:0:2] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:1:0] ################################################# ================================================= +++++++++++++++++++++++++++++++++++++++++++++++++ P1::epsilon +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_10 = __COPPER_HANDSHAKE__ ( "pick_left_1" ) <<[]>>:65535:255] [<<-1>> P1::temp_var_16 = __COPPER_HANDSHAKE__ ( "pick_right_2" ) <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:0:2] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:1:0] ################################################# ================================================= +++++++++++++++++++++++++++++++++++++++++++++++++ pick_left_1 +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_10 = __COPPER_HANDSHAKE__ ( "pick_left_1" ) <<[]>>:0:0] [<<-1>> P1::temp_var_16 = __COPPER_HANDSHAKE__ ( "pick_right_2" ) <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:0:2] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:1:2] ################################################# ================================================= +++++++++++++++++++++++++++++++++++++++++++++++++ P0::epsilon +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_11 = __COPPER_HANDSHAKE__ ( "pick_right_1" ) <<[]>>:65535:255] [<<-1>> P1::temp_var_16 = __COPPER_HANDSHAKE__ ( "pick_right_2" ) <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:0:2] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:1:2] ################################################# ================================================= global counter example dag computed ... Deadlock freedom checked in 12.9 milliseconds ... Cprover formula has 220 variables and 551 clauses ... Cprover formula has 315 variables and 685 clauses ... Cprover formula has 507 variables and 1031 clauses ... <<< BEGIN CONCRETE COUNTEREXAMPLE >>> [<<-1>> {P0::eating = 0} <<[]>>:65535:255] [<<-1>> {P1::eating = 0} <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:65535:255] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:65535:255] ################################################# ================================================= +++++++++++++++++++++++++++++++++++++++++++++++++ P0::epsilon +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> branch ( 1 ) <<[]>>:65535:255] [<<-1>> {P1::eating = 0} <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:65535:255] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:65535:255] ################################################# ================================================= (P0::eating = 0) +++++++++++++++++++++++++++++++++++++++++++++++++ P0::epsilon +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_10 = __COPPER_HANDSHAKE__ ( "pick_left_1" ) <<[]>>:65535:255] [<<-1>> {P1::eating = 0} <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:65535:255] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:65535:255] ################################################# ================================================= (P0::eating = 0) +++++++++++++++++++++++++++++++++++++++++++++++++ P1::epsilon +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_10 = __COPPER_HANDSHAKE__ ( "pick_left_1" ) <<[]>>:65535:255] [<<-1>> branch ( 1 ) <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:65535:255] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:65535:255] ################################################# ================================================= (P0::eating = 0)(P1::eating = 0) +++++++++++++++++++++++++++++++++++++++++++++++++ P1::epsilon +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_10 = __COPPER_HANDSHAKE__ ( "pick_left_1" ) <<[]>>:65535:255] [<<-1>> P1::temp_var_15 = __COPPER_HANDSHAKE__ ( "pick_left_2" ) <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:65535:255] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:65535:255] ################################################# ================================================= (P0::eating = 0)(P1::eating = 0) +++++++++++++++++++++++++++++++++++++++++++++++++ P2::epsilon +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_10 = __COPPER_HANDSHAKE__ ( "pick_left_1" ) <<[]>>:65535:255] [<<-1>> P1::temp_var_15 = __COPPER_HANDSHAKE__ ( "pick_left_2" ) <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:0:0] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:65535:255] ################################################# ================================================= (P0::eating = 0)(P1::eating = 0) +++++++++++++++++++++++++++++++++++++++++++++++++ P3::epsilon +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_10 = __COPPER_HANDSHAKE__ ( "pick_left_1" ) <<[]>>:65535:255] [<<-1>> P1::temp_var_15 = __COPPER_HANDSHAKE__ ( "pick_left_2" ) <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:0:0] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:1:0] ################################################# ================================================= (P0::eating = 0)(P1::eating = 0) +++++++++++++++++++++++++++++++++++++++++++++++++ pick_left_2 +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_10 = __COPPER_HANDSHAKE__ ( "pick_left_1" ) <<[]>>:65535:255] [<<-1>> P1::temp_var_15 = __COPPER_HANDSHAKE__ ( "pick_left_2" ) <<[]>>:0:0] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:0:2] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:1:0] ################################################# ================================================= (P0::eating = 0)(P1::eating = 0) +++++++++++++++++++++++++++++++++++++++++++++++++ P1::epsilon +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_10 = __COPPER_HANDSHAKE__ ( "pick_left_1" ) <<[]>>:65535:255] [<<-1>> P1::temp_var_16 = __COPPER_HANDSHAKE__ ( "pick_right_2" ) <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:0:2] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:1:0] ################################################# ================================================= (P0::eating = 0)(P1::eating = 0) +++++++++++++++++++++++++++++++++++++++++++++++++ pick_left_1 +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_10 = __COPPER_HANDSHAKE__ ( "pick_left_1" ) <<[]>>:0:0] [<<-1>> P1::temp_var_16 = __COPPER_HANDSHAKE__ ( "pick_right_2" ) <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:0:2] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:1:2] ################################################# ================================================= (P0::eating = 0)(P1::eating = 0) +++++++++++++++++++++++++++++++++++++++++++++++++ P0::epsilon +++++++++++++++++++++++++++++++++++++++++++++++++ [<<-1>> P0::temp_var_11 = __COPPER_HANDSHAKE__ ( "pick_right_1" ) <<[]>>:65535:255] [<<-1>> P1::temp_var_16 = __COPPER_HANDSHAKE__ ( "pick_right_2" ) <<[]>>:65535:255] [<<-1>> P2::temp_var_8 = do_fork1 ( ) <<[]>>:0:2] [<<-1>> P3::temp_var_9 = do_fork2 ( ) <<[]>>:1:2] ################################################# ================================================= (P0::eating = 0)(P1::eating = 0) <<< END CONCRETE COUNTEREXAMPLE >>> conformance relation does not exist !! specification abs_2 is invalid ... total global time = 92.5 milliseconds total cpu time = 70.0 milliseconds total input processing time = 18.6 milliseconds total Buchi automaton construction time = 0.0 milliseconds total implementation machine extraction time = 4.0 milliseconds total verification time = 12.9 milliseconds total proof generation time = 0.0 milliseconds total abstraction refinement time = 51.9 milliseconds total CE generation time = 11.0 milliseconds total CE verification time = 0.0 milliseconds total predicate abstraction refinement time = 0.0 milliseconds total LTS abstraction refinement time = 0.0 milliseconds total number of eliminating combinations = 0 max number of eliminating combinations for a CE = 0 max size of eliminating combination = 0 max size of tried combination = 0 number of iterations = 1 number of predicate iterations = 1 number of lts iterations = 0 number of seed branches : 0 number of explored states : 1936 number of theorem prover calls = 2 number of formulas found in cache = 0 number of formulas stored in cache = 2 number of membership calls to MAT = 0 number of MAT membership cache misses = 0 number of candidate calls to MAT = 0 assumption alphabet size = 0 optimal assumption alphabet size = 0 assumption alphabet ratio = 0.000000 total certificate CNF size = 0 total certificate resolution file size = 0 total certificate packed resolution file size = 0 total certificate zipped resolution file size = 0 total witness file size = 0 total witness zipped file size = 0 total certificate zipped file size = 0 Simplify process destroyed ... terminating normally ...