Promela |
Declarator |
accept(2) |
NAME
accept
-
label-name prefix, for specifying Büchi acceptance (liveness).
SYNTAX
accept[a-zA-Z0-9_]*:
stmnt
DESCRIPTION
An accept label is any label-name that starts with the
six-character sequence
accept .
It can appear anywhere a label can appear
(see
labels(3)).
A label always prefixes a statement, and thereby uniquely identifies a local state in a process (cf. definition S.4 in intro(0)), i.e., the source state of the transition that corresponds to the labeled statement.
An accept -label can appear in a proctype , never claim, or trace declaration. The labeled state is then defined within the corresponding transition system. Because a global system state contains a composite of local states (cf. definition S.6) each accept -label also marks a set of global system states, namely those where the current local state of one or more components carries an accept -label. (A never claim or trace definition can be considered to be a special type of process in this context, with all the elements from definition S.4.)
An accept label defines the correctness claim that the labeled global system state can only be visited finitely many times in any infinite system execution.
EXAMPLES
The following
proctype
declaration translates into a transition system with precisely
three local process states: the initial state, the state
in between the send and the receive,
and the (unreachable) final state immediately following the
repetition construct.
The accept label in this model formalizes the requirement that the second state can neither persist forever, nor be revisited infinitely often. In the given program this would imply that execution should eventually always block at the initial state, just before the execution of sema!p.
active proctype dijkstra() { do :: sema!p -> accept: sema?v od }
NOTES
It recommended that
accept -labels
only be used inside
never
claims, to formalize Büchi acceptance conditions.
Never
claims can be mechanically generated from LTL formulae,
including the required acceptance labels.
It should therefore rarely be needed to place additional
accept labels manually.
SEE ALSO
ltl(1), end(2), never(2), progress(2), trace(2), labels(3).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |