// ************************************************************************** // // 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 // // ************************************************************************** // // This is a toy example to demonstrate the application for checking // the boundedness of buffers that are modified by a finite state // control algorithm. // // ************************************************************************** module BoundedBuffer ( int ?guess_max_buffer, !rate_f, !rate_g, !rate_h, buffer, !max_buffer, bool guess, state_f, state_g, state_h ) { pause; state_f = true; max_buffer = guess_max_buffer; always case (state_f) do { next(state_f) = false; next(state_g) = true; next(buffer) = buffer - 1; } (state_g) do { next(state_g) = false; next(state_h) = true; next(buffer) = buffer - 1; } (state_h) do if(guess) { next(state_h) = false; next(state_f) = true; next(buffer) = buffer + 2; } else { next(state_h) = false; next(state_g) = true; next(buffer) = buffer + 1; } default nothing; } satisfies { bounded_buffer : assert E G (buffer <= max_buffer); rates_for_bounded_buffer: assert A ((G (buffer <= max_buffer)) -> (G F(6*rate_f + 3*rate_g + 2*rate_h == 0))); }