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

Re: [tlaplus] Tagged formulas

On Thursday, January 14, 2016 at 12:31:37 PM UTC+2, Stephan Merz wrote:
Sorry for being late to this discussion. I think that basically what you want is

Capture(e) == CHOOSE x : x = e

When I first encountered the problem, that was the very first thing I tried...
with the additional effect that the _expression_ Capture(e) is considered as a level-0 _expression_ by SANY. (If you try writing Capture(x')' for the above definition where x is a state variable, SANY will complain about level-incorrectness.)


It seems to me that this wouldn't cause problems semantically. In fact, the more general solution would be to consider any _expression_

  CHOOSE x : P

to be of level 0, whatever the level of P (currently, P must be of level <= 2, but even an extension to CHOOSE expressions for temporal formulas should be acceptable).

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.