Promela Reference -- poll(5)

Google

Promela

Predefined

poll(5)

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

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

DESCRIPTION
A channel poll operation looks just like a receive statement with square brackets enclosing the list of message fields. 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, is guaranteed to be the same before and after these types of condition are evaluated.

EXAMPLES

qname?[ack,var] && timeout

places an additional constraint on a timeout test.

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. To simulate a poll operation on a synchronous channels, see receive(4).

SEE ALSO
condition(4), receive(4).


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page Updated: 16 December 1997)