************************************************************
    *  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: Fri Jun 16, 2017 22:18:24
    
    Model: /media/gia/Data/Example-Models/F4/F4.imi
    Mode: EF-synthesis.
    Exploration order: layer-based BFS.
    Considering fixpoint variant with bidirectional 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 an L/U-PTA:
    - lower-bound parameters {delta}
    - upper-bound parameters {Delta}
    
    Abstract model built after 0.006 second.
    Memory for abstract model: 869.269 KiB (i.e., 222533 words)
    
    Starting running algorithm AGsafe…
    
    Computing post^1 from 1 state.
    Computing post^2 from 4 states.
    Computing post^3 from 16 states.
    Computing post^4 from 46 states.
    Computing post^5 from 96 states.
    Computing post^6 from 161 states.
    Computing post^7 from 267 states.
    Computing post^8 from 439 states.
    Computing post^9 from 662 states.
    Computing post^10 from 984 states.
      [AGsafe] Found a new state violating the property.
    Computing post^11 from 1101 states.
    Computing post^12 from 1229 states.
    Computing post^13 from 1393 states.
    Computing post^14 from 1478 states.
      [AGsafe] Found a new state violating the property.
    Computing post^15 from 455 states.
    Computing post^16 from 372 states.
    Computing post^17 from 288 states.
    Computing post^18 from 216 states.
    Computing post^19 from 144 states.
    Computing post^20 from 72 states.
    Computing post^21 from 72 states.
    Computing post^22 from 24 states.
    Computing post^23 from 24 states.
    
    Fixpoint reached at a depth of 24: 10003 states with 17707 transitions in the final state space.
    
      [AGsafe] Algorithm completed after 22.578 seconds.
    
    Final constraint such that the system is correct:
     delta >= Delta
    & Delta >= 0
    This good constraint is exact (sound and complete)

    535.550 MiB (i.e., 70195647 words of size 8)
    
    Result written to file '/media/gia/Data/Example-Models/F4/F4-layerBFS-incl2-EF.res'.
    
    ------------------------------------------------------------
    Statistics: State space
    ------------------------------------------------------------
    Number of states                        : 10003
    Number of transitions                   : 17707
    Number of computed states               : 19360
    Total computation time                  : 22.573 seconds
    States/second in state space            : 443.1 (10003/22.573 seconds)
    Computed states/second                  : 857.6 (19360/22.573 seconds)
    Estimated memory                        : 535.650 MiB (i.e., 70208770 words of size 8)
    
    Generating graphical output to '/media/gia/Data/Example-Models/F4/F4-layerBFS-incl2-EF-statespace.jpg'…
    Writing the states description to file '/media/gia/Data/Example-Models/F4/F4-layerBFS-incl2-EF-statespace.states'…
    
    Drawing the cartography…
    Plot cartography in 2D projected on parameters delta and Delta to file '/media/gia/Data/Example-Models/F4/F4-layerBFS-incl2-EF_cart.png'.
    
    ------------------------------------------------------------
     Statistics: Algorithm counters
    ------------------------------------------------------------
    main algorithm                          : 22.577 seconds
    ------------------------------------------------------------
     Statistics: Parsing counters
    ------------------------------------------------------------
    model parsing                           : 0.003 second
    ------------------------------------------------------------
     Statistics: State computation counters
    ------------------------------------------------------------
    number of state comparisons             : 1293172
    number of constraints comparisons       : 296306
    number of new states <= old             : 8220
    number of new states >= old             : 1137
    StateSpace.merging attempts             : 0
    StateSpace.merges                       : 0
    StatesMerging.merging attempts          : 0
    StatesMerging.merges                    : 0
    ------------------------------------------------------------
     Statistics: Graphics-related counters
    ------------------------------------------------------------
    state space drawing                     : 179.183 seconds
    cartography drawing                     : 0.044 second
    ------------------------------------------------------------
     Statistics: Global counter
    ------------------------------------------------------------
    total                                   : 201.864 seconds

    IMITATOR successfully terminated (after 201.866 seconds)
    Estimated memory used: 32.942 GiB (i.e., 4421461450 words of size 8)