In order to incorporate TLA+ in LaTex sources it is best to download the JAR file for Standalone Tools.

• Main TLA+ Site (as of September 2019, version 1.60)
  • At the above site, TLA+ ToolBox/IDE (version 1.6) can be downloaded here.
  • The JAR file is obtainable here. This is referenced from Standalone Tools Overview.
  • Documentation for command line tools

I have done the following

alias tla2tex="java -cp /usr/local/tla-tools/tla2tools.jar tla2tex.TLA" 
alias tlaintex="java -cp /usr/local/tla-tools/tla2tools.jar tla2tex.TeX"

tla2tex model.tla 

This will produce tla.tex.

tlaintex model.tex 

where

% model.tex
\documentclass[12pt]{article}
\usepackage{tlatex}
\usepackage{color}
\definecolor{boxshade}{gray}{.9}\setboolean{shading}{true}
 
\begin{document}
\begin{tla}
  Action == /\ x'   = x - y
            /\ yy'  = 123
            /\ zzz' = zzz
\end{tla}
\end{document}

The style file tlatex.sty must be available. The above produces a LaTeX file model.tex where the tla environment is set to mathematics. The original model.tex file is renamed model.old.

The style file tlatex.sty is available here.

If you are not using the JAR file, you will probably run TLATeX by typing

 java tla2tex.TeX [options] fileName

where [options] is an optional list of options, and fileName is the name of the input file. (If fileName does not contain an extension, then the input file is fileName.tex.) Running TLATeX with the -help option produces a list of all options. Running it with the -info option produces what you are now reading. (The fileName can be omitted when using the -help or -info option.)

The running time of tla2tex.TeX is roughly proportional to the number of separate `tla' environments. You can speed things up by not having tla2tex.TeX reprocess `tla' environments that haven't changed since the last time it was run. To do this, just change those `tla' environments to `notla' environments. Similarly, you can change `pcal' and `ppcal' to `nopcal' or `noppcal' environments.

The only other thing you probably need to know about using tla2tex.TeX is how to shade comments, which is explained in the next section.