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 xo <= 21.0 and yo <= 55.0 resume 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 xo >= 24.0 or yo >= 75.0 resume Off;
  returns xo, yo;
tel

node top (ix, iy : real) returns (probe x, probe y : real ; safe, stabilized : bool)
var
  mem: bool;
  reached: bool;
  safe_init : bool;
  temp: bool;
let
  assume init_cond: ix = iy and iy < 80. and iy > 0.;

  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: not safe;
  guarantee g2: not stabilized;

tel

node test(i: int) returns (a, b, c: int; exit: bool)
var
  x, y: real;
let
  x, y = heater (25.0 -> pre x, 25.0 -> pre y);
  a = int(100. * x);
  b = int(100. * y);
  c = 0;
  exit = (i >= 10000);
tel