(******************************************************************************
 *                 Directory-based cache coherency protocol
 *-----------------------------------------------------------------------------
 *   INRIA - Unite de Recherche Rhone-Alpes
 *   655, avenue de l'Europe
 *   38330 Montbonnot Saint Martin
 *   FRANCE
 *-----------------------------------------------------------------------------
 *   Module       :       cache.lnt
 *   Authors      :       A. Kriouile and W. Serwe
 *   Version      :       1.1
 *   Date         :       2012/05/15 15:58:21
 *****************************************************************************)

module cache is

(******************************************************************************
 * Data types
 *****************************************************************************)

type EVENT_T is
   E1, E2
   with ==, <>
end type

-------------------------------------------------------------------------------

type AGENT_T is
   AGENT_1, AGENT_2, AGENT_3
   with ==, <>
end type

-------------------------------------------------------------------------------

type LINE_T is
   L1, L2, L3
   with ==, <>
end type

-------------------------------------------------------------------------------

function ISLOCAL (L : LINE_T, A : AGENT_T) : BOOL is
   case L in
        L1 -> return (A == AGENT_1)
      | L2 -> return (A == AGENT_2)
      | L3 -> return (A == AGENT_3)
   end case
end function

-------------------------------------------------------------------------------

function ISALLOWEDLINE (L : LINE_T) : BOOL is
   case L in 
        L1  -> return true
      | any -> return false
   end case
end function

-------------------------------------------------------------------------------

type STATUS_T is
   S0, S1, S2
   with ==, <>
end type

-------------------------------------------------------------------------------

function NORMAL (S : STATUS_T, A : AGENT_T) : BOOL is
   case A in
        AGENT_1 -> return true
      | any     -> return (S == S2)
   end case
end function
   
(*****************************************************************************
 * Channel types
 *****************************************************************************)

channel LINE_STATUS_CHANNEL is
   (LINE : LINE_T, STATUS : STATUS_T, AGENT : AGENT_T)
end channel

-------------------------------------------------------------------------------

channel ACTION_EVENT_CHANNEL is
   (AGENT : AGENT_T, EVENT : EVENT_T, LINE : LINE_T)
end channel

(*****************************************************************************
 * Processes
 *****************************************************************************)

process MAIN [ACTION_EVENT    : ACTION_EVENT_CHANNEL,
              GET_LINE_STATUS,
              PUT_LINE_STATUS : LINE_STATUS_CHANNEL]
is
   par GET_LINE_STATUS, PUT_LINE_STATUS in
      par
         AGENT [ACTION_EVENT, GET_LINE_STATUS, PUT_LINE_STATUS] (AGENT_1)
      ||
         AGENT [ACTION_EVENT, GET_LINE_STATUS, PUT_LINE_STATUS] (AGENT_2)
      ||
         AGENT [ACTION_EVENT, GET_LINE_STATUS, PUT_LINE_STATUS] (AGENT_3)
      end par
   ||
      REMOTE_DIRECTORY [GET_LINE_STATUS, PUT_LINE_STATUS]
   end par
end process

-------------------------------------------------------------------------------

process REMOTE_DIRECTORY [GET_LINE_STATUS,
                          PUT_LINE_STATUS : LINE_STATUS_CHANNEL]
is
   var LINE : LINE_T,
       SL1, SL2, SL3,STATUS : STATUS_T,
       AGL1, AGL2, AGL3, AGENT : AGENT_T
   in
      SL1:= S0; SL2:= S0; SL3 := S0;
      AGL1 := AGENT_1; AGL2 := AGENT_2; AGL3 := AGENT_3;
      loop
         alt
 	    GET_LINE_STATUS (?LINE, ?STATUS, ?AGENT) where
	       (((LINE == L1) and (STATUS == SL1) and (AGENT == AGL1)) or
                ((LINE == L2) and (STATUS == SL2) and (AGENT == AGL2)) or
                ((LINE == L3) and (STATUS == SL3) and (AGENT == AGL3)))
               and NORMAL (STATUS, AGENT)
          []
            PUT_LINE_STATUS (?LINE, ?STATUS, ?AGENT) where
               NORMAL (STATUS, AGENT);
            case LINE in
                 L1 -> SL1 := STATUS; AGL1 := AGENT
	       | L2 -> SL2 := STATUS; AGL2 := AGENT
	       | L3 -> SL3 := STATUS; AGL3 := AGENT
            end case
         end alt
      end loop      
   end var
end process

-------------------------------------------------------------------------------

process AGENT [ACTION_EVENT : ACTION_EVENT_CHANNEL,
               GET_LINE_STATUS,
               PUT_LINE_STATUS : LINE_STATUS_CHANNEL] (AGENT_ID : AGENT_T)
is
   var EVENT:EVENT_T, LINE:LINE_T, STATUS:STATUS_T, AGENT:AGENT_T in 
      loop
         ACTION_EVENT (AGENT_ID,?EVENT,?LINE) where ISALLOWEDLINE (LINE);
         GET_LINE_STATUS (LINE, ?STATUS,?AGENT);
         case EVENT in
              E1 -> if ISLOCAL (LINE,AGENT_ID) then
                       case STATUS in
                            S0 | S1 -> PUT_LINE_STATUS (LINE, S1, AGENT_ID)
                          | S2      -> if (AGENT == AGENT_ID) then
                                          PUT_LINE_STATUS (LINE, S2, AGENT_ID)
                                       else
                                          PUT_LINE_STATUS (LINE, S1, AGENT_ID)
                                       end if 
                       end case
                    else
                       PUT_LINE_STATUS (LINE, S1, AGENT_ID)
                    end if
            | E2 -> PUT_LINE_STATUS (LINE, S2, AGENT_ID)
         end case
      end loop
   end var
end process

end module