Symbolic Simulator

The simulator is a validation tool that enables examination of the possible dynamic executions of a system during early design (or modeling) stages. In this sense, it provides an inexpensive mean of fault detection prior to verification by the model-checker. The simulator is also used to visualise executions (i.e. symbolic traces) generated by the verifier. Please see the Symbolic Traces section for a brief introduction of the concept.

The simulator consist of four panels: the leftmost called simulation control, the middle called variables, the upper right called processes, and the lower right called message sequence chart.