Promela Reference -- cond_expr(5)




conditional expression - shorthand for a conditional evaluation.

( any_expr -> any_expr : any_expr )

The conditional expression in Promela is based on the version from the C programming language. To avoid parsing conflicts, though, the syntax differs slightly from C. Where in C one would write

the corresponding expression in Promela is The question mark from the C version is replaced with an arrow symbol, to avoid confusion with the Promela receive operator. The round braces around the conditional expression are required, in this case to avoid the misinterpretation of the arrow symbol as a statement separator.

When the first expression p ( in the example) evaluates to non-zero, the conditional expression as a whole obtains the value of the second expression q ), ( and else it obtains the value of the last expression r ). (

The following example shows a simple way to implement conditional rendezvous operations.

Two dummy rendezvous channels ( q[0] and q[2] ) are used here to deflect handshake attempts that should fail. The handshake can only successfully complete (on channel q[1] ) if both the boolean expression P at the receiver side and the boolean expression Q at the sender side evaluate to true simultaneously. The dummy rendezvous channels q[0] and q[2] that are used here do not contribute any measurable overhead in a verification, since rendezvous channels take up no memory in the state vector.

An alternative way of specifying a conditional rendezvous operation is to add an extra message field to the channel and to use the predefined eval function in the receive statement, as follows.

The handshake can again only happen if both P and Q evaluate to true. Unfortunately, the message field cannot be declared as a boolean, since we need a third value to make sure no match occurs when both P and Q evaluate to false.


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