the ExplorerVisitor received an extension to export the semantic graph into dot notation, which can be rendered with GraphViz:

java -cp tla2tools.jartla2sany.SANY -d ATLA+Spec.tla dot

It optionally includes line numbers if the system property

tla2sany.explorer.DotExplorerVisitor.includeLineNumbers=true

is set.