Promela |
Declarator |
notrace(2) |
NAME
notrace
-
for defining invalid event sequences.
SYNTAX
notrace
{
sequence }
DESCRIPTION
The logical negation of a
trace
definition, subject to the same requirements.
The
notrace
correctness requirement is violated if the event sequence
given in the trace declaration can be matched completely,
that is, if a user-defined
end -state
in the trace definition, or the closing curly brace, is reachable.
SEE ALSO
ltl(1), end(2), never(2), trace(2).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |