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


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

#define Tmax	50.0


// start modes
// off
{
  mode 1;
  invt:
    (and (x >= 18.0) (and (0.0 <= clock) (clock <= Tmax)));
  flow:
    d/dt[x] = -0.1 * x;
    d/dt[clock] = 1.0;

  jump:
    // off -> on (1 -> 2)
      (x <= 18.1) ==> @2(and (x' = x) (clock' = clock));

  // end off
}

// on
{
  mode 2;
  invt:
    (and (x <= 29.0) (and (0.0 <= clock) (clock <= Tmax)));
  flow:
    d/dt[x] = -0.1 * (x - 37.0);
    d/dt[clock] = 1.0;

  jump:
    // on -> off (2 -> 1)
      (x >= 29.0) ==> @1(and (x' = x) (clock' = clock));

  // end on
}
// end modes

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

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