Simulation preference page
Simulation preference page offers the user the possibility to select the Spin simulation mode (random, guided, or interactive),
the number of initial steps skipped (default 0), the maximum number of simulation steps (default 10000), how a
full queue is simulated (either blocks (default) or loses new messages), select simulation
output filters (tracking global and/or local variables, very verbose tracking of
variables, suppress details at the end of simulation, suppress print statements
in simulation) and select or enter extra Spin options.
Optionally, a seed value can be set for random simulation. It ensures repeatability.
The same seed produces the same execution run. If no seed is set, it will be randomly generated for each run.
If checked, the seed value will be printed at the end of simulation.
For guided simulation either the default Spin trail file with the extension trail
added to the original Promela
source file (default) or any other Spin trail file can be selected. The latter option should be used in cases where the verification
run produced more trail files, one for each disclosed error. For example,
the Promela model specified in protocol.pml
file could produce the following error-trail files:
protocol.pml1.trail
,
protocol.pml2.trail
, and
protocol.pml3.trail
. In guided simulation mode, a user can select the option to use pan instead of Spin to simulate the
model containing embedded C-code.
If this option is selected, pan will read and execute the trail, found previously during the verification run. The default pan execute
trail option is -r
, but several other options may be selected. Displaying of MSCs is possible only by
using -g
option.
In any simulation mode a user can select and/or enter several extra Spin options, which are included in Spin simulation command.
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 Simulation preference page is opened after selecting the Simulation option in the Menu Bar Run command or in the Tool Bar,
a click on the OK button opens the Simulation
view, where the simulation can be started.
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.