Promela Reference -- end(2)




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

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

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.

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

It will now be flagged as an invalid end-state error if the system that contains this proctype declaration can terminate in a state where the process of type dijkstra remains at the control state that exists just after the arrow symbol.

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.


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)