Search and Coverage of SPIN: SPIN has a highly optimized state exploration algorithm. It supports random, interactive and guided simulation, and both exhaustive and partial coverage, based on either depth-first or breadth-first search.
To reduce the problem of running out of memory storing the states that have been visited (so that the search will not explore them again), SPIN provides an option called bitstate hashing, also known as supertrace. Bitstate hashing uses memory as a bit vector. When a state is visited during SPIN’s exploration, its state vector is hashed to a bit in memory: the bit indicates whether the state has been visited previously. If a different state vector hashes to the same bit location, SPIN will erroneously conclude that the state has been visited and will terminate exploration from that state. This may lead to false negatives (errors may not be found), but not false positives (no false error reports).
Paradoxically, using the bitstate option may lead to increased coverage of the state space, because more of it can be explored in the given amount of memory.