[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Embedding TLA+ in LaTeX

I saw that a very similar question was asked about 3 years ago:
regarding the effect of hyperref on the compilation of a LaTeX document.

Leslie's reply to Jam's question referred to slightly different commands to what I am using: he said to use TeX.java rather than TLA.java. I am using tla2tex.TeX rather than tla2tex.TLA:
    java -cp ./tla2tools.jar tla2tex.TeX tlatextest.tex,
 as explained at this link,
and indeed the command works well even with the \usepackage{hyperref} command enabled.

The problem for me is at the next step. I use TeXShop routinely and would like to use it for a report that has TLA+ code in it. I also use Overleaf and had the same problem. If hyperref and/or bookmark are enabled, I get a compilation error very similar to what Jam got.

Here is the code of a minimal example, after it has gone through the first step:

    TypeOK ==
        /\ pendMsg \in [Term -> STRING \X {0,1}]
        /\ rcvMsg \in [Term -> STRING ]
        /\ altt \in [Term -> {0,1}]
        /\ msgCnt \in [Term -> Int]
        /\ errCnt \in [Term -> Int]
        /\ swapTerm \in {0,1}
        /\ step \in Int
    \@x{ TypeOK \.{\defeq}}%
      \@x{\@s{16.4} \.{\land}\@s{12.22} pendMsg \.{\in} [ Term \.{\rightarrow}
      {\STRING} \.{\times} \{ 0 ,\, 1 \} ]}%   
      \@x{\@s{16.4} \.{\land}\@s{12.22} rcvMsg \.{\in} [ Term \.{\rightarrow}
      {\STRING} ]}%
      \@x{\@s{16.4} \.{\land}\@s{12.22} altt \.{\in} [ Term \.{\rightarrow} \{ 0
      ,\, 1 \} ]}%
      \@x{\@s{16.4} \.{\land}\@s{12.22} msgCnt \.{\in} [ Term \.{\rightarrow} Int
      \@x{\@s{16.4} \.{\land}\@s{12.22} errCnt\@s{4.19} \.{\in} [ Term
      \.{\rightarrow} Int ]}%
    \@x{\@s{16.4} \.{\land}\@s{12.22} swapTerm \.{\in} \{ 0 ,\, 1 \}}%
    \@x{\@s{16.4} \.{\land}\@s{12.22} step \.{\in} Int}%

If the hyperref package is not included this code compiles with TeXShop without errors and generates the pdf. If hyperref is included this is the error I get:

    LaTeX Warning: Command \. invalid in math mode on input line 19.
    ./tlatextest_GGroups_Question.tex:19: Missing $ inserted.
    <inserted text>
    l.19 \@x{ TypeOK \.{\defeq}}

and no output is generated.

I need hyperref in my documents so I am stuck. Can anyone suggest a workaround?

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/7c378896-0367-4d0d-994e-55c0b6891130n%40googlegroups.com.