-a
option for performing a thorough model
syntax check and generates the source C program for a model-specific
verifier. If the Spin syntax checker detects a syntax error within the
Promela source code, SpinRCP parses its error message and finds out the
line number where the error occurred. The Promela Editor marks this line
with an error icon. The No Syntax Error.
output is written to
the Console if no errors are found.