Re: [tlaplus] Usage of the ! operator

Section 6.2 states:

In general, for any construct that introduces bound identifiers:

• !(e1, . . . , en ) selects the body (the _expression_ in which the bound iden- tifiers may appear) with each _expression_ ei substituted for the ith bound identifier.
• [...]

Thus, Phase2b(a)!(X) represents

/\ X.type = "2a"
/\ X.bal >= maxBal[a]
/\ Send([type |-> "2b", bal |-> X.bal, val |-> X.val, acc |-> a])
/\ maxVBal' = [maxVBal EXCEPT ![a] = X.bal]
/\ maxBal' = [maxBal EXCEPT ![a] = X.bal]
/\ maxVal' = [maxVal EXCEPT ![a] = X.val]

The step in the proof that you originally refer to

<2>1. PICK m \in msgs : Phase2b(a)!(m)

introduces the name `m' for the message for which action Phase2b(a) is performed, adds the assumption `m \in msgs' to the set of hypotheses that are actively used, and by referring to <2>1 inside the proof one invokes the above conjunction (with X replaced by m) without having to retype it.

Hope this helps,

Stephan

On 20 Aug 2019, at 00:48, Saswata Paul <paulsaswata1@xxxxxxxxx> wrote:

Hi,

I have gone through section 6 of the TLA+2 Preliminary Guide and I have reached the following conclusion:

Phase2b(a) ==
\E m \in msgs :
/\ m.type = "2a"
/\ m.bal >= maxBal[a]
   /\ Send([type |-> "2b", bal |-> m.bal, val |-> m.val, acc |-> a])
   /\ maxVBal' = [maxVBal EXCEPT ![a] = m.bal]
   /\ maxBal' = [maxBal EXCEPT ![a] = m.bal]
   /\ maxVal' = [maxVal EXCEPT ![a] = m.val]

Since m is the first bound identifier on the right-hand side of _expression_ Phase2b(a), the _expression_ Phase2b(a)!(X) translates to the following:-

\E X \in msgs :
/\ X.type = "2a"
/\ X.bal >= maxBal[a]
   /\ Send([type |-> "2b", bal |-> X.bal, val |-> X.val, acc |-> a])
   /\ maxVBal' = [maxVBal EXCEPT ![a] = X.bal]
   /\ maxBal' = [maxBal EXCEPT ![a] = X.bal]
   /\ maxVal' = [maxVal EXCEPT ![a] = X.val]

A clarification whether this is correct (or the correct translation if this is wrong) will be really helpful.

Thank you

On Mon, Aug 19, 2019 at 5:07 PM Saswata Paul <paulsaswata1@xxxxxxxxx> wrote:
Thank you.

On Monday, August 19, 2019, Leslie Lamport <tlaplus.ll@xxxxxxxxx> wrote:
The third meaning of ! is for naming subexpressions of an _expression_ and is intended only for use in
proofs. It is explained in section 6 ofTLA+ Version 2 A Preliminary Guide
(https://lamport.azurewebsites.net/tla/tla2-guide.pdf).

Leslie

On Monday, August 19, 2019 at 12:24:37 PM UTC-7, Saswata Paul wrote:
Hi,

  According to the book, I could find only two usages of the ! operator :- in EXCEPT and in operator names.

However, in the formal proof of paxos (https://github.com/tlaplus/v1-tlapm/blob/master/examples/paxos/Paxos.tla), on line 250, the ! operator has been used and I am not quite clear about the context in this case.

I will greatly appreciate it if someone can explain the meaning of this particular line of code:

<2>1. PICK m \in msgs : Phase2b(a)!(m)

Thanks

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/hLYm8vb3n1Y/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8ea5175a-a86e-4565-8ebc-da9e5eb7d97c%40googlegroups.com.

--
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+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAHeFUE-i97gYL22W%2BzZOOYyS%2BuMr-8i9pq_F%3Dp%2BwcdZPvgvvPA%40mail.gmail.com.