Promela |
Basic Statement |
receive |
NAME
receive statement
-
for receiving messages from channels.
SYNTAX
name ? recv_args
name ?? recv_args
name ?< recv_args >
name ??< recv_args >
EXECUTABILITY
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.
EFFECT
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.
DESCRIPTION
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).
EXAMPLES
chan set = [8] of { byte };
byte x;
set!!3; set!!5; set!!2; /* sorted send operations */
set?x; /* get first element */
if
:: set?<x> /* copy first element */
:: set??5 /* is there a 5 in the set? */
:: empty(set)
fi
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.
SEE ALSO
chan
empty
eval
full
len
nempty
nfull
poll
send
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 30 September 2016) |