Tagged formulas

[Ron Pressler]

Hi.

I seem to recall reading that in TLA+ a tagged formula means the formula with all variables tagged. TLC does not seem to be of the same opinion; as a result I sometimes find myself writing the same formula twice -- for the tagged and untagged variables. Did I misunderstand or is this a TLA+ feature unsupported by TLC?

Ron

[Leslie Lamport]

I presume that by "tagged" you mean primed.  Yes, e' means e with all variables in it primed.  Please tell us exactly what TLC is not interpreting as you expect it to.

Leslie

[Ron Pressler]

Yes, of course; I meant primed.

After some experimentation, I now  understand my problem better. Suppose I have these declarations:

    VARIABLES x, y

    Foo(a) == a \cup y

If I then use the primed formula Foo(x)', it will prime both x and y, but in my situation only y' is already determined in the evaluation, so TLC will emit the usual error in such cases, "The identifier x is either undefined or not an operator".

Trying to get around this seems to be of no use:

    LET t == x IN Foo(t)'

yields the same result. Other transformations don't change the situation:

    LET t == x[5].a \cap {2, 3} IN Foo(t)'

Is there a way to capture a value from a variable and pass it into a formula in such a way that priming it will not try to lazily obtain the value from the variable (or, simply put, "forget" the value's dependence on the variable)? While I see the merits of such evaluation, it can also be quite confusing (as in my case), because the value passed to the function is a result of several non-trivial transformations, that it's easy to miss the value's dependence on a variable. 

Ron

[Ron Pressler]

Reading chapter 17 of Specifying Systems, I now better understand TLA+'s evaluation strategy, so I guess my question becomes, is there a way to force the evaluation of an expression before the beta-reduction so that it is no longer subject to priming, as the prime operator (when applied to an expression) seems to be sensitive to a specific evaluation strategy?

Ron

[Leslie Lamport]

A TLA+ specification is a mathematical formula.  "Evaluation' is not a
meaningful concept in mathematics.  TLC is a program, one of its tasks
being to compute the set of possible next states of an action for a
given state.  Since this involves trying to solve an unsolvable
problem, TLC uses certain heuristics.  For example, it will do this
for the action formula (x' = 1) /\ (y' = x') but not for the
equivalent action formula (y' = x') /\ (x' = 1).

TLC's heuristics are insensitive to the use of definitions.  In your
example, it handles Foo(x)' exactly the way it handles (x \cup y)',
which is exactly the way it handles (x' \cup y').

In almost all cases that arise in practice, it is easy to rewrite a
sensible action formula in a form that TLC can handle--for example by
rewriting (y' = x') /\ (x' = 1) as (x' = 1) /\ (y' = x').  Thus, if
you can't find such a rewriting, the odds are that your formula is not
sensible because it doesn't mean what you think it should.  It may
therefore be instructive if you would post an action formula (that is
as simple as possible) that you would like TLC to evaluate but that
it doesn't.

Leslie

[Ron Pressler]

On Thursday, January 7, 2016 at 8:28:17 PM UTC+2, Leslie Lamport wrote:

A TLA+ specification is a mathematical formula.  "Evaluation' is not a
meaningful concept in mathematics. 

Naturally, but once you introduce the concept of expression levels and the way the prime operator interacts differently with expressions of different levels, you can get something that feels like evaluation. Basically I'm looking for a "lowering" operator where:

    Lower(x) == the level-0 expression (constant value) which is equal to x in this state

In almost all cases that arise in practice, it is easy to rewrite a
sensible action formula in a form that TLC can handle

 Not entirely related, but a case where I generally find this a bit burdensome is when functions are concerned. TLC's requirement that x' be determined in a single expression means that I can't write:

    \A t \in DOMAIN x : x'[t] = e \* e is some expression

This is not a problem when only one variable is involved, as you can do:

   x' = [t \in DOMAIN x |-> e]

but it is a hindrance to compositionality when, say, two function variables x and y (say, with the same domain) are involved. I'd like to have a simple formula:

    Foo(a, b) == a' = e1 /\ b' = e2

and then use it as

    \A t \in DOMAIN x (* = DOMAIN y *) : Foo(x[t], y[t])

As it stands, I either need to make a specialized Foo for this case, or have it return a tuple which I then destructure. 

In any case, this is a separate issue from the one I am currently discussing, where:

    VARIABLES x, y

    Foo(a) == a + y

and then I'd want

    Foo(Lower(x[5].f)) = Foo(c) \* If c is a constant and x[5].f = c in this state

Without Lower, I'm forced to define:

    Foo(a) == a + y

    Foo1(a) == a + y'

Now, this isn't too onerous by any means, but I was wondering if there was a way to lower expression levels. I guess there isn't...

Ron

[Ron Pressler]

Scratch that. I've realized that my lowering operator doesn't really make sense. What I wanted was no more than a fine-tuned way to control the application of the prime operator, and I guess that would just be over-complicating things. 

Ron

[Leslie Lamport]

   Basically I'm looking for a "lowering" operator where:
  
   Lower(x) == the level-0 expression (constant value) which
               is equal to x in this state

I can't think of any way to define such an operator, but it may help
to observe that if Foo is defined by

   Foo(a, b) == a' = e1 /\ b' = e2

Then  \E t : (t=x) /\ Foo(t,y)'  is equivalent to Foo(x, y').

   TLC's requirement that x' be determined in a single expression means
   that I can't write:

  
       \A t \in DOMAIN x : x'[t] = e \* e is some expression

  
   This is not a problem when only one variable is involved, as you can
   do:

  
      x' = [t \in DOMAIN x |-> e]

This is exactly the kind of situation that I was talking about.  Those
two formulas are not equivalent.  The second determines the value of
x'.  The first tells you very little about the value of x'.  All it tells
you are the values of x'[t] for t \in DOMAIN x.  It tells you nothing
about the domain of x'.  It doesn't even tell you if x' is a function.
Hence, it's not a sensible formula--at least, not by itself.  The following
formula is equivalent to the second one:

   /\ x' = [t \in DOMAIN x |-> x'[t]]
   /\ \A t \in DOMAIN x : x'[t] = e

but it's hardly simper than the second one.

So, as I wrote before, when TLC doesn't allow you to write something
you think it should, then it's often the case that what you wrote
isn't what you meant to write.  You should learn to read what a
formula says rather than what you want it to say.  This requires that
you stop thinking of TLA+ formula as a program and start thinking of
it as a mathematical assertion.  Occasionally, this is difficult.  For
example, if you write

   f[n \in Nat] == IF n = 0 THEN x ELSE f[n-1]'

it's not easy to realize that if x is a variable, then f[2] is not
equal to the illegal expression (x')'.

Leslie

[Ron Pressler]

On Thursday, January 7, 2016 at 10:08:16 PM UTC+2, Leslie Lamport wrote:

 it may help

to observe that if Foo is defined by

   Foo(a, b) == a' = e1 /\ b' = e2

Then  \E t : (t=x) /\ Foo(t,y)'  is equivalent to Foo(x, y').

Oh, I see. It only helps with boolean expressions, though.

 

Those

two formulas are not equivalent.  The second determines the value of
x'.  The first tells you very little about the value of x'.  All it tells
you are the values of x'[t] for t \in DOMAIN x.  It tells you nothing
about the domain of x'.  It doesn't even tell you if x' is a function.
Hence, it's not a sensible formula--at least, not by itself.  The following
formula is equivalent to the second one:

   /\ x' = [t \in DOMAIN x |-> x'[t]]
   /\ \A t \in DOMAIN x : x'[t] = e

