**************************************************
 *  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.005 second.
 Program checked and converted after 0.034 second.
 
 Computing post^1
   0 states merged.
 Computing post^2
   Adding the following inequality (randomly selected among 2 inequalities):
   Off1 < WCET_2 + Off2
   Adding the following inequality (randomly selected among 2 inequalities):
   Off3 < WCET_1 + Off1
   Adding the following inequality (randomly selected among 2 inequalities):
   Off1 < WCET_3 + Off3
   0 states merged.
 Computing post^3
   Adding the following inequality:
   Off2 < WCET_1 + Off1
   2 states merged.
 Computing post^4
   0 states merged.
 Computing post^5
   Adding the following inequality:
   WCET_2 + WCET_1 <= per1
   0 states merged.
 Computing post^6
   Adding the following inequality (randomly selected among 2 inequalities):
   per1 + Off1 < per2 + Off2
   Adding the following inequality:
   WCET_3 + WCET_2 + WCET_1 + Off2 <= per1 + Off1
   1 states merged.
 Computing post^7
   Adding the following inequality:
   per1 + Off1 < per3 + Off3
   0 states merged.
 Computing post^8
   Adding the following inequality:
   WCET_1 + per1 + Off1 <= per2 + Off2
   Adding the following inequality:
   WCET_1 + per1 + Off1 <= per3 + Off3
   0 states merged.
 Computing post^9
   Adding the following inequality (randomly selected among 2 inequalities):
   per2 + Off2 < 2*per1 + Off1
   Adding the following inequality:
   per2 + Off2 < per3 + Off3
   0 states merged.
 Computing post^10
   Adding the following inequality:
   per3 + Off3 < WCET_2 + per2 + Off2
   Adding the following inequality:
   per3 + Off3 < 2*per1 + Off1
   0 states merged.
 Computing post^11
   Adding the following inequality:
   WCET_2 + per2 + Off2 <= 2*per1 + Off1
   0 states merged.
 Computing post^12
   Adding the following inequality:
   2*per1 + Off1 < WCET_3 + WCET_2 + per2 + Off2
   0 states merged.
 Computing post^13
   0 states merged.
 Computing post^14
   0 states merged.
 Computing post^15
   Adding the following inequality:
   deadlineBasic < 2*per2 + Off2
   Adding the following inequality:
   deadlineBasic < 3*per1 + Off1
   Adding the following inequality:
   deadlineBasic < 2*per3 + Off3
   0 states merged.
 
 Final constraint K  :
   WCET_1 + Off1 > Off2
 & WCET_1 + Off1 > Off3
 & WCET_3 + WCET_2 + per2 + Off2 > 2*per1 + Off1
 & per3 + Off3 > per2 + Off2
 & per2 + Off2 > per1 + Off1
 & WCET_2 + Off2 > Off1
 & per2 + Off2 >= WCET_1 + per1 + Off1
 & WCET_2 + per2 + Off2 > per3 + Off3
 & 2*per1 + Off1 >= WCET_2 + per2 + Off2
 & WCET_3 + Off3 > Off1
 & per1 + Off1 >= WCET_3 + WCET_2 + WCET_1 + Off2
 & 3*per1 + Off1 > deadlineBasic
 & 2*per2 + Off2 > deadlineBasic
 & 2*per3 + Off3 > deadlineBasic
 
 Fixpoint reached after 15 iterations in 1.027 seconds: 49 reachable states with 51 transitions.
 
 Final constraint K0 :
   Off1 >= 0
 & 3*per1 + Off1 > deadlineBasic
 & per3 > per2
 & Off1 + 2*per2 > deadlineBasic
 & per1 >= WCET_3 + WCET_2 + WCET_1
 & WCET_2 + per2 > per3
 & 2*per1 >= WCET_2 + per2
 & WCET_3 + WCET_2 + per2 > 2*per1
 & WCET_1 > 0
 & deadlineBasic >= WCET_3 + WCET_2 + WCET_1 + Off1 + per2
 & Off1 = Off2
 & Off1 = Off3

 HYMITATOR successfully terminated (after 1.795 seconds)