Making PlusCal a first-class language for TLC

32 views
Skip to first unread message

Andrew Helwer

unread,
Jun 28, 2019, 5:02:07 PM6/28/19
to tlaplus
Has there been any discussion or planning around making PlusCal a first-class language for TLC, as in TLC is run on PlusCal directly without requiring translation & it provides error traces that map to PlusCal labels/variables? I'm currently writing a PlusCal spec with several procedures, each of which has some local variables. Following the execution trace would be so, so much nicer if I were redirected to the PlusCal label instead of the TLA+ definition; there is a lot of variable renaming going on that it's tricky to debug what's happening.

Leslie Lamport

unread,
Jun 29, 2019, 6:45:24 AM6/29/19
to tlaplus
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

Leslie Lamport

unread,
Jul 2, 2019, 3:49:44 AM7/2/19
to tlaplus
Mea culpa.  There is no missing feature for going from error messages
to the PlusCal source of the error.  There was just a hole in my
memory.  When clicking on something takes you to the source of an
error in the TLA+ translation, holding the control key down when you
click takes you to the PlusCal source--if such a source exists.  That
includes clicking on TLA+ parsing errors and double-clicking on the
action-location line in an error trace.

Leslie

Andrew Helwer

unread,
Jul 3, 2019, 1:41:44 PM7/3/19
to tlaplus
Thanks, Leslie!
Reply all
Reply to author
Forward
0 new messages