Promela |
Predefined |
np_(5) |
NAME
np_
-
a predefined read-only boolean variable.
SYNTAX
np_
DESCRIPTION
This variable is set to
true
by the system in all global system states
that are marked as progress states, and to
false
in all other states.
The system is in a progress state if
at least one active process is at a local control
state that was marked with a
progress
label, or if a
trace
declaration marks the global state as a a
progress
state.
This predefined variable is meant to be used inside never claims only.
EXAMPLES
Catch non-progress cycles with an explicit
never
claim:
never { /* <>[] np_ */ do :: skip :: np_ -> break od; accept: do :: np_ od }
SEE ALSO
ltl(1), progress(2), never(2).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |