I read the paper in the first link, and I may read it again, but I have a few remarks:
1. Refinement mappings in TLA also allow arbitrary state functions.
2. There are very good reasons to want machine closure, and one of the things mentioned at the end of that paper as an advantage (that there is no necessity in a separate liveness property), is actually a serious disadvantage.
Let me give you an example, using what Lamport calls "raw" TLA, which is TLA which is not stuttering invariant:
Spec1 ≜ t = 1 ∧ x = 1 ∧ ◻(t' = t + 1 ∧ x' = x + 10)
Spec2 ≜ t = 1 ∧ x ∈ Nat ∧ ◻(t' = t + 1 ∧ x' = x + 10 ∧ t = 10 ⇒ x = 100)
The two specifications specify the same behavior. But, in this world, a safety property can imply a liveness property, e.g. x ∈ Nat ∧ ◻(x' = x + 10) ⇒ ◇(x ≥ 100)
Now, this is bad because the second specification is actually not implementable in a computer with complexity similar to that of the behavior as it relies on "angelic" nondeterminism. It is possible to use angelic nondeterminism in TLA (it's important for high-level specs) like so:
Spec3 ≜ t = 1 ∧ x ∈ Nat ∧ ◻[t' = t + 1 ∧ x' = x + 10 ∧ t = 10 ⇒ x = 100]_<t, x> ∧ ◇(t ≥ 10)
(the square brackets mean that either the action is true, or <t, x> are unchanged) But now, the liveness property is not implied by the safety property, and it requires an explicit statement in the formula. That last formula, Spec3, is not machine-closed, and this makes it easier to see that the algorithm implied is unrealizable as written.
> 1. Refinement mappings in TLA also allow arbitrary state functions.
Could you please point me to a reference for this. The completeness result from "The existence of refinement mapping" only includes projection. I know that TLA does allow existential quantification over internal variables (corresponds to hiding) and one can eliminate the quantifier by defining a function. But notice that is just the logical way of specifying "hiding" and is different from having arbitrary refinement mapping.
>2. There are very good reasons to want machine closure ...
Definitely. However, these are the concerns when we are specifying a system -- is the specification correctly models the system that I have in mind. While the comments in the paper -- no necessity to separately analyze liveness -- refers to the easy while proving that a concrete specification "implements" an abstract specification. And this is what your example specifications illustrates (thanks for specific examples, it helped me to understand the point you are making).
> I know that TLA does allow existential quantification over internal variables (corresponds to hiding) and one can eliminate the quantifier by defining a function.
That's what I meant. The functions do not necessarily apply to hidden variables only, but to any variable. E.g., in TLA+, if Spec1 has variable x and Spec2 has variables q and t, you could write:
Spec2 ⇒ INSTANCE Spec1 WITH x ← q + t
Which implements Spec to by mapping (q + t) to x.
> But notice that ... is different from having arbitrary refinement mapping.
Can you explain what you mean?
> However, these are the concerns when we are specifying a system -- is the specification correctly models the system that I have in mind.
Right, but you want an easy way to determine if a specification is machine-closed or not. TLA provides a sufficient syntactic condition. A specification is guaranteed to be machine closed if it can be written as
Init ∧ ◻[M]_vars ∧ Fairness
Where M is an action and `Fairness` is a conjunction of ⬦ clauses containing WF/SF (weak/strong fairness) conditions only. In fact, when testing safety properties alone (which is normally the case), a specification is usually just
Init ∧ ◻[M]_vars
Which TLA guarantees is machine-closed. Otherwise, a ◻ formula alone may not be machine-closed (and may imply a liveness property, like in my example above), and proving whether it is or it isn't may be non-trivial.
1. Refinement mappings in TLA also allow arbitrary state functions.
2. There are very good reasons to want machine closure, and one of the things mentioned at the end of that paper as an advantage (that there is no necessity in a separate liveness property), is actually a serious disadvantage.
Let me give you an example, using what Lamport calls "raw" TLA, which is TLA which is not stuttering invariant:
The two specifications specify the same behavior. But, in this world, a safety property can imply a liveness property, e.g. x ∈ Nat ∧ ◻(x' = x + 10) ⇒ ◇(x ≥ 100)Now, this is bad because the second specification is actually not implementable in a computer with complexity similar to that of the behavior as it relies on "angelic" nondeterminism. It is possible to use angelic nondeterminism in TLA (it's important for high-level specs) like so:
(the square brackets mean that either the action is true, or <t, x> are unchanged) But now, the liveness property is not implied by the safety property, and it requires an explicit statement in the formula. That last formula, Spec3, is not machine-closed, and this makes it easier to see that the algorithm implied is unrealizable as written.