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

On Tue, Jan 22, 2019 at 7:40 PM Apostolis Xekoukoulotakis <apostolis.xe...@xxxxxxxxx> wrote:

I am at the moment only interested in specifications that have actions in them. For me, an action is a form of abstract vector. And Next is a form of a vector field where at each point , there might be multiple actions.

Can we omit the initial conditions in a spec where Next is a union of actions? In the original specification, the initial conditions were crucial, because they needed to respect a global invariant so that the spec refined TCommit.
In my revised spec, I have made the actions more strict, they have complete information about all the variables. I added an Init so as that TLC would accept it for model checking. Pick any Init value for both TCommit and Two Phase Commit.
You will see that the refinement still holds. In my revised spec, there is no need to prove that a global invariant holds.

The reason we do not want the revised spec is because , in reality , most agents work under incomplete information, so we cannot assume that they know everything.

I am trying to identify certain categories of Specs and their morphisms/refinements. (at the moment without liveness properties)

1. Specs with actions without Init, where no global invariant is needed.
2. Specs with actions with Init because a global invariant is needed.
3.Specs where the restrictions is a general temporal formula (with possible liveness properties)

The question was whether the 2nd category is different from the 1st. It seems to me that it is.
Another interesting question is if the 3rd category didn't have liveness properties, only safety properties would it then collapse to the 2nd category. Are there general safety specifications that cannot be written in the form of actions?

On Tue, Jan 22, 2019 at 10:07 AM Stephan Merz <stepha...@xxxxxxxxx> wrote:
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.

Regards,
Stephan

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.
<TwoPhase.tla><TCommit.tla>

--
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.