but it's hardly simper than the second one.

Hmmm, right. Although you could define the first conjunct as a formula

    F(x) == [t \in DOMAIN x |-> x'[t]]

and then my example could be written as:

 

    F(x) /\ F(y) /\ \A t \in DOMAIN x : Foo(x[t], y[t])

which may be simpler than any of the alternatives (but won't work in TLC), especially if you collect all of these into a single formula, 

     Types == F(x) /\ F(y) /\ ....

and conjunct it at a top level with the next-state formula.

So, as I wrote before, when TLC doesn't allow you to write something
you think it should, then it's often the case that what you wrote
isn't what you meant to write.  You should learn to read what a
formula says rather than what you want it to say.  This requires that
you stop thinking of TLA+ formula as a program and start thinking of
it as a mathematical assertion. 

Just when I think I totally get it I'm surprised again, but it all makes sense in the end (and to be fair, theses "problems" usually pop up only when I try to be clever...)

 

Occasionally, this is difficult.  For
example, if you write

   f[n \in Nat] == IF n = 0 THEN x ELSE f[n-1]'

it's not easy to realize that if x is a variable, then f[2] is not
equal to the illegal expression (x')'.

Because f would then be the fixpoint f[n] = x ??

Thanks!

Ron

[Ron Pressler]

BTW, your suggestion of `\E t : t = x` works quite well. At first I defined:

    Capture(var, Action(_)) == \E t \in S : t = var /\ Action(t) \* S is a constant set known to contain the variable var

and it does the capture/lowering I want.

Then I tried:

    Capture(var, Action(_)) == \E t \in {var} : t = var /\ Action(t)

and that works too! I guess that's because the quantification happens outside the priming, and so t is a fresh, bound symbol rather than an expression involving a variable.

Thanks again!

[Leslie Lamport]

I'm not sure what "works quite well".  To clarify things, if

   Action(t) == t = y

   Capture(var, Action(_)) == \E t \in {var} : t = var /\ Action(t)

Then

   Capture(x, Action)' = (\E t \in {x} : t = x /\ (t=y))'
                       = (\E t \in {x'} : t' = x' /\ (t'=y'))
                       = (\E t \in {x'} : t = x' /\ (t=y'))

The last equality holds because t' = t, since \E t introduces t as a constant.

Leslie

[Ron Pressler]

I don't use Capture(x, Action)', but rather Action(t) is my subaction, _within which_ I can now use the parameter t in any formula -- primed or not -- and know that it's a constant that is equal to the current value of x. 

So, if

    VARIABLE x, y

    Foo(a) == a + y

I can do:

    Next == Capture(x, LAMBDA t:

        /\ ... Foo(t) ....  \* = x + y

        /\ ...

        /\ ... Foo(t)' ....) \* = x + y'

So Capture is a capturing/lowering LET (with the caveat that it can only be used in binary valued formulas), which is exactly what I wanted.

Ron

[Ron Pressler]

So, the Capture operator works well, except that it introduces a very significant performance hit when model-checking, so I can’t use it…

I’d like to pursue this point just a bit further, and explain the motivation. One of my specs is for a reliable multicast protocol (similar to Skeen’s algorithm) in a virtual synchrony environment. My variables include communication queues, the set of live machines, the state of the replicated state machine `st[m]` (where m is the machine), and each machine’s view, `view[m]` which is the set of machines m believes to be alive.

I have the concept of a node, which is an abstract machine, which at any point in time is mapped to a single physical machine. Also, I have an operator, let’s call it Address(m, n), which given a machine and a node, is equal to the address (i.e. physical machine) that machine m believes to be that of node n according to view[m]. I could explicitly pass view[m] to Address, but that would make things less convenient.

Now, a step may install a new view, view’, in machine m, in which case the protocol dictates that some messages be re-sent. Therefore, I tried to use Address(m, n)', so that the newly installed view be used. That didn’t work because it turns out that the node n in this case is computed from one of the state’s (`st`) fields, and st' has not yet been computed (as TLC requires). 

I can’t set st' yet because of the problem I mentioned in an earlier email in this conversation, which is that in order to make things composable, the operator handling the change of view works on one message at a time (it is possible that multiple messages are being multicast concurrently), and so my `HandleNewView` operator returns a tuple containing the new value of st for that particular machine and that particular messages, as well as a sequence of messages to be sent (all because I can’t set a variable’s next value one domain point at a time). 

So, perhaps there should be an operator, CAPTURE e, which would be a level-0 value equal to the value of expression e in the current state, so that I could write:

    Address(m, CAPTURE n)'

I thought that having such an operator wouldn’t make much sense because semantically it would be a constant, yet its value would change with the state; now I think it’s just a matter of interpretation. (CAPTURE e) can be interpreted as a syntactic construct that simply says "this subexpression is protected from priming".

Ron

[Leslie Lamport]

If you can precisely specify the meaning of Capture, we might consider it.  That is, for any expression e, define the meaning of Capture(e) in terms of the meaning of e.  The meaning of an action-level expression e is a mapping from pairs of states to values.  I have no idea how to do that. 

Leslie 

[Ron Pressler]

On Thursday, January 14, 2016 at 1:56:03 AM UTC+2, Leslie Lamport wrote:

If you can precisely specify the meaning of Capture, we might consider it.  That is, for any expression e, define the meaning of Capture(e) in terms of the meaning of e.  The meaning of an action-level expression e is a mapping from pairs of states to values.  I have no idea how to do that. 

I'll try:

Given expression e of level 0, 1, or 2, CAPTURE e is level-0 expression having the same value as e.

In other words, CAPTURE e is always equal to e, except that (CAPTURE e)' is also equal to e.

So (CAPTURE e)' is level correct and has level 2 iff e is level-correct and has level at most 2.

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

And

    e == x + x'   |-   <<s, t>>[[e]] = 3, e' is illegal, <<s, t>>[[CAPTURE e]] = 3 and <<s, t>>[[(CAPTURE e)']] = 3

If that somehow poses a problem, e could be limited to levels 0 and 1 only (undefined for 2 and up, so that CAPTURE e could be made level-incorrect if e has level 2 and up).

This operator adds symmetry: Currently, any level-0 expression e could be made level 1 with (e \cup es) where [](es = {}), but there's no way of turning a level-1 expression back to a level-0.

Ron

[Stephan Merz]

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

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Ron Pressler]

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. 

 

[Stephan Merz]

> 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

[Ron Pressler]

On Thursday, January 14, 2016 at 3:42:19 PM UTC+2, Stephan Merz wrote:

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

Hmm, so I may have misunderstood you after all. Trying:

    VARIABLE x

    Capture(e) == CHOOSE k \in {e} : k = e

    Next == /\ x' = x + 1 

                  /\ PrintT(x)                   \* => 1

                  /\ PrintT(x')                  \* => 2

                  /\ PrintT(Capture(x))    \* => 1

                  /\ PrintT(Capture(x)')   \* => 2

    Spec == (x = 1) /\ [][Next]_<<x>>

So Capture(x)' /= Capture(x), and this seems to be more than just level-checking.

If the difference is due to my writing `CHOOSE k \in {e} : k = e` instead of `CHOOSE k : k = e`, then the latter is currently unsupported by TLC anyway.

[Ron Pressler]

On Thursday, January 14, 2016 at 4:03:18 PM UTC+2, Ron Pressler wrote:

    VARIABLE x

    Capture(e) == CHOOSE k \in {e} : k = e

    Next == /\ x' = x + 1 

                  /\ PrintT(x)                   \* => 1

                  /\ PrintT(x')                  \* => 2

                  /\ PrintT(Capture(x))    \* => 1

                  /\ PrintT(Capture(x)')   \* => 2

    Spec == (x = 1) /\ [][Next]_<<x>>

So Capture(x)' /= Capture(x), and this seems to be more than just level-checking.

Just to clarify: My proposal for Capture would yield Capture(x)' = 1 instead of 2 (because Capture(x)' = Capture(x) = x = 1) , so changing the treatment of CHOOSE to display this behavior would change actual semantics. 

[Ron Pressler]

As (CHOOSE k : k = e)' = (CHOOSE k : k = e') and it must be this way (I don't see how CHOOSE could be any different), that's not what CAPTURE is supposed to do. I want (CAPTURE e)' = (CAPTURE e).

[Leslie Lamport]

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

[Leslie Lamport]

Hi Ron,

I should point out another problematic part of what you wrote--namely:

   <<s, t>>[[(CAPTURE e)']] = 1

The semantics of prime is that

   <<s, t>>[[exp']] = t[[exp]].

Therefore, your equality implies that t[[CAPTURE e]] = 1.  Why does
t[[x]] = 2 imply that t[[CAPTURE x]] = 1?

Leslie

[Ron Pressler]

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

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

[Ron Pressler]

I think that this, too, is a matter of interpretation. If you interpret CAPTURE to be a state-level (or even a transition-level, although I see that the latter doesn't make sense) expression, then this is indeed problematic. But if you see CAPTURE as a syntactic operation it makes sense. So I'd like to revise my specification a bit (although it doesn't change any semantics, I believe, only interpretation), and say that: (CAPTURE e)' is a syntax which is semantically equivalent to e. As such, even though the expression (CAPTURE e)' is primed, it is not a transition level expression at all. So  <<s, t>>[[(CAPTURE e)']] does not exist. It is s[[(CAPTURE e)']].

Perhaps it is best, then, to not describe CAPTURE as an operator at all, but as a part of the definition of the priming operator: 

    e' == e with all its variables primed, except those enclosed in a CAPTURE block.

Ron

[Stephan Merz]

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...@gmail.com> 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).
>>>
>

[Ron Pressler]

For completeness, here's my new spec:

    * The priming operator is defined thus: e' == e with all its variables primed, except those enclosed in a CAPTURE block.

    *  It is level-incorrect to write CAPTURE e, if e does not have level at most 1

    *  When appearing in an unprimed expression, CAPTURE e has the same meaning as e.

The spec does not define the syntactic scope (precedence) of CAPTURE, but that is orthogonal. Perhaps it would be better to use some symbol or a special bracketing to delimit the captured expression, rather than use the word CAPTURE, which seems like an operator.

[Ron Pressler]

BTW, the restriction of CAPTURE to level <= 1 expressions comes naturally from CAPTURE being defined in terms of prime and vice-versa: You can only capture expressions that you can prime (and vice-versa).