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