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. Nine different file formats are currently available. SpinRCP launches Spin with option -a (and -o3 if the statement merging is turned off on Automata View preference page) for generating 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, dot transforms this text file to a set of files (one file for automaton) with the previously selected graphical format. Then, if requested in Automata View preference page a dialog window appears, where the automaton to be displayed can be selected. After a click on the button of the selected automaton, a system program, assigned to a given file type is opened and the selected automaton is displayed.

Automata are represented by directed graphs containing states and edges between states. Colored states and edge types have the following meanings:
  1. Blue rectangle represents a Promela end state. It can be either the state where the Promela proctype terminates its execution (after the closing curly bracket) or the state labeled with the "end" prefix (e.g. end1, endstate) within the Promela model.
  2. Red ellipse represents a Promela accept state. Accept states are mainly used within automatic generated never claims.
  3. Green ellipse represents a Promela progress state.
  4. Non-bold edge represents a Promela statement that contains only local variables, otherwise it is bold.
  5. Dotted edge represents the statement(s) within an atomic or d_step block.
A click on the Quit button closes the dialog window and completes Automata View command execution.