--------------------------------------------------------------------------------
--
-- HySAT model of a bouncing ball.
--
-- Author : Christian Herde
--
-- Last Modified :
-- Tue Nov 29 11:22:05 CET 2005
--
--------------------------------------------------------------------------------
--
-- We consider the motion of a bouncing ball which is dropped from an
-- initial hight and which is given a certain initial velocity in horizontal
-- direction. As the ball falls it is accelerated in vertical direction
-- by gravity. The moment when the ball contacts the ground is modeled
-- as a discrete transition ('jump') where the ball loses a certain fraction
-- of its energy. The task of the solver is to find an initial hight and an
-- initial velocity so that the ball hits a hole which is located
-- at a certain distance xh_hole from the starting point. To exclude trivial
-- solutions - those where the ball does not bounce at all - the initial
-- hight and velocity are upper bounded by xv_limit and yh_limit.
--
-- We assume that the ball is moving in horizontal direction with a constant
-- velocity which only changes when the ball hits the ground, i.e. dxh/dt = yh
-- where xh is the horizontal position of the ball and yh is its horizontal
-- velocity. If time advances by an interval of dt, the successor value of xh
-- is given by
--
-- xh_{t+dt} = xh_t + dt * yh_t
--
-- The vertical dynamics of the continuous behaviour of the bouncing ball is
-- given by dxv/dt = yv and dyv/dt = -g, i.e. by dxv/dyv = yv/-g, where
-- xv and yv are the vertical position and the vertical velocity of the ball
-- and g is the acceleration of earth.
--
-- The exact successor values when time advances by an interval of dt are
-- xv_{t+dt} = xv_t + (dt * yv_t - 0.5 * g * dt^2) and
-- yv_{t+dt} = yv_t - dt * g.
--
-- As opposed to this, euler integration yields
-- xvp_{t+dt} = xv_t + dt * yv_t and
-- yvp_{t+dt} = yv_t - dt * g.
--
-- Thus, euler integration entails the following approximation error:
-- xv_{t+dt} - xvp_{t+dt} = -0.5 * g * dt^2
-- yv_{t+dt} - yvp_{t+dt} = 0
--
-- As -0.5 * g * dt^2 is a term which does not vary over time we
-- can subtract it from xvp_{t+dt} which leaves us with an exact linear
-- model of the continuous behaviour of the bouncing ball.
--
--------------------------------------------------------------------------------
DECL
boole jump; -- true iff ball bounces
int [0, 15] n; -- bounce counter
float [0.0, 10000] t; -- global time
float [-100.0, 100.0] xv; -- vertical position of the ball
float [-100.0, 100.0] yv; -- vertical velocity of the ball
float [-100.0, 100.0] xh; -- horizontal position of the ball
float [-100.0, 100.0] yh; -- horizontal velocity of the ball
define dt = 0.2; -- discrete time adances in steps of size dt
define g = 9.8; -- gravitational acceleration on earth
define lv = 0.3; -- loss of speed in vertical direction
define lh = 0.1; -- loss of speed in horizontal direction
define xv_limit = 15.0; -- upper bound of the initial hight
define vh_limit = 5.0; -- upper bound of the initial horizontal speed
define xh_hole = 40.0; -- position of the hole
INIT
-- Conditions at the moment when ball is dropped.
xv <= xv_limit;
yv = 0.0;
xh = 0.0;
yh <= vh_limit;
n = 0;
t = 0.0;
TRANS
-- A jump occurs if the heigth of the ball is zero and the velocity
-- is directed towards the ground.
jump <-> (xv <= 0.0 and yv < 0.0);
-- Continuous part of the dynamics.
!jump ->
(xv' = xv + dt * yv - 0.5 * g * dt^2 and
yv' = yv - dt * g and
xh' = xh + dt * yh and
yh' = yh and
n' = n and
t' = t + dt);
-- Discrete part of the dynamics.
jump ->
(xv' = 0.0 and
yv' = -(1.0 - lv) * yv and
xh' = xh and
yh' = (1.0 - lh) * yh and
n' = n + 1 and
t' = t);
TARGET
-- The ball shall hit the hole on ground level.
xh = xh_hole and xv = 0.0;