Promela |
Predefined |
enabled(5) |
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 }
SEE ALSO
ltl(1), never(2), _last(5), _pid(5), pc_value(5), run(5).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |