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.