--------------------------------------------------------------------------------
--
-- HYSAT sample input file.
--
-- Author : Christian Herde
--
-- Last Modified :
-- Wed Apr 14 10:23:00 CEST 2004
--
--------------------------------------------------------------------------------
DECL
-- Lane.
define x0 = 0.0;
define x1 = 1.0;
define x2 = 3.0;
define x3 = 4.0;
define y0 = 0.0;
define y1 = 4.0;
define y2 = 5.0;
define y3 = 9.0;
-- Teeing-off area.
define xl = 1.5;
define yd = 0.75;
define xr = 2.5;
define yu = 1.25;
-- Position of hole.
define xh = 2.0;
define yh = 8.0;
-- Position of ball.
float [x0, x3] x;
float [y0, y3] y;
-- Horizontal component of velocity.
-- Negative values: left. Positive values: right.
float [-20, 20] vx;
-- Vertical component of velocity.
-- Negative values: down. Positive values: up.
float [-20, 20] vy;
-- Duration of a flow.
float [0.0, 10.0] dt;
-- Locations.
boole s1, s2, s3;
-- To jump or not to jump?
boole jump;
-- Minium duration of a flow. To exclude zeno trajectories.
define flow_min = 0.01;
-- By setting fg to a small negative value it is possible to slightly
-- tilt the lane such that the hole is on a higher level than the
-- teeing-off field.
define fg = -1.8;
-- If fl equals 1.0, the ball loses no energy when colliding with
-- a boundary or an obstacle. Setting it to 0.9, e.g., will cause a
-- loss of 10 per cent in the respective component of the velocity vector.
define fl = 0.6;
INIT
-- Ball is within the teeing-off area.
xl <= x; x <= xr;
yd <= y; y <= yu;
-- x = 2.0;
-- y = 1.0;
-- Motion starts with a flow in location s3.
!jump;
!s1 and !s2 and s3;
TRANS
-- At any time control is at exactly in one location.
s1' + s2' + s3' = 1;
-- The components of the velocity vector are non-zero throughout.
vx != 0 and vy != 0;
-- Jumps and flows alternate.
jump <-> !jump';
-- Jumps don't consume time. Flows do.
jump -> dt = 0;
!jump -> dt > flow_min;
-- Evolution of continuous variables during a flow.
!jump ->
(x' = x + dt * vx and
y' = y + dt * vy + 0.5 * fg * dt^2 and
vx' = vx and
vy' = vy + dt * fg);
-- Flows have to preserve the location invariants.
!jump ->
(x0 <= x' and x' <= x3);
(!jump and s1) ->
(y2 <= y' and y' <= y3);
(!jump and s2) ->
(y1 <= y' and y' <= y2);
(!jump and s3) ->
(y0 <= y' and y' <= y1);
-- The transition relation only talks about start- and endpoints
-- of trajectories, not about the states in-between. We have to make
-- sure that a trajectory does not leave the region defined by the
-- location invariants, thereafter returning to it.
!(!jump and s3 and y' = y1 and vy' < 0);
!(!jump and s2 and y' = y2 and vy' < 0);
!(!jump and s1 and y' = y3 and vy' < 0);
-- Flows do not change the location.
(!jump and s1) -> s1';
(!jump and s2) -> s2';
(!jump and s3) -> s3';
-- Jumps do not change the position of the ball.
jump -> (x' = x and y' = y);
-- Jumps only happen on boundaries.
(jump and s1) -> (x = x0 or x = x3 or y = y3 or y = y2);
(jump and s2) -> (x = x0 or x = x3 or y = y2 or y = y1);
(jump and s3) -> (x = x0 or x = x3 or y = y1 or y = y0);
-- We cannot jump from s1 to s3 or from s3 to s1.
(jump and s1) -> (s1' or s2');
(jump and s3) -> (s3' or s2');
-- How do jumps modify the state?
-- Horizontal component.
(jump and x = x0 and vx < 0) -> vx' = -fl * vx;
(jump and x = x3 and vx > 0) -> vx' = -fl * vx;
(jump and x0 < x and x < x3) -> vx' = vx;
-- We never hit a lower boundary while moving upward.
(jump and s1 and y = y2 and vy > 0) -> false;
(jump and s2 and y = y1 and vy > 0) -> false;
(jump and s3 and y = y0 and vy > 0) -> false;
-- We never hit an upper boundary while moving downward.
(jump and s1 and y = y3 and vy < 0) -> false;
(jump and s2 and y = y2 and vy < 0) -> false;
(jump and s3 and y = y1 and vy < 0) -> false;
-- How do jumps modify the state?
-- Vertical component.
(jump and s1 and y = y3 and vy > 0) -> (s1' and vy' = -fl * vy);
(jump and s1 and y = y2 and vy < 0 and x <= x2) -> (s1' and vy' = -fl * vy);
(jump and s1 and y = y2 and vy < 0 and x > x2) -> (s2' and vy' = vy);
(jump and s1 and y2 < y and y < y3) -> (s1' and vy' = vy);
(jump and s2 and y = y2 and vy > 0 and x > x2) -> (s1' and vy' = vy);
(jump and s2 and y = y2 and vy > 0 and x <= x2) -> (s2' and vy' = -fl * vy);
(jump and s2 and y = y1 and vy < 0 and x >= x1) -> (s2' and vy' = -fl * vy);
(jump and s2 and y = y1 and vy < 0 and x < x1) -> (s3' and vy' = vy);
(jump and s2 and y1 < y and y < y2) -> (s2' and vy' = vy);
(jump and s3 and y = y1 and vy > 0 and x < x1) -> (s2' and vy' = vy);
(jump and s3 and y = y1 and vy > 0 and x >= x1) -> (s3' and vy' = -fl * vy);
(jump and s3 and y = y0 and vy < 0) -> (s3' and vy' = -fl * vy);
(jump and s3 and y0 < y and y < y1) -> (s3' and vy' = vy);
TARGET
x = xh;
y = yh;