I think it's a bit bad practice to mix your model data with the model functions/state
this is wiring, you can wire the pattern in any way you'd like
The constraints of the pattern are only:
This factoring is "unique", you just can't make it up (IMHO)
You can define formalisms on top of it, but you cannot decide arbitrarily what the foundation is, it is foundational.
you can't throw up any formalism in the air and say that one works too,
My point is that TLA+ is a formalism which can be used to describe any state machine as we know it, therefore I claim it is foundational.