condition statement - for conditional execution and synchronization.
( expr != 0)
In Promela, a standalone expression is a valid statement. A condition statement is often used as a guard at the start of an option sequence in a selection or repetition structure. Execution of a condition statement is blocked until the expression evaluates to a non-zero value (or, equivalently, to the boolean value true). All Promela expressions are required to be side effect free.
(1) /* always executable */ (0) /* never executable */ skip /* always executable, same as (1) */ true /* always executable, same as skip */ false /* always blocks, same as (0) */ a == b /* executable only when a equals b */A condition statement can only be executed (passed) if it holds. This means that the statement from the first example can always be passed, the second can never be passed, and the last cannot be passed as long as the values of variables a and b differ. If the variables a and b are local, the result of the evaluation cannot be influenced by other processes, and this statement will work as either true or false , depending on the values of the variables. If at least one of the variables is global, the statement can act as a synchronizer between processes.
Spin Online References
Promela Manual Index
|(Page updated: 28 November 2004)|