(************************************************************ * Result by: IMITATOR 3.1 "Cheese Artichoke" (build HEAD/ec224ec) * Model : 'PTPM/gear/gear-3000.imi' * Generated: Fri Jul 23, 2021 10:25:22 * Command : /root/imitator/bin/imitator PTPM/gear/gear-3000.imi PTPM/gear/gear-EFpmin.imiprop -output-prefix PTPM/gear/gear-3000-EFpmin -no-cumulative-pruning ************************************************************) ------------------------------------------------------------ Number of IPTAs : 2 Number of clocks : 2 Has invariants? : true Has clocks with rate <>1? : false L/U subclass : not L/U Bounded parameters? : false Has silent actions? : true Is strongly deterministic? : true Number of parameters : 3 Number of discrete variables : 0 Number of actions : 7 Total number of locations : 4603 Average locations per IPTA : 2301.5 Total number of transitions : 4609 Average transitions per IPTA : 2304.5 ------------------------------------------------------------ BEGIN CONSTRAINT 25*t > 4308 & 25*tprime >= 4316 & 864 > 5*tprime & 4313 >= 25*t & 25*p1 = 3 OR 25*t > 9459 & 25*tprime >= 9533 & 9542 > 25*tprime & 1906 >= 5*t & 25*p1 = 3 OR 5*t > 1914 & 25*tprime >= 9582 & 9591 > 25*tprime & 9579 >= 25*t & 25*p1 = 3 OR 25*t > 13636 & 25*tprime >= 13644 & 13648 > 25*tprime & 13641 >= 25*t & 25*p1 = 3 OR 5*t > 2732 & 25*tprime >= 13669 & 13672 > 25*tprime & 13666 >= 25*t & 25*p1 = 3 OR 25*t > 13721 & 5*tprime >= 2746 & 13733 > 25*tprime & 13727 >= 25*t & 25*p1 = 3 OR 25*t > 18958 & 25*tprime >= 19032 & 19041 > 25*tprime & 19029 >= 25*t & 25*p1 = 3 OR 25*t > 19057 & 25*tprime >= 19069 & 19078 > 25*tprime & 19066 >= 25*t & 25*p1 = 3 OR 25*t > 20963 & 5*tprime >= 4208 & 21049 > 25*tprime & 21037 >= 25*t & 25*p1 = 3 OR 5*t > 4208 & 25*tprime >= 21052 & 21061 > 25*tprime & 21049 >= 25*t & 25*p1 = 3 OR 25*t > 21936 & 25*tprime >= 21943 & 21948 > 25*tprime & 4388 >= 5*t & 25*p1 = 3 OR 25*t > 23562 & 25*tprime >= 23574 & 23583 > 25*tprime & 23571 >= 25*t & 25*p1 = 3 OR 5*t > 6238 & 25*tprime >= 31198 & 31202 > 25*tprime & 6239 >= 5*t & 25*p1 = 3 OR 25*t > 31349 & 25*tprime >= 31357 & 31362 > 25*tprime & 31354 >= 25*t & 25*p1 = 3 OR 25*t > 33049 & 25*tprime >= 33061 & 6614 > 5*tprime & 33058 >= 25*t & 25*p1 = 3 OR 25*t > 33061 & 25*tprime >= 33073 & 33082 > 25*tprime & 6614 >= 5*t & 25*p1 = 3 OR 5*t > 7462 & 25*tprime >= 37319 & 37322 > 25*tprime & 37316 >= 25*t & 25*p1 = 3 OR 25*t > 42158 & 25*tprime >= 42167 & 8434 > 5*tprime & 42164 >= 25*t & 25*p1 = 3 OR 25*t > 46954 & 25*tprime >= 47029 & 47037 > 25*tprime & 47026 >= 25*t & 25*p1 = 3 OR 25*t > 51633 & 25*tprime >= 51642 & 10329 > 5*tprime & 51639 >= 25*t & 25*p1 = 3 OR 5*t > 10392 & 25*tprime >= 52023 & 52032 > 25*tprime & 10404 >= 5*t & 25*p1 = 3 OR 25*t > 52023 & 5*tprime >= 10407 & 52044 > 25*tprime & 52032 >= 25*t & 25*p1 = 3 OR 5*t > 10407 & 25*tprime >= 52047 & 52056 > 25*tprime & 52044 >= 25*t & 25*p1 = 3 OR 25*t > 52047 & 25*tprime >= 52059 & 52069 > 25*tprime & 52056 >= 25*t & 25*p1 = 3 OR 25*t > 53963 & 5*tprime >= 10811 & 54063 > 25*tprime & 54052 >= 25*t & 25*p1 = 3 OR 25*t > 56162 & 25*tprime >= 56171 & 56174 > 25*tprime & 56168 >= 25*t & 25*p1 = 3 OR 5*t > 11308 & 25*tprime >= 56552 & 56561 > 25*tprime & 56549 >= 25*t & 25*p1 = 3 OR 25*t > 59112 & 25*tprime >= 59121 & 59124 > 25*tprime & 59118 >= 25*t & 25*p1 = 3 OR 25*t > 60839 & 25*tprime >= 60847 & 60851 > 25*tprime & 60844 >= 25*t & 25*p1 = 3 OR 25*t > 61132 & 25*tprime >= 61141 & 61144 > 25*tprime & 61138 >= 25*t & 25*p1 = 3 OR 25*t > 61458 & 25*tprime >= 61522 & 61531 > 25*tprime & 61519 >= 25*t & 25*p1 = 3 OR 5*t > 12706 & 25*tprime >= 63542 & 63551 > 25*tprime & 63539 >= 25*t & 25*p1 = 3 OR 5*t > 13142 & 25*tprime >= 65719 & 65722 > 25*tprime & 65716 >= 25*t & 25*p1 = 3 OR 25*t > 68587 & 25*tprime >= 68596 & 68599 > 25*tprime & 68593 >= 25*t & 25*p1 = 3 END CONSTRAINT ------------------------------------------------------------ Constraint soundness : exact Termination : regular termination Constraint nature : good ------------------------------------------------------------ Number of states : 10554 Number of transitions : 10553 Number of computed states : 11801 Total computation time : 5.913 seconds States/second in state space : 1784.7 (10554/5.913 seconds) Computed states/second : 1995.5 (11801/5.913 seconds) Estimated memory : 1.757 GiB (i.e., 235887087 words of size 8) ------------------------------------------------------------ ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm + parsing : 8.800 seconds main algorithm : 5.913 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing and converting : 2.886 seconds ------------------------------------------------------------ Statistics: State computation counters ------------------------------------------------------------ number of state comparisons : 0 number of constraints comparisons : 0 number of new states <= old : 0 number of new states >= old : 0 StateSpace.merging attempts : 0 StateSpace.merges : 0 ------------------------------------------------------------ Statistics: Graphics-related counters ------------------------------------------------------------ state space drawing : 0.000 second ------------------------------------------------------------ Statistics: Global counter ------------------------------------------------------------ total : 8.819 seconds ------------------------------------------------------------