• Spin does not allow sequential procedures. Solution: inlining.
• Spin does not allow long numbers. Solution: use two ints.
• Spin does not allow expressing -2³² 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.