these-jcb/code/simplepdltopetrinet/tina/tocheck.selt

Selt version 3.1.0 -- 01/07/13 -- LAAS/CNRS
ktz loaded, 12523 states, 60082 transitions
0.119s
operator finished : prop
0.000s
FALSE
  state 0: A_ready B_ready C_ready D_ready child_ready root_ready
  -A_start ... (preserving T)->
  state 31: A_finished*2 A_started*2 B_finished*2 B_started*2 C_finished*4 C_started*4 D_finished*4 
              D_started*4 child_finished*3 root_running
  -root_finish ... (preserving - dead /\ D_finished /\ A_finished /\ B_finished /\ C_finished)->
  state 33: L.dead A_finished*2 A_started*2 B_finished*2 B_started*2 C_finished*4 C_started*4 D_finished*4 
              D_started*4 child_finished*3 root_finished
  [accepting all]
0.001s
TRUE
0.141s
TRUE
0.363s
FALSE
  state 0: A_ready B_ready C_ready D_ready child_ready root_ready
  -A_start ... (preserving T)->
  state 32: L.dead A_finished*2 A_started*2 B_finished*2 B_started*2 C_finished*4 C_started*4 D_finished*4 
              D_started*4 child_finished*3 root_finished
  -L.deadlock ... (preserving C_finished /\ D_finished /\ A_finished /\ B_finished)->
  state 33: L.dead A_finished*2 A_started*2 B_finished*2 B_started*2 C_finished*4 C_started*4 D_finished*4 
              D_started*4 child_finished*3 root_finished
  [accepting all]
0.001s