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