# [tlaplus] Embedding TLA+ in Latex

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?

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.