************************************************************
    *  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: Sat Jun 17, 2017 11:04:08
    
    Model: /media/gia/Data/Example-Models/critical-region4/critical-region4.imi
    Mode: EF-synthesis.
    Exploration order: queue-based BFS with priority [WORK IN PROGRESS].
    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.
    
    Abstract model built after 0.009 second.
    Memory for abstract model: 1083.179 KiB (i.e., 277294 words)
    
    Starting running algorithm AGsafe…
    
    Entering explore_queue_bfs!!!
      [AGsafe] Found a new state violating the property.
    End of Ordering!!! 
    
    
    State space exploration stopped: 42341 states with 93029 transitions in the final state space.
    Exiting explore_queue_bfs!!!
    
      [AGsafe] Algorithm completed after 900.057 seconds.
    
    Final constraint such that the system is correct:
     A >= 0
    & B >= 0
    & 1 > A
    This good constraint is an over-approximation of the actual result (or the actual result itself)

    22.686 GiB (i.e., 3044893441 words of size 8)
    
    Result written to file '/media/gia/Data/Example-Models/critical-region4/critical-region4-queueBFSPRIOR-incl-EF.res'.
    
    ------------------------------------------------------------
    Statistics: State space
    ------------------------------------------------------------
    Number of states                        : 42341
    Number of transitions                   : 93029
    Number of computed states               : 93030
    Total computation time                  : 900.048 seconds
    States/second in state space            : 47.0 (42341/900.048 seconds)
    Computed states/second                  : 103.3 (93030/900.048 seconds)
    Estimated memory                        : 22.686 GiB (i.e., 3044907021 words of size 8)