-------------------------------------------------------------------------------- -- -- 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;