************************************************************
 *  IMITATOR 2.5.0                                          *
 *                                                          *
 *             Etienne ANDRE, Ulrich KUEHNE, Romain SOULAT  *
 *                                             2009 - 2012  *
 *                       LSV, ENS de Cachan & CNRS, France  *
 *  LIPN, Universite Paris 13, Sorbonne Paris Cite, France  *
 ************************************************************
 Model: examples/Scheduling/astrium_basic_thermal_fp.imi
 Mode: inverse method.
 Merging technique of [AFS12] enabled.
 Graphical output will be generated.
 Log (description of states) will be generated.
 
 Parsing completed after 0.006 second.
 Memory for abstract program: 503.02734375 KB (i.e., 128775. words)
 The model contains stopwatches.
 
 Computing post^1 from 1 state.
   Adding the following inequality (randomly selected among 2 inequalities):
   Off1 < Off2
 Computing post^2 from 2 states.
   Adding the following inequality:
   Off3 < Off1 + WCET_1
   Adding the following inequality (randomly selected among 2 inequalities):
   per1 + Off1 < Off2
   Adding the following inequality:
   Off1 < Off3 + WCET_3
 Computing post^3 from 2 states.
 Computing post^4 from 2 states.
   Adding the following inequality:
   per1 < WCET_3 + WCET_1
   Adding the following inequality:
   per1 + Off1 < Off3 + WCET_3 + WCET_1
 Computing post^5 from 2 states.
   Adding the following inequality:
   per1 + Off1 + WCET_1 <= Off2
 Computing post^6 from 2 states.
   Adding the following inequality:
   2*per1 + Off1 < Off2
   Adding the following inequality:
   2*per1 < WCET_3 + 2*WCET_1
   Adding the following inequality:
   2*per1 + Off1 < Off3 + WCET_3 + 2*WCET_1
 Computing post^7 from 2 states.
   Adding the following inequality:
   2*per1 + Off1 + WCET_1 <= Off2
 Computing post^8 from 2 states.
   Adding the following inequality:
   3*per1 + Off1 < Off2
   Adding the following inequality:
   3*per1 < WCET_3 + 3*WCET_1
   Adding the following inequality:
   3*per1 + Off1 < Off3 + WCET_3 + 3*WCET_1
 Computing post^9 from 2 states.
   Adding the following inequality:
   3*per1 + Off1 + WCET_1 <= Off2
 Computing post^10 from 2 states.
   Adding the following inequality:
   4*per1 + Off1 < Off2
   Adding the following inequality (randomly selected among 2 inequalities):
   4*per1 < WCET_3 + 4*WCET_1
   Adding the following inequality (randomly selected among 2 inequalities):
   deadlineBasic < Off3 + WCET_3 + 4*WCET_1
 Computing post^11 from 2 states.
   Adding the following inequality:
   4*per1 + Off1 + WCET_1 <= Off2
 Computing post^12 from 2 states.
   Adding the following inequality:
   5*per1 + Off1 < Off2
 Computing post^13 from 2 states.
   Adding the following inequality:
   5*per1 + Off1 + WCET_1 <= Off2
 Computing post^14 from 2 states.
   Adding the following inequality:
   6*per1 + Off1 < Off2
 Computing post^15 from 2 states.
   Adding the following inequality:
   6*per1 + Off1 + WCET_1 <= Off2
 Computing post^16 from 2 states.
   Adding the following inequality:
   7*per1 + Off1 < Off2
 Computing post^17 from 2 states.
   Adding the following inequality:
   7*per1 + Off1 + WCET_1 <= Off2
 Computing post^18 from 2 states.
   Adding the following inequality:
   8*per1 + Off1 < Off2
 Computing post^19 from 2 states.
   Adding the following inequality:
   8*per1 + Off1 + WCET_1 <= Off2
 Computing post^20 from 2 states.
   Adding the following inequality:
   9*per1 + Off1 < Off2
 Computing post^21 from 2 states.
   Adding the following inequality:
   9*per1 + Off1 + WCET_1 <= Off2
 Computing post^22 from 2 states.
   Adding the following inequality:
   Off2 < 10*per1 + Off1
 Computing post^23 from 2 states.
   Adding the following inequality:
   10*per1 + Off1 < Off2 + WCET_2
 Computing post^24 from 2 states.
 Computing post^25 from 2 states.
   Adding the following inequality:
   11*per1 + Off1 < Off2 + WCET_2 + WCET_1
 Computing post^26 from 2 states.
 Computing post^27 from 2 states.
   Adding the following inequality:
   12*per1 + Off1 < Off2 + WCET_2 + 2*WCET_1
 Computing post^28 from 2 states.
 Computing post^29 from 2 states.
   Adding the following inequality:
   Off2 + WCET_2 + 3*WCET_1 <= 13*per1 + Off1
 Computing post^30 from 2 states.
 Computing post^31 from 2 states.
 Computing post^32 from 2 states.
   Adding the following inequality:
   deadlineBasic < 14*per1 + Off1
 
 Fixpoint reached after 33 iterations: 63 reachable states with 62 transitions.
 Analysis may have been non-deterministic:
 4 random selections have been performed.
 
 Final constraint K0  (12 inequalities):
  Off3 + 13*per1 >= Off2 + WCET_2 + 3*WCET_1
 & Off3 + 10*per1 > Off2
 & Off2 + WCET_2 + 2*WCET_1 > Off3 + 12*per1
 & Off2 >= Off3 + 9*per1 + WCET_1
 & deadlineBasic >= Off3 + 13*per1 + WCET_1
 & WCET_1 > 0
 & per2 + Off2 >= Off3 + 13*per1 + WCET_1
 & Off3 + 14*per1 > deadlineBasic
 & Off3 >= 0
 & Off3 + WCET_3 + 4*WCET_1 > deadlineBasic
 & per3 >= 13*per1 + WCET_1
 & Off3 = Off1
 
 Inverse method successfully finished after 0.283 second.
 
 Generating graphical output...
 Writing to file the states description...

 IMITATOR successfully terminated (after 0.375 second)