Verification
The most complex preference page in SpinRCP is the Verification preference page.
In the upper part the user can export current verification parameters (verification profile) to an
xml file and import or reload a previously saved verification profile. Verification options are
accessible below in two tabs: Basic Options and Advanced Options.
In the Basic Options tab a user can select a correctness property to be proved (either
safety or liveness) with several additional options, the search mode (exhaustive, bitstate hashing
or hash-compact), how a full queue behaves in verification (either blocks or loses new messages),
the explicit use of user entered compile-time and run-time parameters that supersede the clicked
options and elsewhere entered parameters, and how a never claim (if any) is specified. A never
claim can be specified in four different ways. In the first one, which is a default, a never
claim or an LTL formula is specified in the model itself. In the text field right to the label a
name of the never claim/LTL formula to be checked against the model has to be written. Such an
in-model never claim specification is possible since Spin Version 6. The second way is to enter
an LTL formula in the text field. The third one is to enter or select the file name, in which the
single-line LTL formula is written. The last way to specify a never claim is to enter or select a
file name with a contained never claim.
In the Advanced Options tab it is possible to enter several advanced verification parameters
(the amount of the available physical memory in megabytes, the estimated state space size, the
maximum search depth, number of hash-functions in bitstate mode, extra verifier generation options,
extra compile-time directives, and extra run-time options) and select some error-trapping and
verification run type options.