How does TLC decide the location to report for an action?

[tal...@xxxxxxxxx]

If I define some actions like this:

------------------------------- MODULE Test -------------------------------

EXTENDS Integers

VARIABLES a, b

X == a' = a + 1
Y == a' = a - 1

ComponentA ==
  \/ X
  \/ Y

ComponentB == ...

Next ==
  \/ (ComponentA /\ UNCHANGED b)
  \/ ComponentB

Spec ==
  /\ a = 0
  /\ b = 0
  /\ [][Next]_<<a, b>> 

=============================================================================

Then if TLC finds a problem, it displays the list of actions not as X and Y but instead as e.g. <Next line 18, ...> (the ComponentA /\ UNCHANGED b line).

Is there some way I can convince it to show the more precise locations (X or Y)?

In this example, I could write "UNCHANGED b" in every action of ComponentA, but if I'm reusing components then this isn't possible.

I tried adding a "VARIABLE otherVars" to my ComponentA module and using INSTANCE, e.g.

----------- MODULE ComponentA ---------------

VARIABLE a, otherVars

X == a' = a + 1 /\ UNCHANGED otherVars
Y == a' = a - 1 /\ UNCHANGED otherVars

Next ==
  \/ X
  \/ Y
  
=============================================

VARIABLES a, b

A == INSTANCE ComponentA WITH otherVars <- << b >>

Next ==
  \/ A!Next
  \/ ComponentB

But then it just reports the actions as "A!Next".