// Hyst v1.17
// Hybrid Automaton in dReach
// Converted from file: ../../examples/biology9d/biology9d.xml
// Command Line arguments: -dreach ../../examples/biology9d/biology9d.xml


//Vars
[0, 0.2] time;
[-1000,1000] x1;
[-1000,1000] x2;
[-1000,1000] x3;
[-1000,1000] x4;
[-1000,1000] x5;
[-1000,1000] x6;
[-1000,1000] x7;
[-1000,1000] x8;
[-1000,1000] x9;



// start modes
// running
{
  mode 1;
  invt:
  flow:
    d/dt[x1] = 50.0 * x3 - x1 * x6;
    d/dt[x2] = 100.0 * x4 - x2 * x6;
    d/dt[x3] = x1 * x6 - 50.0 * x3;
    d/dt[x4] = x2 * x6 - 100.0 * x4;
    d/dt[x5] = 500.0 * x3 + 50.0 * x1 - 10.0 * x5;
    d/dt[x6] = 50.0 * x5 + 50.0 * x3 + 100.0 * x4 - x6 * (x1 + x2 + 2.0 * x8 + 1.0);
    d/dt[x7] = 50.0 * x4 + 0.01 * x2 - 0.5 * x7;
    d/dt[x8] = 5.0 * x7 - 2.0 * x6 * x8 + x9 - 0.2 * x8;
    d/dt[x9] = 2.0 * x6 * x8 - x9;

  jump:

  // end running
}
// end modes

init:
@1 (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (x1 >= 0.09) (x1 <= 0.11)) (x2 >= 0.09)) (x2 <= 0.11)) (x3 >= 0.09)) (x3 <= 0.11)) (x4 >= 0.09)) (x4 <= 0.11)) (x5 >= 0.09)) (x5 <= 0.11)) (x6 >= 0.09)) (x6 <= 0.11)) (x7 >= 0.09)) (x7 <= 0.11)) (x8 >= 0.09)) (x8 <= 0.11)) (x9 >= 0.09)) (x9 <= 0.11));

goal:
@1 (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (x1 >= 0.09) (x1 <= 0.11)) (x2 >= 0.09)) (x2 <= 0.11)) (x3 >= 0.09)) (x3 <= 0.11)) (x4 >= 0.09)) (x4 <= 0.11)) (x5 >= 0.09)) (x5 <= 0.11)) (x6 >= 0.09)) (x6 <= 0.11)) (x7 >= 0.09)) (x7 <= 0.11)) (x8 >= 0.09)) (x8 <= 0.11)) (x9 >= 0.09)) (x9 <= 0.11));
