Spin theory

• Generates a Büchi Automaton from the Promela specification.

  • Finite-state machine w/ special acceptance conditions
  • Transitions correspond to executability of statements

• Depth-first search of state space, with each state stored in a hashtable to detect cycles and prevent duplication of work

  • If x followed by y leads to the same state as y followed by x, will not re-traverse the succeeding steps

• If memory is not sufficient to hold all states, may ignore hashtable collisions: requires one bit per entry. # collisions provides approximate coverage metric

Notes: