Differences

This shows you the differences between two versions of the page.

--- tla:latex [2019/09/02 16:34]
jonathan
+++ tla:latex [2019/09/02 17:00] (current)
jonathan [More Documentation]
@@ Line 1: / Line 1: @@
 ====== Latex Command Line Options ======
-In order to incorporate TLA+ in LaTex sources it is best to download the JAR file.
+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 201)
+  * [[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]].
+    * 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.

Software Engineering Documentation

User Tools

Site Tools

Differences

Page Tools