Promela Reference -- comments(1)

Promela

Meta Term

comments


NAME
comments - default preprocessing rules for comments.

SYNTAX
/'*' [ any_ascii_char ]* '*'/

DESCRIPTION
A comment starts with the two character sequence /* and ends at the first occurrence of the two character sequence */ . In between these two delimiters, any text, including newlines and control characters, is allowed. None of the text has semantic meaning in Promela.

A comment can be placed at any point in a verification model where white space (spaces, tabs, newlines) can appear.

EXAMPLES

This Promela fragment is indistinguishable to the parser to the following Promela text, written without comments:

NOTES
Comments are removed from the Promela source before any other operation is performed. The comments are removed by invoking the standard C preprocessor cpp (or any equivalent program, such as gcc -E ), which then runs as an external program in the background. This means that the precise rules for comments are determined by the specific C preprocessor that is used. Some preprocessors, for instance, accept the C++ commenting style, where comments can start with two forward slashes and end at the first newline. The specific preprocessor that is used can be set by the user. For more details on this, see the manual page for macros .

With the default preprocessor, conform ANSI-C conventions, comments do not nest. Be careful, therefore, that if a closing comment delimiter is accidentily deleted, all text up to and including the end of the next comment may be stripped.

On a PC, Spin first tries to use a small, built-in macro preprocessor. When this fails, for instance, when macros with multiple parameters are used or when additional preprocessor directives are provided on the command line, the standard external C preprocessor is called. The use of the built-in preprocessor can, with older PC operating systems, avoid the the awkward brief appearance of an external shell window in the parsing phase.

SEE ALSO
macros


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