************************************************************
 *  IMITATOR 2.10.4 "Butter Jellyfish"                      *
 *                                                          *
 *                                    Etienne Andre et al.  *
 *                                             2009 - 2018  *
 *                       LSV, ENS de Cachan & CNRS, France  *
 *                       LIPN, Universite Paris 13, France  *
 *                                         www.imitator.fr  *
 *                                                          *
 *                   Build: 2477 (2018-07-02 09:42:27 UTC)  *
 *                                            HEAD/5b53333  *
 ************************************************************
 Model: GNC-ReacNM-param-offset.imi
 Mode: EF-synthesis.
 Considering fixpoint variant with monodirectional inclusion of symbolic zones (instead of equality).
 Merging technique of [AFS13] enabled.
 The result will be written to a file.
 The model contains stopwatches.
 Starting running algorithm AGsafe…
 
 Computing post^1 from 1 state.
 Computing post^2 from 1 state.
 Computing post^3 from 4 states.
 Computing post^4 from 9 states.
 Computing post^5 from 17 states.
 Computing post^6 from 29 states.
 Computing post^7 from 41 states.
 Computing post^8 from 49 states.
 Computing post^9 from 53 states.
   4 states merged within 55 states.
 Computing post^10 from 51 states.
   5 states merged within 46 states.
 Computing post^11 from 41 states.
   [AGsafe] Found a new state violating the property.
   7 states merged within 38 states.
 Computing post^12 from 31 states.
   1 state merged within 33 states.
 Computing post^13 from 32 states.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   16 states merged within 52 states.
 Computing post^14 from 36 states.
   7 states merged within 54 states.
 Computing post^15 from 47 states.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   14 states merged within 82 states.
 Computing post^16 from 68 states.
   10 states merged within 97 states.
 Computing post^17 from 87 states.
   29 states merged within 135 states.
 Computing post^18 from 106 states.
   35 states merged within 137 states.
 Computing post^19 from 102 states.
   23 states merged within 151 states.
 Computing post^20 from 128 states.
   24 states merged within 231 states.
 Computing post^21 from 207 states.
   43 states merged within 356 states.
 Computing post^22 from 313 states.
   46 states merged within 477 states.
 Computing post^23 from 431 states.
   125 states merged within 524 states.
 Computing post^24 from 399 states.
   48 states merged within 312 states.
 Computing post^25 from 264 states.
   76 states merged within 363 states.
 Computing post^26 from 287 states.
   69 states merged within 391 states.
 Computing post^27 from 322 states.
   131 states merged within 562 states.
 Computing post^28 from 431 states.
   136 states merged within 529 states.
 Computing post^29 from 393 states.
   101 states merged within 516 states.
 Computing post^30 from 415 states.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   77 states merged within 506 states.
 Computing post^31 from 431 states.
   55 states merged within 577 states.
 Computing post^32 from 525 states.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   111 states merged within 671 states.
 Computing post^33 from 563 states.
   109 states merged within 566 states.
 Computing post^34 from 457 states.
   121 states merged within 717 states.
 Computing post^35 from 596 states.
   37 states merged within 900 states.
 Computing post^36 from 863 states.
   21 states merged within 1062 states.
 Computing post^37 from 1041 states.
   10 states merged within 873 states.
 Computing post^38 from 863 states.
   7 states merged within 436 states.
 Computing post^39 from 429 states.
   3 states merged within 104 states.
 Computing post^40 from 101 states.
   4 states merged within 110 states.
 Computing post^41 from 106 states.
   5 states merged within 111 states.
 Computing post^42 from 106 states.
   7 states merged within 199 states.
 Computing post^43 from 192 states.
   10 states merged within 111 states.
 Computing post^44 from 101 states.
   5 states merged within 106 states.
 Computing post^45 from 101 states.
   3 states merged within 119 states.
 Computing post^46 from 116 states.
   5 states merged within 151 states.
 Computing post^47 from 146 states.
 Computing post^48 from 434 states.
   22 states merged within 719 states.
 Computing post^49 from 697 states.
   7 states merged within 684 states.
 Computing post^50 from 677 states.
   87 states merged within 567 states.
 Computing post^51 from 480 states.
   9 states merged within 297 states.
 Computing post^52 from 288 states.
   8 states merged within 205 states.
 Computing post^53 from 197 states.
 Computing post^54 from 111 states.
   8 states merged within 210 states.
 Computing post^55 from 202 states.
   4 states merged within 115 states.
 Computing post^56 from 111 states.
   5 states merged within 116 states.
 Computing post^57 from 111 states.
   5 states merged within 134 states.
 Computing post^58 from 129 states.
 Computing post^59 from 176 states.
   8 states merged within 601 states.
 Computing post^60 from 593 states.
   24 states merged within 1128 states.
 Computing post^61 from 1104 states.
   9 states merged within 1315 states.
 Computing post^62 from 1306 states.
   11 states merged within 1043 states.
 Computing post^63 from 1032 states.
   10 states merged within 512 states.
 Computing post^64 from 502 states.
 Computing post^65 from 122 states.
   7 states merged within 134 states.
 Computing post^66 from 127 states.
   5 states merged within 132 states.
 Computing post^67 from 127 states.
   4 states merged within 239 states.
 Computing post^68 from 235 states.
   9 states merged within 132 states.
 Computing post^69 from 123 states.
   5 states merged within 128 states.
 Computing post^70 from 123 states.
   2 states merged within 140 states.
 Computing post^71 from 138 states.
   5 states merged within 173 states.
 Computing post^72 from 168 states.
   8 states merged within 530 states.
 Computing post^73 from 522 states.
   16 states merged within 867 states.
 Computing post^74 from 851 states.
   17 states merged within 848 states.
 Computing post^75 from 831 states.
   91 states merged within 681 states.
 Computing post^76 from 590 states.
   10 states merged within 364 states.
 Computing post^77 from 354 states.
   3 states merged within 244 states.
 Computing post^78 from 241 states.
 Computing post^79 from 133 states.
   8 states merged within 254 states.
 Computing post^80 from 246 states.
   3 states merged within 136 states.
 Computing post^81 from 133 states.
   5 states merged within 138 states.
 Computing post^82 from 133 states.
   3 states merged within 154 states.
 Computing post^83 from 151 states.
 Computing post^84 from 198 states.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   [AGsafe] Found a new state violating the property.
   14 states merged within 335 states.
 Computing post^85 from 325 states.
   14 states merged within 246 states.
 Computing post^86 from 232 states.
   26 states merged within 386 states.
 Computing post^87 from 360 states.
   2 states merged within 646 states.
 Computing post^88 from 644 states.
 Computing post^89 from 1000 states.
 Computing post^90 from 1212 states.
 Computing post^91 from 1140 states.
 Computing post^92 from 812 states.
 Computing post^93 from 412 states.
 Computing post^94 from 132 states.
 Computing post^95 from 20 states.
 Computing post^96 from 20 states.
 Computing post^97 from 20 states.
 Computing post^98 from 40 states.
 Computing post^99 from 20 states.
 Computing post^100 from 20 states.
 Computing post^101 from 20 states.
 Computing post^102 from 20 states.
   5 states merged within 80 states.
 Computing post^103 from 80 states.
   21 states merged within 140 states.
 Computing post^104 from 140 states.
   33 states merged within 140 states.
 Computing post^105 from 140 states.
   36 states merged within 107 states.
 Computing post^106 from 94 states.
   6 states merged within 48 states.
 Computing post^107 from 48 states.
 Computing post^108 from 28 states.
 Computing post^109 from 14 states.
 Computing post^110 from 28 states.
 Computing post^111 from 14 states.
 Computing post^112 from 14 states.
 Computing post^113 from 14 states.
 Computing post^114 from 14 states.
 Computing post^115 from 32 states.
 Computing post^116 from 48 states.
 Computing post^117 from 32 states.
 Computing post^118 from 8 states.
 
 Fixpoint reached at a depth of 119: 34645 states with 83797 transitions in the final state space.
 
   [AGsafe] Algorithm completed after 955.663 seconds.
 
 Final constraint such that the system is correct:
  11 >= offsetT2
 & offsetT3 >= 0
 & offsetT2 >= 0
 & 1 >= offsetT3
 & offsetT1 = 0
 OR
   11 >= offsetT3
 & offsetT3 > 1
 & offsetT2 > 0
 & 1 >= offsetT2
 & offsetT1 = 0
 OR
   11 >= offsetT2
 & offsetT1 > 0
 & offsetT2 >= 0
 & 4 >= offsetT1
 & offsetT3 = 0
 OR
   offsetT1 >= 0
 & 11 >= offsetT3
 & offsetT3 > 1 + offsetT1
 & 4 >= offsetT1
 & offsetT2 = 0
 OR
   offsetT1 + 1 >= offsetT3
 & offsetT1 > 0
 & offsetT3 > 0
 & 4 >= offsetT1
 & offsetT2 = 0
 This good constraint is exact (sound and complete)
 
 Result written to file 'GNC-ReacNM-param-offset.res'.

 IMITATOR successfully terminated (after 958.920 seconds)