I think you'd be better off starting with a simpler formalism for this, like Linear Temporal Logic. That's a good pick because there's a straightforward mapping to Büchi automata. This will give you some more intuition on model checking in general, but TLA+ is much more complex than LTL.

(The most popular model checker for TLA+, TLC, is a brute forcer that represents the state space as a directed graph. Lamport talks about it a bit in Specifying Systems.)