Promela |
Meta Term |
inline |
NAME
inline -
a stylized version of a macro.
SYNTAX
inline name ( [ arg_lst ] ) { sequence }
DESCRIPTION
An
inline definition must appear before its first use, and must
always be defined globally, that is, at the same level as a
proctype declaration.
An
inline definition works much like a preprocessor macro, in the
sense that it just defines a replacement text for a
symbolic name, possibly with parameters.
It does not define a new variable scope.
The body of an
inline is directly pasted into the body of a
proctype at each point of invocation.
An invocation (an
inline call) is performed with a syntax that is similar to a
procedure call in C, but, like a macro, a Promela
inline cannot return a value to the caller.
An inline call may appear anywhere a stand-alone Promela statement can appear. This means that, unlike a macro call, an inline call cannot appear in a parameter list of the run operator, and it cannot be used as an operand in an expression. It also cannot be used on the left- or right-hand side of an assignment statement.
The parameters to an inline definition are typically names of variables.
An inline definition may itself contain other inline calls, but it may not call itself recursively.
EXAMPLES
The following example illustrates the use of
inline definitions in a version of the alternating bit protocol.
mtype = { msg0, msg1, ack0, ack1 }; chan sender = [1] of { mtype }; chan receiver = [1] of { mtype }; 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; } inline phase(msg, good_ack, bad_ack) { do :: sender?good_ack -> break :: sender?bad_ack :: timeout -> if :: receiver!msg; :: skip /* lose message */ fi; 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 inline definition where possible. In some cases, in the example for instance 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 Promela scope rules for variables are not affected by
inline definitions.
If, for instance, the body of an
inline contains variable declarations, their scope would be
the same as if they were declared outside the
inline , at the point of invocation.
The scope of such variables is the entire body of the
proctype in which the invocation appears.
If such an
inline would be invoked in two different places within the same
proctype , the declaration would also appear twice, and a syntax error
would result.
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 27 November 2010) |