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