1 files changed, 53 insertions, 0 deletions
diff --git a/tests/source/tst_heater.scade b/tests/source/tst_heater.scade
new file mode 100755
index 0000000..c9212e9
--- /dev/null
+++ b/tests/source/tst_heater.scade
@@ -0,0 +1,53 @@
+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