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.
Ron