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) |