====== Channel types ======


Channels are similar to data types. Instead of relating a user-defined
channel to built-in data, we relate them to a built-in channel types
instead. The methods required for supporting the full functionality of
a channel are operations necessary to send and receive data on the
channel, rather than a read and write operation on a data value.

<code act>
defchan e1of2 <: chan(bool) (bool d0,d1,e)
{
   spec {
    exclhi(d0,d1)
   }
}
</code>

Port lists for channel types can be data types (built-in or
user-defined) or channels. Processes are not valid types for ports of a
channel type.

===== Channel methods =====


There are eight possible methods that can be defined for a channel type:

   * Methods for sending and receiving values on the channel
      * ''set'', ''send_up'', ''send_rest'': together these three operations implement a send operation on the channel. The send operation consists of two parts: (i) setting the data value to be sent (''set''); (ii) completing the synchronization (''send_up''); and (iii) completing the rest of the protocol (''send_rest'').
      * ''get'', ''recv_up'', ''recv_rest'': together these three operations implement a receive operation on the channel. The receive operation consists of three parts: (i) getting the value that has been transmitted along the channel (''get''); (ii) completing the synchronization operation (''recv_up''); and (iii) completing the rest of the protocol (''recv_rest'').
   * Methods for initializing  the channel on reset, if needed.
      * ''send_init'' : this is used to initialize the sender end of the channel on reset.
      * ''recv_init'' : this is used to initialize the receiver end of the channel on reset.

For channels, there are two special methods that are used for probe operations with different syntax. Both of these have to be specified via an expression, rather than the normal method syntax.
      * ''send_probe'': this is the probe operation for the sending end of the channel. It corresponds to the receiver being ready to communicate.
      * ''recv_probe'': this is the probe operation for the receiving end of the channel. It corresponds to the sending being ready to communicate.

The send operation ''X!e'' in the CHP language corresponds to two
parts: setting the data value, followed by the synchronization
operation, and possibly the reset phase of the handshake. 
Setting the data value also indicates that the sender is
ready to communicate. It is illegal to set the data value multiple
times without an intervening synchronization operation. Finally,
attempting to set the data value might block if the previous channel
operation has not completed as yet. Whether or not this could occur
depends on the channel protocol.

The receive operation ''X?v'' in the CHP language corresponds to
three parts: receiving the data value, followed by the synchronization
operation, and finally the rest of the handshake. 
Attempting to get the data value from the channel will
block if the sender has not provided any value. Once a value has been
extracted from the channel, the synchronization operation can be
executed. Prior to the synchronization, multiple get operations can be
executed; the channel must be designed so that subsequent get
operations will return the same value as the first one, and will be
guaranteed not to block. The get operation is used to implement a CHP
value probe, where the receiver can peek at the value pending in the
channel without attempting a synchronization operation.

An example definition of a Boolean channel where the channel has an
lazy-active send and passive receive is below. Note that for a channel,
''self'' corresponds to the type of the data being sent or received
on the channel.

<code act>
defchan e1of2 <: chan(bool) (bool d0,d1,e)
{
   spec {
    exclhi(d0,d1)
   }
   methods {
    set {
      [e];[self->d1+[]~self->d0+]
    }
    send_up {
      [~e]
    }
    send_rest {
      d0-,d1-
    }
    get {
     [d0->self-[]d1->self+]
    }
    recv_up {
     e-
    }
    recv_rest {
     [~d0&~d1];e+
    }
    recv_probe = (d0|d1);
   }
}
</code>

In the example above, the ''set'', ''send_up'', and ''send_rest'' methods
specify the sequence of operations on the channel variables that are
invoked for a send action. The ''get'', ''recv_up'', and ''recv_rest'' methods
specify the sequence of operations used to perform a receive. The
special variable ''self'' is used to specify the ''bool'' value
that is being either sent or received on the channel.

This channel has an active send and passive receive, and hence probes
are only supported at the receiver. The ''recv_probe'' method
expression specifies the Boolean expression corresponding to the probe
at the receiver end of the channel. A ''send_probe'' can be
specified in a similar way when the sender is passive and receiver is
active.

The ''e1of2'' channel has been specified to perform a four-phase
handshake protocol. If the channel were to correspond to a two-phase
protocol, a different sequence of actions can be specified instead.

When defining an exchange channel, the special variable ''selfack'' is
used to specify the value being received by the sender, and being sent by the receiver.