Re: Tagged formulas

[Leslie Lamport <tlapl...@xxxxxxxxx>]

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.

Also, I still don't understand the semantics of CAPTURE.  Your write

    For 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"?

Leslie