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 not 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).