module BASIC_fifo_model_lib =
   process basic_FIFO =
        { type mess_type;
          integer size_fifo;
          %mess_type default_mess;% }
        ( ? mess_type mess_in;
          ! mess_type mess_out;
            integer nb_mess;
            boolean OK_in;
            boolean OK_out;
        )
      (| (| in_and_out := mess_in ^* mess_out
          | (| nb_mess := (znb_mess when in_and_out when OK_out)
                          default ((znb_mess + 1) when ^mess_in when OK_in)
                          default ((znb_mess - 1) when ^mess_out when OK_out)
                          default znb_mess
             | znb_mess := nb_mess$ init 0
             |)
          |)
       | (| OK_in := znb_mess < size_fifo
          | OK_out := znb_mess > 0
          |)
       | (| (| mess_in_value := mess_in cell ^nb_mess
             | zmess_in_value := mess_in_value $
             | mess_in_value ^= nb_mess ^= C_mess_in
             | C_mess_in := ^mess_in default false
             | zC_mess_in := C_mess_in $ init false
             | shifted_mess_in := zmess_in_value when zC_mess_in
             |)
          | (| sliding_buffer := shifted_mess_in window size_fifo
             | buffer := sliding_buffer cell ^nb_mess
             |)
          | mess_out := (previous_mess_out when (not OK_out) when ^mess_out)
                        default (buffer[size_fifo - znb_mess] when ^mess_out)
          | previous_mess_out := mess_out$ %init default_mess%
          |)
       |)
      where 
      event in_and_out;
      boolean C_mess_in, zC_mess_in;
      [size_fifo] mess_type sliding_buffer, buffer;
      integer znb_mess;
      mess_type mess_in_value, zmess_in_value, shifted_mess_in, previous_mess_out;
      end; 

end %BASIC_fifo_model_lib%;