summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-22 09:04:13 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-22 09:04:13 +0200
commit7e1cf88f181aa0596361b5b5d784f8e4b9b19266 (patch)
treeb6a112c49083605aaea837cb7b4bcf51a9a4b89c /tests
parentbebab48e94ad156341f12fe90224e67e98477ca8 (diff)
downloadscade-analyzer-7e1cf88f181aa0596361b5b5d784f8e4b9b19266.tar.gz
scade-analyzer-7e1cf88f181aa0596361b5b5d784f8e4b9b19266.zip
Add support for octagons.
Diffstat (limited to 'tests')
-rwxr-xr-xtests/source/tst_heater.scade53
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