Counterexample
==============

goal: f3
formula: ([][0,5] ((on1 > 0.5) -> (<>[0,1] (x1 >= 30))))
bound: 2
delta: 0.0

Constants
---------
c0 = 0.98
c1 = 0.97
d0 = 0.01
d1 = 0.03
h0 = 100
h1 = 200
k0 = 0.015
k1 = 0.045

Variables
---------
x0: [10.0, 35.0]
x1: [10.0, 35.0]

Initial condition
-----------------
(and (on0 = 0) (x0 = 20) (on1 = 0) (x1 = 18))

Bound 0
-------
time: 0.0 -> 3.2283774193217525
mode: (and (on0 = 0) (on1 = 0))

invariant:
  (and (x0 > 10) (x1 > 10))

flow:
  d/dt[x0] = ((- 0.015) * ((0.98 * x0) - (0.01 * x1)))
  d/dt[x1] = ((- 0.045) * ((0.97 * x1) - (0.03 * x0)))

state:
  x0: 20.0 -> 19.08098236175477
  x1: 18.0 -> 15.71345614453407

next mode: (and (on0 = 0) (on1 = 1))
jump candidates:
  (x0 <= 17) => (and (on0' = 1) (on1' = on1) (x0' = x0) (x1' = x1))
  (x1 <= 16) => (and (on1' = 1) (on0' = on0) (x0' = x0) (x1' = x1))

Bound 1
-------
time: 3.2283774193217525 -> 4.496277878089819
mode: (and (on0 = 0) (on1 = 1))

invariant:
  (and (10 < x0) (x1 < 30))

flow:
  d/dt[x0] = ((- 0.015) * ((0.98 * x0) - (0.01 * x1)))
  d/dt[x1] = (0.045 * (200 - ((0.97 * x1) - (0.03 * x0))))

state:
  x0: 19.08098236175477 -> 18.73258397375819
  x1: 15.71345614453407 -> 26.000000353359702

next mode: (and (on0 = 0) (on1 = 0))
jump candidates:
  (x0 <= 17) => (and (on0' = 1) (on1' = 0) (x0' = x0) (x1' = x1))
  (x1 >= 26) => (and (on1' = 0) (on0' = on0) (x0' = x0) (x1' = x1))

Bound 2
-------
time: 4.496277878089819 -> 10.0
mode: (and (on0 = 0) (on1 = 0))

invariant:
  (and (x0 > 10) (x1 > 10))

flow:
  d/dt[x0] = ((- 0.015) * ((0.98 * x0) - (0.01 * x1)))
  d/dt[x1] = ((- 0.045) * ((0.97 * x1) - (0.03 * x0)))

state:
  x0: 18.73258397375819 -> 17.295066951588694
  x1: 26.000000353359702 -> 20.566196553837255