(************************************************************ * Result by: IMITATOR 3.1 "Cheese Artichoke" (build HEAD/ec224ec) * Model : 'PTPM/gear/gear-6000.imi' * Generated: Fri Jul 23, 2021 10:25:41 * Command : /root/imitator/bin/imitator PTPM/gear/gear-6000.imi PTPM/gear/gear-EFpmin.imiprop -output-prefix PTPM/gear/gear-6000-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 : 9003 Average locations per IPTA : 4501.5 Total number of transitions : 9009 Average transitions per IPTA : 4504.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 > 2737 & 25*tprime >= 13693 & 13697 > 25*tprime & 2738 >= 5*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 > 25961 & 25*tprime >= 26023 & 5206 > 5*tprime & 5204 >= 5*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 > 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 & 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 & 54064 > 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 25*t > 64279 & 25*tprime >= 64286 & 64291 > 25*tprime & 64283 >= 25*t & 25*p1 = 3 OR 25*t > 65613 & 25*tprime >= 65621 & 2625 > tprime & 65618 >= 25*t & 25*p1 = 3 OR 25*t > 66052 & 25*tprime >= 66064 & 66073 > 25*tprime & 66061 >= 25*t & 25*p1 = 3 OR 25*t > 68587 & 25*tprime >= 68596 & 68599 > 25*tprime & 68593 >= 25*t & 25*p1 = 3 OR 25*t > 78246 & 25*tprime >= 78254 & 78258 > 25*tprime & 78251 >= 25*t & 25*p1 = 3 OR 25*t > 79446 & 25*tprime >= 79453 & 79549 > 25*tprime & 3178 >= t & 25*p1 = 3 OR 25*t > 79714 & 25*tprime >= 79723 & 79726 > 25*tprime & 15944 >= 5*t & 25*p1 = 3 OR 25*t > 84611 & 5*tprime >= 16924 & 84623 > 25*tprime & 84617 >= 25*t & 25*p1 = 3 OR 25*t > 86963 & 25*tprime >= 87033 & 87042 > 25*tprime & 17406 >= 5*t & 25*p1 = 3 OR 5*t > 17789 & 25*tprime >= 88953 & 89036 > 25*tprime & 3558 >= t & 25*p1 = 3 OR 5*t > 17838 & 25*tprime >= 89198 & 89201 > 25*tprime & 17839 >= 5*t & 25*p1 = 3 OR 25*t > 89263 & 25*tprime >= 89272 & 3571 > tprime & 89269 >= 25*t & 25*p1 = 3 OR 25*t > 93829 & 25*tprime >= 93838 & 93841 > 25*tprime & 18767 >= 5*t & 25*p1 = 3 OR 5*t > 18892 & tprime >= 3781 & 94534 > 25*tprime & 94522 >= 25*t & 25*p1 = 3 OR t > 3781 & 25*tprime >= 94537 & 94546 > 25*tprime & 94534 >= 25*t & 25*p1 = 3 OR 25*t > 94537 & 25*tprime >= 94549 & 94567 > 25*tprime & 94546 >= 25*t & 25*p1 = 3 OR 25*t > 96463 & 5*tprime >= 19304 & 96529 > 25*tprime & 96517 >= 25*t & 25*p1 = 3 OR 25*t > 98689 & 25*tprime >= 98698 & 98701 > 25*tprime & 19739 >= 5*t & 25*p1 = 3 OR 5*t > 19806 & 25*tprime >= 99042 & 99051 > 25*tprime & 99039 >= 25*t & 25*p1 = 3 OR 25*t > 100963 & 25*tprime >= 101037 & 101046 > 25*tprime & 101034 >= 25*t & 25*p1 = 3 OR 25*t > 101578 & 25*tprime >= 101586 & 20318 > 5*tprime & 101583 >= 25*t & 25*p1 = 3 OR 25*t > 101663 & 25*tprime >= 101672 & 101676 > 25*tprime & 101669 >= 25*t & 25*p1 = 3 OR 25*t > 103291 & tprime >= 4132 & 103304 > 25*tprime & 103297 >= 25*t & 25*p1 = 3 OR 25*t > 103457 & 5*tprime >= 20707 & 103543 > 25*tprime & 103532 >= 25*t & 25*p1 = 3 OR 25*t > 103961 & 25*tprime >= 104024 & 104051 > 25*tprime & 104021 >= 25*t & 25*p1 = 3 OR 25*t > 108457 & 25*tprime >= 108529 & 108538 > 25*tprime & 108526 >= 25*t & 25*p1 = 3 OR 25*t > 108529 & 25*tprime >= 108541 & 108563 > 25*tprime & 108538 >= 25*t & 25*p1 = 3 OR 25*t > 108541 & 25*tprime >= 108566 & 4343 > tprime & 108563 >= 25*t & 25*p1 = 3 OR 25*t > 110463 & 25*tprime >= 110524 & 110533 > 25*tprime & 110521 >= 25*t & 25*p1 = 3 OR 25*t > 111163 & 25*tprime >= 111171 & 4447 > tprime & 111168 >= 25*t & 25*p1 = 3 OR 25*t > 111298 & 25*tprime >= 111306 & 22262 > 5*tprime & 111303 >= 25*t & 25*p1 = 3 OR 25*t > 115631 & 5*tprime >= 23128 & 115643 > 25*tprime & 115637 >= 25*t & 25*p1 = 3 OR 25*t > 117259 & 25*tprime >= 117268 & 117271 > 25*tprime & 23453 >= 5*t & 25*p1 = 3 OR 5*t > 23467 & 25*tprime >= 117341 & 117344 > 25*tprime & 117338 >= 25*t & 25*p1 = 3 OR 25*t > 120711 & 5*tprime >= 24144 & 120723 > 25*tprime & 120717 >= 25*t & 25*p1 = 3 OR 25*t > 120822 & 25*tprime >= 120829 & 120834 > 25*tprime & 120826 >= 25*t & 25*p1 = 3 OR 25*t > 120858 & 25*tprime >= 120866 & 24174 > 5*tprime & 120863 >= 25*t & 25*p1 = 3 OR 25*t > 122241 & tprime >= 4890 & 122253 > 25*tprime & 122247 >= 25*t & 25*p1 = 3 OR 5*t > 25364 & 25*tprime >= 126828 & 126831 > 25*tprime & 5073 >= t & 25*p1 = 3 OR 25*t > 127113 & 25*tprime >= 127122 & 5085 > tprime & 127119 >= 25*t & 25*p1 = 3 OR 25*t > 129462 & 25*tprime >= 129523 & 129532 > 25*tprime & 25904 >= 5*t & 25*p1 = 3 OR 25*t > 131679 & 25*tprime >= 131688 & 131691 > 25*tprime & 26337 >= 5*t & 25*p1 = 3 OR 5*t > 26392 & 5*tprime >= 26404 & 132029 > 25*tprime & 132017 >= 25*t & 25*p1 = 3 OR 25*t > 133963 & 25*tprime >= 134028 & 134037 > 25*tprime & 5361 >= t & 25*p1 = 3 OR 25*t > 134028 & 5*tprime >= 26808 & 134061 > 25*tprime & 134037 >= 25*t & 25*p1 = 3 OR 25*t > 134678 & 25*tprime >= 134687 & 26938 > 5*tprime & 134684 >= 25*t & 25*p1 = 3 OR 25*t > 141458 & 25*tprime >= 141532 & 141541 > 25*tprime & 141529 >= 25*t & 25*p1 = 3 OR 25*t > 141532 & 25*tprime >= 141544 & 141553 > 25*tprime & 141541 >= 25*t & 25*p1 = 3 OR 25*t > 143463 & 5*tprime >= 28703 & 143524 > 25*tprime & 143512 >= 25*t & 25*p1 = 3 OR 5*t > 28703 & 25*tprime >= 143527 & 143536 > 25*tprime & 143524 >= 25*t & 25*p1 = 3 OR 25*t > 143552 & 25*tprime >= 143564 & 143573 > 25*tprime & 143561 >= 25*t & 25*p1 = 3 OR 25*t > 144264 & 25*tprime >= 144272 & 144276 > 25*tprime & 144269 >= 25*t & 25*p1 = 3 OR 5*t > 29139 & 5*tprime >= 29141 & 145708 > 25*tprime & 145702 >= 25*t & 25*p1 = 3 END CONSTRAINT ------------------------------------------------------------ Constraint soundness : exact Termination : regular termination Constraint nature : good ------------------------------------------------------------ Number of states : 20603 Number of transitions : 20602 Number of computed states : 23007 Total computation time : 9.978 seconds States/second in state space : 2064.7 (20603/9.978 seconds) Computed states/second : 2305.7 (23007/9.978 seconds) Estimated memory : 6.092 GiB (i.e., 817785584 words of size 8) ------------------------------------------------------------ ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm + parsing : 23.061 seconds main algorithm : 9.978 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing and converting : 13.082 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 : 23.132 seconds ------------------------------------------------------------