[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Fri, 12 Feb 2016 00:46:33 -0800 (PST)

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

**Follow-Ups**:**Re: [tlaplus] Correctness of refinement mapping***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] problem in verifying liveness properties** - Next by Date:
**Re: [tlaplus] Correctness of refinement mapping** - Previous by thread:
**Re: [tlaplus] Invariance under transition order** - Next by thread:
**Re: [tlaplus] Correctness of refinement mapping** - Index(es):