TLATeX--A Typesetter for TLA+ Specifications
Mountain View, California
Last modified 13 January 2003
TLATeX is a Java program that uses the LaTeX document production
system to typeset TLA+ specifications.
TLA+ is a specification language based on TLA, the Temporal Logic of
TLA web page
for general information about TLA.
A description of TLATeX can be found in the
book Specifying Systems.
A shorter introduction can be found
Send your comments, questions, suggestions, complaints, or
Downloading, Installing, and Running TLATeX
The current version of TLATeX is
Version 0.95 of 11 November 2001
See the main TLA+ tools page for
instructions on how to download, install, and run TLATeX.
TLATeX calls the LaTeX program to do the actual typesetting.
So, you need to have LaTeX installed in order to run TLATeX.
Moreover, if you want TLATeX to produce shaded comments (and you
probably do), you may also need a program to convert LaTeX's
dvi output to Postscript or pdf.
MikTex, a free version of LaTeX for Windows, can be obtained
The MikTex distribution includes: LaTeX, the Yap
viewer for dvi files, the dvips program for converting dvi
files to Postscript files, and the dvipdfm program for
converting dvi files to pdf files.
LaTeX is also available for all Unix platforms. One possible source