Crate libtlafmt

A library crate for formatting TLA+ specs.

This crate is the formatter implementation for tlafmt.

Inner Workings

Formatting a TLA file occurs in three phases within this crate:

1. The input file is parsed into an abstract syntax tree.
2. The AST is then lowered into a formatter-specific representation.
3. The format representation is rendered into output text.

Step (1) is performed when calling ParsedFile::new() to initialise a new instance, and steps (2) and (3) are performed when ParsedFile::format() is called, writing the output to a provided std::io::Write sink.

Testing

Run the tests with:

% cargo test --workspace

Some tests make use of cargo-insta.

In addition to unit tests, a corpus of example TLA specs¹ are formatted and a snapshot of their output generated² after each test run. These snapshots have to be “accepted” using cargo-insta (if their change is desirable) to cause future tests runs to pass.

---

1. A majority sample of the official TLA examples repo - see libtlafmt/tests/corpus/ in the code repo. ↩

2. See libtlafmt/tests/snapshots/ in the code repo. ↩

Structs

ParsedFile

A parsed TLA file ready for formatting.

Enums

Error

Errors during AST parsing, lowering or rendering.