Promela |
Declarator |
chan |
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 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 also the sorted send option in the manual page for
send and the random receive option in the manual page for
receive ).
The keyword chan can be followed by one or more names, in a comma-separated list, each optionally followed by a channel initializer. The syntax
chan a, b, c[3]declares the names a , b , and c as uninitialized channels, the last one as an array of three elements.
A channel variable must be initialized before it can be used to transfer 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 a process is instantiated 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 channel capacity is larger than zero, a buffered channel is initialized, with the given number of slots to store messages. If the capacity is specified to be zero, a rendezvous port, also called a synchronous channel, is created. Rendezvous ports can pass messages only through synchronous handshakes between sender and receiver, but they cannot store messages.
All data types can be used inside a channel initializer, including typedef structure names, but not including the typename unsigned .
EXAMPLES
The following channel declaration contains an initializer:
chan a = [16] of { short }
The initializer says that channel
a can store up to 16 messages.
Each message is defined to have only one single field,
which must be of type
short . Similarly,
chan c[3] = [0] of { mtype }
initializes an array of three rendezvous channels
for messages that contain just one message field, of type
mtype . The following is an example of the declaration of a channel that can pass messages with multiple fields:
chan qname = [8] of { mtype, int, chan, byte }
This time the channel can store up to eight messages,
each consisting of four fields of the types listed.
The
chan field can be used to pass a channel identifier
from one process to another.
In this way, a channel that is declared locally within
one process, can be made accessible to other processes.
A locally declared and instantiated channel disappears, though,
when the process that contain the declaration dies.
NOTES
The first field in a channel type declaration is conventionally
of type
mtype , and is used to store a message type indicator in symbolic form.
In verification, buffered channels contribute significantly to verification complexity. For an initial verification run, choose a small channel capacity, of, say, two or three slots. If the verification completes swiftly, consider increasing the capacity to a larger size.
SEE ALSO
arrays
datatypes
empty
full
len
mtype
nempty
nfull
poll
receive
send
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |