Action names from other modules don't get displayed in error trace

[Alexander-N]

When actions are instantiated from other modules for example

s1 == INSTANCE step1

Next == \E task \in Tasks:
  \/ Cancel(task)
  \/ s1!Acquire(task)
  \/ s1!Release(task)
  \/ s1!WakeUp(task)
  \/ s1!Finished

then their names don't seem to get displayed in the error trace. For example this spec with this TLC output produces the following:

[lemmy]

This is what works for the Toolbox trace explorer: https://github.com/tlaplus/tlaplus/blob/6bc82f7746ccdfbdf49cdef24448666d11e5e218/toolbox/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCState.java#L82-L121

[alygin]

@Alexander-N, I've fixed displaying of such error trace items, but TLC doesn't provide the exact action location, it points to the INSTANCE clause in the module being checked, so the link in the check result view also leads to that clause, not to the external module.

@lemmy, it looks like the Toolbox does the same. Is it possible to provide the real action location in such error trace items from TLC? I mean, this:

<s1!Acquire line 26, col 1 to line 38, col 29 of module step1>

instead of the current

<s1!Acquire line 19, col 1 to line 19, col 20 of module step2>

[lemmy]

@alygin Not impossible but nothing I can commit to in the foreseeable future. The way how TLC reads specs into (sub-)actions causes confusion in a couple of places (coverage, ...).

[alygin]

Published in v1.6.0-alpha.1