[tlaplus] Bug or quirk for how TLC interprets EXCEPT?

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

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.