[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:

VARIABLE x

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.