• Spin does not allow sequential procedures. Solution: inlining.
  • Spin does not allow long numbers. Solution: use two ints.
  • Spin does not allow expressing -232 as a numeric constant. Solution: 1<<31.
  • Spin does not know anything about locks, events, delegates. Solution: abandon locks and delegates, model events as booleans.
  • Spin runs out of space using standard search. Solution: use COLLAPSE, and, when it fails, automata.