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
/* comment */ init /* comment */ { int /* an integer */ v /* variable */; v /* this / * is * / okay */ ++; }This Promela fragment is indistinguishable to the parser to the following Promela text, written without comments:
init { int v; v++; }
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) |