TLATeX Version 1.0 of 18 August 2012 CONTENTS -------- INTRODUCTION HOW TLATeX TYPESETS THE SPECIFICATION HOW TLATeX TYPESETS COMMENTS TROUBLESHOOTING USING LaTeX COMMANDS IN COMMENTS INTRODUCTION ------------ TLATeX is a Java program for typesetting TLA+ specifications with LaTeX. It was written by Leslie Lamport, based on ideas by Dmitri Samborski. TLATeX produces a LaTeX dvi file and an optional Postscript or pdf file, either of which can be displayed on the screen or printed. TLATeX requires that the LaTeX program be installed on your system. Producing Postscript or pdf output also requires a program to convert from dvi to Postscript or pdf. For information about obtaining LaTeX and a Postscript or pdf converter, see http://www.research.compaq.com/SRC/tla/tlatex/tlatex.html 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.TLA [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.tla.) The input file must contain a complete TLA+ module. 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 only other things you probably need to know about using TLATeX are (i) how to shade comments, which is explained in the next section, and (ii) that the -number option causes TLATeX to print line numbers in the left margin. TLATeX's output should be good enough for most users. Later sections describe how you can get TLATeX to do a better job, and will explain what happened in the unlikely case that it produces weird output. However, if you happen to use any of the two-character sequences `~ `^ `. in a comment, you'd better read the section on how TLATeX formats comments. COMMENT SHADING --------------- The -shade option causes TLATeX to typeset comments in shaded boxes. A specification generally looks best when comments are shaded. However, shading is not supported by most programs for viewing and printing dvi files. Hence, it may be necessary to create a Postscript or pdf file from the dvi file to view a specification with shaded comments. Here are all the options relevant to shading. -noPcalShade When the -shade option is chosen, this option causes a PlusCal algorithm (which appear in a comment) not to be shaded. (The algorithm's comments will be shaded.) -grayLevel num Determines the darkness of the shading. It is a number between 0 and 1, where 0 means completely black and 1 means white. The default value is .85. The actual degree of shading depends on the output device, and can vary from printer to printer and from screen to screen. You will have to experiment to find the right value for your system. -ps -nops These options tell TLATeX to create or not to create a Postscript or pdf output file. The default is to create one if the -shade option is specified, and otherwise not to. -psCommand cmd This is the command run by TLATeX to produce the Postscript or pdf output file. Its default value is "dvips". TLATeX calls the operating system with the command cmd dviFile where dviFile is the name of the dvi file produced by running LaTeX. If some more sophisticated command is needed, you should use the -nops option and run a separate program to create the Postscript or pdf file. HOW TLATeX TYPESETS THE SPECIFICATION ------------------------------------- TLATeX should typeset the specification itself pretty much the way you would want it to. It preserves most of the meaningful alignments in the specification. For example, if the specification contains Action == /\ x' = x - y /\ yy' = 123 /\ zzz' = zzz then the "/\" and "=" symbols will be aligned in the output. 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 "+". TLATeX typesets the single TLA+ module that must appear in the input file. It will also typeset any material that precedes and follows the module as if it were a comment. (However, that text won't be shaded.) The -noProlog and -noEpilog options suppress typesetting of material that precedes and follows the module, respectively. TLATeX does not check that the specification is syntactically correct TLA+ input. However, it will report an error if the specification contains an illegal lexeme, such as ";". HOW TLATeX TYPESETS COMMENTS ---------------------------- TLATeX now formats a PlusCal algorithm that appears inside a specification. A PlusCal algorithm appears inside a comment that is delimited by `(*' and `*)'. Everthing in the comment outside the PlusCal code is formatted like a comment. Comments inside the PlusCal code are formatted like ordinary comments in the specification. --------------------------------------------------------------- | WARNING: A left single-quote (`) has special meaning to | | TLATeX. Enclosing a word in single-quotes like `foo' is | | harmless, while `` and '' are just typeset as double-quotes. | | But beware of an unmatched left-quote and of the following | | two-character sequences: | | | | `~ `^ `. | | | | See below for further details about what single-quotes and | | these special sequences mean. | --------------------------------------------------------------- TLATeX 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. In a multi-line comment, TLATeX usually consider a sequence of non-blank lines to be a single paragraph, in which case it will typeset them as one paragraph and ignore the line breaks in the input. TLATeX does its best to do a sensible job of typesetting comments. You can help it by ending each sentence with a period (".") and by adding blank lines to indicate logical separation of items. There are three ways in which TLATeX can mess up the typesetting of comments: 1. Parts of a specification, such as identifiers and certain operators like "-", should be typeset differently from ordinary text. Identifiers should be italicized, and the minus in the expression "x-y" should be typeset differently from the dash in "x-ray". TLATeX gets this right most of the time, but it does make mistakes. You can tell TLATeX to treat something as part of a specification by putting single quotes (` and ') around it. You can tell TLATeX to treat something as ordinary text by putting `^ and ^' around it. For example: \*********************************** \* To find the latest value of `bar', \* see `^http::/frob/bar^'. \*********************************** But, this is seldom necessary. TLATeX usually does the right thing. -------------------------------------------------------- | WARNING: Do not put any character between `^ and ^' | | except letters, numbers, and ordinary punctuation. In | | particular, do not put any of the following characters | | between `^ and ^': | | | | _ ~ # $ % ^ & < > \ " | | | | See the section on using LaTeX commands in comments | | for further information about what can go between | | `^ and ^'. | -------------------------------------------------------- The -tlaComment option causes TLATeX to lean more towards considering a word to be an identifier. But it usually does a better job without this option. 2. TLATeX does not do any fancy formatting of paragraphs. For example, TLATeX will not precisely align the "A"s when typesetting: \*********************** \* gnat: A tiny insect. \* \* gnu: A short word. \*********************** You can tell TLATeX to typeset a sequence of lines precisely the way they appear in the input, using a fixed-width font, by enclosing the lines with `. and .' , as in: \********************************************** \* The following picture explains everything: \* \* `. ----------- -------- \* | Processor |------->| Memory | \* ----------- -------- .' \********************************************** Using `. and .' is the only reasonable thing to do for a diagram. However, if you know (or want to learn) LaTeX, the section below on using LaTeX commands in comments will explain how you can get TLATeX to do a good job of formatting things like lists and tables. 3. A paragraph may be typeset "loosely", with one or more lines containing lots of space between the words. This happens if there is no good way to typeset the paragraph. If this bothers you, the easiest solution is to rewrite the paragraph. You can also try to fix the problem with LaTeX commands. (See the section below on using LaTeX commands to format comments.) TLATeX ignores any (* ... *) comment that appears within another comment. So, you can get it not to typeset part of a comment by enclosing that part between (* and *). But a better way to omit part of a comment is to enclose it between `~ and ~'. ADJUSTING THE FORMAT OF THE OUTPUT ---------------------------------- The following options allow you to adjust the font size, the dimensions of the printed area, and the position of the text on the page. -ptSize num Specifies the size of the font. Legal values are 10, 11, or 12, which cause the specification to be typeset in a 10-, 11-, or 12-point font. The default value is 10. -textwidth num -textheight num These specify the width and height of the typeset output, in points. A point is 1/72 of an inch, or about 1/3 mm. -hoffset num -voffset num These specify distances, in points, by which the text should be moved horizontally or vertically on the page. Exactly where on a page the text appears depends on the printer or screen-display program. You may have to adjust this value to get the output to appear centered on the printed page, or for the entire output to be visible when viewed on the screen. OUTPUT FILES ------------ TLATeX itself writes two or three 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. TLATeX also runs the separate LaTeX program and possibly a program to produce a Postscript or pdf file. These programs produce additional 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 TLATeX is run. -out fileName If f is the root of fileName, then f.tex is the name of the LaTeX input file that TLATeX writes to produce the final output. TLATeX then runs LaTeX with f.tex as input, producing the following files: f.dvi - The dvi output file. f.log - A log file, containing LaTeX's messages. In this file, an "overfull hbox" warning means that a specification line is too wide and extends into the right margin, and an "underfull hbox" warning means that LaTeX could find no good line breaks in a comment paragraph. Unfortunately, the line numbers in the file refer to the f.tex file, not to the specification. But by examining the f.tex file, you can probably figure out where the corresponding part of the specification is. f.aux - A LaTeX auxiliary file that is of no interest. The default -out file name is the root of the input file name. -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 -out file. The only reason to specify a separate -alignOut file is for trouble-shooting, as described in the section below. -tlaOut fileName This option writes to fileName a file that is almost the same as the input file. (The extension "tla" is added to fileName if it has no extension.) The -tlaOut file differs from the input in that any portion of a comment enclosed by `^ and ^' is removed, and every occurrence of the two-character strings `~, ~', `., and .' is replaced by two blanks. As explained below, the -tlaOut option can be used to maintain a version of the specification that is readable in ASCII while using LaTeX commands to provide high-quality typesetting of comments. The default is not to write a -tlaOut file. -style fileName Normally, TLATeX inserts a copy of the tlatex package file in the LaTeX input files that it writes. The -style option causes it instead to insert a "\usepackage" command to read the LaTeX package named fileName. (LaTeX package files have the extension "sty". That extension is added to fileName if it's not already there.) The tlatex style defines a number of special commands that are written by TLATeX in its LaTeX input files. The package file specified by the -style option must also define those commands. Any package file should therefore be created by modifying the standard tlatex package, which is the file tlatex.sty in the same directory as TLATeX's Java program files. You might want to create a new -style package to change the way TLATeX formats the specification, or to define additional commands for use in `~ ... ~' text in comments. TROUBLE-SHOOTING ---------------- TLATeX's error messages should be self-explanatory. However, it calls upon the operating system up to three time to execute other programs: - It runs LaTeX on the -alignOut file that it wrote. - It runs LaTeX on the -out file that it wrote. - It may run the -psCommand to create the Postscript or pdf output file. After each of the last two executions, TLATeX writes a message asserting that the appropriate output file was written. It might lie. Any of those executions might fail, possibly causing no output file to be written. Such a failure can even cause the operating system never to return control to TLATeX, so TLATeX never terminates. Such a failure is the likely problem if TLATeX does not produce a dvi file or a Postscript/pdf file, or if it never terminates. In that case, you should try rerunning TLATeX using the -alignOut option to write a separate alignment file. Reading the two log files that LaTeX produces, or any error file produced by the psCommand, may shed light on the problem. Normally, the LaTeX input files written by TLATeX should not produce any LaTeX errors. However, incorrect LaTeX commands introduced in `^ ... ^' regions can cause LaTeX to fail. USING LaTeX COMMANDS TO FORMAT COMMENTS --------------------------------------- TLATeX puts any text enclosed between `^ and ^' in a comment into the LaTeX input file exactly as it appears. This allows you to insert LaTeX formating commands in comments. There are two ways to use this. 1. You can enclose between `^ and ^' a short phrase appearing on a single line of input. LaTeX typesets that phrase as part of the enclosing paragraph. 2. You can enclose one or more complete lines of a multi-line comment between `^ and ^'. That text is typeset as one or more separate paragraphs whose prevailing left margin is determined by the position of the `^. For example, the input \********************************** \* The first comment paragraph. \* \* The second comment \* paragraph. \* \* `^ Some LaTeX-formated \* text ^' \********************************** causes the LaTeX-formated text to be typeset in a separate paragraph whose prevailing left margin is the same as in the second comment paragraph. LaTeX typesets the text between `^ and ^' in LR mode for a one-line comment and in paragraph mode for a multi-line comment. The LaTeX file produced by TLATeX defines a "describe" environment that is useful for formating text in a multi-line `^ ... ^'. This environment is the same as the standard LaTeX "description" environment, except that it takes an argument, which should be the widest item label in the environment. For example, the input might contain \*********************** \* `^ \begin{describe}{gnat:} \* \item[gnat:] A tiny insect. \* \* \item[gnu:] A short word. \* \end{describe} ^' \*********************** Putting LaTeX commands in comments makes the comments in the input file rather unreadable. You can maintain both a typeset and an ASCII-readable version of the specification by enclosing text that should appear only in the ASCII version between `~ and ~'. You can then accompany each `^ ... ^' region with its ASCII version enclosed by `~ and ~'. For example, the input file could contain \************************************* \* `^ \begin{describe}{gnat: } \* \item[gnat:] A tiny insect. \* \* \item[gnu:] A short word. \* \end{describe} ^' \* `~ gnat: A tiny insect. \* \* gnu: A short word. ~' \************************************* The option "-tlaOut fileName" causes TLATeX to write to fileName a version of the original specification with `^ ... ^' regions deleted, and `~ and ~' strings replaced by spaces. (It also replaces `. and .' strings by spaces.) In the example above, the tlaOut file would contain the comment: \************************************* \* \* gnat: A tiny insect. \* \* gnu: A short word. \************************************* (The blank line at the top was produced by the end-of-line character that follows the ^'.) ----------------------------------------------------------------- | WARNING: An error in a LaTeX command inside `^ ... ^' text can | | cause TLATeX not to produce any output. See the section above | | on Trouble-Shooting | -----------------------------------------------------------------