module TUPLE_ARRAY (TYPES, CHANNELS) is

process Tuple_Array [G1, G2: Operation] (val1, val2: Nat) is
   -- process modeling an array of tuples of variables; (val1, val2) is the
   -- initial value
   var t: Tuple_array, i: Pid, v1, v2: Nat in
      t := Tuple_array (Tuple (val1, val2));
      loop
         alt
            G1 (Read, ?i, ?v1, ?v2, ?any Pid)
               where (v1 == t[Nat (i)].v1) and (v2 == t[Nat (i)].v2)
          []
            G1 (Write, ?i, ?v1, ?any Pid);
            t[Nat (i)] := Tuple (v1, t[Nat (i)].v2)
          []
            G2 (Write, ?i, ?v2, ?any Pid);
            t[Nat (i)] := Tuple (t[Nat (i)].v1, v2)
         end alt
      end loop
   end var
end process

end module