**************************************************
 *  HYMITATOR 1.0                                 *
 *   Etienne ANDRE, Ulrich KUEHNE, Romain SOULAT  *
 *                                   2009 - 2012  *
 *     Laboratoire Specification et Verification  *
 *                  ENS de Cachan & CNRS, France  *
 **************************************************
 Mode: inverse method.
 *** Warning: Considering a limit of 10 for the depth of the Post operation.
 
 Parsing done after 0.007 second.
 Program checked and converted after 0.01 second.
 
 Computing post^1
   0 states merged.
 Computing post^2
   Adding the following inequality:
   C1 <= ptpPeriod
   Adding the following inequality:
   driftDelta + C2 <= D2
   Adding the following inequality:
   C2 <= audPeriod
   0 states merged.
 Computing post^3
   Adding the following inequality (randomly selected among 2 inequalities):
   0 < C2
   Adding the following inequality:
   D2 <= audPeriod + driftDelta
   Adding the following inequality:
   D2 <= ptpPeriod + driftDelta
   Adding the following inequality:
   D2 < driftDelta + C1 + C2
   Adding the following inequality:
   C1 + C2 <= ptpPeriod
   Adding the following inequality:
   audPeriod < C1 + C2
   5 states merged.
 Computing post^4
   Adding the following inequality:
   audPeriod + C1 <= ptpPeriod
   Adding the following inequality:
   C1 + 2*C2 <= ptpPeriod
   Adding the following inequality:
   C1 + 2*C2 <= 2*audPeriod
   13 states merged.
 Computing post^5
   Adding the following inequality:
   2*audPeriod < ptpPeriod
   Adding the following inequality:
   audPeriod + C1 + C2 <= ptpPeriod
   12 states merged.
 Computing post^6
   11 states merged.
 Computing post^7
   Adding the following inequality:
   ptpPeriod < 5*audPeriod
   Adding the following inequality:
   ptpPeriod + C2 <= 5*audPeriod
   Adding the following inequality:
   3*audPeriod <= ptpPeriod
   9 states merged.
 Computing post^8
   4 states merged.
 Computing post^9
   3 states merged.
 Computing post^10
   2 states merged.
 *** Warning: The limit number of iterations (10) has been reached. Post^* now stops, although there were still 3 states to explore at this iteration.
 
 Final constraint K  :
   ptpPeriod >= 3*audPeriod
 & audPeriod + driftDelta >= D2
 & C2 > 0
 & D2 >= driftDelta + C2
 & C1 + C2 > audPeriod
 & 2*audPeriod >= C1 + 2*C2
 & 5*audPeriod >= ptpPeriod + C2
 
 Fixpoint reached after 10 iterations in 2.101 seconds: 60 reachable states with 103 transitions.
 
 Final constraint K0 :
   C2 > 0
 & audPeriod >= C1
 & 2*audPeriod >= C1 + 2*C2
 & ptpPeriod >= 4*audPeriod
 & C1 + C2 > audPeriod
 & 5*audPeriod >= ptpPeriod + C2
 & audPeriod + driftDelta = D2

 HYMITATOR successfully terminated (after 2.957 seconds)