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


//Vars
[0, 15.0] time;
[-1000,1000] x;
[-1000,1000] y;
[-1000,1000] z;



// start modes
// l1
{
  mode 1;
  invt:
  flow:
    d/dt[x] = -9.0 * (x - 2.0) - 7.0 * (y + 2.0) + z - 1.0 + 0.2 * (x - 2.0) * (y + 2.0) + 0.1 * (y + 2.0) * (z - 1.0) + 0.1 * (x - 2.0) * (z - 1.0) + 0.5 * (z - 1.0) * (z - 1.0);
    d/dt[y] = 6.0 * (x - 2.0) + 4.0 * (y + 2.0) + z - 1.0;
    d/dt[z] = 3.0 * (x - 2.0) + 2.0 * (y + 2.0) - 2.5 * (z - 1.0);

  jump:
    // l1 -> l2 (1 -> 2)
      (and (1.7 <= x) (and (x <= 2.3) (and (-2.3 <= y) (and (y <= -1.7) (and (0.7 <= z) (z <= 1.3)))))) ==> @2(and (x' = x) (y' = y) (z' = z));

  // end l1
}

// l2
{
  mode 2;
  invt:
  flow:
    d/dt[x] = 2.2 * x + 3.6 * y + 3.9 * z;
    d/dt[y] = 3.0 * x + 2.4 * y + 3.4 * z - 0.01 * x * x;
    d/dt[z] = -5.0 * x - 5.4 * y - 6.7 * z;

  jump:

  // end l2
}
// end modes

init:
@1 (and (and (and (and (and (x >= 3.0) (x <= 3.5)) (y >= -3.0)) (y <= -2.5)) (z >= 0.9)) (z <= 1.3));

goal:
@1 (and (and (and (and (and (x >= 3.0) (x <= 3.5)) (y >= -3.0)) (y <= -2.5)) (z >= 0.9)) (z <= 1.3));
