From 818c737eb01abe1a47894c1fbfc35c3a3af804ef Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ansys.com>
Date: Wed, 30 Jul 2014 09:54:46 +0200
Subject: The heater example is not a very good example...

---
 tests/source/tst_heater.scade | 24 ++++++++++++++++++------
 1 file changed, 18 insertions(+), 6 deletions(-)

(limited to 'tests/source')

diff --git a/tests/source/tst_heater.scade b/tests/source/tst_heater.scade
index c9212e9..3b34965 100644
--- a/tests/source/tst_heater.scade
+++ b/tests/source/tst_heater.scade
@@ -11,7 +11,7 @@ let
       yo = -3.0 * yi * dt + yi;
     tel
     until 
-      if xi <= 21.0 and yi <= 55.0 restart On;
+      if xo <= 21.0 and yo <= 55.0 resume On;
 
     state On
     --unless 
@@ -21,20 +21,21 @@ let
       yo = 2.0 * (150.0 - yi) * dt + yi;
     tel
     until 
-      if xi >= 24.0 or yi >= 75.0 restart Off;
+      if xo >= 24.0 or yo >= 75.0 resume Off;
   returns xo, yo;
 tel
 
-node top (ix, iy : real) returns (x,y : real ; safe, stabilized : bool)
+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;
+  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;
 
@@ -47,7 +48,18 @@ let
 
   stabilized = not mem or temp;
 
-  guarantee g1: safe;
-  guarantee g2: stabilized;
+  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
-- 
cgit v1.2.3