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