| 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
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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion visit https://groups.google.com/d/msgid/tlaplus/8F641343-18AE-4DDE-8C45-0DA4182796E8%40gmail.com. |