Simulation
Simulation option in the Tool Bar Run command opens the
Simulation
preference page, where the user can select the mode of simulation (random,
guided, interactive), different simulation options and set simulation parameters.
A click on the OK button opens the
Simulation view, where the simulation can be started.
Random simulation is a good approach for first
examination of a Promela model behavior by observing its execution run.
At each point of the execution path where more nondeterministic choices can be
taken, a choice for the continuation of the execution run is selected at random.
Guided simulation uses an error-trail file produced during a
verification run. Therefore, if the verification discloses an error, guided
simulation will be used for
displaying the execution run that violates the checked property of a model.
Either the default Spin trail file with the extension
.trail
added to the
original Promela source file or any other Spin trail file can be selected for
guided simulation. The latter option should be used in cases where the verification
run produced more trail files, one for each disclosed error. For example, verification of
the protocol.pml
Promela model can produce the following error-trail files:
protocol.pml1.trail
,
protocol.pml2.trail
, and
protocol.pml3.trail
.
Interactive simulation allows a user to select one from all executable
Promela statements at a given moment in the interactive simulation dialog, in
order to resolve the non-deterministic continuation of the execution run.
A click on the Quit button closes the dialog and terminates the interactive
simulation.
Two Java threads run in parallel during the simulation: a Spin simulation
thread and an MSC refreshing thread. The simulation thread executes the
Spin simulation (random, guided, or interactive) and displays Spin textual simulation outputs on the Console.
In parallel, the MSC refreshing thread is displaying the MSC in the
MSC Viewer window.
The variable values' and queue contents' values are updated in two separate
tables at the bottom of the Simulation View.