************************************************************
    *  IMITATOR 2.9.2-working "Butter Incaberry"               *
    *                                                          *
    *                     Etienne Andre, Ulrich Kuehne et al.  *
    *                                             2009 - 2017  *
    *                       LSV, ENS de Cachan & CNRS, France  *
    *                       LIPN, Universite Paris 13, France  *
    *                                         www.imitator.fr  *
    *                                                          *
    *                   Build: 2363 (2017-06-08 17:40:33 UTC)  *
    *                                       explorder/5c40e39  *
    ************************************************************
    Analysis time: Sun Jun 18, 2017 14:19:25
    
    Model: /media/gia/Data/Example-Models/Sched2.100.2/Sched2.100.2.imi
    Mode: EF-synthesis.
    Exploration order: layer-based BFS.
    Considering fixpoint variant with monodirectional inclusion of symbolic zones (instead of equality).
    The cartography will be drawn.
    The result will be written to a file.
    The trace set(s) will be generated in a graphical mode.
    Description of states will be output.
    This model is a U-PTA.
    
    Abstract model built after 0.009 second.
    Memory for abstract model: 979.484 KiB (i.e., 250748 words)
    
    Starting running algorithm AGsafe…
    
    Computing post^1 from 1 state.
    Computing post^2 from 1 state.
      [AGsafe] Found a new state violating the property.
    Computing post^3 from 2 states.
    Computing post^4 from 3 states.
    Computing post^5 from 3 states.
    Computing post^6 from 4 states.
      [AGsafe] Found a new state violating the property.
      [AGsafe] Found a new state violating the property.
    Computing post^7 from 5 states.
    Computing post^8 from 6 states.
    Computing post^9 from 6 states.
      [AGsafe] Found a new state violating the property.
      [AGsafe] Found a new state violating the property.
    Computing post^10 from 6 states.
      [AGsafe] Found a new state violating the property.
    Computing post^11 from 15 states.
    Computing post^12 from 20 states.
      [AGsafe] Found a new state violating the property.
    Computing post^13 from 9 states.
    Computing post^14 from 6 states.
    Computing post^15 from 9 states.
    Computing post^16 from 8 states.
    Computing post^17 from 8 states.
    Computing post^18 from 17 states.
    Computing post^19 from 34 states.
    Computing post^20 from 22 states.
    Computing post^21 from 16 states.
    Computing post^22 from 12 states.
    Computing post^23 from 14 states.
    Computing post^24 from 7 states.
    Computing post^25 from 7 states.
    Computing post^26 from 11 states.
    Computing post^27 from 11 states.
    Computing post^28 from 8 states.
    Computing post^29 from 21 states.
    Computing post^30 from 18 states.
    Computing post^31 from 15 states.
    Computing post^32 from 4 states.
    Computing post^33 from 4 states.
    Computing post^34 from 4 states.
    Computing post^35 from 8 states.
    Computing post^36 from 6 states.
    Computing post^37 from 8 states.
    Computing post^38 from 7 states.
    Computing post^39 from 6 states.
    Computing post^40 from 8 states.
    Computing post^41 from 8 states.
    Computing post^42 from 10 states.
    Computing post^43 from 8 states.
    Computing post^44 from 7 states.
      [AGsafe] Found a new state violating the property.
      [AGsafe] Found a new state violating the property.
    Computing post^45 from 5 states.
    Computing post^46 from 5 states.
    Computing post^47 from 5 states.
    Computing post^48 from 5 states.
    Computing post^49 from 10 states.
    Computing post^50 from 10 states.
    Computing post^51 from 9 states.
    Computing post^52 from 14 states.
    Computing post^53 from 11 states.
    Computing post^54 from 5 states.
    Computing post^55 from 5 states.
    Computing post^56 from 5 states.
    Computing post^57 from 8 states.
    Computing post^58 from 7 states.
    Computing post^59 from 7 states.
    Computing post^60 from 6 states.
    Computing post^61 from 6 states.
    Computing post^62 from 9 states.
    Computing post^63 from 9 states.
    Computing post^64 from 8 states.
    Computing post^65 from 6 states.
    Computing post^66 from 5 states.
      [AGsafe] Found a new state violating the property.
    Computing post^67 from 8 states.
    Computing post^68 from 8 states.
    Computing post^69 from 8 states.
    Computing post^70 from 8 states.
    Computing post^71 from 15 states.
    Computing post^72 from 13 states.
    Computing post^73 from 11 states.
    Computing post^74 from 15 states.
    Computing post^75 from 12 states.
    Computing post^76 from 6 states.
    Computing post^77 from 5 states.
    Computing post^78 from 5 states.
    Computing post^79 from 7 states.
    Computing post^80 from 6 states.
    Computing post^81 from 5 states.
    Computing post^82 from 5 states.
    Computing post^83 from 5 states.
    Computing post^84 from 7 states.
    Computing post^85 from 7 states.
    Computing post^86 from 9 states.
    Computing post^87 from 9 states.
    Computing post^88 from 7 states.
      [AGsafe] Found a new state violating the property.
    Computing post^89 from 11 states.
    Computing post^90 from 11 states.
    Computing post^91 from 11 states.
    Computing post^92 from 11 states.
    Computing post^93 from 19 states.
    Computing post^94 from 16 states.
    Computing post^95 from 13 states.
    Computing post^96 from 19 states.
    Computing post^97 from 17 states.
    Computing post^98 from 9 states.
    Computing post^99 from 7 states.
    Computing post^100 from 7 states.
    Computing post^101 from 11 states.
    Computing post^102 from 9 states.
    Computing post^103 from 9 states.
    Computing post^104 from 8 states.
    Computing post^105 from 7 states.
    Computing post^106 from 10 states.
    Computing post^107 from 9 states.
    Computing post^108 from 12 states.
    Computing post^109 from 13 states.
    Computing post^110 from 7 states.
      [AGsafe] Found a new state violating the property.
    Computing post^111 from 10 states.
    Computing post^112 from 10 states.
    Computing post^113 from 10 states.
    Computing post^114 from 10 states.
    Computing post^115 from 18 states.
    Computing post^116 from 15 states.
    Computing post^117 from 15 states.
    Computing post^118 from 23 states.
    Computing post^119 from 20 states.
    Computing post^120 from 11 states.
    Computing post^121 from 8 states.
    Computing post^122 from 7 states.
    Computing post^123 from 9 states.
    Computing post^124 from 8 states.
    Computing post^125 from 8 states.
    Computing post^126 from 7 states.
    Computing post^127 from 7 states.
    Computing post^128 from 10 states.
    Computing post^129 from 9 states.
    Computing post^130 from 12 states.
    Computing post^131 from 16 states.
    Computing post^132 from 14 states.
      [AGsafe] Found a new state violating the property.
    Computing post^133 from 15 states.
    Computing post^134 from 14 states.
    Computing post^135 from 14 states.
    Computing post^136 from 14 states.
    Computing post^137 from 23 states.
    Computing post^138 from 17 states.
    Computing post^139 from 16 states.
    Computing post^140 from 27 states.
    Computing post^141 from 25 states.
    Computing post^142 from 13 states.
    Computing post^143 from 9 states.
    Computing post^144 from 9 states.
    Computing post^145 from 12 states.
    Computing post^146 from 10 states.
    Computing post^147 from 9 states.
    Computing post^148 from 9 states.
    Computing post^149 from 9 states.
    Computing post^150 from 13 states.
    Computing post^151 from 13 states.
    Computing post^152 from 19 states.
    Computing post^153 from 19 states.
    Computing post^154 from 14 states.
      [AGsafe] Found a new state violating the property.
    Computing post^155 from 16 states.
    Computing post^156 from 16 states.
    Computing post^157 from 14 states.
    Computing post^158 from 14 states.
    Computing post^159 from 23 states.
    Computing post^160 from 19 states.
    Computing post^161 from 16 states.
    Computing post^162 from 27 states.
    Computing post^163 from 25 states.
    Computing post^164 from 13 states.
    Computing post^165 from 12 states.
    Computing post^166 from 9 states.
    Computing post^167 from 14 states.
    Computing post^168 from 11 states.
    Computing post^169 from 9 states.
    Computing post^170 from 9 states.
    Computing post^171 from 9 states.
    Computing post^172 from 13 states.
    Computing post^173 from 12 states.
    Computing post^174 from 15 states.
    Computing post^175 from 17 states.
    Computing post^176 from 10 states.
    Computing post^177 from 12 states.
    Computing post^178 from 12 states.
    Computing post^179 from 12 states.
    Computing post^180 from 12 states.
    Computing post^181 from 22 states.
    Computing post^182 from 17 states.
    Computing post^183 from 16 states.
    Computing post^184 from 24 states.
    Computing post^185 from 22 states.
    Computing post^186 from 13 states.
    Computing post^187 from 6 states.
    Computing post^188 from 6 states.
    Computing post^189 from 11 states.
    Computing post^190 from 9 states.
    Computing post^191 from 6 states.
    Computing post^192 from 6 states.
    Computing post^193 from 6 states.
    Computing post^194 from 9 states.
    Computing post^195 from 9 states.
    Computing post^196 from 11 states.
    Computing post^197 from 16 states.
    Computing post^198 from 11 states.
    Computing post^199 from 12 states.
    Computing post^200 from 12 states.
    Computing post^201 from 12 states.
    Computing post^202 from 12 states.
    Computing post^203 from 22 states.
    Computing post^204 from 20 states.
    Computing post^205 from 15 states.
    Computing post^206 from 20 states.
    Computing post^207 from 20 states.
    Computing post^208 from 11 states.
    Computing post^209 from 7 states.
    Computing post^210 from 7 states.
    Computing post^211 from 12 states.
    Computing post^212 from 8 states.
    Computing post^213 from 6 states.
    Computing post^214 from 6 states.
    Computing post^215 from 6 states.
    Computing post^216 from 9 states.
    Computing post^217 from 9 states.
    Computing post^218 from 11 states.
    Computing post^219 from 17 states.
    Computing post^220 from 11 states.
    Computing post^221 from 12 states.
    Computing post^222 from 12 states.
    Computing post^223 from 12 states.
    Computing post^224 from 12 states.
    Computing post^225 from 21 states.
    Computing post^226 from 14 states.
    Computing post^227 from 14 states.
    Computing post^228 from 25 states.
    Computing post^229 from 16 states.
    Computing post^230 from 11 states.
    Computing post^231 from 8 states.
    Computing post^232 from 6 states.
    Computing post^233 from 10 states.
    Computing post^234 from 9 states.
    Computing post^235 from 8 states.
    Computing post^236 from 7 states.
    Computing post^237 from 7 states.
    Computing post^238 from 10 states.
    Computing post^239 from 10 states.
    Computing post^240 from 13 states.
    Computing post^241 from 14 states.
    Computing post^242 from 10 states.
    Computing post^243 from 14 states.
    Computing post^244 from 13 states.
    Computing post^245 from 13 states.
    Computing post^246 from 13 states.
    Computing post^247 from 24 states.
    Computing post^248 from 21 states.
    Computing post^249 from 18 states.
    Computing post^250 from 25 states.
    Computing post^251 from 20 states.
    Computing post^252 from 15 states.
    Computing post^253 from 14 states.
    Computing post^254 from 14 states.
    Computing post^255 from 25 states.
    Computing post^256 from 14 states.
    Computing post^257 from 13 states.
    Computing post^258 from 12 states.
    Computing post^259 from 12 states.
    Computing post^260 from 18 states.
    Computing post^261 from 18 states.
    Computing post^262 from 24 states.
    Computing post^263 from 27 states.
    Computing post^264 from 14 states.
    Computing post^265 from 15 states.
    Computing post^266 from 13 states.
    Computing post^267 from 12 states.
    Computing post^268 from 11 states.
    Computing post^269 from 17 states.
    Computing post^270 from 13 states.
    Computing post^271 from 20 states.
    Computing post^272 from 23 states.
    Computing post^273 from 22 states.
    Computing post^274 from 15 states.
    Computing post^275 from 12 states.
    Computing post^276 from 11 states.
    Computing post^277 from 19 states.
    Computing post^278 from 15 states.
    Computing post^279 from 16 states.
    Computing post^280 from 13 states.
    Computing post^281 from 12 states.
    Computing post^282 from 18 states.
    Computing post^283 from 18 states.
    Computing post^284 from 22 states.
    Computing post^285 from 24 states.
    Computing post^286 from 16 states.
    Computing post^287 from 11 states.
    Computing post^288 from 11 states.
    Computing post^289 from 11 states.
    Computing post^290 from 10 states.
    Computing post^291 from 18 states.
    Computing post^292 from 14 states.
    Computing post^293 from 20 states.
    Computing post^294 from 24 states.
    Computing post^295 from 19 states.
    Computing post^296 from 14 states.
    Computing post^297 from 12 states.
    Computing post^298 from 11 states.
    Computing post^299 from 15 states.
    Computing post^300 from 11 states.
    Computing post^301 from 13 states.
    Computing post^302 from 12 states.
    Computing post^303 from 10 states.
    Computing post^304 from 15 states.
    Computing post^305 from 15 states.
    Computing post^306 from 19 states.
    Computing post^307 from 23 states.
    Computing post^308 from 13 states.
    Computing post^309 from 12 states.
    Computing post^310 from 12 states.
    Computing post^311 from 11 states.
    Computing post^312 from 11 states.
    Computing post^313 from 16 states.
    Computing post^314 from 15 states.
    Computing post^315 from 24 states.
    Computing post^316 from 31 states.
    Computing post^317 from 22 states.
    Computing post^318 from 15 states.
    Computing post^319 from 11 states.
    Computing post^320 from 11 states.
    Computing post^321 from 18 states.
    Computing post^322 from 13 states.
    Computing post^323 from 6 states.
    Computing post^324 from 4 states.
    Computing post^325 from 3 states.
    Computing post^326 from 4 states.
    Computing post^327 from 4 states.
    Computing post^328 from 4 states.
    Computing post^329 from 5 states.
    Computing post^330 from 5 states.
    Computing post^331 from 5 states.
    Computing post^332 from 5 states.
    Computing post^333 from 5 states.
    Computing post^334 from 5 states.
    Computing post^335 from 5 states.
    Computing post^336 from 5 states.
    Computing post^337 from 8 states.
    Computing post^338 from 4 states.
    Computing post^339 from 3 states.
    Computing post^340 from 1 state.
    Computing post^341 from 2 states.
    Computing post^342 from 2 states.
    Computing post^343 from 2 states.
    Computing post^344 from 2 states.
    Computing post^345 from 2 states.
    Computing post^346 from 2 states.
    Computing post^347 from 2 states.
    Computing post^348 from 4 states.
    Computing post^349 from 4 states.
    Computing post^350 from 4 states.
    Computing post^351 from 7 states.
    Computing post^352 from 6 states.
    Computing post^353 from 5 states.
    Computing post^354 from 5 states.
    Computing post^355 from 5 states.
    Computing post^356 from 5 states.
    Computing post^357 from 5 states.
    Computing post^358 from 4 states.
    Computing post^359 from 8 states.
    Computing post^360 from 4 states.
    Computing post^361 from 2 states.
    Computing post^362 from 1 state.
    Computing post^363 from 2 states.
    Computing post^364 from 2 states.
    Computing post^365 from 2 states.
    Computing post^366 from 4 states.
    Computing post^367 from 4 states.
    Computing post^368 from 4 states.
    Computing post^369 from 4 states.
    Computing post^370 from 6 states.
    Computing post^371 from 6 states.
    Computing post^372 from 4 states.
    Computing post^373 from 7 states.
    Computing post^374 from 9 states.
    Computing post^375 from 7 states.
    Computing post^376 from 4 states.
    Computing post^377 from 4 states.
    Computing post^378 from 4 states.
    Computing post^379 from 4 states.
    Computing post^380 from 9 states.
    Computing post^381 from 16 states.
    Computing post^382 from 8 states.
    Computing post^383 from 3 states.
    Computing post^384 from 1 state.
    Computing post^385 from 2 states.
    Computing post^386 from 2 states.
    Computing post^387 from 2 states.
    Computing post^388 from 4 states.
    Computing post^389 from 4 states.
    Computing post^390 from 4 states.
    Computing post^391 from 4 states.
    Computing post^392 from 4 states.
    Computing post^393 from 4 states.
    
    Fixpoint reached at a depth of 394: 5700 states with 7714 transitions in the final state space.
    
      [AGsafe] Algorithm completed after 148.177 seconds.
    
    Final constraint such that the system is correct:
     C3_WORST >= 20
    & b >= 10
    & 100 >= 2*b + C3_WORST
    This good constraint is exact (sound and complete)

    409.521 MiB (i.e., 53676764 words of size 8)
    
    Result written to file '/media/gia/Data/Example-Models/Sched2.100.2/Sched2.100.2-layerBFS-incl-EF.res'.
    
    ------------------------------------------------------------
    Statistics: State space
    ------------------------------------------------------------
    Number of states                        : 5700
    Number of transitions                   : 7714
    Number of computed states               : 7715
    Total computation time                  : 148.169 seconds
    States/second in state space            : 38.4 (5700/148.169 seconds)
    Computed states/second                  : 52.0 (7715/148.169 seconds)
    Estimated memory                        : 409.623 MiB (i.e., 53690179 words of size 8)
    
    Generating graphical output to '/media/gia/Data/Example-Models/Sched2.100.2/Sched2.100.2-layerBFS-incl-EF-statespace.jpg'…
    Writing the states description to file '/media/gia/Data/Example-Models/Sched2.100.2/Sched2.100.2-layerBFS-incl-EF-statespace.states'…
    
    Drawing the cartography…
    Plot cartography in 2D projected on parameters b and C3_WORST to file '/media/gia/Data/Example-Models/Sched2.100.2/Sched2.100.2-layerBFS-incl-EF_cart.png'.
    
    ------------------------------------------------------------
     Statistics: Algorithm counters
    ------------------------------------------------------------
    main algorithm                          : 148.177 seconds
    ------------------------------------------------------------
     Statistics: Parsing counters
    ------------------------------------------------------------
    model parsing                           : 0.006 second
    ------------------------------------------------------------
     Statistics: State computation counters
    ------------------------------------------------------------
    number of state comparisons             : 2078752
    number of constraints comparisons       : 2078752
    number of new states <= old             : 2015
    number of new states >= old             : 0
    StateSpace.merging attempts             : 0
    StateSpace.merges                       : 0
    StatesMerging.merging attempts          : 0
    StatesMerging.merges                    : 0
    ------------------------------------------------------------
     Statistics: Graphics-related counters
    ------------------------------------------------------------
    state space drawing                     : 46.564 seconds
    cartography drawing                     : 0.048 second
    ------------------------------------------------------------
     Statistics: Global counter
    ------------------------------------------------------------
    total                                   : 194.802 seconds

    IMITATOR successfully terminated (after 194.804 seconds)
    Estimated memory used: 10.474 GiB (i.e., 1405868167 words of size 8)