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.