Promela |
Declarator |
chan(2) |
NAME
chan
-
syntax for declaring and initializing message passing channels.
SYNTAX
chan
name
chan
name = '['
const ']' of {
typename [,
typename ] * }
DESCRIPTION
Channels are used to transfer messages (cf. definitions
S.2 and S.3 in intro(0)) between active processes.
Channels are declared using the keyword
chan ,
either locally or globally, much like integer variables,
Channels by default store messages in first-in first-out order
(but see
send(4) and
receive(4)).
A single keyword chan can be followed by either a single name, or a comma-separated list of names, each optionally followed by a channel initializer.
The syntax
chan a, b; chan c[3]declares the names a , b , and c as channel names, the last one as an array of three elements (see arrays(2)). A channel must be initialized before it can be used to store messages. It is rare to declare just a channel name without initialization, but it occurs in, for instance, proctype parameter lists, where the initialized version of a channel is not passed to the process until the time of process instantiation with a run operator.
The channel initializer specifies a channel capacity, as a constant, and the structure of the messages that can be stored in the channel, as a comma-separated list of type names. If the capacity is larger than zero, a normal buffered channel is initialized, with the given number of slots to store messages. If the capacity is specified to be zero, a rendezvous , also called a synchronous , channel, is created. Rendezvous channels can pass messages only through synchronous handshakes between sender and receiver, but they cannot buffer messages (see send(4), receive(4)).
EXAMPLES
The following channel declaration contains an initializer.
chan a = [16] of { short }
The initializer says that channel
a
can store up to sixteen messages of type
short .
Similarly,
chan c[3] = [0] of { mtype }
initializes an array of 3 rendezvous channels
for messages that contain just one message field, of type
mtype .
If the messages to be passed by the channel have more than one field, the declaration looks as follows:
chan qname = [8] of { mtype, int, chan, byte }
This time, we have defined a single channel that can store up to
eight messages, each consisting of four fields: an
mtype ,
followed by an
int ,
followed by a channel name, and a
byte .
The
chan
field can be used to pass a channel identifier (a number)
from one process to another.
NOTES
The first field in a channel type declaration is conventionally an
mtype ,
which is used to store a message type indicator in symbolic form.
See
mtype(2).
In verification, buffered channels contribute significantly to verification complexity. For an initial verification run, choose a small channel capacity, of say 2 or 4. If the verification completes swiftly, you can consider increasing the capacity to a larger size.
SEE ALSO
arrays(2), mtype(2), send(4), receive(4), empty(5), full(5), len(5), nempty(5), nfull(5), poll(5).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |