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: 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.