NAME
procedures - for structuring a program text.

DESCRIPTION
There is no explicit support in Promela for defining procedures or functions. The reason is that there are several other mechanisms that can provide the same functionality.

The most efficient method to define a procedure is to use a macro or an inline definition. This amounts to an automatic inlining of the text of a procedure call into the body of each process that invokes it. A disadvantage of a macro is that line-number references will be restricted to the location of the macro-call, not a line number within a macro definition itself. This problem does not exist with and inline definition.

Another disadvantage, common to macros and inlines, is that no local variables limited in scope to the procedure body can be used.

A third method, that does not have the above two disadvantages, but can be less efficient, is to declare a separate process with the text of the procedure. The best way to do this is to define this process as a permanent active process, that acts as a server: responding to requests from the user processes via a special globally defined channel, and responding to these requests via a user provided local channel (for an example, see float(7)).

A less attractive method would be to instantiate a new copy of a process once for each procedure call, and wait for that process to return a result (via a global variable or a message channel) and disappear from the system before proceeding. This is less attractive because it produces the overhead of lots of process creations and deletions, and because in an asynchronous system one can never be certain when precisely a terminated process will be removed from the system.

SEE ALSO
inline(1), macros(1), active(2), proctype(2).