Simulation

Simulation option in the Menu 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 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.