module VARIABLE_ARRAY (TYPES, CHANNELS) is

process Variable_Array [G: Operation] (val: Nat) is
   -- process modeling an array of N variables; "val" is the initial value
   var a: Nat_array, i: Pid, v: Nat in
      a := Nat_Array (val);
      loop
         alt
            G (Read, ?i, ?v, ?any Pid) where (v == a[Nat (i)])
         []
            G (Write, ?i, ?v, ?any Pid);
            a[Nat (i)] := v
         end alt
      end loop
   end var
end process

end module