texinfo.txt

              tla2tex.TeX Version 1.0 of 18 August 2012

CONTENTS
--------
  INTRODUCTION
  COMMENT SHADING
  HOW tla2tex.TeX TYPESETS TLA+ FORMULAS
  HOW tla2tex.TeX TYPESETS COMMENTS
  OUTPUT FILES
  TROUBLESHOOTING


INTRODUCTION 
------------ 

tla2tex.TeX is a version of the TLATeX Java program for use in putting
TLA+ formulas into LaTeX documents.  It was written by Leslie Lamport,
based on ideas by Dmitri Samborski.

tla2tex.TeX takes as input a LaTeX source file.  It interprets any
`tla' environment to be TLA+ "code".  It modifies the LaTeX source
file by writing, after each `tla' environment, a `tlatex' environment
containing LaTeX commands for typesetting the contents of the `tla'
environment--first deleting any `tlatex' environment that follows the
`tla' environment.  (It renames the old version of the input file to
have the extension "old".)

tla2tex.TeX handles `pcal' and `ppcal' environments the same way as
it handles `tla' environments, except that it interprets the text
in a `pcal' environment to be PlusCal code written with the C syntax,
and text in a `ppcal' environment to be PlusCal code written with
the P syntax.  Except as noted, everything said below about
`tla' environments applies to `pcal' and `ppcal' environments.

The LaTeX source file must contain a

   \usepackage{tlatex}

command, and the tlatex.sty file must be placed in a directory in
which LaTeX looks for package files.

If you're writing a LaTeX document, you probably have already
installed TeX and LaTeX on your system.  Use the -latexCommand option
if you run LaTeX on your system by typing something other than
"latex".

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.

The only other thing you probably need to know about using tla2tex.TeX
is how to shade comments, which is explained in the next section.


COMMENT SHADING
---------------
To shade comments, add the following commands to the preamble
of the LaTeX source file (that is, before the \begin{document}
command):

   \usepackage{color}
   \definecolor{boxshade}{gray}{<shade-value>}
   \setboolean{shading}{true}

where <shade-value> is a number between 0 and 1, smaller numbers producing
darker shading.  The value .85 seems to work pretty well.


HOW tla2tex.TeX TYPESETS A tla ENVIRONMENT
-----------------------------------------
The `tlatex' environment produced by tla2tex.TeX from a `tla'
environment should do what would want it to.  It preserves most of the
meaningful alignments in the TLA+ "code".  For example, it will
typeset
\begin{tla}
  Action == /\ x'   = x - y
            /\ yy'  = 123
            /\ zzz' = zzz
\end{tla}
so that the "/\" and "=" symbols are aligned.  Extra spaces in the
input will be reflected in the output.  However, TLATeX treats 0 and 1
space between symbols the same, so "x+y" and "x + y" produce the same
output, but "x  +  y" produces extra space around the "+".

In `pcal' and `ppcal' environments, tla2tex.TeX tries to align the
PlusCal code as well as the TLA+ expressions that appear in the code.

The `tla' environment can appear anywhere in the LaTeX file at which a
complete paragraph could appear.  The \begin{tla} and \end{tla}
commands must each appear on a line by itself.

tla2tex.TeX does not check that the TLA+ "code" is syntactically
correct TLA+.  However, it will report an error if it encounters an
illegal lexeme, such as ";".  (Of course, ";" is illegal only in a
`tla' environment, not in a `pcal' or `ppcal' environment.)

HOW tla2tex.TeX TYPESETS pcal and ppcal ENVIRONMENTS
----------------------------------------------------
The `pcal' and `ppcal' environments are similar to the `tla' environment
except that tla2tex.TeX treats the text of a `pcal' environment as all or
part of a PlusCal algorithm written with the C-syntax.  The `ppcal'
environment is similar, except for an algorithm written with PlusCal's
P-syntax.

HOW tla2tex.TeX TYPESETS COMMENTS
--------------------------------
tla2tex.TeX distinguishes between one-line and multi-line comments.  A
one-line comment is any comment that is not a multi-line comment.
Multi-line comments can be typed in any of the following three ways:

  (*************************)
  (* This is the text of a *)
  (* multi-line comment.   *)
  (*************************)

  \********************
  \* This is the text 
  \* of the comment.  
  \********************

  (* This is the text
     of the comment.   *)

In the first two ways, the "(*" or "\*" characters on the left must
all be aligned, and the last line of "*" characters is optional.  In
the first way, nothing may appear to the right of the
comment--otherwise, the input is considered to be a sequence of
separate one-line comments.  

tla2tex.TeX typesets a single-line comment in LR-mode, just as if it
were the argument of an \hbox command.  It typesets a multi-line
comment in paragraph mode, as if it were inside a `minipage'
environment.  Any special formatting of a comment that you want must
be produced by LaTeX commands within the coment.  For example, instead
of typing

  \* foo > bar+2 need not always hold.

you would probably type

  \* $foo > bar+2$ need \emph{not} always hold.

Note: the tlatex package changes the way LaTeX formats text in math
mode so that multi-letter identifiers look better.  FOr example,
$different$ comes out looking like \emph{different}.  If you're
writing a document that contains TLA+ formulas, this is probably what
you want.  But it means that some more traditional math formulas may
not come out looking as good as usual.


OUTPUT FILES
------------
tla2tex.TeX writes several files.  The names of these are normally
determined from the name of the input file.  However, options allow
you to specify the name of each of these files.  In the following
description, the root of a file name is the name with any extension or
path specifier removed; for example, the root of c:\frob\bar.tla is
bar.  All file names are interpreted relative to the directory in
which tla2tex.TeX is run.

-out fileName
   If f is the root of fileName, then f.tex is the name of the 
   ouput produced by tla2tex.TeX.

-alignOut fileName
   This specifies the root name of the LaTeX alignment file written by
   TLATeX, which is described in the section below on Trouble-Shooting.
   If f is the root of fileName, then the alignment file is named
   f.tex, and running LaTeX on it produces the files f.dvi, f.log, and
   f.aux.  Only the f.log file is of interest.  The default value of
   -alignOut is the "tlatex". 


TROUBLE-SHOOTING
----------------
The error messages should be self-explanatory.  tla2tex.TeX reads the
log file produced by LaTeX the last time it processed the input file.
It uses this information to determine the value of LaTeX's \linewidth
parameter for each of the `tla' environments.  (That value depends on
the context in which the `tla' environment occurs.)  It issues a
warning if the number of `tla' environments in the file has changed
since LaTeX was run on the file, so the \linewidth information is not
current.  The output produced by tla2tex.TeX usually doesn't depend on
the \linewidth values, so the results will be fine even if the wrong
values were used.  To be safe, you should run LaTeX on the input
file before running tla2tex.TeX.