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.)
Precisely.
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.