Verification
Verification option in the Tool Bar opens the quite complex
Verification
preference page. After selecting and/or entering the appropriate
verification parameters and clicking the OK button, the model
syntax check using the default
and extra verifier generation options (if specified on the Verification
preference page) is performed first.
If there is no syntax error within the model, the model-specific verifier
pan.c
source C file is
generated. After that, the C compiler is invoked that compiles the
verifier source file using the compile-time options (according to the
selections in the Verification preference page) to the verifier
executable file called
pan
. Finally, the verifier
runs using the selected options and parameters entered on the Verification
preference page.
A printout of a verification run is shown in the Console View.
If the verification finds an error, a counterexample is generated
and saved in a so-called error-trail file with the file extension
.trail
appended to the
original Promela model file name. If selected, multiple error-trail
files may be produced. The trail file(s) can be used in a guided
simulation that replays the execution that violated the property.