Automata View
Automata View option in the Menu Bar Run command 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:
- 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.
- Red ellipse represents a Promela accept state. Accept states are mainly used within
automatic generated never claims.
- Green ellipse represents a Promela progress state.
- Non-bold edge represents a Promela statement that contains only local variables, otherwise it is bold.
- 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.