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.