Very nicely written. In addition, the example chosen was itself lovely to play with. Explicit-state model checkers do this at scale. Readers may be interested

Very nicely written. In addition, the example chosen was itself lovely to play with. Explicit-state model checkers do this at scale. Readers may be interested in the internals of the TLA+ model checker, esp. the encoding of the state and dealing with disk. Model Checking TLA+ Specifications by Yuan Yu, Panagiotis Manolios, and Leslie Lamport (1999) https://lamport.azurewebsites.net/pubs/yuanyu-model-checking.ps https://lamport.azurewebsites.net/pubs/yuanyu-model-checking...