Promela Reference -- eval(5)

Promela

Predefined

eval(5)

NAME
eval - allow use of a variable as if it were a constant.

SYNTAX
eval( varref )

DESCRIPTION
The unary operator eval can be used in receive statements to force a match of a message field with the current value of a local or global variable. Normally, such a match can only be forced by specifying a constant value. If the variable name is used directly, without the eval operator, it would not serve as a match but instead it would be assigned the incoming value from the message field when the receive statement is executed.

EXAMPLES

mtype = { msg, ack };
chan q = [4] of { mtype };

mtype x;

x = ack; q?eval(x)	/* same as: q?ack */
x = msg; q?eval(x)	/* same as: q?msg */

SEE ALSO
receive(4).


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