(************************************************************ * Result by: IMITATOR 3.1 "Cheese Artichoke" (build HEAD/ec224ec) * Model : 'PTPM/gear/gear-7000.imi' * Generated: Fri Jul 23, 2021 10:25:24 * Command : /root/imitator/bin/imitator PTPM/gear/gear-7000.imi PTPM/gear/gear-EFpmin.imiprop -output-prefix PTPM/gear/gear-7000-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 : 10323 Average locations per IPTA : 5161.5 Total number of transitions : 10329 Average transitions per IPTA : 5164.5 ------------------------------------------------------------ BEGIN CONSTRAINT 25*t > 4308 & 25*tprime >= 4316 & 864 > 5*tprime & 4313 >= 25*t & 25*p1 = 3 OR 25*t > 7049 & 5*tprime >= 1412 & 7069 > 25*tprime & 7057 >= 25*t & 25*p1 = 3 OR 25*t > 9167 & 25*tprime >= 9176 & 9179 > 25*tprime & 9173 >= 25*t & 25*p1 = 3 OR 5*t > 1892 & 25*tprime >= 9521 & 1906 > 5*tprime & 9518 >= 25*t & 25*p1 = 3 OR 25*t > 13758 & 25*tprime >= 13767 & 2754 > 5*tprime & 13764 >= 25*t & 25*p1 = 3 OR 25*t > 17236 & 25*tprime >= 17242 & 17248 > 25*tprime & 17239 >= 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 > 23562 & 25*tprime >= 23574 & 23583 > 25*tprime & 23571 >= 25*t & 25*p1 = 3 OR 25*t > 25961 & 25*tprime >= 26023 & 5206 > 5*tprime & 5204 >= 5*t & 25*p1 = 3 OR 25*t > 28458 & 25*tprime >= 28532 & 28541 > 25*tprime & 28529 >= 25*t & 25*p1 = 3 OR 5*t > 6238 & 25*tprime >= 31198 & 31202 > 25*tprime & 6239 >= 5*t & 25*p1 = 3 OR 25*t > 31337 & 5*tprime >= 6269 & 31349 > 25*tprime & 31342 >= 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 25*t > 35621 & 5*tprime >= 7126 & 35633 > 25*tprime & 35627 >= 25*t & 25*p1 = 3 OR 25*t > 37298 & 25*tprime >= 37307 & 7462 > 5*tprime & 37304 >= 25*t & 25*p1 = 3 OR 25*t > 42109 & 25*tprime >= 42118 & 42121 > 25*tprime & 8423 >= 5*t & 25*p1 = 3 OR 25*t > 46724 & 25*tprime >= 46733 & 46736 > 25*tprime & 9346 >= 5*t & 25*p1 = 3 OR 25*t > 49462 & 25*tprime >= 49514 & 49521 > 25*tprime & 49511 >= 25*t & 25*p1 = 3 OR 25*t > 51437 & 25*tprime >= 51446 & 51449 > 25*tprime & 51443 >= 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 & 54063 > 25*tprime & 54052 >= 25*t & 25*p1 = 3 OR t > 2246 & 25*tprime >= 56159 & 56162 > 25*tprime & 56156 >= 25*t & 25*p1 = 3 OR 5*t > 11308 & 25*tprime >= 56552 & 56561 > 25*tprime & 56549 >= 25*t & 25*p1 = 3 OR t > 2364 & 25*tprime >= 59109 & 59112 > 25*tprime & 59106 >= 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 > 64168 & 25*tprime >= 64177 & 12836 > 5*tprime & 64174 >= 25*t & 25*p1 = 3 OR 25*t > 65698 & 25*tprime >= 65707 & 13142 > 5*tprime & 65704 >= 25*t & 25*p1 = 3 OR 25*t > 68587 & 25*tprime >= 68596 & 68599 > 25*tprime & 68593 >= 25*t & 25*p1 = 3 OR 25*t > 68663 & 25*tprime >= 68669 & 68673 > 25*tprime & 68666 >= 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 > 84318 & 25*tprime >= 84326 & 16866 > 5*tprime & 84323 >= 25*t & 25*p1 = 3 OR 5*t > 16883 & 25*tprime >= 84424 & 84427 > 25*tprime & 84421 >= 25*t & 25*p1 = 3 OR 5*t > 17789 & 25*tprime >= 88953 & 89073 > 25*tprime & 3558 >= t & 25*p1 = 3 OR 25*t > 89238 & 25*tprime >= 89247 & 3570 > tprime & 89244 >= 25*t & 25*p1 = 3 OR 25*t > 93707 & 5*tprime >= 18743 & 93719 > 25*tprime & 93712 >= 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 & 94564 > 25*tprime & 94546 >= 25*t & 25*p1 = 3 OR 25*t > 96463 & 5*tprime >= 19304 & 96541 > 25*tprime & 96517 >= 25*t & 25*p1 = 3 OR 25*t > 97184 & 25*tprime >= 97191 & 97196 > 25*tprime & 97188 >= 25*t & 25*p1 = 3 OR 5*t > 19723 & 25*tprime >= 98624 & 98627 > 25*tprime & 98621 >= 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 > 101638 & 25*tprime >= 101648 & 101651 > 25*tprime & 20329 >= 5*t & 25*p1 = 3 OR 25*t > 103279 & 25*tprime >= 103288 & 103291 > 25*tprime & 20657 >= 5*t & 25*p1 = 3 OR 25*t > 103961 & 25*tprime >= 104024 & 104052 > 25*tprime & 104021 >= 25*t & 25*p1 = 3 OR 25*t > 108457 & 25*tprime >= 108529 & 108563 > 25*tprime & 108526 >= 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 > 117259 & 25*tprime >= 117268 & 117271 > 25*tprime & 23453 >= 5*t & 25*p1 = 3 OR 25*t > 117406 & 5*tprime >= 23483 & 117418 > 25*tprime & 117412 >= 25*t & 25*p1 = 3 OR 25*t > 120589 & 25*tprime >= 120597 & 120601 > 25*tprime & 120594 >= 25*t & 25*p1 = 3 OR 25*t > 120628 & 25*tprime >= 120634 & 120637 > 25*tprime & 120631 >= 25*t & 25*p1 = 3 OR 25*t > 126808 & 25*tprime >= 126816 & 25364 > 5*tprime & 126813 >= 25*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 & 132041 > 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 & 134067 > 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 > 136257 & 25*tprime >= 136266 & 136269 > 25*tprime & 136263 >= 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 5*t > 28887 & 25*tprime >= 144443 & 144447 > 25*tprime & 28888 >= 5*t & 25*p1 = 3 OR 5*t > 29149 & 25*tprime >= 145753 & 145756 > 25*tprime & 5830 >= t & 25*p1 = 3 OR 25*t > 145793 & 25*tprime >= 145802 & 145806 > 25*tprime & 145799 >= 25*t & 25*p1 = 3 OR 25*t > 153052 & 25*tprime >= 153063 & 153072 > 25*tprime & 30612 >= 5*t & 25*p1 = 3 OR 25*t > 153063 & tprime >= 6123 & 153084 > 25*tprime & 153072 >= 25*t & 25*p1 = 3 OR 25*t > 153702 & 5*tprime >= 30742 & 153714 > 25*tprime & 153707 >= 25*t & 25*p1 = 3 OR 25*t > 159822 & 25*tprime >= 159831 & 159834 > 25*tprime & 159828 >= 25*t & 25*p1 = 3 OR 25*t > 169248 & 25*tprime >= 169257 & 33852 > 5*tprime & 169254 >= 25*t & 25*p1 = 3 OR 5*t > 34907 & 25*tprime >= 174547 & 174556 > 25*tprime & 174544 >= 25*t & 25*p1 = 3 END CONSTRAINT ------------------------------------------------------------ Constraint soundness : exact Termination : regular termination Constraint nature : good ------------------------------------------------------------ Number of states : 23629 Number of transitions : 23628 Number of computed states : 26409 Total computation time : 13.665 seconds States/second in state space : 1729.1 (23629/13.665 seconds) Computed states/second : 1932.5 (26409/13.665 seconds) Estimated memory : 7.899 GiB (i.e., 1060278493 words of size 8) ------------------------------------------------------------ ------------------------------------------------------------ Statistics: Algorithm counters ------------------------------------------------------------ main algorithm + parsing : 31.673 seconds main algorithm : 13.665 seconds ------------------------------------------------------------ Statistics: Parsing counters ------------------------------------------------------------ model parsing and converting : 18.007 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 : 31.884 seconds ------------------------------------------------------------