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.