Promela Reference -- eval(5)

Promela

Predefined

eval


NAME
eval - predefined unary function to turn an expression into a constant.

SYNTAX
eval( any_expr )

DESCRIPTION
The intended use of 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. If a variable name is used directly, without the eval function, the variable would be assigned the value from the corresponding message field, instead of serving as a match of values.

EXAMPLES
In the following example the two receive operations are only executable if the precise values specified were sent to channel q : first an ack and then a msg .

Without the eval function, writing simply would mean that whatever value was sent to the channel (e.g., the value other ) would be assigned to x when the receive operation is executed.

NOTES
Any expression can be used as an argument to the eval function. The result of the evaluation of the expression is then used as if it were a constant value.

This mechanism can also be used to specify a conditional rendezvous operation, for instance by using the value true in the sender and using a conditional expression with an eval function at the receiver; see also the manual page for conditional expressions.

SEE ALSO
cond_expr
condition
poll
receive


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