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

[thomas...@gmail.com]

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]

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]

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]

It sounds reasonable. Feel free to open a Github issue for it here.

[Christian Barthel]

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>