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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Thu, 7 Jan 2016 13:09:12 -0800 (PST)*References*: <71319d03-6ab4-48a7-a6a2-53e7c9c48a51@googlegroups.com> <20d67976-47a3-440d-942e-51f3b035554e@googlegroups.com>

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 writef[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

**Follow-Ups**:**Re: Tagged formulas***From:*Ron Pressler

**References**:**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:
**Re: Tagged formulas** - Index(es):