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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Fri, 15 Jan 2016 09:18:21 +0100*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> <717f8f09-a566-4334-b186-2d5c40d2a88e@googlegroups.com> <835F9366-B9D4-4B4A-8159-EB5D201AF01B@gmail.com>

My sincere apologies for these messages: I don't know what I was thinking. Of course the level of CHOOSE x : x = e is determined by the level of e, and CAPTURE cannot be defined in TLA+. Stephan > On 14 Jan 2016, at 14:42, Stephan Merz <Stepha...@xxxxxxxxx> wrote: >>> >>> Sorry for being late to this discussion. I think that basically what you want is >>> >>> Capture(e) == CHOOSE x : x = e >>> >>> 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. > > 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. > > Stephan >

**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

**Re: [tlaplus] Tagged formulas***From:*Ron Pressler

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

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