About

A parser for the Temporal Logic of Actions (TLA+). The parser is based on combinators. The lexer is generated with ply using lex. Classes for a TLA+ abstract tree are included and used for representing the result of parsing.

To install:

pip install tla

To parse a string:

from tla import parser

module_text = r'''
---- MODULE Foo ----
foo == TRUE
====================
'''

tree = parser.parse(module_text)

To parse the string module_text from above and print a formatted version:

from tla import parser
from tla.to_str import Nodes

# The abstract syntax tree classes can be changed using
# the optional argument `nodes` of the function `parser.parse`.
tree = parser.parse(module_text, nodes=Nodes)
text = tree.to_str(width=80)
print(text)

More examples can be found in the directory examples/

To implement a new translator of TLA+ to an intended output format, either:

• use the visitor pattern with the module ast.visit, or
• subclass the class tla.ast.Nodes, and override AST node classes and their methods as needed. An example of this approach is the module tla.to_str, which can be copied as a starting point for implementing a translator.

This parser is a translation to Python from OCaml of the parser in tlapm, the TLA+ proof manager. The Python source code includes in comments the corresponding OCaml source code. Comments in each module mention the OCaml files on which that module is based.

This parser is slower than the OCaml implementation.

The module tla._combinators can be used to write other parsers.

Documentation

In the Markdown file doc.md

Tests

Require nose. Run with:

cd tests/
nosetests .

See also the file tests/README.md.

License

BSD-3, see LICENSE file.