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

SYNTAX
enabled( name )

DESCRIPTION
This predefined unary operator can only be used inside a never claim declaration, or, equivalently, in the macro definition for a propositional variable that is used in an LTL formula.

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

If enabled(pid) is true , the corresponding process could execute a statement, if given the chance to execute. Of course, the executability status can change if another process executes a statement first.

EXAMPLES

never {

	/* it is not possible for the process with pid=1

	 * to remain enabled without ever executing

	 */

accept:	do

	:: _last != 1 && enabled(1)

	od

}

NOTES
The use of this operator is incompatible with partial order reduction algorithms, and can therefore increase the cost of a verification.

SEE ALSO
ltl(1), never(2), _last(5), _pid(5), pc_value(5), run(5).