Simulation
Simulation option in the Menu Bar Run command opens the
Simulation
preference page, where the user can
select the type of simulation (random, interactive, guided), the number
of initial steps skipped, the maximum number of simulation steps, how a
full queue is simulated (either blocks or loses new messages), a seed
value for the random simulation, and the trail file for the guided simulation.
Then the Simulation view opens and the simulation can start.
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.
A seed value can be set for random simulation. It ensures repeatability.
The same seed produces the same execution run.
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.
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,
the protocol.pml Promela model can produce the following error-trail files:
protocol.pml1.trail
,
protocol.pml2.trail
, and
protocol.pml3.trail
.
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 and displays Spin textual simulation outputs on the Console.
In parallel, the MSC refreshing thread is displaying the MSC in the MSC Viewer.
Currently, continuous and message-by-message simulations are available.
The variable values' and queue contents' values are updated in two separate
tables at the bottom of the Simulation View.
Several Simulation View options to adapt the display of MSCs are available
below the simulation buttons. The user can do the following:
- select a subset of messages that will be ignored and not displayed in the MSC diagram,
- select a subset of messages that will be displayed in the MSC diagram,
- rename selected messages,
- join two or more processes into a new virtual process, and
- select whether to show or hide message parameters.
For each option, a hint about the input command syntax which has to be typed
into the corresponding textfield together with an example of use is displayed
if you place the cursor above that textfield. In order to illustrate some of
these options, an MSC with a virtual process called
joined23
that joins
original processes with IDs
2
and
3
and with the renamed messages, where each
message ID was prefixed by letter
'm
' is shown here. You can see how the
corresponding MSC is being changed accordingly.