Hello,
I am trying to develop a refinement mapping between two specs H and L, where H is a high level description of a distributed system and L is a lower level one. My belief is that there exists a refinement mapping from L to H that works by re-ordering the events in the lower level spec in accordance with the partial ordering of events in the system. In L, a behavior represents a sequence of events that occur on different nodes of a distributed system. I want my refinement mapping to re-order the states/events of a behavior in a way that both satisfies the partial ordering and gives a valid refinement mapping from L to H.
For example, consider some transition from state A to state B in L such that there is no causal dependence between A and B i.e. the event that transitioned the system to A and the event that transitioned the system to B can be considered concurrent. If the A -> B transition cannot be made to correspond to any transition in H under a refinement map, but a transition B -> A can be, then it seems that a refinement mapping should be able to take advantage of this freedom to re-order events.
When thinking about how I would define this, such a mapping feels more natural to define over behaviors as opposed to states i.e. defining a function f that maps behaviors in L to behaviors in H where f may re-order states of L. This feels harder to do when only mapping from states in L to states in H. My understanding is that a refinement mapping is defined as function f : S_L -> S_H, where S_L is the set of states of spec L and S_H is the set of states in spec H, such that f maps initial states in L to those in H, and maps transitions in L to transitions in H. From [1] and [2], I understand that in some cases I may need to add auxiliary variables to permit a refinement mapping, but it’s not clear to me yet whether this is required for my scenario.
Does anyone have any suggestions on a good way to approach this? Or perhaps there is an alternate perspective on this problem that would simplify things. Conceptually, my goal feels reasonable, but I'm unsure how to actually define this in TLA+. I am also interested if this type of refinement mapping (i.e. re-ordering partially ordered events) has appeared elsewhere when defining refinement mappings between specifications of concurrent systems.
[1] https://www.microsoft.com/en-us/research/publication/the-existence-of-refinement-mappings/
[2] https://lamport.azurewebsites.net/tla/hiding-and-refinement.pdf