(for example, A is MinMax1 and B is MinMax2 in the paper "Auxiliary Variables in TLA+" by Leslie Lamport and Stephan Merz, 2017)
we add a refinement mapping like
M == INSTANCE B WITH vb <- va
to module A and check that
THEOREM Spec => M!Spec,
where vb is a variable of B, va is a variable of A,
Spec is the specification of A, and M!Spec refers to the specification of B.
Suppose that the refinement mapping is wrong.
This will raise an error like "Action property line xx of module B is violated" and produce an error trace.
However, the error trace only shows the variables of module A.
How to watch the variables (for example vb here) of the instantiated module B in the error trace?
It may help to "debug" the refinement mapping.
What is your experience in debugging a wrong refinement mapping
given that the error information "Action property line xx of module xx is violated" is hard to use.
Thanks.