**************************************************
 *  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.003 second.
 Program checked and converted after 0.007 second.
 
 Computing post^1
   0 states merged.
 Computing post^2
   1 states merged.
 Computing post^3
   2 states merged.
 Computing post^4
   0 states merged.
 Computing post^5
   1 states merged.
 Computing post^6
   Adding the following inequality:
   10 <= wcet_m1_job1 + wcet_m2_job1 + wcet_m2_job2
   5 states merged.
 Computing post^7
   7 states merged.
 Computing post^8
   Adding the following inequality:
   10 <= wcet_m2_job1 + wcet_m3_job1 + wcet_m2_job2
   4 states merged.
 Computing post^9
   2 states merged.
 Computing post^10
   0 states merged.
 
 Final constraint K  :
   wcet_m1_job1 + wcet_m2_job1 + wcet_m2_job2 >= 10
 & wcet_m2_job1 + wcet_m3_job1 + wcet_m2_job2 >= 10
 
 Fixpoint reached after 10 iterations in 0.111 second: 53 reachable states with 70 transitions.
 
 Final constraint K0 :
   10 > wcet_m2_job1 + wcet_m2_job2
 & 10 > wcet_m1_job1 + wcet_m2_job2
 & wcet_m2_job1 + wcet_m3_job1 + wcet_m2_job2 >= 10
 & 10 > wcet_m1_job1 + wcet_m2_job1 + wcet_m3_job1
 & wcet_m1_job1 + wcet_m2_job1 + wcet_m2_job2 >= 10
 & deadline = 10

 HYMITATOR successfully terminated (after 0.446 second)