Promela |
Meta Terms |
Inline(1) |
NAME
inline
-
a procedure mechanism.
SYNTAX
inline
name ( [
arg_lst ] )
{
sequence }
DESCRIPTION
An
inline
definition must appear before its first use, and must
always be global, i.e., defined at the same level as a
proctype
declaration.
The body of an
inline
is pasted into the body of a
proctype
at each point of invocation.
An invocation (an
inline
call)
is performed with the same syntax as a procedure call in
an imperative language, such as
C (see Examples).
An
inline
call can appear wherever a statement can appear.
The parameters to an inline definition are typically names of variables.
Inline calls can be recursive, but not cyclic.
EXAMPLES
The following example illustrates the use of
inline
definitions on the simple alternating bit protocol.
It requires Spin version 3.2 or later.
mtype = { msg0, msg1, ack0, ack1 }; chan sender = [1] of { mtype }; chan receiver = [1] of { mtype }; inline phase(msg, good_ack, bad_ack) { do :: sender?good_ack -> break :: sender?bad_ack :: timeout -> if :: receiver!msg; :: skip /* lose message */ fi; od } inline recv(cur_msg, cur_ack, lst_msg, lst_ack) { do :: receiver?cur_msg -> sender!cur_ack; break /* accept */ :: receiver?lst_msg -> sender!lst_ack od; } active proctype Sender() { do :: phase(msg1, ack1, ack0); phase(msg0, ack0, ack1) od } active proctype Receiver() { do :: recv(msg1, ack1, msg0, ack0); recv(msg0, ack0, msg1, ack1) od }In simulations, line number references are preserved, and will point to the source line inside the definition of an inline wherever possible. In some cases, e.g., at the start of the Sender and the Receiver process, the control point is inside the proctype body, and not yet inside the inline .
NOTES
The scope rules for variables are not changed by
inline
definitions.
The body of the
inline
may contain variable declarations, but these would act just
like when they are declared at the point of invocation.
Their scope is always the entire body of the
proctype
in which the invocation appears.
SEE ALSO
macros(1).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |