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

active proctype main () {
	byte x;
L:	(x < 3) ->
	x++
}
never {	/* process main cannot remain at L forever */
accept:	do
	:: main@L
	od
}

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:

init@label	/* invalid */
never[0]@label	/* invalid */

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.

Another problem exists in Spin Version 6 and later, when the new scope rules for variables are used (this is the default). The scope rules are enforced by prefixing variable names with a scope identifier. This means that if count is a local variable in proctype dijkstra, then it is no longer visible to the verifier under that name, but it may be called something like _3_count.
One way to make a remote variable reference work with Spin Version 6 and later is then to look up the internal name with spin -d model.pml, and prefix that name with the scope identifier, which is listed at the end of the entry in the symbol table. Or, maybe easier, lookup the name in pan.h for the proctype declaration.
Still easier is to simply turn off the new scope rules when parsing the model, which you can do with the -O (capital letter Oh) flag to spin: spin -O -a model.pml.

SEE ALSO
_pid
active
condition
hidden
proctype
run