(******************************************************************************
 *             Sequentially consistent, distributed cache memory
 *-----------------------------------------------------------------------------
 *   INRIA - Unite de Recherche Rhone-Alpes
 *   655, avenue de l'Europe
 *   38330 Montbonnot Saint Martin
 *   FRANCE
 *-----------------------------------------------------------------------------
 *   Module       :       MEMORY_FONC_T.lnt
 *   Authors      :       A. Kriouile, W. Serwe, and H. Garavel
 *   Version      :       1.3
 *   Date         :       2016/01/08 11:32:13
 *****************************************************************************)

module MEMORY_FONC_T (TYPES_COMMON) is

process MEMORY [sync   : NONE, 
                mw, mr : INDEX_ELEM_CHANNEL] (in var M : MEM_OF_ELEM) is
   var el : ELEM in
      loop
         sync;
         alt
            mw (?any INDEX, ?el);
            M := Insert (M, el)
          []
            el := any ELEM;
            mr (?any INDEX, el) where ok (M, el)
	  []
	    null
         end alt
      end loop
   end var
end process

end module