Embedding TLA+ in Latex
Jam
\usepackage{tlatex}I put a simple TLA+ spec in a file (this is not valid, but I only need the snippet with q:
----------------------------- MODULE Spec -----------------------------q' = q + 1 \* Comment is here=============================================================================
\batchmode %% Suppresses most terminal output.
\documentclass{article}
\setlength{\textwidth}{360pt}
\setlength{\textheight}{541pt}
\usepackage{tla}
\begin{document}
\tlatex
\@x{}\moduleLeftDash\@xx{ {\MODULE} Spec}\moduleRightDash\@xx{}%
\@x{ q \.{'} \.{=} q \.{+} 1}%
\@y{\@s{0}%
Comment is here
}%
\@xx{}%
\@x{}\bottombar\@xx{}%
\@pvspace{8.0pt}%
\end{document}
Out of which I only used the part surrounded by empty lines. But after i pasted the lines in my document, I got several errors:
Please use \mathaccent for accents in math mode.
\add@accent ...@spacefactor \spacefactor }\accent #1 #2\egroup \spacefactor ... l.23 \@x{ q \.{'} \.{=} q \.{+} 1} % I'm changing \accent to \mathaccent here; wish me luck. (Accents are not the same in formulas as they are in text.) ! Missing { inserted. <to be read again> ^ l.23 \@x{ q \.{'} \.{=} q \.{+} 1} %You can't use `\spacefactor' in math mode.
\add@accent ...}\accent #1 #2\egroup \spacefactor
\accent@spacefactor
l.23 \@x{ q \.{'} \.{=} q \.{+} 1}
%
Missing } inserted.
<inserted text>
}
l.23 \@x{ q \.{'} \.{=} q \.{+} 1}
%
I've inserted something that you may have forgotten.
(See the <inserted text> above.)
With luck, this will get me unwedged. But if you
really didn't forget anything, try typing `2' now; then
my insertion and my current dilemma will both disappear.
Missing character: There is no � in font txex!
Missing character: There is no � in font txex!
Missing character: There is no � in font txex!
! Undefined control sequence.
<argument> \colorbox
{boxshade}{\usebox {\tempboxa }}
l.26 }
%
The control sequence at the end of the top line
of your error message was never \def'ed. If you have
misspelled it (e.g., `\hobx'), type `I' and the correct
spelling (e.g., `I\hbox'). Otherwise just continue,
and I'll forget about whatever was undefined.
The text comes out garbled. But i have found that if i dont use the package hyperref, almost all errors disappear, and the code looks correctly formatted except for the commend due to the following error:
<argument> \colorbox
{boxshade}{\usebox {\tempboxa }}
l.26 }
%
The control sequence at the end of the top line
of your error message was never \def'ed. If you have
misspelled it (e.g., `\hobx'), type `I' and the correct
spelling (e.g., `I\hbox'). Otherwise just continue,
and I'll forget about whatever was undefined.
Unfortunately I'm not proficient enough in Latex to even know what is happening. Has anyone here encountered these issues?
Leslie Lamport
Leslie