// **************************************************************************
//
//    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));  
}