Syntax Check

Syntax Check option in the Tool Bar 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.