[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

What if every action could use all the variables? Would we need to define Init?

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?

Attachment: TwoPhase.tla
Description: Binary data

Attachment: TCommit.tla
Description: Binary data