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

Re: [tlaplus] Tagged formulas

On Thursday, January 14, 2016 at 3:42:19 PM UTC+2, Stephan Merz wrote:
> That was my original intuition. I don't know what TLA+'s policy on backwards compatibility is, but changing the action semantics of CHOOSE now may break existing specs in possibly subtle ways.

No, it shouldn't. A CHOOSE _expression_ returns a value, i.e., a constant. So the proposed change doesn't break the semantics but only the level-checking algorithm, which we know to be an approximation.

Hmm, so I may have misunderstood you after all. Trying:


    Capture(e) == CHOOSE k \in {e} : k = e

    Next == /\ x' = x + 1 

                  /\ PrintT(x)                   \* => 1

                  /\ PrintT(x')                  \* => 2

                  /\ PrintT(Capture(x))    \* => 1

                  /\ PrintT(Capture(x)')   \* => 2

    Spec == (x = 1) /\ [][Next]_<<x>>

So Capture(x)' /= Capture(x), and this seems to be more than just level-checking.

If the difference is due to my writing `CHOOSE k \in {e} : k = e` instead of `CHOOSE k : k = e`, then the latter is currently unsupported by TLC anyway.