Fun!

Reminds me that one of my favourite exercises in TLA+ is to design an elevator call system.