diff options
author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-30 09:54:46 +0200 |
---|---|---|
committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-07-30 09:54:46 +0200 |
commit | 818c737eb01abe1a47894c1fbfc35c3a3af804ef (patch) | |
tree | 07eabe71e340a26d2b46251ae14bff29c364ac61 /tests/source | |
parent | 96c8e33777663aa79e3dc7bbf3860ee250f602d4 (diff) | |
download | scade-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.scade | 24 |
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 |