(******************************************************************************
 *             Sequentially consistent, distributed cache memory
 *-----------------------------------------------------------------------------
 *   INRIA - Unite de Recherche Rhone-Alpes
 *   655, avenue de l'Europe
 *   38330 Montbonnot Saint Martin
 *   FRANCE
 *-----------------------------------------------------------------------------
 *   Module       :       ELEM_E12_SAMEADDR_I.lnt
 *   Authors      :       A. Kriouile, W. Serwe, and H. Garavel
 *   Version      :       1.1
 *   Date         :       2016/05/29 10:47:11
 *****************************************************************************)

module ELEM_E12_SAMEADDR_I is
-- scenario with two processes and two elements e1 and e2

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

type INDEX is
   -- contains exactly as many elements as processes in the system
   1, 2
   with ==
end type

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

type ELEM is
   -- elements represent pairs (address, datum); as in the abstract program
   -- the actual addresses or data are not needed, it is sufficient to have
   -- functions:
   -- (a) "first" telling if two elements have the same component "address"
   -- (b) "datum" telling which process may write which elements
   eps, e1, e2
   with ==, <>, <, ord, last
   -- "<" is an arbitrary lexical order between elements different from eps
   -- which is used to have a normal form of sets and memories; it is needed
   -- only if there are at least two elements different from eps
end type

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

function first (E1, E2 : elem) : Bool is
   -- expresses that two elements (may) have the same address component
   use E1, E2;
   return true
end function

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

function datum (I : index, E : elem) : Bool is
   -- true iff element E may be written by process having index I
   case I in
      1 -> return true
    | 2 -> return E == eps
   end case
end function

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

end module