Promela |
Predefined |
pc_value |
NAME
pc_value -
a predefined, integer function for use in
never claims.
SYNTAX
pc_value( any_expr )
DESCRIPTION
The call
pc_value(x) returns the current control
state (an integer) of the process with instantiation number
x . The correspondence between the state numbers reported by
pc_value and statements or line numbers in the Promela source can be checked
with run-time option
-d on the verifiers generated by Spin, as in:
$ spin -a model.pml $ cc -o pan pan.c $ ./pan -d \&...The use of this function 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 }This claim 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.
NOTES
As the example indicates, this function is primarily
supported for experimental use, and may not survive
in future revisions of the language.
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 28 November 2004) |