# Hyst v1.17
# Hybrid Automaton in Flow*
# Converted from: ../../examples/biology9d/biology9d.xml
# Using command line arguments: -flowstar ../../examples/biology9d/biology9d.xml


hybrid reachability
{
  # Vars
  state var x1, x2, x3, x4, x5, x6, x7, x8, x9

  setting
  {
    fixed steps .001
    time .2
    remainder estimation 1e-4
    identity precondition
    gnuplot octagon x1,x2
    adaptive orders { min 3, max 8 } 
    cutoff 1e-15
    precision 53
    output out
    max jumps 99999999
    print on
  }

  modes
  {
    running
    {
      poly ode 3
      {
        x1' = 50.0 * x3 - x1 * x6
        x2' = 100.0 * x4 - x2 * x6
        x3' = x1 * x6 - 50.0 * x3
        x4' = x2 * x6 - 100.0 * x4
        x5' = 500.0 * x3 + 50.0 * x1 - 10.0 * x5
        x6' = 50.0 * x5 + 50.0 * x3 + 100.0 * x4 - x6 * (x1 + x2 + 2.0 * x8 + 1.0)
        x7' = 50.0 * x4 + 0.01 * x2 - 0.5 * x7
        x8' = 5.0 * x7 - 2.0 * x6 * x8 + x9 - 0.2 * x8
        x9' = 2.0 * x6 * x8 - x9
      }
      inv
      {
      }
    }
  }

  jumps
  {
  }

  init
  {
    running
    {
      x1 in [.09, .11]
      x2 in [.09, .11]
      x3 in [.09, .11]
      x4 in [.09, .11]
      x5 in [.09, .11]
      x6 in [.09, .11]
      x7 in [.09, .11]
      x8 in [.09, .11]
      x9 in [.09, .11]
    }
  }
}
