Promela Reference -- enabled(5)

Promela

Predefined

enabled


NAME
enabled - predefined boolean function for testing the enabledness of a process from within a never claim.

SYNTAX
enabled( any_expr )

DESCRIPTION
This predefined function can only be used inside a never claim, or equivalently in the symbol definition for an LTL formula.

Given the instantiation number of an active process, the function returns true if the process has at least one executable statement in its current control state, and false otherwise. When given the instantiation number of a non-existing process, the function always returns false.

In every global state where enabled(p) returns true, the process with instantiation number p has at least one executable statement. Of course, the executability status of that process can change after the next execution step is taken in the system, which may or may not be from process p .

EXAMPLES
The following never claim attempts to match executions in which the process with instantiation number one remains enabled infinitely long without ever executing.

NOTES
The use of this function is incompatible with Spin's partial order reduction strategy, and can therefore increase the computational requirements of a verification.

SEE ALSO
_last
_pid
ltl
never
pc_value
run


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