Usage of the ! operator

[Saswata Paul]

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

[Leslie Lamport]

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

[Saswata Paul]

Thank you. 

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

[Saswata Paul]

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 <paulsa...@gmail.com> wrote:

Thank you. 

On Monday, August 19, 2019, Leslie Lamport <tlapl...@gmail.com> 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+u...@googlegroups.com.

[Stephan Merz]

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

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

[Leslie Lamport]

Mea culpa.  One can no longer write  a SV!< b  in TLA+.  Version 2 of TLA+ allows this expression to be written in the  more readable form  SV!<(a, b).  I had forgotten that it also disallows the previous syntax.  So, this is a bug in the Decompose Proof command.

Leslie

[Saswata Paul]

Yes. Now it is clear. Thank you. 

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.

--
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/A8DAE3C3-661B-4F08-BF9B-7551E4ED2D09%40gmail.com.