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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Thu, 14 Jan 2016 05:37:54 -0800 (PST)*References*: <71319d03-6ab4-48a7-a6a2-53e7c9c48a51@googlegroups.com> <20d67976-47a3-440d-942e-51f3b035554e@googlegroups.com> <393668fc-f7ac-49ad-9f04-598c39d1a771@googlegroups.com> <c6c1cac0-c5d4-46c0-b236-31b9ba2d7d0d@googlegroups.com> <8ef22b8b-cc07-431d-80e9-fa297c087b26@googlegroups.com> <5bcb7c5f-c787-4450-a8f0-efc8f5c64477@googlegroups.com> <63612f81-4693-4928-ad1d-01b0b6024bf8@googlegroups.com> <1cd6ed97-44cb-417a-a97c-bf6ddda91177@googlegroups.com> <5caa4203-e771-4b99-bf70-a621abc9fc51@googlegroups.com> <96A7260B-97B7-4289-A08F-AE26EABD8735@gmail.com>

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 isCapture(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 : Pto 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.

**Follow-Ups**:**Re: [tlaplus] Tagged formulas***From:*Stephan Merz

**References**:**Tagged formulas***From:*Ron Pressler

**Re: Tagged formulas***From:*Leslie Lamport

**Re: Tagged formulas***From:*Ron Pressler

**Re: Tagged formulas***From:*Ron Pressler

**Re: Tagged formulas***From:*Leslie Lamport

**Re: Tagged formulas***From:*Ron Pressler

**Re: Tagged formulas***From:*Ron Pressler

**Re: Tagged formulas***From:*Leslie Lamport

**Re: Tagged formulas***From:*Ron Pressler

**Re: [tlaplus] Tagged formulas***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Tagged formulas** - Next by Date:
**Re: [tlaplus] Tagged formulas** - Previous by thread:
**Re: [tlaplus] Tagged formulas** - Next by thread:
**Re: [tlaplus] Tagged formulas** - Index(es):