Promela Reference -- macros(1)


Meta Term


macros and include files - preprocessing support.


#define name	token-string
#define name(arg, ..., arg)	token-string
#ifdef name
#ifndef name
#if constant-expression
#undef name
#include "filename"

Promela source text is always processed by the C preprocessor, conventionally named cpp , before being parsed by Spin. When properly compiled, Spin has a link to the C preprocessor built-in, so that this first processing step becomes invisible to the user. If a problem arises, though, or if a different preprocessor should be used, Spin recognizes an option -Pxxx that allows one to define a full pathname for an alternative preprocessor. The only requirement is that this preprocessor should read standard input and write its result on standard output.


It is always wise to put braces around the replacement text in the macro-definitions to make sure the precedence of operator evaluation is preserved when a macro name is used in a different context, for example, within a composite boolean expression.

The details of the working of the preprocessor can be system dependent. For the specifics, consult the manual pages for cpp that came with the C compiler that is installed on your system.

On PCs, if no macros with more than one parameter appear in the model, and no extra compiler directives are defined on the command line, Spin will use a simple built-in version of the C preprocessor to bypass the call on the external program. When needed, this call can be suppressed by adding a dummy compiler directive to the command line, as in:

The call could also be suppressed by adding a dummy macro definition with more than one parameter to the model itself, as in: The preprocessor that is used can be modified in several ways. The default preprocessor, for instance, can be set to m4 by recompiling Spin itself with the compiler directive -DCPP=/bin/m4 . The choice of preprocessor can also be changed on the command line, for instance, by invoking Spin as: Extra definitions can be passed to the preprocessor from the command line, as in: which has the same effect as adding the following two definitions at the start of the model: as well as passing the additional directive -I/usr/greg to the preprocessor, which results in the addition of directory /usr/greg to the list of directories that the preprocessor will search for include files.


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)