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) |