tlatex fragments and beamer presentations

18 views
Skip to first unread message

Marko Schuetz-Schmuck

unread,
Aug 1, 2019, 12:13:33 PM8/1/19
to tlaplus
Dear All,

I'm preparing some beamer slides to summarize some of Leslies video
lectures and it seems there is a conflict between tlatex and
beamer. Apparently \. is defined in both and running latex on the
resulting file will end with

Runaway argument?
! File ended while scanning use of \next.

I intend to use prepare more beamer slides that will involve TLA+ and
would welcome advice on how others deal with this combination.

Here is a simplified example

\documentclass[compress,notes=hide]{beamer}
\let\oldImplies=\implies
\let\implies=\undefined
\usepackage{tlatex}
\begin{document}

\begin{frame}{Slide title}
\begin{tla}
IF pc = "start" THEN
i' \in 0..1000 /\
pc' = "middle"
ELSE IF pc = "middle" THEN
i' = i + 1 /\
pc' = "done"
ELSE FALSE
\end{tla}
\begin{tlatex}
\@x{ {\IF} pc \.{=}\@w{start} \.{\THEN}}%
\@x{\@s{13.31} i \.{'}\@s{5.25} \.{\in} 0 \.{\dotdot} 1000 \.{\land}}%
\@x{\@s{13.31} pc \.{'} \.{=}\@w{middle}}%
\@x{ \.{\ELSE} {\IF} pc \.{=}\@w{middle} \.{\THEN}}%
\@x{\@s{12.29} i \.{'} \.{=} i \.{+} 1 \.{\land}}%
\@x{\@s{12.29} pc \.{'} \.{=}\@w{done}}%
\@x{ \.{\ELSE} {\FALSE}}%
\end{tlatex}
\end{frame}
\end{document}


Best regards,

Marko
signature.asc

Markus Kuppe

unread,
Aug 1, 2019, 2:41:02 PM8/1/19
to 'Marko Schuetz-Schmuck' via tlaplus
Hi Marko,

I frequently embed TLA+ and PlusCal in Beamer presentations. Although I
use LyX [1] as a front-end to LaTex, my setup [2] might be useful for
you. See the lyx, latex, and pdf files [3] as a proof of concept for
your if-then-else above.

Hope this helps,
Markus

[1] https://www.lyx.org/
[2] https://lemmster.de/tla-in-lyx.html
[3] https://tla.msr-inria.inria.fr/kuppe/poc.zip


Marko Schuetz-Schmuck

unread,
Aug 2, 2019, 5:00:46 AM8/2/19
to Markus Kuppe, 'Marko Schuetz-Schmuck' via tlaplus
Dear Markus,

thank you very much! I had an older tlatex.sty, but the main key to
the solution was to use fragile with the beamer frame.

Best regards,

Marko
> --
> 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+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e01b34b3-7b14-3ba2-a3bd-b7aa11f0da8e%40lemmster.de.

--
Prof. Dr. Marko Schütz-Schmuck
Department of Mathematical Sciences
University of Puerto Rico at Mayagüez
Mayagüez, PR 00681
signature.asc
Reply all
Reply to author
Forward
0 new messages