I think one of Lamport's arguments was that at specification level one shouldn't go for an imperative approach. Imperative is good for "how to" instructions (programs). Declarative is good for "what is" or "what should be" instructions (specifications). So in that sense TLA+ was about helping you build state machines via simple declarative syntax. Of course this was Lamport's argument, in practice, your approach may work just as well. Will definitely be interested to see how your approach evolves.