[tlaplus] Re: SANY debugging mode

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

I haven't found such docs yet but for anyone else who finds this - the relevant source code is here: https://github.com/tlaplus/tlaplus/blob/6932e19083fc6df42473464857fc1280cb5aaecc/tlatools/org.lamport.tlatools/src/tla2sany/explorer/Explorer.java#L389

It looks like you have the following commands:

• cst which prints out the concrete syntax tree, with node names mostly corresponding to the JavaCC grammar
• mt which prints out the table of loaded modules and the definitions they contain
• mt* not sure what this prints out; all possible definitions available in the module? STRING, TRUE, FALSE, etc.
• dot don't know what this does, doesn't seem to print anything when used

Which is all fine, I was mostly looking for the cst functionality anyway!

Andrew

On Thursday, April 29, 2021 at 11:55:59 AM UTC-4 Andrew Helwer wrote:

SANY has the -d flag which sends you into a sort of REPL where you can explore the spec's parse tree. In Specifying Systems it says of this option "The documentation that comes with the analyzer explains how to do this" - where is this documentation?

Thanks,

Andrew

-- 
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/223451af-44c0-4170-8d13-d6cfc997b085n%40googlegroups.com.