**************************************************
 *                  HYMITATOR 1.0                 *
 *                                   2009 - 2012  *
 *   Etienne ANDRE, Ulrich KUEHNE, Romain SOULAT  *
 *     Laboratoire Specification et Verification  *
 *                  ENS de Cachan & CNRS, France  *
 **************************************************
 Mode: inverse method.
 
 Parsing done after 0.003 second.
 Program checked and converted after 0.007 second.
 
 Computing post^1
 Computing post^2
 Computing post^3
 Computing post^4
   Adding the following inequality:
   11*a < 8*b
 Computing post^5
 Computing post^6
 Computing post^7
 Computing post^8
 Computing post^9
 
 Final constraint K  :
   8*b > 11*a
 
 Fixpoint reached after 9 iterations in 0.024 second: 24 reachable states with 42 transitions.
 
 Final constraint K0 :
   a >= 0
 & 8*b > 11*a

 HYMITATOR successfully terminated (after 0.175 second)