-------------------------------------------------------------------------------- -- -- Water-level monitor from -- Alur et al.: The algorithmic analysis of hybrid systems. -- -- Author : Christian Herde -- -- Last Modified : -- Fri Dec 12 16:00:00 CET 2008 -- -------------------------------------------------------------------------------- DECL -- Variables have to be declared before first use. boole flow; boole v0, v1, v2, v3; float [0.0, 10.0] dt; float [0.0, 20.0] x, y; INIT -- Characterization of initial state. flow; v0 and !v1 and !v2 and !v3; y = 1; x = 0; TRANS -- Alternation between flows and jumps. flow <-> !flow'; -- Possible successor locations. (!flow and v0) -> v1'; (!flow and v1) -> v2'; (!flow and v2) -> v3'; (!flow and v3) -> v0'; (flow and v0) -> v0'; (flow and v1) -> v1'; (flow and v2) -> v2'; (flow and v3) -> v3'; -- Flows. v0 and v0' -> (x' = x + dt -- successor value of x and y' = y + dt -- succsssor value of y and y' <= 10.0 -- location invariant of v0 and dt > 0.0); -- flows consume time v1 and v1' -> (x' = x + dt and y' = y + dt and x' <= 2.0 and dt > 0.0); v2 and v2' -> (x' = x + dt and y' = y - 2 * dt and y' >= 5.0 and dt > 0.0); v3 and v3' -> (x' = x + dt and y' = y - 2 * dt and x' <= 2.0 and dt > 0.0); -- Jumps. v0 and v1' -> (y = 10.0 -- guard and x' = 0 -- action and y' = y -- implicit action and x' <= 2 -- invariant of target location and dt = 0.0); -- jumps do not consume time v1 and v2' -> (x = 2.0 and x' = x and y' = y and y' >= 5 and dt = 0.0); v2 and v3' -> (y = 5.0 and x' = 0 and y' = y and x' <= 2 and dt = 0.0); v3 and v0' -> (x = 2.0 and x' = x and y' = y and y' <= 10 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. v0 and y = 0;