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