**************************************************
 *  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.007 second.
 Program checked and converted after 0.065 second.
 
 Computing post^1
   Adding the following inequality:
   offset_1_1 < offset_2_1
   0 states merged.
 Computing post^2
   0 states merged.
 Computing post^3
   0 states merged.
 Computing post^4
   Adding the following inequality:
   offset_1_1 + wcet1_1 + wcet2_1 <= offset_2_2
   1 states merged.
 Computing post^5
   1 states merged.
 Computing post^6
   1 states merged.
 Computing post^7
   3 states merged.
 Computing post^8
   2 states merged.
 Computing post^9
   5 states merged.
 Computing post^10
   5 states merged.
 Computing post^11
   9 states merged.
 Computing post^12
   7 states merged.
 Computing post^13
   6 states merged.
 Computing post^14
   10 states merged.
 Computing post^15
   0 states merged.
 
 Final constraint K  :
   offset_2_1 > offset_1_1
 & offset_2_2 >= offset_1_1 + wcet1_1 + wcet2_1
 
 Fixpoint reached after 15 iterations in 85.304 seconds: 215 reachable states with 264 transitions.
 
 Final constraint K0 :
   offset_1_1 >= 0
 & offset_1_1 + wcet1_1 > offset_2_1
 & wcet1_2 > 0
 & wcet1_3 > 0
 & wcet1_4 > 0
 & wcet2_1 > 0
 & wcet2_2 > 0
 & wcet2_3 > 0
 & wcet2_3 >= bcet2_3
 & wcet2_2 >= bcet2_2
 & wcet2_1 >= bcet2_1
 & wcet1_4 >= bcet1_4
 & wcet1_3 >= bcet1_3
 & wcet1_2 >= bcet1_2
 & wcet1_1 >= bcet1_1
 & offset_2_1 > offset_1_1
 & offset_2_2 >= offset_1_1 + wcet1_1 + wcet2_1
 & priority1_1 = 2
 & priority1_2 = 4
 & priority1_3 = 2
 & priority1_4 = 4
 & priority2_1 = 3
 & priority2_2 = 3
 & priority2_3 = 1

 HYMITATOR successfully terminated (after 88.864 seconds)