module MEMORY (TYPES, CHANNELS) is

process Memory [G: Operation] (init: Nat) is
   var a: Nat_array, val: Nat, i, v: Nat in
      a := Nat_Array (init);
      val := init;
      loop
         alt
          -- cells allocated by the processes
            G (Read, ?i, ?v, ?any Pid) where (i < N) and (v == a[i])
          []
            G (Write, ?i, ?v, ?any Pid) where (i < N);
            a[i] := v
          []
          -- cell initially pointed to by the queue lock
            G (Read, N, val, ?any Pid)
          []
            G (Write, N, ?val, ?any Pid)
         end alt
      end loop
   end var
end process

end module