Get the raw LaTeX from the spec instead of an exported PDF?

Skip to first unread message

Aug 25, 2020, 12:06:27 PM8/25/20
to tlaplus
Hello! I have a spec that I designed in the Toolbox, and I want to take the spec and include it into a paper I'm writing.  Is there a way to export the raw LaTeX code from the toolbox instead of just the PDF? 

Willy Schultz

Aug 25, 2020, 1:12:57 PM8/25/20
to tlaplus
I'm not sure if there's an officially supported way to get the TeX source directly from inside the Toolbox, but if you click "File > Produce PDF Version", the TeX output from the PDF generation should be placed in the *.toolbox directory of your spec. For example, if your module is named "Spec", you should find a .tex file at "Spec.toolbox/Spec.tex". You could retrieve it manually from that location. If you want to bypass the Toolbox entirely, you can generate the TeX source from the command line using the `java tla2tex.TLA` tool directly.

Aug 25, 2020, 4:29:54 PM8/25/20
to tlaplus
That works, I was able to grab it from the `.toolbox` folder.  

I can't imagine it would be too hard to add this as an official feature for the toolbox, would it? It has to produce the TeX anyway to create the PDF, I would think it would be pretty straightforward to add an option to have a little menu-item underneath saying "export TeX" or something. 

Willy Schultz

Aug 25, 2020, 5:47:45 PM8/25/20
to tlaplus
It sounds reasonable. Feel free to open a Github issue for it here.

Christian Barthel

Aug 27, 2020, 3:37:03 AM8/27/20
to, tlaplus
I think you can embed TLA+ code within a LaTeX document and
generate the pretty printed version of it. To do so: create a
document like this:

%< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %<
% filename: test.tex
\author{Christian Barthel}

\section{My test}
------------------------------- MODULE HC ------------------
EXTENDS Naturals

vars == <<hr>>

Init == /\ hr \in 1..12
Next == /\ hr' = IF hr = 12 THEN 1 ELSE hr + 1

Spec == Init /\ [][Next]_vars

Invariant == [](hr \in (1..12))
%< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %<

Then, it is possible to generate pretty printed TLA+ code

java -cp tla2tools.jar tla2tex.TeX test.tex

This will basically fill in the LaTeX code between
"\begin{tlatex}" and "\end{tlatex}". And finally compile it to a
PDF file:

pdflatex test.tex

See also:

Christian Barthel <>
Reply all
Reply to author
0 new messages