Promela |
Control-Flow |
labels(3) |
NAME
label
-
to identify a unique control state in a
proctype
declaration.
DESCRIPTION
Any statement or control-flow construct can be preceded by label.
The label can, but need not, be used as a destination of a
goto
or in a remote reference inside a
never
claim.
Label-names must be unique within the surrounding
proctype ,
trace ,
or
never
claim declaration.
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.
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 and unlabeled) final state
immediately following the repetition construct.
active proctype dijkstra()
{
S1: do
:: q!p ->
S2: q?v
:: true
od
/* S3 */
}
The state labeled
S1
has two outgoing transitions:
one corresponding to the send statement
q!p ,
and one corresponding to the conditional statement
true .
Observe carefully that there is no separate control
state at the start of each guard in a selection or
repetition construct.
NOTES
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.
SEE ALSO
accept(2), progress(2), end(2), goto(3), remoterefs(5).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |