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 .
mtype = { msg, ack, other }; 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 */Without the eval function, writing simply
q?xwould 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) |