Promela Reference -- np_(5)

Promela

Predefined

np_


NAME
np_ - a global, predefined, read-only boolean variable.

SYNTAX
np_

DESCRIPTION
This global predefined, read-only variable is defined to be true in all global system states that are not explicitly marked as progress states, and is 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 user-defined progress label, or if the current global system state is marked by a progress label in an event trace definition.

The np_ variable is meant to be used exclusively inside never claims, to define system properties.

EXAMPLES
The following non-deterministic never claim accepts all non-progress cycles:

This claim is identical to the one that the verifier generates, and automatically adds to the model, when the verifier source is compiled with the directive -DNP , as in: Note that the claim automaton allows for an arbitrary, finite-length prefix of the computation where either progress or non-progress states can occur. The claim automaton can move to its accepting state only when the system is in a non-progress state, and it can only stay there infinitely long if the system can indefinitely remain in non-progress states only.

SEE ALSO
condition
ltl
never
progress


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