====== Latex Command Line Options ======

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

  * [[https://lamport.azurewebsites.net/tla/tla.html|Main TLA+ Site]] (as of September 2019, version 1.60)
    * At the above site, TLA+ ToolBox/IDE (version 1.6) can be downloaded [[https://lamport.azurewebsites.net/tla/tla.html|here]]. 
    * The JAR file is obtainable [[https://tla.msr-inria.inria.fr/tlatoolbox/dist/|here]]. This is referenced from [[https://lamport.azurewebsites.net/tla/standalone-tools.html?back-link=tools.html#tlatex?unhideBut@EQhide-tlatex@AMPunhideDiv@EQtlatex|Standalone Tools Overview]].
    * [[https://lamport.azurewebsites.net/tla/current-tools.pdf| Documentation for command line tools]]

I have done the following

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

===== Convert a TLA file to TeX file =====

<code>
tla2tex model.tla 
</code>

This will produce ''tla.tex''. 

===== Convert snippets of ASCII/TLA in a TeX file to mathematical mode =====

<code>
tlaintex model.tex 
</code>

where

<code latex>
% 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}
</code>

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''.

==== Style file ====

The style file ''tlatex.sty'' is available [[:latex:sty|here]].

==== More Documentation ====
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.

Read [[https://lamport.azurewebsites.net/tla/texinfo.txt|here]] for more.