[tlaplus] Embedding TLA+ in Latex

From: Jam <wawrzynchonewicz@xxxxxxxxx>

Date: Sun, 5 May 2019 08:18:33 -0700 (PDT)

Hello. I've been trying to embed formatted TLA+ in a Latex document. I have downloaded and imported the style from here https://lamport.azurewebsites.net/tla/tlatex.sty, and I added it to my text with

\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
=============================================================================

Then, i ran the tla2tex tool on it, which resulted in the following output

\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?

tlaplus+unsubscribe@xxxxxxxxxxxxxxxx

tlaplus@xxxxxxxxxxxxxxxx

https://groups.google.com/group/tlaplus

https://groups.google.com/d/optout