**************************************************
 *  HYMITATOR 1.0                                 *
 *   Etienne ANDRE, Ulrich KUEHNE, Romain SOULAT  *
 *                                   2009 - 2012  *
 *     Laboratoire Specification et Verification  *
 *                  ENS de Cachan & CNRS, France  *
 **************************************************
 Mode: inverse method.
 
 Parsing done after 0.021 second.
 Program checked and converted after 0.091 second.
 
 Computing post^1
   0 states merged.
 Computing post^2
   3 states merged.
 Computing post^3
   6 states merged.
 Computing post^4
   12 states merged.
 Computing post^5
   Adding the following inequality:
   wcet_m_2_job_3 < 25
   Adding the following inequality:
   20 < wcet_m_2_job_3
   23 states merged.
 Computing post^6
   31 states merged.
 Computing post^7
   Adding the following inequality:
   20 < wcet_m_4_job_3
   35 states merged.
 Computing post^8
   64 states merged.
 Computing post^9
   97 states merged.
 Computing post^10
   Adding the following inequality:
   wcet_m_4_job_3 <= 62
   145 states merged.
 Computing post^11
   205 states merged.
 Computing post^12
   Adding the following inequality:
   wcet_m_4_job_3 < 32
   253 states merged.
 Computing post^13
   Adding the following inequality:
   wcet_m_2_job_3 < 24
   310 states merged.
 Computing post^14
   Adding the following inequality:
   wcet_m_4_job_3 <= 31
   Adding the following inequality:
   41 <= wcet_m_2_job_3 + wcet_m_4_job_3
   346 states merged.
 Computing post^15
   Adding the following inequality:
   24 <= wcet_m_4_job_3
   Adding the following inequality:
   wcet_m_4_job_3 > 24
   Adding the following inequality:
   22 <= wcet_m_2_job_3
   Adding the following inequality:
   124 <= wcet_m_2_job_3 + wcet_m_4_job_3 + wcet_m_3_job_3
   332 states merged.
 Computing post^16
   320 states merged.
 Computing post^17
   Adding the following inequality:
   150 <= wcet_m_2_job_3 + wcet_m_4_job_3 + wcet_m_3_job_3
   266 states merged.
 Computing post^18
   Adding the following inequality:
   wcet_m_4_job_3 < 31
   270 states merged.
 Computing post^19
   245 states merged.
 Computing post^20
   183 states merged.
 Computing post^21
   163 states merged.
 Computing post^22
   154 states merged.
 Computing post^23
   120 states merged.
 Computing post^24
   Adding the following inequality:
   wcet_m_3_job_3 < 100
   114 states merged.
 Computing post^25
   92 states merged.
 Computing post^26
   44 states merged.
 Computing post^27
   17 states merged.
 Computing post^28
   4 states merged.
 Computing post^29
   0 states merged.
 Computing post^30
   0 states merged.
 
 Final constraint K  :
   100 > wcet_m_3_job_3
 & wcet_m_2_job_3 >= 22
 & 31 > wcet_m_4_job_3
 & wcet_m_2_job_3 + wcet_m_4_job_3 + wcet_m_3_job_3 >= 150
 & 24 > wcet_m_2_job_3
 
 Fixpoint reached after 30 iterations in 160.637 seconds: 4903 reachable states with 9043 transitions.