************************************************************
 *  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-3-Reacts-no-param-with-switch.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 19 states.
 Computing post^6 from 37 states.
 Computing post^7 from 57 states.
 Computing post^8 from 73 states.
 Computing post^9 from 85 states.
 Computing post^10 from 87 states.
 Computing post^11 from 73 states.
 Computing post^12 from 52 states.
 Computing post^13 from 33 states.
 Computing post^14 from 16 states.
 Computing post^15 from 4 states.
 Computing post^16 from 4 states.
 Computing post^17 from 4 states.
 Computing post^18 from 4 states.
 Computing post^19 from 4 states.
 Computing post^20 from 4 states.
 Computing post^21 from 17 states.
 Computing post^22 from 22 states.
 Computing post^23 from 9 states.
 Computing post^24 from 9 states.
 Computing post^25 from 9 states.
 Computing post^26 from 9 states.
 Computing post^27 from 9 states.
 Computing post^28 from 27 states.
 Computing post^29 from 27 states.
 Computing post^30 from 9 states.
 Computing post^31 from 9 states.
 Computing post^32 from 9 states.
 Computing post^33 from 9 states.
 Computing post^34 from 9 states.
 Computing post^35 from 18 states.
 Computing post^36 from 9 states.
 Computing post^37 from 9 states.
 Computing post^38 from 9 states.
 Computing post^39 from 9 states.
 Computing post^40 from 9 states.
 Computing post^41 from 54 states.
 Computing post^42 from 141 states.
 Computing post^43 from 213 states.
 Computing post^44 from 198 states.
 Computing post^45 from 105 states.
 Computing post^46 from 24 states.
 Computing post^47 from 15 states.
 Computing post^48 from 15 states.
 Computing post^49 from 15 states.
 Computing post^50 from 15 states.
 Computing post^51 from 15 states.
 Computing post^52 from 45 states.
 Computing post^53 from 45 states.
 Computing post^54 from 15 states.
 Computing post^55 from 15 states.
 Computing post^56 from 15 states.
 Computing post^57 from 15 states.
 Computing post^58 from 15 states.
 Computing post^59 from 45 states.
 Computing post^60 from 45 states.
 Computing post^61 from 15 states.
 Computing post^62 from 15 states.
 Computing post^63 from 15 states.
 Computing post^64 from 15 states.
 Computing post^65 from 15 states.
 Computing post^66 from 30 states.
 Computing post^67 from 15 states.
 Computing post^68 from 15 states.
 Computing post^69 from 15 states.
 Computing post^70 from 15 states.
 Computing post^71 from 15 states.
 Computing post^72 from 84 states.
 Computing post^73 from 195 states.
 Computing post^74 from 255 states.
 Computing post^75 from 210 states.
 Computing post^76 from 105 states.
 Computing post^77 from 24 states.
 Computing post^78 from 15 states.
 Computing post^79 from 15 states.
 Computing post^80 from 15 states.
 Computing post^81 from 15 states.
 Computing post^82 from 15 states.
 Computing post^83 from 45 states.
 Computing post^84 from 45 states.
 Computing post^85 from 15 states.
 Computing post^86 from 15 states.
 Computing post^87 from 15 states.
 Computing post^88 from 15 states.
 Computing post^89 from 15 states.
 Computing post^90 from 45 states.
 Computing post^91 from 45 states.
 Computing post^92 from 15 states.
 Computing post^93 from 15 states.
 Computing post^94 from 15 states.
 Computing post^95 from 15 states.
 Computing post^96 from 15 states.
 Computing post^97 from 45 states.
 Computing post^98 from 60 states.
   14 states merged within 74 states.
 Computing post^99 from 60 states.
   8 states merged within 53 states.
 Computing post^100 from 45 states.
   5 states merged within 50 states.
 Computing post^101 from 45 states.
 Computing post^102 from 45 states.
   6 states merged within 120 states.
 Computing post^103 from 114 states.
 Computing post^104 from 383 states.
 Computing post^105 from 833 states.
 Computing post^106 from 1393 states.
 Computing post^107 from 1844 states.
 Computing post^108 from 1870 states.
 Computing post^109 from 1419 states.
 Computing post^110 from 779 states.
 Computing post^111 from 280 states.
 Computing post^112 from 55 states.
 Computing post^113 from 38 states.
 Computing post^114 from 22 states.
 Computing post^115 from 22 states.
 Computing post^116 from 21 states.
 Computing post^117 from 21 states.
 Computing post^118 from 58 states.
 Computing post^119 from 53 states.
 Computing post^120 from 16 states.
 Computing post^121 from 16 states.
 Computing post^122 from 16 states.
 Computing post^123 from 16 states.
 Computing post^124 from 16 states.
 Computing post^125 from 48 states.
 Computing post^126 from 48 states.
 Computing post^127 from 16 states.
 Computing post^128 from 16 states.
 Computing post^129 from 16 states.
 Computing post^130 from 16 states.
 Computing post^131 from 16 states.
 Computing post^132 from 32 states.
 Computing post^133 from 16 states.
 Computing post^134 from 16 states.
 Computing post^135 from 16 states.
 Computing post^136 from 16 states.
 Computing post^137 from 16 states.
 Computing post^138 from 86 states.
 Computing post^139 from 184 states.
 Computing post^140 from 212 states.
 Computing post^141 from 152 states.
 Computing post^142 from 70 states.
 Computing post^143 from 16 states.
 Computing post^144 from 10 states.
 Computing post^145 from 10 states.
 Computing post^146 from 10 states.
 Computing post^147 from 10 states.
 Computing post^148 from 10 states.
 Computing post^149 from 30 states.
 Computing post^150 from 30 states.
 Computing post^151 from 10 states.
 Computing post^152 from 10 states.
 Computing post^153 from 10 states.
 Computing post^154 from 10 states.
 Computing post^155 from 10 states.
 Computing post^156 from 30 states.
 Computing post^157 from 30 states.
 Computing post^158 from 10 states.
 Computing post^159 from 10 states.
 Computing post^160 from 10 states.
 Computing post^161 from 10 states.
 Computing post^162 from 10 states.
 Computing post^163 from 20 states.
 Computing post^164 from 10 states.
 Computing post^165 from 10 states.
 Computing post^166 from 10 states.
 Computing post^167 from 10 states.
 Computing post^168 from 10 states.
 Computing post^169 from 56 states.
 Computing post^170 from 130 states.
 Computing post^171 from 170 states.
 Computing post^172 from 140 states.
 Computing post^173 from 70 states.
 Computing post^174 from 16 states.
 Computing post^175 from 10 states.
 Computing post^176 from 10 states.
 Computing post^177 from 10 states.
 Computing post^178 from 10 states.
 Computing post^179 from 10 states.
 Computing post^180 from 30 states.
 Computing post^181 from 30 states.
 Computing post^182 from 10 states.
 Computing post^183 from 10 states.
 Computing post^184 from 10 states.
 Computing post^185 from 10 states.
 Computing post^186 from 10 states.
 Computing post^187 from 30 states.
 Computing post^188 from 30 states.
 Computing post^189 from 10 states.
 Computing post^190 from 10 states.
 Computing post^191 from 10 states.
 Computing post^192 from 10 states.
 Computing post^193 from 10 states.
 Computing post^194 from 30 states.
 Computing post^195 from 40 states.
   4 states merged within 44 states.
 Computing post^196 from 40 states.
   2 states merged within 32 states.
 Computing post^197 from 30 states.
   6 states merged within 36 states.
 Computing post^198 from 30 states.
 Computing post^199 from 30 states.
   7 states merged within 83 states.
 Computing post^200 from 76 states.
 Computing post^201 from 252 states.
 Computing post^202 from 530 states.
 Computing post^203 from 850 states.
 Computing post^204 from 1106 states.
 Computing post^205 from 1158 states.
 Computing post^206 from 954 states.
 Computing post^207 from 590 states.
 Computing post^208 from 250 states.
 Computing post^209 from 66 states.
 Computing post^210 from 36 states.
 Computing post^211 from 22 states.
 Computing post^212 from 22 states.
 Computing post^213 from 20 states.
 Computing post^214 from 20 states.
 Computing post^215 from 50 states.
 Computing post^216 from 40 states.
 Computing post^217 from 10 states.
 Computing post^218 from 10 states.
 Computing post^219 from 10 states.
 Computing post^220 from 10 states.
 Computing post^221 from 10 states.
 Computing post^222 from 20 states.
 Computing post^223 from 10 states.
 
 Fixpoint reached at a depth of 224: 21447 states with 70841 transitions in the final state space.
 
   [AGsafe] Algorithm completed after 476.466 seconds.
 
 Final constraint such that the system is correct:
 True
 This good constraint is exact (sound and complete)
 
 Result written to file 'GNC-3-Reacts-no-param-with-switch.res'.

 IMITATOR successfully terminated (after 476.473 seconds)