Promela Reference -- inline(1)


Meta Term


inline - a stylized version of a macro.

inline name ( [ arg_lst ] ) { sequence }

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.

The following example illustrates the use of inline definitions in a version of the alternating bit protocol.

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 .

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)