diff options
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 |