(************************************************************ * Result output by IMITATOR * Version : IMITATOR 2.10.4 "Butter Jellyfish" (build 2477) * Git : HEAD/5b53333 * Model : 'accel_6000.imi' * Generated: Thu Aug 23, 2018 16:37:18 * Command : ./imitator accel_6000.imi -mode EFunsafe -no-inclusion-test-in-EF -incl -verbose experiments -output-result ************************************************************) ------------------------------------------------------------ Number of IPTAs : 2 Number of clocks : 2 Has stopwatches? : false L/U subclass : not L/U Number of parameters : 3 Number of discrete variables : 0 Number of actions : 11 Total number of locations : 15390 Average locations per IPTA : 7695.0 ------------------------------------------------------------ BEGIN CONSTRAINT 6509 >= 25*t & 25*tprime > 6707 & 25*t > 6463 & 6788 > 25*tprime & 25*p10 + 25*t >= 6682 OR 3851 > 5*tprime & 5*tprime > 3831 & 19069 >= 25*t & 25*t > 19068 & 5*p10 + 5*t >= 3826 OR 25*t > 58463 & 11702 >= 5*t & 58618 > 25*tprime & 25*tprime > 58597 & 25*p10 + 25*t >= 58572 OR 63009 >= 25*t & 25*tprime > 63216 & 25*t > 62964 & 63417 > 25*tprime & 25*p10 + 25*t >= 63191 OR 14202 >= 5*t & 25*tprime > 71233 & 25*t > 70961 & 2858 > tprime & 25*p10 + 25*t >= 71208 OR 25*t > 82462 & 82512 >= 25*t & 16568 > 5*tprime & 5*tprime > 16567 & 5*p10 + 5*t >= 16562 OR 25*t > 138463 & 138511 >= 25*t & 25*tprime > 138721 & 138737 > 25*tprime & 25*p10 + 25*t >= 138696 END CONSTRAINT ------------------------------------------------------------ Constraint soundness : exact Termination : regular termination Constraint nature : bad ------------------------------------------------------------ Number of states : 39152 Number of transitions : 39151 Number of computed states : 39152 Total computation time : 10.148 seconds States/second in state space : 3857.7 (39152/10.148 seconds) Computed states/second : 3857.7 (39152/10.148 seconds) Estimated memory : 16.710 GiB (i.e., 2242812452 words of size 8) ------------------------------------------------------------ ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm + parsing : 19.830 seconds main algorithm : 10.148 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.112 second model converting : 9.564 seconds model parsing and converting : 9.681 seconds ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 33534 number of constraints comparisons : 0 number of new states <= old : 0 number of new states >= old : 0 StateSpace.merging attempts : 0 StateSpace.merges : 0 StateSpace.add_state : 0.372 second (39152 calls | 9.52160450991e-06 second/call) StateSpace.compute_predecessors : 0.000 second (0 call) StateSpace.counter_get_location : 0.038 second (150989 calls | 2.56985002173e-07 second/call) StateSpace.get_state : 0.130 second (150989 calls | 8.62279132927e-07 second/call) StateSpace.add_transition : 0.059 second (39151 calls | 1.52090117014e-06 second/call) StateSpace.get_successors : 0.000 second (0 call) StateSpace.get_transitions : 0.000 second (0 call) StateSpace.nb_states : 0.000 second (1 call | 9.53674316407e-07 second/call) StateSpace.nb_transitions : 0.000 second (1 call | 0. second/call) StateSpace.empty_states_for_comparison : 0.000 second (0 call) StatesMerging.merging attempts : 0 StatesMerging.merges : 0 early unsat states (local discrete guard): 0 early unsat states (local continuous guard): 8 skipped actions : 8 unsatisfiable constraints : 0 unsatisfiable global discrete constraints: 0 different combinations : 0 early unsat (D^g) : 0 next transitions : 0.412 second legal transitions exist : 1.549 seconds compute locations,guards,updates : 0.144 second StateBased.add_transition_to_state_space: 0.105 second (39151 calls | 2.68749032349e-06 second/call) StateBased.explore_layer_bfs : 10.144 seconds (1 call | 10.1449930668 second/call) StateBased.post_from_one_state : 9.847 seconds (39145 calls | 0.00025157686668 second/call) StateBased.process_post_n : 0.004 second (15377 calls | 2.72575835378e-07 second/call) StateBased.gcmajor : 0.003 second (15377 calls | 2.43705744055e-07 second/call) EFsynth.process_state : 0.025 second (39152 calls | 6.58616709817e-07 second/call) EFsynth.compute_p_constraint_with_cache : 0.452 second (39151 calls | 1.1548067655e-05 second/call) EFsynth.add_a_new_state : 1.135 seconds (39151 calls | 2.89941375422e-05 second/call) ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 19.840 seconds ------------------------------------------------------------