Promela Reference -- poll(5)

Promela

Predefined

poll


NAME
poll - a side effect free test for the executability of a non-rendezvous receive statements.

SYNTAX
name ? '[' recv_args ']'
name ?? '[' recv_args ']'

DESCRIPTION
A channel poll operation looks just like a receive statement, but with the list of message fields enclosed in square brackets. It returns either true or false, depending on the executability of the corresponding receive (i.e., the same operation written without the square brackets). Because its evaluation is side effect free, this form can be used freely in expressions or even assignments where a standard receive operation cannot be used.

The state of the channel, and all variables used, is guaranteed not to change as a result of the evaluation of this condition statement.

EXAMPLES
In the following example we use a channel poll operation to place an additional constraint on a timeout condition:

NOTES
Channel poll operations do not work on rendezvous channels because synchronous channels never store messages that a poll operation could refer to. Messages are always passed instantly from sender to receiver in a rendezvous handshake.

It is relatively simple to create a conditional receive operation, with the help of a channel poll operation. For instance, if we want to define an extra boolean condition P that must hold before a given receive operation may be executed, we can write simply:

This is harder to do for rendezvous channels; see the manual page for cond_expr for some examples.

SEE ALSO
cond_expr
condition
eval
receive


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)