************************************************************
 *  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/LA02_2.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.01 second.
 *** Warning: 'wcet_m_0_job_1', which is assigned a valuation in pi0, is not a valid parameter name.
 *** Warning: 'wcet_m_1_job_1', which is assigned a valuation in pi0, is not a valid parameter name.
 *** Warning: 'wcet_m_2_job_1', which is assigned a valuation in pi0, is not a valid parameter name.
 *** Warning: 'wcet_m_3_job_1', which is assigned a valuation in pi0, is not a valid parameter name.
 *** Warning: 'wcet_m_4_job_1', which is assigned a valuation in pi0, is not a valid parameter name.
 *** Warning: 'deadline', which is assigned a valuation in pi0, is not a valid parameter name.
 Memory for abstract program: 770.890625 KB (i.e., 197348. words)
 The model contains stopwatches.
 
 Computing post^1 from 1 state.
 Computing post^2 from 3 states.
 Computing post^3 from 6 states.
   Adding the following inequality:
   20 < wcet_m_4_job_2
 Computing post^4 from 7 states.
 Computing post^5 from 10 states.
   Adding the following inequality:
   20 < wcet_m_2_job_2
 Computing post^6 from 11 states.
 Computing post^7 from 14 states.
 Computing post^8 from 20 states.
 Computing post^9 from 29 states.
   Adding the following inequality:
   wcet_m_0_job_2 < 87
   Adding the following inequality:
   wcet_m_1_job_2 < 20
 Computing post^10 from 39 states.
   Adding the following inequality:
   20 < wcet_m_3_job_2
 Computing post^11 from 44 states.
   Adding the following inequality:
   wcet_m_0_job_2 < 31
 Computing post^12 from 46 states.
   Adding the following inequality:
   wcet_m_3_job_2 < 87
 Computing post^13 from 46 states.
 Computing post^14 from 49 states.
 Computing post^15 from 46 states.
   Adding the following inequality:
   93 < wcet_m_4_job_2 + wcet_m_2_job_2 + wcet_m_0_job_2 + wcet_m_1_job_2
   Adding the following inequality:
   17 < wcet_m_0_job_2
 Computing post^16 from 43 states.
 Computing post^17 from 38 states.
   Adding the following inequality:
   wcet_m_3_job_2 < 76 + wcet_m_1_job_2
   Adding the following inequality:
   17 < wcet_m_1_job_2
   Adding the following inequality:
   93 <= wcet_m_2_job_2 + wcet_m_0_job_2 + wcet_m_3_job_2
 Computing post^18 from 31 states.
 Computing post^19 from 23 states.
 Computing post^20 from 14 states.
 Computing post^21 from 5 states.
 Computing post^22 from 1 state.
 
 Fixpoint reached after 23 iterations: 383 reachable states with 533 transitions.
 Analysis has been fully deterministic.
 
 Final constraint K0  (11 inequalities):
  20 > wcet_m_1_job_2
 & wcet_m_3_job_2 > 31 + wcet_m_1_job_2
 & 87 > wcet_m_3_job_2
 & wcet_m_1_job_2 > 17
 & wcet_m_0_job_2 > 17
 & wcet_m_2_job_2 > 20
 & 93 >= wcet_m_4_job_2 + wcet_m_2_job_2 + wcet_m_0_job_2
 & wcet_m_2_job_2 + wcet_m_0_job_2 + wcet_m_3_job_2 >= 93
 & wcet_m_4_job_2 > 20
 & 31 > wcet_m_0_job_2
 & wcet_m_4_job_2 + wcet_m_2_job_2 + wcet_m_0_job_2 + wcet_m_1_job_2 > 93
 
 Inverse method successfully finished after 15.008 seconds.
 
 Generating graphical output...
 Writing to file the states description...

 IMITATOR successfully terminated (after 17.083 seconds)