summaryrefslogtreecommitdiff
path: root/tests/source
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-30 09:54:46 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-30 09:54:46 +0200
commit818c737eb01abe1a47894c1fbfc35c3a3af804ef (patch)
tree07eabe71e340a26d2b46251ae14bff29c364ac61 /tests/source
parent96c8e33777663aa79e3dc7bbf3860ee250f602d4 (diff)
downloadscade-analyzer-818c737eb01abe1a47894c1fbfc35c3a3af804ef.tar.gz
scade-analyzer-818c737eb01abe1a47894c1fbfc35c3a3af804ef.zip
The heater example is not a very good example...
Diffstat (limited to 'tests/source')
-rw-r--r--tests/source/tst_heater.scade24
1 files changed, 18 insertions, 6 deletions
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