-------------------------------------------------------------------------------- -- -- Temperature control system from -- Alur et al.: The algorithmic analysis of hybrid systems. -- -- Author : Christian Herde -- -- Last Modified : -- Fri Dec 12 16:00:00 CET 2008 -- -------------------------------------------------------------------------------- DECL boole flow; boole v0, v1, v2, v3; float [0.0, 100.0] dt; float [-100.0, 100.0] x1, x2, th; INIT -- Characterization of initial state. flow; v0 and !v1 and !v2 and !v3; x1 = 6.0; x2 = 6.0; TRANS -- Alternation between flows and jumps. flow <-> !flow'; -- Possible successor locations. (!flow and v0) -> (v1' or v2' or v3'); (!flow and v1) -> v0'; (!flow and v2) -> v0'; (!flow and v3) -> false; (flow and v0) -> v0'; (flow and v1) -> v1'; (flow and v2) -> v2'; (flow and v3) -> v3'; -- Flows. v0 and v0' -> (x1' = x1 + dt and x2' = x2 + dt and th' >= th + 0.9 * dt and th' <= th + 1.1 * dt and th' <= 15.0 and dt > 0.0); v1 and v1' -> (x1' = x1 + dt and x2' = x2 + dt and th' >= th - 4.1 * dt and th' <= th - 3.9 * dt and th' >= 3.0 and dt > 0.0); v2 and v2' -> (x1' = x1 + dt and x2' = x2 + dt and th' >= th - 3.1 * dt and th' <= th - 2.9 * dt and th' >= 3.0 and dt > 0.0); -- Jumps. v0 and v1' -> (x1 >= 6.0 and th = 15.0 and x1' = x1 and x2' = x2 and th' = th and th' >= 3.0 and dt = 0.0); v1 and v0' -> (th = 3.0 and x1' = 0.0 and x2' = x2 and th' = th and th' <= 15.0 and dt = 0.0); v0 and v2' -> (x2 >= 6.0 and th = 15.0 and x1' = x1 and x2' = x2 and th' = th and th' >= 3.0 and dt = 0.0); v2 and v0' -> (th = 3.0 and x2' = 0.0 and x2' = x2 and th' = th and th' <= 15.0 and dt = 0.0); v0 and v3' -> (x1 < 6.0 and x2 < 6.0 and th = 15.0 and x1' = x1 and x2' = x2 and th' = th and dt = 0.0); -- At any time the automaton is exactly in one state. v0' + v1' + v2' + v3' = 1; TARGET -- Characterization of state to be reached. v3;