to identify a unique control state in a
Any statement or control-flow construct can be preceded by label.
The label can, but need not, be used as a destination of a
or in a remote reference inside a
Label-names must be unique within the surrounding
A label always prefixes a statement, and thereby
uniquely identifies a control state in a transition system,
i.e., the source state of the transition that corresponds
to the labeled statement.
Multiple labels on a single statement are allowed.
declaration translates into a transition system with precisely
three local process states: initial state
in between the send and the receive,
and the (unreachable and unlabeled) final state
immediately following the repetition construct.
active proctype dijkstra()
:: q!p ->
/* S3 */
The state labeled
has two outgoing transitions:
one corresponding to the send statement
and one corresponding to the conditional statement
Observe carefully that there is no separate control
state at the start of each guard in a selection or
A labelname can be any alphanumeric character-string that
satisfies the same requirements as an identifier (i.e., it
may not start with a digit or an underscore).
Remember that the guards from a
selection or repetition construct cannot be prefixed by
labels individually. See
if(3) for details.
accept(2), progress(2), end(2), goto(3), remoterefs(5).