> 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.
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).