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