(************************************************************ * Result output by IMITATOR * Version : IMITATOR 2.10.4 "Butter Jellyfish" (build 2477) * Git : HEAD/5b53333 * Model : 'gear_3000.imi' * Generated: Thu Aug 23, 2018 16:28:31 * Command : ./imitator gear_3000.imi -mode EFmax -no-inclusion-test-in-EF -incl -verbose experiments -output-result -output-prefix gear_3000-maxp1 ************************************************************) ------------------------------------------------------------ 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 : 7 Total number of locations : 4603 Average locations per IPTA : 2301.5 ------------------------------------------------------------ BEGIN CONSTRAINT p1 >= 0 & 16 >= 5*p1 END CONSTRAINT ------------------------------------------------------------ Constraint soundness : exact Termination : regular termination Constraint nature : good ------------------------------------------------------------ Number of states : 10448 Number of transitions : 10447 Number of computed states : 10452 Total computation time : 2.852 seconds States/second in state space : 3662.1 (10448/2.852 seconds) Computed states/second : 3663.5 (10452/2.852 seconds) Estimated memory : 1.648 GiB (i.e., 221224083 words of size 8) ------------------------------------------------------------ ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm + parsing : 3.633 seconds main algorithm : 2.852 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing : 0.030 second model converting : 0.748 second model parsing and converting : 0.780 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 7103 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.069 second (10448 calls | 6.62643000324e-06 second/call) StateSpace.compute_predecessors : 0.000 second (0 call) StateSpace.counter_get_location : 0.009 second (39696 calls | 2.45619906096e-07 second/call) StateSpace.get_state : 0.030 second (39696 calls | 7.78235816418e-07 second/call) StateSpace.add_transition : 0.019 second (10447 calls | 1.81975884564e-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 | 0. second/call) StateSpace.nb_transitions : 0.000 second (1 call | 9.53674316407e-07 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): 1243 skipped actions : 1243 unsatisfiable constraints : 0 unsatisfiable global discrete constraints: 0 different combinations : 0 early unsat (D^g) : 0 next transitions : 0.052 second legal transitions exist : 0.507 second compute locations,guards,updates : 0.029 second StateBased.add_transition_to_state_space: 0.024 second (10447 calls | 2.36907780793e-06 second/call) StateBased.explore_layer_bfs : 2.851 seconds (1 call | 2.85198283196 second/call) StateBased.post_from_one_state : 2.747 seconds (10448 calls | 0.000263009191838 second/call) StateBased.process_post_n : 0.001 second (4597 calls | 2.85874093541e-07 second/call) StateBased.gcmajor : 0.001 second (4597 calls | 2.43916157824e-07 second/call) ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 3.664 seconds ------------------------------------------------------------