Promela Reference -- else(5)

Google

Promela

Predefined

else(5)

NAME
else - a system defined condition statement.

SYNTAX
else

DESCRIPTION
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 control state where the else appears (see intro(0)).

It is an error to define control flow constructs in which more than one else applies to the same control state (e.g., by defining more than one else statement within a single selection or repetition construct).

EXAMPLES 

if

:: a > b -> ...

:: a == b -> ...

:: else -> ...	/* evaluates to: a <= b */

fi
The semantics above would allow for an else to occur outside selection or repetition constructs, in a non-branching sequence of statements. The rules then say that the else is equivalent to a skip because it has no alternatives within the local context. The Spin parser, however, will flag such use as an error.

In the following example 

A:	do

	:: if

	   :: x > 0 -> x--

	   :: else  -> break

	   fi

	:: else -> x = 10

	od
both else constructs apply to the same control state, labeled A . (The current simulator is often forgiving of small non-fatal errors like this one. The verifier is meant to reliably traps all errors.)

NOTES
The executability of the else depends only on local context within a process. The Promela semantics for timeout can be seen as a system version of the else . A timeout is executable only when no alternative statement within the system is executable.

SEE ALSO
skip(1), condition(4), timeout(5).

Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage 		(Page Updated: 16 December 1997)