************************************************************
    *  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 19:46:13
    
    Model: /media/gia/Data/Example-Models/Sched2.50.2/Sched2.50.2.imi
    Mode: EF-synthesis.
    Exploration order: layer-based BFS.
    Considering fixpoint variant with bidirectional inclusion of symbolic zones (instead of equality).
    Merging technique of [AFS13] enabled.
    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.008 second.
    Memory for abstract model: 979.906 KiB (i.e., 250856 words)
    
    Starting running algorithm AGsafe…
    
    Computing post^1 from 1 state.
    Computing post^2 from 1 state.
    Computing post^3 from 2 states.
    Computing post^4 from 3 states.
    Computing post^5 from 2 states.
    Computing post^6 from 3 states.
      [AGsafe] Found a new state violating the property.
    Computing post^7 from 5 states.
    Computing post^8 from 8 states.
    Computing post^9 from 5 states.
      [AGsafe] Found a new state violating the property.
    Computing post^10 from 5 states.
      [AGsafe] Found a new state violating the property.
    Computing post^11 from 13 states.
    Computing post^12 from 18 states.
      [AGsafe] Found a new state violating the property.
    Computing post^13 from 8 states.
    Computing post^14 from 8 states.
    Computing post^15 from 9 states.
    Computing post^16 from 8 states.
    Computing post^17 from 8 states.
      2 states merged within 18 states.
    Computing post^18 from 16 states.
    Computing post^19 from 26 states.
    Computing post^20 from 19 states.
      1 state merged within 10 states.
    Computing post^21 from 9 states.
    Computing post^22 from 7 states.
    Computing post^23 from 8 states.
    Computing post^24 from 6 states.
    Computing post^25 from 6 states.
      2 states merged within 10 states.
    Computing post^26 from 8 states.
    Computing post^27 from 8 states.
      1 state merged within 6 states.
    Computing post^28 from 5 states.
    Computing post^29 from 13 states.
    Computing post^30 from 10 states.
    Computing post^31 from 9 states.
    Computing post^32 from 3 states.
    Computing post^33 from 3 states.
    Computing post^34 from 3 states.
    Computing post^35 from 6 states.
      1 state merged within 4 states.
    Computing post^36 from 4 states.
      1 state merged within 6 states.
    Computing post^37 from 6 states.
    Computing post^38 from 5 states.
    Computing post^39 from 5 states.
      4 states merged within 7 states.
    Computing post^40 from 5 states.
    Computing post^41 from 5 states.
      1 state merged within 8 states.
    Computing post^42 from 7 states.
      2 states merged within 6 states.
    Computing post^43 from 5 states.
      1 state merged within 6 states.
    Computing post^44 from 6 states.
      [AGsafe] Found a new state violating the property.
    Computing post^45 from 5 states.
    Computing post^46 from 4 states.
    Computing post^47 from 4 states.
      2 states merged within 4 states.
    Computing post^48 from 3 states.
    Computing post^49 from 6 states.
    Computing post^50 from 6 states.
    Computing post^51 from 6 states.
    Computing post^52 from 8 states.
    Computing post^53 from 8 states.
    Computing post^54 from 4 states.
    Computing post^55 from 4 states.
    Computing post^56 from 4 states.
    Computing post^57 from 6 states.
    Computing post^58 from 6 states.
    Computing post^59 from 4 states.
    Computing post^60 from 4 states.
    Computing post^61 from 4 states.
    Computing post^62 from 6 states.
    Computing post^63 from 6 states.
      1 state merged within 8 states.
    Computing post^64 from 8 states.
    Computing post^65 from 6 states.
      1 state merged within 5 states.
    Computing post^66 from 4 states.
      [AGsafe] Found a new state violating the property.
    Computing post^67 from 5 states.
      1 state merged within 5 states.
    Computing post^68 from 5 states.
    Computing post^69 from 4 states.
      1 state merged within 4 states.
    Computing post^70 from 4 states.
    Computing post^71 from 7 states.
    Computing post^72 from 6 states.
    Computing post^73 from 6 states.
    Computing post^74 from 8 states.
    Computing post^75 from 8 states.
    Computing post^76 from 4 states.
    Computing post^77 from 4 states.
    Computing post^78 from 4 states.
    Computing post^79 from 6 states.
      2 states merged within 6 states.
    Computing post^80 from 6 states.
    Computing post^81 from 6 states.
    Computing post^82 from 4 states.
    Computing post^83 from 4 states.
    Computing post^84 from 6 states.
    Computing post^85 from 6 states.
      2 states merged within 9 states.
    Computing post^86 from 9 states.
      1 state merged within 7 states.
    Computing post^87 from 6 states.
      2 states merged within 5 states.
    Computing post^88 from 4 states.
    Computing post^89 from 5 states.
    Computing post^90 from 4 states.
    Computing post^91 from 4 states.
      1 state merged within 4 states.
    Computing post^92 from 4 states.
      1 state merged within 8 states.
    Computing post^93 from 8 states.
      1 state merged within 7 states.
    Computing post^94 from 7 states.
    Computing post^95 from 10 states.
      1 state merged within 11 states.
    Computing post^96 from 11 states.
    Computing post^97 from 10 states.
    Computing post^98 from 5 states.
    Computing post^99 from 5 states.
    Computing post^100 from 5 states.
      1 state merged within 8 states.
    Computing post^101 from 8 states.
    Computing post^102 from 5 states.
    Computing post^103 from 8 states.
    Computing post^104 from 7 states.
    Computing post^105 from 6 states.
      1 state merged within 9 states.
    Computing post^106 from 9 states.
    Computing post^107 from 8 states.
      1 state merged within 9 states.
    Computing post^108 from 9 states.
      2 states merged within 9 states.
    Computing post^109 from 8 states.
      2 states merged within 7 states.
    Computing post^110 from 6 states.
    Computing post^111 from 7 states.
      1 state merged within 6 states.
    Computing post^112 from 6 states.
    Computing post^113 from 5 states.
      1 state merged within 5 states.
    Computing post^114 from 5 states.
    Computing post^115 from 8 states.
    Computing post^116 from 6 states.
    Computing post^117 from 10 states.
      3 states merged within 13 states.
    Computing post^118 from 13 states.
    Computing post^119 from 10 states.
      1 state merged within 6 states.
    Computing post^120 from 6 states.
    Computing post^121 from 6 states.
    Computing post^122 from 6 states.
      1 state merged within 9 states.
    Computing post^123 from 9 states.
      2 states merged within 8 states.
    Computing post^124 from 8 states.
      1 state merged within 10 states.
    Computing post^125 from 10 states.
      1 state merged within 7 states.
    Computing post^126 from 6 states.
    Computing post^127 from 6 states.
      1 state merged within 9 states.
    Computing post^128 from 8 states.
    Computing post^129 from 8 states.
      3 states merged within 13 states.
    Computing post^130 from 10 states.
      4 states merged within 11 states.
    Computing post^131 from 8 states.
      2 states merged within 7 states.
    Computing post^132 from 6 states.
    Computing post^133 from 9 states.
      1 state merged within 7 states.
    Computing post^134 from 7 states.
    Computing post^135 from 6 states.
      1 state merged within 6 states.
    Computing post^136 from 6 states.
    Computing post^137 from 10 states.
      3 states merged within 10 states.
    Computing post^138 from 7 states.
    Computing post^139 from 4 states.
    Computing post^140 from 2 states.
    Computing post^141 from 2 states.
    Computing post^142 from 1 state.
    Computing post^143 from 2 states.
    Computing post^144 from 2 states.
    Computing post^145 from 2 states.
    Computing post^146 from 2 states.
    Computing post^147 from 2 states.
      2 states merged within 2 states.
    Computing post^148 from 1 state.
    Computing post^149 from 1 state.
    Computing post^150 from 2 states.
    Computing post^151 from 2 states.
      2 states merged within 3 states.
    Computing post^152 from 3 states.
    Computing post^153 from 5 states.
    Computing post^154 from 5 states.
    Computing post^155 from 5 states.
    Computing post^156 from 5 states.
    Computing post^157 from 5 states.
    Computing post^158 from 5 states.
    Computing post^159 from 6 states.
      2 states merged within 6 states.
    Computing post^160 from 5 states.
    Computing post^161 from 6 states.
    Computing post^162 from 3 states.
    Computing post^163 from 3 states.
    Computing post^164 from 1 state.
    Computing post^165 from 2 states.
    Computing post^166 from 2 states.
    Computing post^167 from 2 states.
    Computing post^168 from 2 states.
    Computing post^169 from 2 states.
      2 states merged within 2 states.
    Computing post^170 from 1 state.
    Computing post^171 from 1 state.
    Computing post^172 from 2 states.
    Computing post^173 from 2 states.
      2 states merged within 3 states.
    Computing post^174 from 3 states.
    Computing post^175 from 5 states.
    Computing post^176 from 4 states.
    Computing post^177 from 3 states.
    Computing post^178 from 3 states.
    Computing post^179 from 3 states.
    Computing post^180 from 3 states.
    Computing post^181 from 3 states.
      2 states merged within 6 states.
    Computing post^182 from 5 states.
      2 states merged within 10 states.
    Computing post^183 from 10 states.
      1 state merged within 5 states.
    Computing post^184 from 5 states.
      1 state merged within 3 states.
    Computing post^185 from 3 states.
      1 state merged within 2 states.
    Computing post^186 from 1 state.
      2 states merged within 2 states.
    Computing post^187 from 2 states.
      2 states merged within 2 states.
    Computing post^188 from 2 states.
      2 states merged within 2 states.
    Computing post^189 from 2 states.
      4 states merged within 4 states.
    Computing post^190 from 3 states.
      2 states merged within 3 states.
    Computing post^191 from 3 states.
      3 states merged within 3 states.
    Computing post^192 from 2 states.
      1 state merged within 2 states.
    Computing post^193 from 2 states.
      2 states merged within 3 states.
    Computing post^194 from 3 states.
      2 states merged within 3 states.
    Computing post^195 from 3 states.
      3 states merged within 3 states.
    Computing post^196 from 3 states.
      4 states merged within 5 states.
    Computing post^197 from 5 states.
      3 states merged within 6 states.
    Computing post^198 from 6 states.
      2 states merged within 5 states.
    Computing post^199 from 5 states.
      2 states merged within 3 states.
    Computing post^200 from 3 states.
      2 states merged within 3 states.
    Computing post^201 from 3 states.
      2 states merged within 3 states.
    Computing post^202 from 3 states.
      2 states merged within 3 states.
    Computing post^203 from 3 states.
      4 states merged within 4 states.
    Computing post^204 from 4 states.
      8 states merged within 8 states.
    Computing post^205 from 8 states.
      4 states merged within 6 states.
    Computing post^206 from 5 states.
      2 states merged within 2 states.
    Computing post^207 from 2 states.
    
    Fixpoint reached at a depth of 208: 473 states with 634 transitions in the final state space.
    
      [AGsafe] Algorithm completed after 35.205 seconds.
    
    Final constraint such that the system is correct:
     C3_WORST >= 20
    & b >= 10
    & 50 >= 2*b + C3_WORST
    This good constraint is exact (sound and complete)

    73.007 MiB (i.e., 9569276 words of size 8)
    
    Result written to file '/media/gia/Data/Example-Models/Sched2.50.2/Sched2.50.2-layerBFS-incl2-merge-EF.res'.
    
    ------------------------------------------------------------
    Statistics: State space
    ------------------------------------------------------------
    Number of states                        : 473
    Number of transitions                   : 634
    Number of computed states               : 1991
    Total computation time                  : 35.196 seconds
    States/second in state space            : 13.4 (473/35.196 seconds)
    Computed states/second                  : 56.5 (1991/35.196 seconds)
    Estimated memory                        : 73.110 MiB (i.e., 9582728 words of size 8)
    
    Generating graphical output to '/media/gia/Data/Example-Models/Sched2.50.2/Sched2.50.2-layerBFS-incl2-merge-EF-statespace.jpg'…
    Writing the states description to file '/media/gia/Data/Example-Models/Sched2.50.2/Sched2.50.2-layerBFS-incl2-merge-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.50.2/Sched2.50.2-layerBFS-incl2-merge-EF_cart.png'.
    
    ------------------------------------------------------------
     Statistics: Algorithm counters
    ------------------------------------------------------------
    main algorithm                          : 35.204 seconds
    ------------------------------------------------------------
     Statistics: Parsing counters
    ------------------------------------------------------------
    model parsing                           : 0.006 second
    ------------------------------------------------------------
     Statistics: State computation counters
    ------------------------------------------------------------
    number of state comparisons             : 80316
    number of constraints comparisons       : 80316
    number of new states <= old             : 446
    number of new states >= old             : 931
    StateSpace.merging attempts             : 48982
    StateSpace.merges                       : 141
    StatesMerging.merging attempts          : 0
    StatesMerging.merges                    : 0
    ------------------------------------------------------------
     Statistics: Graphics-related counters
    ------------------------------------------------------------
    state space drawing                     : 110.331 seconds
    cartography drawing                     : 0.038 second
    ------------------------------------------------------------
     Statistics: Global counter
    ------------------------------------------------------------
    total                                   : 145.582 seconds

    IMITATOR successfully terminated (after 145.584 seconds)
    Estimated memory used: 150.327 MiB (i.e., 19703661 words of size 8)