NAME
macro definitions and include files - default preprocessing rules.

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 by default processed by the standard C preprocessor, conventionally named cpp, before being parsed by Spin. When properly compiled, Spin is has a pointer to this preprocessor builtin, 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
Macro definitions are especially useful in combination with never(2) claims, to defined shorthands for symbolic propositions. The are also useful as a simple mechanism to replace the procedure call mechanism that Promela lacks.

#define p	(a>b)

never {	" <>!p "

	do

	:: p

	:: !p -> assert(false) /* violation */

	od

}

NOTES
The details of the working of the preprocessor are determined by the properties of the local preprocessor that is invoked. For the specifics, consult the manual pages for cpp or m4 on your system.

SEE ALSO
comments(1),never(2)