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