If we know the state of all the variables, then we can make the actions stricter and thus not need to define the initial conditions. Here I have the Two Phase Commit and TCommit. I changed the init conditions so that one is 'aborted' , the other 'commited' and the rest 'working'.
If you give RM the numbers {0, 1, 2} , then you will see that the TPC refines TC.
This is because some actions know that this is an invalid state and do not trigger.
In other words, with complete information about the state from all participants, init is not needed and refinement can be thought as local, per action.
Would I be correct if I said that TLA is useful only when information is incomplete?