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


//Vars
[0, 20.0] time;
[-1000,1000] x;
[-1000,1000] clock;
[-1000,1000] tglobal;

#define eps	0.1
#define tmax	20.0


// start modes
// loc1
{
  mode 1;
  invt:
    (and (x <= 10.0) (and (clock <= tmax) (tglobal <= tmax)));
  flow:
    d/dt[x] = 1.0;
    d/dt[clock] = 1.0;
    d/dt[tglobal] = 1.0;

  jump:
    // loc1 -> loc2 (1 -> 2)
      (and (x >= 9.0) (clock >= eps)) ==> @2(and (x' = x) (clock' = clock) (tglobal' = tglobal));

  // end loc1
}

// loc2
{
  mode 2;
  invt:
    (and (x >= 2.0) (and (clock <= tmax) (tglobal <= tmax)));
  flow:
    d/dt[x] = -2.0;
    d/dt[clock] = 1.0;
    d/dt[tglobal] = 1.0;

  jump:
    // loc2 -> loc1 (2 -> 1)
      (and (x <= 3.0) (clock >= eps)) ==> @1(and (x' = x) (clock' = clock) (tglobal' = tglobal));

  // end loc2
}
// end modes

init:
@1 (and (and (x = 5.0) (clock = 0.0)) (tglobal = 0.0));

goal:
@1 (and (and (x = 5.0) (clock = 0.0)) (tglobal = 0.0));
