blob: c9212e93bf282e6a398de7a6d93e0e2c0ae2954e (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
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
|