Promela |
Predefined |
remoterefs(5) |
NAME
Remote reference
-
mechanism for determining the current
local state of an active process from within a
never
claim.
SYNTAX
name '['
any_expr ']' @
name
DESCRIPTION
The remote reference operator takes three arguments:
the first is the name of a previously declared
proctype ,
the second is
an expression, which is evaluated to yield the instantiation
number (i.e., the pid) of a currently executing process of that type, and
the third argument is the name of a label that is defined
within the
proctype .
The expression returns a non-zero value if and only if the process referred to is currently in the local control state marked by the label-name specified.
EXAMPLES
active proctype main () {
L: skip;
skip
}
never { /* process 0 cannot remain at L forever */
accept: do
:: main[0]@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[0]@label /* no good */ never[0]@label /* no good */ trace[0]@label /* no good */ notrace[0]@label /* no good */It is simple to avoid using init , and use an active proctype declaration instead, as shown in the example.
SEE ALSO
active(2), proctype(2), _pid(5), run(5).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |