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) |