NAME
end - label-name prefix for marking valid termination states.

SYNTAX
end[a-zA-Z0-9_]*: stmnt

DESCRIPTION
An end-state label is any label name that starts with the three-character sequence end . End-state labels can be used in proctype , trace , and notrace declarations.

When used in a proctype declaration, the end-state label marks a local control state that is acceptable as a valid termination point for all instantiations of that proctype .

If used in an event trace definition, the end-state label marks a global control state that corresponds to a valid termination point for the system as a whole.

If used in an event notrace definition, though, the normal meaning reverses: the event trace is now considered to have been completely matched when the end state is reached, thus signifying an error condition, rather than normal system termination.

End-state labels have no special meaning when used in never claims.

EXAMPLES
In the following example the end-state label defines that the expected termination point of the process is at the start of the loop.

active proctype dijkstra()
{
end:	do
	:: sema!p -> sema?v
	od	
}

NOTES
It is considered an invalid end-state error if a system can terminate in a state where not all active processes are either at the end of their code (i.e., at the closing curly brace of their proctype declarations) or at a local state that is marked with and end-state label.

If the run-time option -q is used with the compiled verifier, an additional constraint is applied for a state to be considered a valid end state: all message channels must then also be empty.

SEE ALSO
accept
labels
notrace
progress
trace