SANY debugging mode

[Andrew Helwer]

SANY has the -d flag which sends you into a sort of REPL where you can explore the spec's parse tree. In Specifying Systems it says of this option "The documentation that comes with the analyzer explains how to do this" - where is this documentation?

Thanks,

Andrew

[Andrew Helwer]

I haven't found such docs yet but for anyone else who finds this - the relevant source code is here: https://github.com/tlaplus/tlaplus/blob/6932e19083fc6df42473464857fc1280cb5aaecc/tlatools/org.lamport.tlatools/src/tla2sany/explorer/Explorer.java#L389

It looks like you have the following commands:

• cst which prints out the concrete syntax tree, with node names mostly corresponding to the JavaCC grammar
• mt which prints out the table of loaded modules and the definitions they contain
• mt* not sure what this prints out; all possible definitions available in the module? STRING, TRUE, FALSE, etc.
• dot don't know what this does, doesn't seem to print anything when used

Which is all fine, I was mostly looking for the cst functionality anyway!

Andrew

[Markus Kuppe]

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.

[Leslie Lamport]

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.