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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Thu, 14 Jan 2016 23:53:07 -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> <fd048441-9135-4bab-bf6a-2a535985eb0e@googlegroups.com>

On Friday, January 15, 2016 at 2:37:02 AM UTC+2, Leslie Lamport wrote:

Hi Ron,

First of all, you are proposing to add a fundamentally new kind of

operator to TLA (and not just to TLA+). In 25 years, no one to my

knowledge has seen any need for such an operator. So, I'm not about

to add it because one user finds that it makes writing his specs more

convenient.

Not only that, but a novice user :) Which is why I'm not saying TLA+ should have the operator, only proposing that it may. In addition, there are workarounds -- e.g. instead of:

VARIABLE x, y

Foo(t) == t + x

and then

Foo(3) = 3 + x

Foo(CAPTURE y)' = y + x'

we can define:

Foo(t) == t + x

Foo1(t) == t + x'

which is what I did on several occasions.

But as to it being a new kind of operator, I think that might depend on interpretation. It could be interpreted to be no more than a syntactic form to delimit the scope of the priming operator. The motivation is that the use of the priming operator can be surprising and puzzling, and CAPTURE could possibly make the intent of the spec clearer by "taming the prime".

Also, I still don't understand the semantics of CAPTURE. Your writeFor example, suppose x is a vatiable s.t. s[[x]] = 1 and t[[x]] = 2, then

e == x |- s[[e]] = 1, <<s, t>>[[e']] = 2, s[[CAPTURE e]] = 1,<<s, t>>[[(CAPTURE e)']] = 1, s[[CAPTURE e']] = 2

The last equality, s[[CAPTURE e']] = 2, makes no sense. How can the

value of a formula that doesn't mention t depend on the value of x in

state t? Is it because "t" is the next letter in the alphabet after "s",

so t[[CAPTURE e']] will equal the value of x in whatever state I decide

to name "u"?

Right. So it may be better to limit CAPTURE e for expressions e of level at most 1. I wasn't sure whether it was useful at all to have CAPTURE work on level-2 expressions, but I thought I could give it meaningful semantics. But it doesn't make sense.

Ron

**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: Tagged formulas***From:*Leslie Lamport

- Prev by Date:
**Re: Tagged formulas** - Next by Date:
**Re: Tagged formulas** - Previous by thread:
**Re: Tagged formulas** - Next by thread:
**Exploring TLC checkpoint states** - Index(es):