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

Re: [tlaplus] What if every action could use all the variables? Would we need to define Init?

I am not sure that I understand your question (and since nobody else answered, I am perhaps not the only one). In particular, your modified specification has an initial condition, and it is not clear to me why it would somehow indicate that you can get rid of initial conditions.

In general, note that nothing in TLA+ requires you to state an initial condition. For example,

  [][x \in Nat /\ x' = x+1]_x

is a well-formed TLA+ formula with well-defined semantics. It can be thought of as a specification that has two kinds of behaviors:

- in the first kind, the value of variable x is not a natural number in the initial state, and it never changes along the behavior;
- in the second kind, the initial value of x is a natural number and it may increase any number of times along the behavior.

You could even rule out the first kind of behaviors by adding a liveness condition such as

  []<>(x \in Nat)

rather than adding the obvious initial condition.

Since a specification is a definition, there is nothing "wrong" with the above specification. Whether it is useful is another question. In particular, TLC expects specifications to be of the form

  Init /\ [][Next]_v /\ L

and it expects the initial condition to fix values for all of the variables used in the specification. This is a simplifying assumption, and you could certainly come up with reasonable specifications that do not fix the values of some variables initially because they will be needed only later. This is fairly frequently case in PlusCal when you declare a variable without specifying an initial value; the PlusCal translator then adds default initializations to make TLC happy.

Not sure if I even started answering your question – please feel free to rephrase it.


On 21 Jan 2019, at 03:08, Apostolis Xekoukoulotakis <apostolis.xe...@xxxxxxxxx> wrote:

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?

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.