A click on the Simulation button in the Tool bar opens the Simulation preference page. It
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.
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. 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.
Simulation preference page
Interactive simulation dialog
Interactive simulation allows you to select one out of all executable Promela statements in order to resolve the
nondeterministic continuation of the execution run. The selection can be done in the interactive simulation dialog.
A click on the Quit button closes the dialog and terminates the interactive simulation.
Guided simulation uses an error-trail file produced in a verification run. Therefore, if the verification
discloses an error, the 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 Promela model specified in protocol.pml file could
produce the following error-trail files: protocol.pml1.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
After the Simulation button in the Tool Bar has been pressed and
the Simulation preference page confirmed the Simulation View is shown. At the top of the view
there is a label showing the selected simulation type (Random Simulation, Guided Simulation,
or Interactive Simulation) including the Promela model filename and four Simulation/Replay
buttons: Run, Stop, Message Step, and Single Step. The simulation type can be changed by
clicking the View Menu (a small downward pointing arrow in the top right corner of the
Simulation View) and selecting the new simulation type from the drop-down menu that appears.
During the simulation/replay, two Java threads run in parallel: a Spin simulation/replay thread and an MSC
refreshing thread. The simulation/replay thread executes the Spin simulation (random, guided, or
interactive) and displays Spin textual simulation outputs on the Console. The variable values
and queue contents values are updated in two separate tables at the bottom of the Simulation View.
The current simulation step number is shown at the top of the tables. In parallel, the MSC
refreshing thread is displaying the MSC in MSC Viewer window »on the fly«.
By clicking the Run button, the simulation starts and continues without stopping till the end
or till the click on the Stop button. MSCs are being refreshed periodically each time
the MSC refresh interval expires as given on the MSC Viewer preference page. The default and
minimal value of the MSC refresh interval are 5 and 1 millisecond, respectively. During the
simulation run the replay buttons Message Step and Single Step are being disabled. They become
enabled again when the simulation ends or is stopped. By clicking the Single Step button,
a user can replay the simulation run step by
step through Promela model statements. On the other side, by clicking the Message Step button,
MSC is being drawn message by message (if any message is sent and received in the model at all)
and process by process (each time a new process has been created). Message by message and step
by step simulation replay can be combined. For example, by successive clicking the Message
Step button a user could come to the interesting part of the simulation trace, then replay it
in detail by clicking the Single Step button and finally use the Message Step button again.
Not only the simulation run, but also the replay run can be stopped with a click on the Stop
Spin textual simulation
outputs on the Console
A random simulation MSC for leader.pml
MSC Viewer preference page
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 the first four options, a hint about the input command syntax which has to be typed into the
corresponding text field together with an example of use is displayed if you place the cursor
above that text field. In order to illustrate some of these options, the display of an MSC
with a virtual process called
that joins original processes with IDs
and with the
renamed messages, where each message ID was prefixed by letter
' is requested. In the MSC Viewer you can see how the
corresponding MSC is being changed accordingly.
Simulation view with parameters
An MSC View with the renamed
messages and a virtual process
Each Spin simulation output is written to a file. Its name is obtained by concatenating the name
of a Promela model, simulation mode (rnd_sim,
gui_sim or int_sim), and file extension
out. For example, the Spin random simulation output of
leader.pml Promela model is stored to file name
An already generated simulation trail from a file of type
out can be graphically displayed in the MSC Viewer in two
different ways, either by a double-click on an
out file in the
Model Navigator View or by a click on the Import Trail button in the Tool Bar when the
Simulation View is active and selecting an
out file from the Import Trail dialog. An
out file can be read into the SpinRCP's text editor as text
if you right-click it in the Model Navigator View and select Open With > Text Editor.