MSC Viewer

The MSC Viewer is used for a graphical display of the Spin simulation output trail. It works in two different modes.

In the first one it displays an already generated simulation trail from a file of type out. This kind of MSC display can be achieved 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.

The second mode of displaying the MSC is "on-the-fly" when the simulation is running. In this mode, two Java threads run in parallel: a Spin simulation thread and an MSC refreshing thread. The simulation thread executes the Spin simulation (random, guided, or interactive). Simulation output is parsed line by line and for each new parsed line the list of created processes and messages that have been sent and received up to this time is updated. In parallel, the MSC refreshing thread is refreshing the MSC displayed in MSC Viewer. If any new process or any new message has been added to the corresponding list since the last screen refresh, the MSC is changed accordingly.