module ARCH_TREE (FUNCTIONS, CHANNELS, EXTENDED_VARIABLE_ARRAY, MESI_CACHE, VIRTUAL) is

-------------------------------------------------------------------------------
-- Architecture of systems communicating by means of 2*N shared variables,
-- represented as the cells a[0], ..., a[N-1] and c[0], ..., c[N-1] of two
-- N-variable arrays.
-------------------------------------------------------------------------------

process Arch_Tree [NCS: Pid, CS: Access, A, C: Operation, MU: Latency] is
   par NCS, CS, A, C in
      Protocol [NCS, CS, A, C]
    ||
      L [NCS, CS, A, C, MU]
   end par
end process

-------------------------------------------------------------------------------
-- Auxiliary process for compositional generation: protocol without latencies
-------------------------------------------------------------------------------

process Protocol [NCS: Pid, CS: Access, A, C: Operation] is
   par A, C in
      par
         P [NCS, CS, A, C] (0 of Pid)
       ||
         P [NCS, CS, A, C] (1 of Pid)
       ||
         P [NCS, CS, A, C] (2 of Pid)
       ||
         P [NCS, CS, A, C] (3 of Pid)
       ||
         P [NCS, CS, A, C] (4 of Pid)
      end par
    ||
      par
         Variable_Array [A] (0 of Nat)
       ||
         Extended_Variable_Array [A] (0 of Nat, 1 of Nat)
       ||
         Extended_Variable_Array [A] (0 of Nat, 2 of Nat)
       ||
         Variable_Array [C] (0 of Nat)
       ||
	 Cell [C] (5 of Nat, 0 of Nat) 
       ||
	 Cell [C] (6 of Nat, 0 of Nat) 
      end par
   end par
end process

-------------------------------------------------------------------------------
-- Auxiliary process for inserting latencies
-------------------------------------------------------------------------------

process L [NCS: Pid, CS: Access, A, C: Operation, MU: Latency] is
   var
      a_0_4, a_5_9, a_10_14, c_0_4: Cache_Array,
      c_5, c_6, a_i, c_i: Cache,
      index: Nat, pid: Pid,
      acc: Access,
      op: Operation,
      cop: Cached_Operation
   in
      a_0_4   := cache_array (cache (Invalid));
      a_5_9   := cache_array (cache (Invalid));
      a_10_14 := cache_array (cache (Invalid));
      c_0_4   := cache_array (cache (Invalid));
      c_5     := cache (Invalid);
      c_6     := cache (Invalid);
      loop
         alt
            A (?op, ?index, ?any Nat, ?pid) where index < N;
            a_i := a_0_4[index];
            cop := update_caches (pid, op, !?a_i);
            a_0_4[index] := a_i;
            MU (cop, pid)
          []
            A (?op, ?index, ?any Nat, ?pid) where (index >= N) and (index < (2*N));
            a_i := a_5_9[index - N];
            cop := update_caches (pid, op, !?a_i);
            a_5_9[index - N] := a_i;
            MU (cop, pid)
          []
            A (?op, ?index, ?any Nat, ?pid) where (index >= (2*N)) and (index < (3*N));
            a_i := a_10_14[index - (2*N)];
            cop := update_caches (pid, op, !?a_i);
            a_10_14[index - (2*N)] := a_i;
            MU (cop, pid)
          []
            C (?op, ?index, ?any Nat, ?pid) where index < N;
            c_i := c_0_4[index];
            cop := update_caches (pid, op, !?c_i);
            c_0_4[index] := c_i;
            MU (cop, pid)
          []
            C (?op, 5 of Nat, ?any Nat, ?pid);
            cop := update_caches (pid, op, !?c_5);
            MU (cop, pid)
          []
            C (?op, 6 of Nat, ?any Nat, ?pid);
            cop := update_caches (pid, op, !?c_6);
            MU (cop, pid)
          []
            CS (?acc, ?pid);
            if acc == Enter then
               MU (acc, pid)
            end if
          []
            NCS (?pid);
            MU (Work, pid)
         end alt
      end loop
   end var
end process

end module