--
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.
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.
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.• [...]
<2>1. PICK m \in msgs : Phase2b(a)!(m)
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.
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.