Syntax Check

Syntax Check option in the Menu Bar Run command uses Spin -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.