Promela |
Predefined |
pc_value(5) |
NAME
pc_value
-
a predefined unary operator for use in
never
claims.
SYNTAX
pc_value(
any_expr )
DESCRIPTION
The expression
pc_value(pid)
is a predefined function that returns the current control
state (an integer) of the process with instantiation number
pid .
The correspondence between the state numbers reported by
pc_value
and statements or line numbers in the Promela source can be checked
with runtime option -d on the verifiers generated by Spin.
The use of this operator is restricted to
never
claims.
EXAMPLES
never { do :: pc_value(1) <= pc_value(2) && pc_value(2) <= pc_value(3) && pc_value(3) <= pc_value(4) && pc_value(4) <= pc_value(5) od }The claim above is a flawed attempt to enforce a symmetry reduction among five processes. This particular attempt is flawed in that it does not necessarily preserve the correctness properties of the system being verified.
SEE ALSO
never(2).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |