NAME
end - label-name prefix, for specifying expected termination.

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

DESCRIPTION
An end-state label is any label-name that starts with the three-character sequence end . It marks a control state that is acceptable as a valid termination point for all processes of the corresponding proctype . It can appear anywhere a label can appear (see labels(3)).

End-state labels have the above semantics when used in proctype declarations to indicate valid end-states, or event notrace declarations to indicate invalid global end-states. They have no special meaning when used in never claims.

It is considered an error (an invalid endstate) if the system can terminate in a state where not all active processes are either at the end of their code (the closing curly brace) or at a local state that is labeled as an end -state.

If the run-time option -q is used with the compiled verifier that is generated by Spin, there is an additional constraint to prevent an invalid end-state from being reported: all message channels are also required to be empty.

If an end -state label is used in a notrace definition, the event trace is considered to have been completely matched when the end -state that is identified in this way is reached.

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, and not in the middle.

active proctype dijkstra()

{

end:	do

	:: sema!p -> sema?v

	od	

}

SEE ALSO
accept(2), progress(2), notrace(2), labels(3).