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

Re: [tlaplus] Re: SANY debugging mode

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

  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:

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