(************************************************************ * Result output by IMITATOR * Version : IMITATOR 2.10.4 "Butter Jellyfish" (build 2477) * Git : HEAD/5b53333 * Model : 'example2.imi' * Generated: Wed May 29, 2019 10:45:54 * Command : imitator example2.imi -mode EF -output-result ************************************************************) ------------------------------------------------------------ Number of IPTAs : 3 Number of clocks : 6 Has stopwatches? : true L/U subclass : L/U-PTA Number of parameters : 2 Number of discrete variables : 3 Number of actions : 9 Total number of locations : 13 Average locations per IPTA : 4.3 ------------------------------------------------------------ BEGIN CONSTRAINT BCETStep3 >= 0 & 2 >= WCETStep3 & WCETStep3 >= BCETStep3 END CONSTRAINT ------------------------------------------------------------ Constraint soundness : exact Termination : regular termination Constraint nature : good ------------------------------------------------------------ Number of states : 11 Number of transitions : 11 Number of computed states : 12 Total computation time : 0.019 second States/second in state space : 572.9 (11/0.019 second) Computed states/second : 625.0 (12/0.019 second) Estimated memory : 2.884 MiB (i.e., 378124 words of size 8) ------------------------------------------------------------ ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm + parsing : 0.038 second main algorithm : 0.019 second ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing and converting : 0.018 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 12 number of constraints comparisons : 5 number of new states <= old : 0 number of new states >= old : 0 StateSpace.merging attempts : 0 StateSpace.merges : 0 StatesMerging.merging attempts : 0 StatesMerging.merges : 0 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 0.038 second ------------------------------------------------------------