Promela Reference -- remoterefs(5)

Promela

Predefined

remoterefs


NAME
remote references - a mechanism for testing the local control state of an active process, or the value of a local variable in an active process from within a never claim.

SYNTAX
name [ '[' any_expr ']' ] @ labelname

name [ '[' any_expr ']' ] : varname

DESCRIPTION
The remote reference operators take either two or three arguments: the first, required, argument is the name of a previously declared proctype , a second, optional, argument is an expression enclosed in square brackets, which provides the process instantiation number of an active process. With the first form of remote reference, the third argument is the name of a control-flow label that must exist within the named proctype . With the second form, the third argument is the name of a local variable from the named proctype .

The second argument can be omitted, together with the square brackets, if there is known to be only one instantiated process of the type that is named.

A remote reference expression returns a non-zero value if and only if the process referred to is currently in the local control state that was marked by the label name given.

EXAMPLES

NOTES
Because init , never , trace , and notrace are not valid proctype names but keywords, it is not possible to refer to the state of these special processes with a remote reference:

Note that the use of init , can always be avoided, by replacing it with an active proctype .

A remote variable reference, the second form of a remote reference, bypasses the standard scope rules of Promela by making it possible for the never claim to refer to the current value of local variables inside a running process.

For instance, if we wanted to refer to the variable count in the process of type Dijkstra in the example on page _ch4_end, we could do so with the syntax Dijkstra[0]:count , or if there is only one such process, we can use the shorter form Dijkstra:count .

The use of remote variable references is not compatible with Spin's partial order reduction strategy. A wiser strategy is therefore usually to turn local variables whose values are relevant to a global correctness property into global variables, so that they can be referenced as such. See especially the manual page for hidden for an efficient way of doing this that preserves the benefits of partial order reduction.

SEE ALSO
_pid
active
condition
hidden
proctype
run


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