The Apalache Module

Similar to the TLC module, we provide a module called Apalache, which can be found in Apalache.tla. Many of the operators in that module are used internally by Apalache, when rewriting a TLA+ specification. It is useful to read the comments to the operators defined in Apalache.tla, as they will help you in understanding the detailed output produced by the tool.

See the detailed description of the Apalache operators.