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

*From*: "'Alex Weisberger' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Sun, 7 Mar 2021 20:21:07 -0500*References*: <ef992a35-8d35-48ff-ac1f-d0ea544ffa8an@googlegroups.com>

That is interesting, I would have thought that the answer would be syntactically invalid at first glance. But, in thinking about how the EXCEPT operator would be implemented, it probably has no knowledge of what the function's domain is, and simply loops over all of the provided exceptions, applying each one. This leads to a kind of "mutability" of the function, where the subsequent re-definitions build off of the result of the previous one.

Moving away from how it's implemented, Lamport does go over how the generalized EXCEPT operator behaves in "The Operators of TLA+": https://www.hpl.hp.com/techreports/Compaq-DEC/SRC-TN-1997-006A.pdf (page 11)

[f EXCEPT e1, e2, e3] is just a shorthand for [[[f EXCEPT e1] EXCEPT e2] EXCEPT e3], so each subsequent exception does operate on the result of the previous.

I never read about the EXCEPT operator to this level of depth, so yes, thanks for sharing!

On Sun, Mar 7, 2021 at 7:47 PM Andrew Helwer <andrew.helwer@xxxxxxxxx> wrote:

Consider the following _expression_:LET f == [n \in 0..10 |-> n] IN

[f EXCEPT ![1] = @ + 1, ![1] = @ + 1, ![1] = @ + 1]Fairly weird, because we're assigning the value of 1 multiple times using its previous value each time. What do you expect the value of the final function on 1 to be? Runtime exception? 2? Turns out it's 4!Sort of a weird quirk I found when exploring how TLC interprets functions, don't know whether it's a bug necessarily but thought people might find it interesting.Andrew--

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/ef992a35-8d35-48ff-ac1f-d0ea544ffa8an%40googlegroups.com.

- Alex Weisberger, Senior Software Engineer: House Manage

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/CAC7YZZ%3Dty46QFMmgZxz9EK9KNXqw1wJ59GYq8udNBku78zFZ1g%40mail.gmail.com.

**References**:**[tlaplus] Bug or quirk for how TLC interprets EXCEPT?***From:*Andrew Helwer

- Prev by Date:
**[tlaplus] Bug or quirk for how TLC interprets EXCEPT?** - Next by Date:
**Re: [tlaplus] TLA+ Specification for Einsteins Riddle** - Previous by thread:
**[tlaplus] Bug or quirk for how TLC interprets EXCEPT?** - Next by thread:
**[tlaplus] Using TLA+ for Simulation-proofs** - Index(es):