Promela Reference -- eval(5)

Google

Promela

Predefined

eval(5)

NAME
eval - allow use of an expression where a constant is needed.

SYNTAX
eval( expression )

DESCRIPTION
The intended use of the unary operator eval is 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 */

NOTES
In version 3.3 and later, an expression can be used inside the eval construct. In earlier versions only a variable name could be used.

SEE ALSO
receive(4).


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