[tlaplus] Making PlusCal a first-class language for TLC

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

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.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7f29c57f-e6c4-49ae-bec2-0fb2e53202c4%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.