[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:
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.