Promela Reference -- receive(4)


Basic Statement


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 question mark, are executable if the first message in the channel matches the pattern from the receive statement.

The second and fourth form of the statement, written with a double question mark, are executable if there exists at least one message anywhere in the channel that matches the pattern from the receive statement. The first such message is then used.

A match of a message is obtained if all message fields that contain constant values in the receive statement equal the values of the corresponding message fields in the message.

If a variable appears in the list of arguments to the receive statement, the value from the corresponding field in the message that is matched is copied into that variable upon reception of the message. If no angle brackets are used, the message is removed from the channel buffer after the values are copied. If angle brackets are used, the message is not removed and remains in the channel.

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. The types of the variables used in the message fields must be compatible with the corresponding fields from the channel declaration. 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 always match precisely.

The first form of the receive statement is most commonly used. The remaining forms serve only special purposes, and can only be used on buffered message channels.

The second form of the receive statement, written with two question marks, is called a random receive statement. The variants with angle brackets have no special name.

Because all four types of receive statements discussed here can have side effects, they cannot be used inside expressions (see the manual page poll for some alternatives).


In this example we first send three values into a channel that can contain up to eight messages with one single field of type byte . The values are within the range that is expected, so no value truncations will occur. The use of the sorted send operator (the double exclamation) causes the three values to be stored in numerical order. A regular receive operation is now used to retrieve the first element from the channel, which should be the value two.

The selection statement that follows has three options for execution. If the channel is empty at this point, only the third statement will be executable. If the channel is non-empty, and contains at least one message with the value five, the second option will be executable. Because of the use of the random receive operator (the double question mark), the target message may appear anywhere in the channel buffer and need not be the first message. It is removed from the channel when matched. The first option in the selection structure is executable if the channel contains any message at all. Its effect when executed will be to copy the value of the first message that is in the channel at this point into variable x . If all is well, this should be the value three. If this option is executed, the message will remain in the channel buffer, due to the use of the angle brackets.


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 30 September 2016)