Re: [tlaplus] Re: SANY debugging mode

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

On 29.04.21 12:26, Andrew Helwer wrote:
>   * dot don't know what this does, doesn't seem to print anything when used


Assuming a spec A.tla in $CWD,

      java -cp /path/to/tla2tools.jar tla2sany.SANY -d A.tla dot

creates a file A.dot that contains A's AST in GraphViz notation.

To include line numbers in A.dot, do:

      java 
-Dtla2sany.explorer.DotExplorerVisitor.includeLineNumbers=true -cp 
/path/to/tla2tools.jar tla2sany.SANY -d A.tla dot


xdot is a lightweight tool to render A.dot.

M.

--
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/58d18b92-832c-a5e8-a8fa-809e1186576c%40lemmster.de.