************************************************************
 *  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/full_cpr08.imi
 Mode: inverse method.
 Merging technique of [AFS12] enabled.
 Graphical output will be generated.
 Log (description of states) will be generated.
 *** Warning: Considering a limit of 30 for the depth of the Post operation.
 
 Parsing completed after 0.005 second.
 Memory for abstract program: 378.3046875 KB (i.e., 96846. words)
 The model contains stopwatches.
 
 Computing post^1 from 1 state.
   Adding the following inequality:
   O_2 > 0
 Computing post^2 from 2 states.
   Adding the following inequality:
   O_2 < 10
   Adding the following inequality:
   6 < C_1 + C_2
 Computing post^3 from 5 states.
   Adding the following inequality (randomly selected among 2 inequalities):
   O_2 + 6 < 2*C_1 + C_2
 Computing post^4 from 8 states.
 Computing post^5 from 8 states.
   Adding the following inequality:
   C_1 < 5
 Computing post^6 from 12 states.
 Computing post^7 from 16 states.
   Adding the following inequality:
   7 < 3*C_1
 Computing post^8 from 14 states.
 Computing post^9 from 12 states.
 Computing post^10 from 9 states.
 Computing post^11 from 7 states.
 Computing post^12 from 12 states.
 Computing post^13 from 12 states.
 Computing post^14 from 9 states.
 Computing post^15 from 15 states.
 Computing post^16 from 15 states.
   Adding the following inequality:
   17 < 6*C_1
 Computing post^17 from 10 states.
 Computing post^18 from 15 states.
 Computing post^19 from 15 states.
 Computing post^20 from 11 states.
 Computing post^21 from 18 states.
 Computing post^22 from 18 states.
 Computing post^23 from 13 states.
 Computing post^24 from 21 states.
 Computing post^25 from 21 states.
 Computing post^26 from 15 states.
 Computing post^27 from 24 states.
 Computing post^28 from 24 states.
 Computing post^29 from 17 states.
 Computing post^30 from 27 states.
 *** Warning: The limit depth (30) has been reached. The exploration now stops, although there were still 27 states to explore.
 
 Fixpoint reached after 31 iterations: 369 reachable states with 485 transitions.
 Analysis may have been non-deterministic:
 1 random selection have been performed.
 
 Final constraint K0  (10 inequalities):
  O_2 + C_2 > 6
 & 3 >= O_2
 & 6 >= C_2
 & 6*O_2 > 17
 & O_1 = 0
 & O_2 = C_1
 & D_1 = 7
 & D_2 = 6
 & T_1 = 10
 & T_2 = 10
 
 Inverse method successfully finished after 6.301 seconds.
 
 Generating graphical output...
 Writing to file the states description...

 IMITATOR successfully terminated (after 7.009 seconds)