Promela Reference -- else(5)




else - a system defined condition statement.


The predefined condition statement else is intended to be used as a guard (i.e., the first statement) of an option sequence inside selection or repetition constructs.

An else condition statement is executable if and only if no other statement within the same process is executable at the same local control state (i.e., process state).

It is an error to define control flow constructs in which more than one else may need to be evaluated in a single process state.


In the first example, the condition statement else is equivalent to the regular expression statement (a < b) .

Note also that round braces are optional around expression statements.

In this example:

both else statements apply to the same control state, which is marked with the label A here. To show the ambiguity more clearly, we can rewrite this example also as: It is unclear what should happen when (x < 0) , and therefore the Spin parser will reject constructions such as these.

Another construction that the parser will reject is the use of an else in combination with an operation on a channel, for instance, as follows:

Note that a race condition is built-in to this type of code. How long should the process wait, for instance, before deciding that the message receive operation will not be executable? The problem can be avoided by using message poll operations, for instance, as follows: Now the meaning is clear, if the message a is present in channel q when control reaches the statement that was marked with the label A , then that message will be retrieved, otherwise the else clause will be selected.

The semantics as given would in principle also allow for an else to be used outside selection or repetition constructs, in a non-branching sequence of statements. The else would then be equivalent to a skip statement, since it would have no alternatives within the local context. The Promela parser, however, will flag such use as an error.

The executability of the else statement depends only on local context within a process. The Promela semantics for timeout can be seen as a global version of else . A timeout is executable only when no alternative statement within the global context of the system is executable. A timeout may not be combined with an else in the same selection construct.


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