************************************************** * HYMITATOR 1.0 * * 2009 - 2012 * * Etienne ANDRE, Ulrich KUEHNE, Romain SOULAT * * Laboratoire Specification et Verification * * ENS de Cachan & CNRS, France * ************************************************** Plot variables x, y Mode: inverse method. Parsing done after 0.022 second. Program checked and converted after 0.025 second. Computing post^1 Computing post^2 Adding the following inequality: 15 < 11*v0 Final constraint K : 11*v0 > 15 Fixpoint reached after 2 iterations in 0.008 second: 3 reachable states with 3 transitions. Plotting reachable states projected on variables x, y Final constraint K0 : 11*v0 > 15 & 5 >= 3*v0 HYMITATOR successfully terminated (after 0.324 second)