Re: [tlaplus] Re: SANY debugging mode

[Leslie Lamport <tlaplus.ll@xxxxxxxxx>]

Here is some documentation for the SANY stand-alone parser:

The switches for the sany parser are:

  -s : parsing only, no semantic analysis

  -l : omit level checking

  -d : debugging mode, see below

  -stat : does not seem to do anything

Debugging mode provides a command line with the following 

commands, where N is a number

  mt [N] : prints module table, which seems to be a context/symbol table,

           giving the list of defined/declared symbols, their name,

           and their UID.  If N is given, it prints to depth N.

           Default is N = 2   

          

  mt* [N] : Like mt, except it also prints the Naturals module 

            if it's EXTENDed and it prints the module

            contexts.

  cst : Prints concrete syntax tree of everything.  It accepts

        a second argument but seems to ignore it

  s token : Seems to print concrete syntax tree for object

            corresponding to token.  Note: if token is omitted,

            it seems to take the token to be the 2nd token in

            the last command with two tokens.

  N1 [N2] : prints the node with uid = N1 to depth N2.  Default

            seems to be N2 = 4.

  qu : quit

  

Note: If either the -l or -s switches are used, or if an error occurs,

then level checking is not done.  This implies that any command that

tries to print level information will throw an exception.

To find a module's Theorem, Assumption, UseOrHide, and Instance nodes,

print the module node, whose node uid is obtained with the mt command.

The uids of OpDef nodes are also obtained from the mt command.

On Thursday, April 29, 2021 at 1:01:55 PM UTC-7 Markus Alexander Kuppe wrote:

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/7a41e884-89a9-4b50-82d2-23159870d2bfn%40googlegroups.com.