Promela |
Declarator |
end(2) |
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).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |