> Decline to buy: property stays with bank (auction abstracted out)

Ignoring an entire game mechanic is really stretching the definition of “abstracted out”…

Also, at the bottom it defines a “Liveness: someone eventually wins” property which I believe cannot be proven. Monopoly doesn’t have any rules forcing the game to end eventually. There is only a probabilistic guarantee, and even that only applies if the players are trying to win; if the players are conspiring to prevent the game from ending then they’re unlikely to fail.

PlusCal is recommended as the gentler on-ramp to TLA+ for first learning.