Hi Andrew,
Selecting a portion of the TLA+ translation and hitting F10 takes you
to the corresponding PlusCal source (if one exists). I believe that
double clicking on a link in an error message to a line of the TLA+
translation used to take you to the PlusCal source, but bit rot seems to
have destroyed that feature. But clicking and hitting F10 works fine.
Unfortunately, getting from the action line in an error trace to the
PlusCal source for the action isn't so nice because double-clicking on
the action line doesn't move focus to the module editor. That should
be easy enough to fix and I hope it will be done soon, so double-clicking
on the line and hitting F10 will work. For now, try hitting Control + F7
a few times to move the focus before hitting F10.
It would be possible to hide under the covers the TLA+ translation and
the mapping from error locations reported by TLC to locations in the
PlusCal code. And it might be doable in a few months if you were
willing to give up features like profiling. But I suspect that it
would make debugging PlusCal code harder. Rewriting TLC to work
directly on PlusCal would probably take a few person-years of effort;
I wouldn't want to hazard a guess on the number. In any case, I will
provide no encouragement to any such project because it would
eliminate one of the purposes of PlusCal: to serve as a gateway drug
to TLA+.
Leslie