Promela |
Predefined |
cond_expr(5) |
NAME
conditional expression
-
shorthand for a conditional evaluation.
SYNTAX
(
any_expr ->
any_expr :
any_expr )
DESCRIPTION
The conditional expression in Promela is based on the
C-version To avoid parsing conflicts, though, the syntax differs slightly from
C. The braces around a conditional expression are required.
When the first expression evaluates to a non-zero result, the conditional expression as a whole obtains the value of the second expression, and else it evaluates to the last expression.
EXAMPLES
chan q[3] = [0] of { mtype };
sender: q[cond2 -> 1 : 2]!msg -> ...
receiver: q[cond1 -> 1 : 0]?msg -> ...
The example shows a simple way to implement conditional
rendezvous operations (see also
receive(4)). Two dummy rendezvous channels (
q[0]
and
q[2] )
are used to deflect handshake attempts that should fail.
The handshake can only successfully complete (on
q[1] )
if both
cond1
at the receiver side and
cond2
at the sender side hold.
SEE ALSO
condition(4).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |