(************************************************************ * Result output by IMITATOR * Version : IMITATOR 2.11 "Butter Kouign-amann" (build 2550) * Git : HEAD/8c484cd * Model : 'bank.imi' * Generated: Tue Apr 14, 2020 12:06:04 * Command : ./imitator-v2.11-amd64 -mode EFunsafe -merge -incl2 -output-result bank.imi ************************************************************) ------------------------------------------------------------ Number of IPTAs : 4 Number of clocks : 7 Has stopwatches? : true L/U subclass : not L/U Number of parameters : 4 Number of discrete variables : 0 Number of actions : 11 Total number of locations : 23 Average locations per IPTA : 5.7 ------------------------------------------------------------ BEGIN CONSTRAINT 50 >= total_time & total_time >= 30 & total_dam >= 0 & lambda_Browser = total_dam & total_cost = 20 OR lambda_Browser >= 0 & total_cost = 40 & total_time = 90 & total_dam = 12 END CONSTRAINT ------------------------------------------------------------ Constraint soundness : exact Termination : regular termination Constraint nature : bad ------------------------------------------------------------ Number of states : 21 Number of transitions : 27 Number of computed states : 28 Total computation time : 0.019 second States/second in state space : 1100.7 (21/0.019 second) Computed states/second : 1467.7 (28/0.019 second) Estimated memory : 2.440 MiB (i.e., 319946 words of size 8) ------------------------------------------------------------ ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm + parsing : 0.021 second main algorithm : 0.019 second ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing and converting : 0.002 second ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 13 number of constraints comparisons : 7 number of new states <= old : 7 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.022 second ------------------------------------------------------------