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>