Promela Reference -- labels(3)

Promela

Control-Flow

labels


NAME
label - to identify a unique control state in a proctype declaration.

SYNTAX
name : stmnt

DESCRIPTION
Any statement or control-flow construct can be preceded by a label. The label can, but need not, be used as a destination of a goto or can be used in a remote reference inside a never claim. Label names must be unique within the surrounding proctype , trace , notrace , or never claim declaration.

A label always prefixes a statement, and thereby uniquely identifies a control state in a transition system, that is, the source state of the transition that corresponds to the labeled statement.

Any number of labels can be attached to a single statement.

EXAMPLES
The following proctype declaration translates into a transition system with precisely three local process states: initial state S1 , state S2 in between the send and the receive, and the (unreachable) final state S3 , immediately following the repetition construct.

The first state has two labels: S0 and S1 . This state has two outgoing transitions: one corresponding to the send statement q!p , and one corresponding to the condition statement true . Observe carefully that there is no separate control state at the start of each guard in a selection or repetition construct. Both guards share the same start state S1 .

NOTES
A label name can be any alphanumeric character string, with the exception that the first character in the label name may not be a digit or an underscore symbol.

The guard statement in a selection or repetition construct cannot be prefixed by a label individually; see the manual page for if and do for details.

The first statement of an inline also cannot have a label. It will prompt the error: instead of { Label: statement ... } use Label: { statement ... }. The reason is that the inline will be inlined into the main body of the specification (at the point where the inline is invoked) as a sequence in curly braces. To avoid the problem -- put a skip statement at the start of the inline.

There are three types of labels with special meaning, see the manual pages named accept , end , and progress .

SEE ALSO
accept
do
end
if
goto
progress
remoterefs


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 19 February 2007)