module EXTENDED_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;
   -- the difference to the module VARIABLE_ARRAY is the type of the index:
   -- to be consistent with accesses to further array elements, here type Nat
   -- is used instead of type Pid
   var a: Nat_array, i: Nat, v: Nat in
      a := Nat_Array (val);
      loop
         alt
            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
         end alt
      end loop
   end var
end process

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

process Extended_Variable_Array [G: Operation] (val: Nat, f: Nat) is
   -- process modeling the elements [f*N .. ((f+1)*N)-1] of the extended array
   var a: Nat_array, i, v: Nat in
      a := Nat_Array (val);
      loop
         alt
            G (Read, ?i, ?v, ?any Pid)
               where (i >= (f*N)) and (i < ((f+1)*N)) and (v == a[i - (f*N)])
          []
            G (Write, ?i, ?v, ?any Pid)
               where (i >= (f*N)) and (i < ((f+1)*N));
            a[i - (f*N)] := v
         end alt
      end loop
   end var
end process

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

process Cell [G: Operation] (index: Nat, in var val: Nat) is
   -- process modeling one element of the extended array
   loop
      alt
         G (Read, index, val, ?any Pid)
       []
         G (Write, index, ?val, ?any Pid)
      end alt
   end loop
end process

end module