Re:Computation and State Machines (2008) [pdf]
by pron on Friday January 06, 2017 @10:15AM
(#13336859)
> 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.
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:
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
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 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.