**************************************************
 *                  HYMITATOR 1.0                 *
 *                                   2009 - 2012  *
 *   Etienne ANDRE, Ulrich KUEHNE, Romain SOULAT  *
 *     Laboratoire Specification et Verification  *
 *                  ENS de Cachan & CNRS, France  *
 **************************************************
 Mode: abstract reachability analysis.
 
 Parsing done after 0.001 second.
 Program checked and converted after 0.003 second.
 
 Computing post^1
 Computing post^2
 Found a counterexample.
 
 Fixpoint reached after 2 iterations in 0.021 second: 4 reachable states with 5 transitions.
 Spurious counterexample!
 separating predicate: M <= w
 Computing post^1
 Computing post^2
 Computing post^3
 Found a counterexample.
 
 Fixpoint reached after 3 iterations in 0.012 second: 5 reachable states with 6 transitions.
 Spurious counterexample!
 separating predicate: w > max
 Computing post^1
 Computing post^2
 Computing post^3
 Found a counterexample.
 
 Fixpoint reached after 3 iterations in 0.024 second: 9 reachable states with 12 transitions.
 Spurious counterexample!
 separating predicate: delay + w > max + x
 Computing post^1
 Computing post^2
 Computing post^3
 Found a counterexample.
 
 Fixpoint reached after 3 iterations in 0.04 second: 10 reachable states with 14 transitions.
 Spurious counterexample!
 separating predicate: delay + M > max
 Computing post^1
 Computing post^2
 Computing post^3
 Computing post^4
 Computing post^5
 Found a counterexample.
 
 Fixpoint reached after 5 iterations in 0.068 second: 10 reachable states with 18 transitions.
 Spurious counterexample!
 separating predicate: m >= M
 Computing post^1
 Computing post^2
 Computing post^3
 Computing post^4
 Computing post^5
 Computing post^6
 Found a counterexample.
 
 Fixpoint reached after 6 iterations in 0.05 second: 7 reachable states with 11 transitions.
 Spurious counterexample!
 separating predicate: min > w
 Computing post^1
 Computing post^2
 Computing post^3
 Computing post^4
 Computing post^5
 Computing post^6
 Found a counterexample.
 
 Fixpoint reached after 6 iterations in 0.117 second: 13 reachable states with 25 transitions.
 Spurious counterexample!
 separating predicate: 2*delay + min > w + 2*x
 Computing post^1
 Computing post^2
 Computing post^3
 Computing post^4
 Computing post^5
 Computing post^6
 Found a counterexample.
 
 Fixpoint reached after 6 iterations in 0.199 second: 21 reachable states with 38 transitions.
 Spurious counterexample!
 separating predicate: 2*delay + min > m
 Computing post^1
 Computing post^2
 Computing post^3
 Computing post^4
 Computing post^5
 Computing post^6
 Computing post^7
 
 Fixpoint reached after 7 iterations in 0.117 second: 9 reachable states with 15 transitions.
 System verified SUCCESSFULLY!
 
 Final set of predicates:
 p0: 2*delay + min > m
 p1: 2*delay + min > w + 2*x
 p2: min > w
 p3: m >= M
 p4: delay + M > max
 p5: delay + w > max + x
 p6: w > max
 p7: M <= w
 Abstract initial state projected on parameters: 
   min > 0
 & delay >= 0
 & 100 >= M
 & M > m
 & 10 >= delay
 & max >= delay + M
 & m >= 2*delay + min

 HYMITATOR successfully terminated (after 0.886 second)