Promela Reference -- pc_value(5)

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:

The use of this function is restricted to never claims.

EXAMPLES

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.

SEE ALSO
condition
never


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)