This is a formatter for the TLA+ language.
It uses tlaplus tools' SANY library to parse your specification, and it applies some (at the moment) predefined format to it.
This is still ALPHA software, not everything is handled at the moment, so it might break your specs.
- A formatter for the tla+ language.
- It should be configurable but also provide sane defaults.
- It should never add useless chars (no extra spaces or extra newlines)
- It should never break any specs. No user configuration should ever lead to broken specs.
- The output should be stable. Applying the formatter to the output of a previous formatter run should not change it.
- It should be fast.
If you have specific requests for configuration options you would like to have, please consider opening an issue.
Currently the idea is to follow the same ideas behind rustfmt. A user level formatter config and a project level formatter config.
To see some examples of current reformatting, compare:
More examples are in the test/java/resources/{inputs|outputs} folders. These sources are taken from the TLA+ Examples repo.
If you want to try it out, go to the build page of the latest commit, and download the "Package.zip" file from the artifact section at the bottom of the page (Example).
You will need at least java 11 (same requirement as tlatools).
Unzip the file, and you can invoke the formatter like this:
java -jar tlaplus-formatter.jar <INFILE> [OUTFILE]
It will print your reformatted spec in output. If the optional "OUTFILE" parameter is specified, it will write the output to that file.
You can use the input file as output file as well. Run with -help parameter for the help text.
It's a work in progress, see PR-327 on vscode-tlaplus repo.
Because it uses SANY underneath (TLC's parser), your spec needs to first succeed SANY's parsing process, otherwise the formatter won't be able to reformat your file.
Some of the constants used in the code are coming from SANY's codebase, specifically from this file: src/tla2sany/st/SyntaxTreeConstants.java (check tlaplus repo).