Verification preference page
The most complex preference page in SpinRCP is the Verification preference page.
In the upper part a user can export current verification parameters (verification profile) to an
xml
file and import or reload a previously saved verification profile. The current verification profile
file name including date and time of its creation are shown. Verification options are
accessible below in three tabs: Basic Options, Advanced Options, and Iterative/Swarm Run.
In the Basic Options tab a user can select first a correctness property to be proved (either
safety (default) or liveness) and several additional options (assertion violations and invalid end states
for safety properties, non-progress or acceptance cycles with/without weak fairness for liveness properties,
and whether to report unreachable code and check xr/xs assertions or not for both correctness properties types.
Then, the storage mode (exhaustive, bitstate hashing or hash-compact) can be selected. Two lossless
compression methods (minimized automata and collapse compression) are available for the exhaustive storage mode.
If any never claim exists, it may be considered in the model verification process by clicking the
Apply never claim button. 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.
By checking the Use these parameters checkbox, the Compile-time and Run-time text fields become enabled
and a user can explicitly enter the compile-time and run-time parameters that supersede
the clicked options and parameters entered elsewhere. All other buttons, checkboxes, labels,
and text boxes become disabled.
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, the size for minimized automaton,
extra verifier generation options, extra compile-time directives, and extra run-time options).
Next, some error-trapping options can be selected. A user can enter an error number at which verification
will stop or require that verification does not stop at errors. Additional options in error trapping is
to save all error trails, add complexity profiling and compute variable ranges.
Similar as in simulation, the behavior of a full queue in the verification process can be selected.
It may either block (default) or lose new messages.
In the last group of options on this tag, two different search modes can be selected (depth-first search (default)
or breadth-first search). In both options, partial ordered reduction may be applied for reducing the number
of reachable states. In the depth-first search mode, two additional options are available: iterative search
for short trail and bounded context switching using a given bound (default 0).
The Iterative/Swarm Run tag can be used to apply iterative sequential or swarm parallel runs of a
pan
verifier if the bitstate hashing storage mode is selected. If the verification process uses other
storage modes, exhaustive or hash-compact, all buttons, labels, and text fields on this tag are disabled.
Two bitstate search refinements are available: iterative sequential runs (default) of pan
verifier
with the hashtable size increasing step by step from -w18
upto -w35
until an error is
found and so-called swarm parallel runs, where N instances of pan
verifiers are executed in
parallel (on N cores) and -w
is incremented every M runs. For each run, several other parameters
are also randomized for spreading search in different directions and thus increasing the covered fraction of
state space. Values for parameters N and M have to be set. The default value for N and M are 10 and 1,
respectively.
A click on the Restore Defaults button restores the default selections of options and default values of parameters.
A click on the Apply button applies the selected options and entered/selected parameters.
A click on the OK button applies the selected options and entered/selected parameters and closes the page.
If the Verification preference page is opened after selecting the Verification option in the Menu Bar Run command
or in the Tool Bar, a click on the OK button starts the verification.
A click on the Cancel button cancels the selected options and entered/selected parameters, reverts their value
to the previous ones and closes the page.