TLA+ code to TeX code
- Put your
tla
code in between\begin{tla}
and\end{tla}
in file liketla2tex-example-tla.tex
.- Ignore the code in between
\begin{\tlatex}
and\end{\tlatex}
now.
- Ignore the code in between
- Run
java -cp tla2tools.jar tla2tex.TeX tlatex-example-tla.tex
- This will automatically generate that code in between
\begin{\tlatex}
and\end{\tlatex}
. - Important Note:
You'd better run
java -cp
under the directory oftlatex-example-tla.tex
. Otherwise, you may get arenaming
error and information indicating that some.new
file was generated in a different directory. -cp tla2tools.jar
: make sure thattla2tools.jar
is in your path; useyour-path-to-tla2tools.jar
when necessary.
- This will automatically generate that code in between
- Compile
tlatex-example-tla.tex
to produce the pdf version which can be inserted into your LaTeX document as usual.- Make sure that
tlatex.sty
is in your path.
- Make sure that
For detailed info, see tla2tex-readme.md.