About

A parser for the Temporal Logic of Actions (TLA+). The parser is based on the LR(1) algorithm with state merging, and has time complexity linear in the size of the input. The lexer and parser are generated using parstools.

The syntax tree is represented as named-tuples, using typing.NamedTuple. Each node has line and column information for its start and end.

To install:

pip install tla

To parse a string:

import tla

module_text = r'''
    ---- MODULE name ----
    operator == TRUE
    ====================
    '''

tree = tla.parse(module_text)
print(tree)
text = tla.pformat_ast(tree)
print(text)

More examples can be found in the directory examples/. To implement a new translator of TLA+, as example the module tla._pprint can be used, or the class tla._utils.Traversal.

Documentation

In the Markdown file doc.md.

Tests

Use pytest. Run with:

cd tests/
pytest -v --continue-on-collection-errors .

License

BSD-3, read LICENSE file.

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

tla-0.0.4.tar.gz (149.6 kB view details)

Uploaded Dec 24, 2025 Source

File details

Details for the file tla-0.0.4.tar.gz.

File metadata

Download URL: tla-0.0.4.tar.gz
Upload date: Dec 24, 2025
Size: 149.6 kB
Tags: Source
Uploaded using Trusted Publishing? No
Uploaded via: twine/6.2.0 CPython/3.14.2+

File hashes

Hashes for tla-0.0.4.tar.gz
Algorithm	Hash digest
SHA256	`2b5bcf29060558c9cc31df05b905bb29e061136f1b6e6334f9d9f920f3c67adc`
MD5	`c71a5120084ce9fdb60507c4a2afc606`
BLAKE2b-256	`b23363e9df85813569824ab65ae610032137485a630a8cfa996011909fae0632`