TLATeX

[Pedro Paiva]

Hi there,

I'm trying to use the tlatex package within the tex editor (texstudio) to write TLA+ expressions. I included the \usepackage{tlatex} line and tried to write something simple like

\begin{tla}
    Action == /\ x'   = x - y
    /\ y'  = y
\end{tla}

It builds with no errors, but nothing appears in the generated pdf file. Probably I'm doing something wrong. Could someone help me? Thanks!

Best regards,

Pedro

--

Pedro Yuri Arbs Paiva

Engenheiro Eletrônico

Instituto Tecnológico de Aeronáutica (T-16)

(+55) 12 98106-4129

[Leslie Lamport]

I know nothing about texstudio and don't know what "It builds with no
errors" means.  To run tlatex on a LaTeX file foo.tex, you should run
a command something like

   java tla2tex.TeX foo

This rewrites the file foo.tex, inserting appropriate LaTeX commands
below each tla environment.  It does not run LaTeX.

I have no idea how the texstudio tex editor reacts if the file foo.tex
is changed by an external program.

Leslie

[Pedro Paiva]

Thanks, Mr. Lamport, it works fine!

Best regards,

--
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@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.