Automata View
Automata View option in the Tool Bar opens the
Automata View
preference page,
where the user can select in which graphical format the automata should be displayed.
Ten different file formats are currently available. SpinRCP uses options
-o3
and
-a
to generate the verifier source C code, then compiles it to
pan
and runs
pan
using run-time option
-D
.
This option generates state
tables for each
proctype
and each never claim in the
format accepted by the dot tool from Graphviz. These state tables are redirected to a text
file. Next, the dot tool transforms this text file to a set of files
(one file for automaton) with the previously selected graphical format.
Then, a dialog appears, where the automaton to be displayed can be selected.
Finally, a system program, assigned to a given file type is opened and the
selected automaton is displayed.