**************************************************
 *  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.031 second.
 
 Computing post^1
   Adding the following inequality (randomly selected among 2 inequalities):
   Off1 < Off2
   0 states merged.
 Computing post^2
   Adding the following inequality:
   Off3 < WCET_1 + Off1
   Adding the following inequality:
   Off3 < Off2
   Adding the following inequality:
   Off1 < WCET_3 + Off3
   0 states merged.
 Computing post^3
   Adding the following inequality:
   WCET_1 + Off1 <= Off2
   0 states merged.
 Computing post^4
   Adding the following inequality:
   Off2 < per1 + Off1
   Adding the following inequality:
   Off2 < WCET_3 + WCET_1 + Off1
   Adding the following inequality:
   Off2 < WCET_3 + WCET_1 + Off3
   0 states merged.
 Computing post^5
   Adding the following inequality:
   per1 + Off1 < WCET_2 + Off2
   0 states merged.
 Computing post^6
   0 states merged.
 Computing post^7
   Adding the following inequality:
   deadlineBasic < WCET_2 + WCET_1 + Off2
   Adding the following inequality:
   deadlineBasic < 2*per1 + Off1
   0 states merged.
 
 Final constraint K  :
   WCET_3 + WCET_1 + Off3 > Off2
 & WCET_2 + Off2 > per1 + Off1
 & WCET_1 + Off1 > Off3
 & per1 + Off1 > Off2
 & WCET_3 + WCET_1 + Off1 > Off2
 & Off2 > Off1
 & Off2 >= WCET_1 + Off1
 & WCET_2 + WCET_1 + Off2 > deadlineBasic
 & 2*per1 + Off1 > deadlineBasic
 
 Fixpoint reached after 7 iterations in 0.186 second: 13 reachable states with 12 transitions.
 
 Final constraint K0 :
   Off1 >= 0
 & WCET_2 + WCET_1 + Off2 > deadlineBasic
 & per1 + Off1 > Off2
 & 2*per1 + Off1 > deadlineBasic
 & WCET_1 > 0
 & Off2 >= WCET_1 + Off1
 & WCET_3 + WCET_1 + Off1 > Off2
 & per2 + Off2 >= WCET_1 + per1 + Off1
 & per3 >= WCET_1 + per1
 & deadlineBasic >= WCET_1 + per1 + Off1
 & Off1 = Off3

 HYMITATOR successfully terminated (after 0.302 second)