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

54 views
Skip to first unread message

thomas...@gmail.com

unread,
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

unread,
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.

thomas...@gmail.com

unread,
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

unread,
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

unread,
Aug 27, 2020, 3:37:03 AM8/27/20
to thomas...@gmail.com, tlaplus
Hello,
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
\documentclass[11pt]{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{graphicx}
\usepackage{tlatex}
\usepackage{color}
\definecolor{boxshade}{gray}{0.85}
\setboolean{shading}{true}
\newcommand{\figscale}{.65}
\begin{document}
\title{Testing}
\author{Christian Barthel}

\section{My test}
\begin{figure}[!h]
\begin{tla}
------------------------------- MODULE HC ------------------
EXTENDS Naturals
VARIABLES hr

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))
===========================================================
\end{tla}
\begin{tlatex}
\end{tlatex}
\end{figure}
\end{document}
%< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %<

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

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:
https://github.com/hengxin/tla2tex


--
Christian Barthel <b...@online.de>
Reply all
Reply to author
Forward
0 new messages