State Tables
State Tables option in the Menu Bar Run command
opens the State Tables
preference page. After selecting
the appropriate verifier state tables version, turning statement merging
on or off, and clicking the OK button, the Spin verifier is generated,
then compiled, and then pan
is run with -d
option for producing
state tables for each proctype
and each never claim in the model.
Spin output is postprocessed and the most useful information is pretty-printed on the Console.
The following information is contained in each state table: the source and target state of
the transition (From State and To State), the transition ID, the transition type
(A=atomic, D=d_step, L=local, G=global), source-state labels (p=progress, e=end, a=accept),
the line number and the statement in the Promela model source file causing the transition.