(******************************************************************************
 *             Sequentially consistent, distributed cache memory
 *-----------------------------------------------------------------------------
 *   INRIA - Unite de Recherche Rhone-Alpes
 *   655, avenue de l'Europe
 *   38330 Montbonnot Saint Martin
 *   FRANCE
 *-----------------------------------------------------------------------------
 *   Module       :       S4.lnt
 *   Authors      :       A. Kriouile and W. Serwe
 *   Version      :       1.2
 *   Date         :       2017/10/04 15:25:12
 *****************************************************************************)

-- LNT program describing property S4, which says that the first cache
-- update of E1 and E2 takes place in the same order in processes 1 and 2

-- The property is described by two processes that first synchronize to fix
-- the order in which they both execute the cache updates, and then they
-- asynchronously cache update the two elements in this order, where each
-- cache update may be repeated indefinitely

module S4 (ELEM_E12_4P) is

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

process MAIN [CU : any] is
   hide sync : any in
      par sync in
         P [sync, CU] (1 of INDEX) 
      || P [sync, CU] (2 of INDEX)
      end par
   end hide
end process

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

process P [sync, CU : any] (ind : INDEX) is
   alt
      sync (1 of NAT);
      CU (ind, e1);
      P1 [CU] (ind, e1);
      CU (ind, e2);
      P2 [CU] (ind)
    []
      sync (2 of NAT);
      CU (ind, e2);
      P1 [CU] (ind, e2);
      CU (ind, e1);
      P2 [CU] (ind)
   end alt
end process

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

process P1 [CU : any] (ind : INDEX, e : ELEM) is
   -- accept an arbitrary number of rendezvous of the form "CU (ind, e)"
   loop L in
      alt
	 CU (ind, e)
       []
	 break L
      end alt 
   end loop
end process

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

process P2 [CU : any] (ind : INDEX) is
   -- accept an arbitrary number of rendezvous on gate CU with first offer "ind"
   loop
      alt
         CU (ind, e1)
       []
         CU (ind, e2)
      end alt
   end loop
end process

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

end module