Include TLA+ in LyX documents and export it pretty-printed to PDF

Create a wrapper script for tla2tex.TeX (part of tlatools), put it onto $PATH and name it



# Creating dummy file ${OUTPUT%.*}.tex for tla2tex to remove. It apparently needs this.
touch ${OUTPUT%.*}.tex

# Running tla2tex.TeX on $INPUT and writing output to ${OUTPUT%.*}.tex. Expects the TLA+Toolbox to
# be installed to /opt/TLA+Toolbox
java -cp /opt/TLA+Toolbox/plugins/org.lamport.tlatools_1.0.0.*/ tla2tex.TeX -out ${OUTPUT%.*}.tex $INPUT

# Converting ${OUTPUT%.*}.tex back to $OUTPUT for LyX to read it
cp ${OUTPUT%.*}.tex $OUTPUT

Open up LyX and create two new "File Formats" under Tools > Preferences > File Handling > File Formats:

Format: LaTeX (tla2tex)
Short name: tla2tex
Extensions: tex

Format: PDF (tla2tex)
(Check "Document format", "Show in export menu", "Vector graphics format")
Short name: pdf4tla2tex
Extensions: pdf
Shortcut: T
Viewer: qpdfview --unique

Also create two new LyX "Converters" under Tools > Preferences > File Handling > Converters:

From/To: LaTeX (plain) -> LaTeX (tla2tex)
Converter: $$o $$i

From/To: LaTeX (tla2tex) -> PDF (tla2tex)
Converter: pdflatex $$i
Extra flag: latex=pdflatex

Afterwards run Tools > reconfigure and restart LyX. TLA+ statements can then be included in LyX documents inside LyX's \ERT within a "tla" or "pcal" environment provided the document's LaTeX preamble declares a \usepackage{tlatex} as explained in the tla2tex help and be exported via File > Export > PDF (tla2tex):

(* A standard definition of spec.              *)
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

Ideally, the excerpts were sourced from the .tla file directly so that one wouldn't need to copy&paste parts of a specification into the .tex document. Someone might want to look into This. The catchfilebetweentags packages seems to be a viable candidate.

Last posts

  1. Forcefully re-resolve a stale PDE target definition
  2. Cross-compile kernel module (ext2) for Samsung nx300 on Ubuntu 14.04
  3. Auto backup files from the Samsung NX300 camera in the background
  4. SWTError: No more handles [gtk_init_check() failed] running platform tests (on Linux)
  5. Apache Felix HTTP whiteboard pattern on Equinox