--------------------------------------------------------------------------------
--
-- HYSAT sample input file.
--
-- Author : Christian Herde
--
-- Last Modified :
-- Wed Apr 14 10:23:00 CEST 2004
--
--------------------------------------------------------------------------------
DECL
boole jump;
float [0.0, 1000.0] t;
float [0.0, 100.0] dt;
boole off, on, open; -- locations of hybrid automaton
float [-30, 30] t_i; -- temperature inside freezer cell
define t_a = 20.0; -- ambient temperature
float [0, 1] p; -- timer
float [0, 2] q; -- door needs to be kept close for at least q hours
define c_on = -16.0; -- switch-on threshold
define c_off = -20.0; -- switch-off threshold
define k_open = 2.2; -- heat transfer coefficient if door is open
define k_closed = 0.3; -- heat transfer coefficient if door is closed
define r = 3.333333333; -- r := 1 / k_closed
define c = 14.0; -- cooling rate if compressor is on
INIT
-- Characterization of initial state.
off and !on and !open;
t_i = -18.0;
q = 0.0;
p = 0.0;
t = 0.0;
TRANS
-- Accumulate dts.
t' = t + dt;
-- At any time the automaton is exactly in one state.
on' + off' + open' = 1;
-- Jumps and flows alternate.
jump' <-> !jump;
-- Jumps.
jump -> ((off and on' and t_i >= c_on and
t_i' = t_i and p' = p and q' = q) or
(on and off' and t_i <= c_off and
t_i' = t_i and p' = p and q' = q) or
(off and open' and p >= q and
t_i' = t_i and p' = 0.0) or
(on and open' and p >= q and
t_i' = t_i and p' = 0.0) or
(open and off' and t_i <= c_on and
t_i' = t_i and q' = 2.0 * p and p' = 0) or
(open and on' and t_i >= c_off and
t_i' = t_i and q' = 2.0 * p and p' = 0));
jump -> dt = 0.0;
-- Flows.
!jump ->
((off and off' and
t_i' = (t_i - t_a) * exp(-k_closed * dt) + t_a and
t_i' <= c_on and
p' = p + dt and
q' = q) or
(on and on' and
t_i' = (r * c + t_i - t_a) * exp(-k_closed * dt) - r * c + t_a and
t_i' >= c_off and
p' = p + dt and
q' = q) or
(open and open' and
t_i' = (t_i - t_a) * exp(-k_open * dt) + t_a and
p' = p + dt and
p' <= 0.05 and
q' = q));
!jump -> dt > 0.0;
TARGET
-- Characterization of state to be reached.
t_i >= 0.0;