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

}

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