TLATeX--A Typesetter for TLA+ Specifications

Leslie Lamport
Microsoft Research
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 Actions. See the 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 here . Send your comments, questions, suggestions, complaints, or congratulations to Leslie Lamport.

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.

Obtaining LaTeX

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 here. 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 is here.