Re: [tlaplus] Usage of the ! operator

[Saswata Paul <paulsaswata1@xxxxxxxxx>]

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@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAHeFUE83VQFednaFqZBB3uk5oA3wD5WeSbgmYwf8Q8i8u9G7Bg%40mail.gmail.com.