```// **************************************************************************
//
//    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.
//
// BallHoles describes the case that the wind speed is a constant value.
//
// The example has been taken from the following reference:
//
// **************************************************************************

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

module BallHoles(
real ?a_x, ?Vx_init, ?Vy_init, ?c
) {
hybrid real Vx,Vy,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;
}until(((cont(H) <= 0.0)&(cont(Vy) <= 0.0)));
if ((cont(H)<= 0.0)&(cont(Vy) <= 0.0)) {
//Case 1: the ball hits the ground
next(a) = a_x; next(Vy) = -c*Vy; next(n) = n+1;
} else {
//Case 2: the ball does not hit the ground
next(Vy) = -c*Vy; next(n) = n+1;
}
}
pause;
} satisfies {
// Specify sequence property
assert EF (exists(i = 0..N-1) ((S_min[i]<=B)&(B<=S_max[i])&(H<=0.0));
}
```