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

-- The action sync is used in order to make all the actions (separated by [])
-- in fact atomic; otherwise there are (internal) states in which some of the
-- choices are not available; partially this is due to the fact that some
-- actions synchronise all processes (mw), some 2 of them (mr)
-- and some can be executed by a single process (cl, r, w, ..)

-- The structure of the process PJ is the same as that of PI except that
-- there are no message via the diagnostic port "diag": initially synchronize
-- with everybody on sync; then repeat for ever synchronize on one of the
-- possible actions (either as a sender, a receiver or "let pass") and then
-- synchronize on sync.

-- In this module, the abstraction from all local variables of process P(ind)
-- is done by hand by eliminating them from the program. This is much more
-- efficient with the version of CAESAR used in the 90s.

-- In all local actions (not in mw) the paramenter el:ELEM is uniformly
-- forced to be "eps", as all transitions can take place with none or with 
-- all possible values of el. However, due to artificial synchronisation
-- of all processes on all actions (also local ones), the elimination of
-- a parameter would imply the obligation to change the description of the
-- other processes.

module PJ_SSVAR_EPS_OUT (TYPES_COMMON) is

process PJ [sync                 : NONE, 
            w, r, mw, cu, mr, cl : INDEX_ELEM_CHANNEL] (ind : index) is
   var el : ELEM, j : INDEX, AD : SET_OF_ELEM, Output : BUF_OF_ELEM in
      AD := empt_s;  
      Output := empt_b;
      loop
         sync;
         alt
            -- WRITE
            el := any ELEM;
            w (ind, el) where notIsIn (AD, el) and datum (ind, el);
            AD := Insert (AD, el);
            Output := Enqueue (Output, el, false)
          []
            -- READ
            r (ind, eps)
          []
            -- MEMORY_WRITE
            el := any ELEM;
            alt
               mw (ind, el)
                  where first (Output, el) and
                        not ((el == eps) or empty (Output));
               Output := Dequeue (Output)
            []
               mw (ind, el)
                  where first (Output, el) and ((el == eps) or empty (Output))
            end alt
          []
            -- mw from another process
            mw (?j, ?any ELEM) where not (j == ind)
          []
            -- CACHE_UPDATE
            cu (ind, eps)
          []
            -- MEMORY_READ
            mr (ind, eps)
          []
            -- CLEAR_CACHE
            cl (ind, eps)
          []
            -- PASSIVE SYNCHRONISATIONS
            -- synchronizes all processes on all actions in order to guarantee 
            -- the update of the variables directly after each step
            r (?j, ?any ELEM) where not(j == ind)
          []
            w (?j, ?any ELEM) where not (j == ind)
          []
            cu (?j, ?any ELEM) where not (j == ind)
          []
            mr (?j, ?any ELEM) where not (j == ind)
          []
            cl (?j, ?any ELEM) where not (j == ind)
         end alt
      end loop
   end var
end process

end module