const dt : real = 0.001;

node heater(xi,yi : real) returns (xo, yo: real)
let
  automaton
    initial state Off
    --unless 
    --  if xi <= 21.0 and yi <= 55.0 restart On;
    let
      xo = -xi * dt + xi;
      yo = -3.0 * yi * dt + yi;
    tel
    until 
      if xi <= 21.0 and yi <= 55.0 restart On;

    state On
    --unless 
    --  if xi >= 24.0 or yi >= 75.0 restart Off;
    let
      xo = (100.0 - xi) * dt + xi;
      yo = 2.0 * (150.0 - yi) * dt + yi;
    tel
    until 
      if xi >= 24.0 or yi >= 75.0 restart Off;
  returns xo, yo;
tel

node top (ix, iy : real) returns (x,y : real ; safe, stabilized : bool)
var
  mem: bool;
  reached: bool;
  safe_init : bool;
  temp: bool;
let
  assume init_cond: ix = iy;

  x,y = heater (ix -> pre x, iy -> pre y);
  safe_init = (ix=iy and iy < 80.0) -> pre safe_init;
  safe = not safe_init or y < 80.0;

  reached = x >= 21.0 and x <= 24.0 and y >= 55.0 and y <= 75.0;
  temp = x>=20.0 and x<=25.0;
  
  mem = 
    (ix > 21.0 and ix < 24.0 and iy >= 55.0 and iy <= 75.0) 
    -> reached or pre mem;

  stabilized = not mem or temp;

  guarantee g1: safe;
  guarantee g2: stabilized;

tel