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

Re: [tlaplus] Invariance under transition order

On Tuesday, February 2, 2016 at 11:53:29 AM UTC+2, Stephan Merz wrote:

Does this make sense?

Yes! Thank you!

Just earlier today I discovered two of Lamport's papers, The Existence of Refinement Mappings  and Reduction in TLA,  that provide the theoretical justification for this. In particular, they show how auxiliary history and prophecy variables can be used to check commutativity of transitions. The second paper in particular addresses the exact problem I'm facing.