module CHANNELS (TYPES) is

channel Access is
   (a: Access, i: Pid)
end channel

channel Pid is
   (i: Pid)
end channel

channel Operation is
   (op: Operation, j: Pid, i: Pid),   
   -- Read_and_Increment
   (op: Operation, n: Nat, i: Pid),
   -- (1) Read/Write of a shared variable
   -- (2) Read_and_Increment of a queue
   (op: Operation, j: Pid, n: Nat, i: Pid),
   -- (1) Read/Write of an array or tuple
   -- (1) Write of a tuple cell
   (op: Operation, n: Nat, m: Nat, i: Pid),
   -- (1) Read/Write of an array or memory cell
   -- (2) Fetch_and_Store of a queue / pointer
   (op: Operation, j: Pid, n: Nat, m: Nat, i: Pid),
   -- (1) Read of a tuple (atomic read of to arrays)
   -- (2) Read/Write of an token cell
   (op: Operation, n: Nat, m: Nat, b: Bool, i: Pid)
   -- Compare_and_Swap of a queue
end channel

channel Latency is
   (a: Access, i: Pid),
   -- entry/leave of critical or non-critical section
   (op: Cached_Operation, i: Pid)
   -- variable access:
   -- (a) without cache: same profile as entry/leave of (non-)critical section
   -- (b) with cache
end channel

end module