[tlaplus] Usage of the ! operator

[Saswata Paul <paulsaswata1@xxxxxxxxx>]

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 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/dd8d25b8-90ac-4fb2-b919-4fcf6325f6c3%40googlegroups.com.