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

*From*: Saswata Paul <paulsaswata1@xxxxxxxxx>*Date*: Tue, 20 Aug 2019 13:31:09 -0400*References*: <dd8d25b8-90ac-4fb2-b919-4fcf6325f6c3@googlegroups.com> <8ea5175a-a86e-4565-8ebc-da9e5eb7d97c@googlegroups.com> <CAHeFUE83VQFednaFqZBB3uk5oA3wD5WeSbgmYwf8Q8i8u9G7Bg@mail.gmail.com> <CAHeFUE-i97gYL22W+zZOOYyS+uMr-8i9pq_F=p+wcdZPvgvvPA@mail.gmail.com> <A8DAE3C3-661B-4F08-BF9B-7551E4ED2D09@gmail.com>

Yes. Now it is clear. Thank you.

On Tuesday, August 20, 2019, Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

--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,StephanOn 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 youOn 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/ ), on line 250, the ! operator has been used and I am not quite clear about the context in this case.paxos/Paxos.tla 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

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

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAHeFUE8JDWj%3DfYOpE9oUQ2dS9H_vr6UuejPMTrq7wmpzNTSomg%40mail.gmail.com.

**References**:**[tlaplus] Usage of the ! operator***From:*Saswata Paul

**[tlaplus] Re: Usage of the ! operator***From:*Leslie Lamport

**Re: [tlaplus] Usage of the ! operator***From:*Saswata Paul

**Re: [tlaplus] Usage of the ! operator***From:*Saswata Paul

**Re: [tlaplus] Usage of the ! operator***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Record Equality** - Next by Date:
**[tlaplus] Scope of the QED keyword** - Previous by thread:
**Re: [tlaplus] Usage of the ! operator** - Next by thread:
**[tlaplus] Re: Usage of the ! operator** - Index(es):