Hi Andrew,
I don’t know an elegant _expression_ of machine closure in TLA+, below is a clumsy way to express the closure of a given formula F.
For notational simplicity, let’s assume that F contains a single (free) state variable x. I’ll write F(x) to make this explicit, and write F(y) for the formula F with y substituted for x. Let’s start by defining a couple of auxiliary formulas:
H(x,h) == h = << x >> /\ [][x’ # x /\ h’ = Append(h,x’)]_<<x,h>>
The variable h is a history variable that records the previous values of x. Note that both of the following are valid:
\AA x : \EE h : H(x,h)
F(x) <=> \EE h : F(x) /\ H(x,h)
Now we can define the machine closure of F(x) as the formula
CF(x) == \EE hx :
/\ H(x, hx) \* record the values of x as hx
/\ [](LET n == Len(hx) \* fix the current length of the history
IN \EE y, hy : \* find a new sequence y and history hy such that
/\ F(y) /\ H(y,hy) \* y satisfies F and agrees with x on all values up to step n
/\ [](\A i \in 1 .. Min(n, Len(hy)) : hy[i] = hx[i]))
Note that, like F(x), CF(x) again has precisely one free state variable x. Now, F is machine closed iff
\AA x, hx :
CF(x) /\ H(x,hx) =>
[](LET n == Len(hx)
IN \EE y, hy : F(y) /\ H(y,hy) /\ [](\A i \in 1 .. Min(n, Len(hy)) : hy[i] = hx[i]))
that is, any finite prefix of a behavior satisfying CF can be extended to some behavior satisfying F. Really, all these formulas do is mirror the semantic definitions of machine closure in TLA+, that’s why they are not really satisfactory.
Because no tool supports reasoning about \EE and \AA, I don’t see how to mechanically check machine closure of a formula.
What do you think?
Stephan
