Re: [tlaplus] Get the raw LaTeX from the spec instead of an exported PDF?

[Christian Barthel <bch@xxxxxxxxx>]

"thomas...@xxxxxxxxx" <thomasgebert@xxxxxxxxx> writes:

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

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 <bch@xxxxxxxxx>

-- 
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/87r1rsbkv8.fsf%40barthel.ch.