Promela Reference -- receive(4)





receive statement - for receiving messages from channels.

name ? recv_args
name ?? recv_args
name ? < recv_args >
name ?? < recv_args >

The first and the third form of the statement, written with a single '?,' are executable if and only if the oldest message in the channel matches the pattern from the receive statement.
The second and fourth form of the statement, written with a double '??,' are executable if there exists at least one message in the channel that matches the pattern from the receive statement. The oldest such message is then used.
A match is obtained if and only if all message fields specified with constants in the receive statement equal the values found in the corresponding message fields from the message.
For rendezvous channels, there is considered to be one message in the channel while a rendezvous offer is in progress (see Intro(0), and send(4)), and the channel is considered to be empty at all other times.

All message fields specified with a variable reference in the receive statement are assigned the value found in the message from the channel that is matched. In the first two forms above, written without angle brackets, the message itself is then removed from the channel; in the last two forms (written with angle brackets) the message is not removed.

The number of message fields that is specified in the receive statement must always match the number of fields that is declared in the channel declaration for the channel addressed, and the types of the fields must be compatible. For integer data types, an equal or larger value range for the variable is considered to be compatible (e.g., a byte field may be received in a short variable, etc.). Message fields that were declared to contain a user-defined data type or a chan must match precisely.

The first form of the receive statement is the standard fifo receive. The second form, written with two question marks, is called a random receive statement. The third form, a fifo receive with angle brackets, is called a fifo poll statement. The last form, a random receive with angle brackets, is called a random receive poll , statement.

Because all these statements can have side-effects on the variables that appear in the argument lists, they cannot be used inside expressions (but see also poll(5)).


chan set = [8] of { byte };

byte x;

set!!3; set!!5; set!!2;	/* add 3 elements to the set, sorted */

set?x;			/* retrieve the smallest element */


:: set??[5]		/* is there still a 5 in the set? */

:: else


The use of angle brackets has no effect for rendezvous channels.

It is relatively simple to create a conditional receive operation, using channel poll operations (see poll(5)), if the channel is buffered (i.e., has a non-zero capacity). If the channel is a rendezvous channel, however, this can be more complicated. Consider the following rendezvous arrangement:

global:		chan port = [0] of { byte };

sender:		port!mesg(12)

receiver:	port?mesg(data)

We want to define an extra boolean condition P that must hold before the rendezvous send operation becomes executable, and a boolean condition Q that must hold before the matching receive becomes executable. We can specify this with the help of two additional rendezvous channels, as follows.
global:		chan port[3] = [0] { byte };

sender:		port[(1-P)]!mesg(12)

receiver:	port[(2-Q)]?mesg(data

When P is false , the sender attempts to handshake on port[1] , and when Q is false , the receiver attempts to handshake on port[2] . Only when both P and Q are true can sender and receiver handshake via port[0] .

chan(2), send(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)