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.

active proctype dijkstra()
{
S0:
S1:	do
	:: q!p ->
S2:		q?v
	:: true
	od
/* S3 */
}

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