```// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************
// Throwing a ball from the ground with a non-zero speed, the ball will bounce
// continuously according to the environment conditions, e.g. the wind and the
// gravity. However, there are some holes on the ground where the ball will not
// be able to bounce again if it falls into the hole. The safe region starts
// from the right hand side edge of the furthest hole to the infinite.
//
// BallHolesTs describes the case that the wind speed is sampled every Ts
// unit time.
//
// The example has been taken from the following reference:
//
// **************************************************************************

macro N =?,
S_min[N] = ?,
S_max[N] = ?;

module BallHolesTs
(
real ?a_x, ?Vx_init, ?Vy_init, ?Ts ?c
) {
hybrid real Vx,Vy,T,B,H; real a; nat n;
// Initialization configuration
Vx = Vx_init; Vy = Vy_init; a = a_x;
// Ball Bounces
loop{
// Continuous dynamics
flow{
drv(B)  <- cont(Vx); drv(Vx) <- a;
drv(H)  <- cont(Vy); drv(Vy) <- -9.8;
drv(T)  <- 1.0;
}until((cont(T) >= Ts) or ((cont(H) <= 0.0)&(cont(Vy) <= 0.0)));

if((T >= Ts) & ((cont(H)<= 0.0)&(cont(Vy) <= 0.0))) {
//Case 1: the ball hits the ground at the sample time
next(a) = a_x; next(T) = 0.0;
next(Vy) = -c*Vy; next(n) = n+1;
} else {
if((T >= Ts) & !((cont(H)<= 0.0)&(cont(Vy) <= 0.0))) {
//Case 2: sample time, the ball does not hit the ground
next(a)= a_x; next(T) = 0.0;
} else {
//Case 3: the ball hits the ground not at the sample time
next(Vy) = -c*Vy; next(n) = n+1;
}
}
pause;
}
} satisfies {// Specification
assert EF (exists(i = 0..N-1) ((S_min[i]<=B)&(B<=S_max[i])&(H<=0.0));
}
```