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

Re: [tlaplus] Re: SANY debugging mode

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.


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.