format-check — checks whether an ATerm conforms to a given regular tree grammar (RTG)


format-check [--rtg file] [--rtg-nf file] [-s s |--start s] [--xhtml] [--vis] [--fast] [--check] [-i file | --input file] [-o file | --output file] [-b] [-S | --silent] [--verbose level] [-k level | --keep level] [-h | -? | --help] [--about] [--version]


format-check checks the input ATerm against a regular tree grammar (RTG), to see if this term is part of the language defined in the RTG. If this is not the case, then the ATerm contains format errors, analogous to syntax errors in normal source code. format-check can operate in three modes: plain, visualize and XHTML.

The plain mode is used by default. In this mode, format errors are reported and no result is written the the output (stdout or file). Hence, if format-check is included in a pipeline, then the following tool will probably fail. If the input term is correct, then it is written to the output.

The visualize mode is enabled with the --vis option. In visualize mode, format errors are reported and in a pretty-printed ATerm will be written to the output. All innermost parts of the ATerm that cause format errors are printed in red, if your terminal supports control characters for colors. If you want to inspect the ATerm with a pager, like more or less, then you should use the -r flag.

The XHTML mode is enabled with the --xhtml option. In XHTML mode, format errors are reported and a report in XHTML will be written to the output. The result should be inspected in a web browser (not IE6). As with the visualize mode, this report shows the parts of the ATerm that are not formatted correctly. By moving your mouse over the nodes of ATerm, you can see the non-terminals that have be inferred by format-check.

format-check reports all innermost format errors. That is, only the deepest format errors are reported. A format error is reported by showing the ATerm that is not in the correct format, and the inferred types of the children of the ATerm. In XHTML and visualize mode a format error of term in a list is presented by a red comma and term. This means that a type has been inferred for the term itself, but that it is not expected at this point in the list. If only the term is red, then no type could be inferred for the term itself.

In all modes format-check succeeds (exit code 0) if the ATerm contains no format errors. If the term does contain format errors, then format-check fails (exit code 1).


Grammar Options

--rtg file

Use the regular tree grammar defined in file.

--rtg-nf file

Use the normalized, regular tree grammar defined in file.

-s s, --start s

Use s as the start symbol, i.e. root of the ATerm. By default, the start non-terminals defined for in the regular tree grammar are used.

Reporting Options


Output report as an XHTML document. See above for a detailed description.


Output report as a coloured, pretty-printed ATerm. See above for a detailed description.


Run as fast as possible. Might reduce quality of error messages.

Other Options


Check tool dependencies.

Common Input/Output Options

-i file

The input term given by the file name file.

In the absence of the -i option, input will be read from stdin.

-o file

The output will be written to the file given by the file name file.

In the absence of the -o option, output will be written to stdout.


The output will be written in the binary (BAF) ATerm format.

ATerms in the BAF format require a lot less space than ones in the TAF format, but the Java ATerm library does not currently support baf ATerms. ATerms in the baf format is the preferred format of exchange between Stratego tools.

Common Debugging Options


See --version.

-h, -?, --help

Display usage information.

--keep int

Keep intermediate results produced by the internal stages in the pretty-printing process. This is only useful for debugging. A high value of int indicates increased eagerness for keeping intermediate results.

Default setting is 0, indicating that no intermediates will be kept.

-S, --silent

Silent execution. Same as --verbose 0.

--verbose int

Set verbosity level to numerical value int. The higher the number, the more information about pp-aterm's inner workings are printed.

Alternatively, int can be set to either of the following verbosity levels, given in increasing order of verbosity: emergency, alert, critical, error, warning, notice, info, debug, vomit.


Displays the tool name and version.


To check the ATerm tree.trm against the regular tree grammar in tree-grammar.rtg, issue:

$ format-check --rtg tree-grammar.rtg -i tree.trm -o tree.checked.trm

If the term in tree.trm is syntactially valid, i.e. it conforms to the regular tree grammar, it will be copied to tree.checked.trm. If not, format-check wille exit with an error code and tree.checked.trm will not be written to.

Reporting Bugs

Please report bugs to


Copyright (C) 2002-2005 Eelco Visser

This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.