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