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