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 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) |