Promela |
Meta Term |
macros |
NAME
macros and include files - preprocessing support.
SYNTAX
#define name token-string #define name(arg, ..., arg) token-string #ifdef name #ifndef name #if constant-expression #else #endif #undef name #include "filename"
DESCRIPTION
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.
EXAMPLES
#include "promela_model" #define p (a>b) never { /* <>!p */ do :: !p -> assert(false) :: else /* else ignore */ od }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.
NOTES
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:
$ spin -DDUMMY -a modelThe call could also be suppressed by adding a dummy macro definition with more than one parameter to the model itself, as in:
#define dummy(a,b) (a+b)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:
$ spin -P/bin/m4 modelExtra definitions can be passed to the preprocessor from the command line, as in:
$ spin -E-I/usr/greg -DMAX=5 -UXAM modelwhich has the same effect as adding the following two definitions at the start of the model:
#define MAX 5 #undef XAMas 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) |