[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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.