Promela Reference -- labels(3)





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

name : stmnt

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.

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


/* 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.

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

Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page Updated: 16 December 1997)