| Hi Ron,
the soundness of adding auxiliary variables is ensured by the corresponding introduction rules. For example, a simple history variable may be added using a rule such as
Init /\ [][Next]_v => \EE h : Init /\ h = h0 /\ [][Next /\ h' = f(h,v) /\ v' # v]_<<v,h>>
and the validity of this formula (for arbitrary h0 and f) is proved once and for all.
Now, when you use a refinement mapping to prove that the spec on the right-hand side refines some high-level specification, you may conclude that so does the spec on the left-hand side, by transitivity of implication.
In other words, the soundness of auxiliary variables is not checked by TLC but ensured by following syntactic patterns when introducing these variables. There should be a chapter about this in a future version of the Hyperbook.
Best, Stephan
Hi. This question is similar to one that has been asked before (but perhaps with a different focus): As far as I understand, every TLA+ spec-mapping (INSTANCE/WITH) that is "simple", i.e. does not require auxiliary variables, is indeed a refinement mapping. But once auxiliary variables are needed, things are not so clear. Abadi and Lamport proved that if specification B implements A, then, provided B satisfies some reasonable conditions, there is a refinement mapping from any B behavior to an A behavior, that possibly requires auxiliary history and/or prophecy variables. What isn't clear to me is the opposite direction: given a mapping from B to A that has auxiliary variables, how do we ensure that it is a valid refinement mapping, namely that every added variable indeed satisfies the requirements of a history/prophecy variable?
I am working on a reduction in the same vein as the ones discussed in this paper (by Cohen and Lamport), and while I believe I can get a "working" mapping with auxiliary variables, I get the sense that checking that the auxiliary variables are valid histories/prophecies is no easier than checking my original hypothesis (that B implements A). Short of model checking for hidden variables, is there a way TLC can assist in ensuring the validity of a refinement mapping?
Ron
--
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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|