Embedding TLA+ in LaTeX

[Paolo Dini]

I saw that a very similar question was asked about 3 years ago:

    https://groups.google.com/g/tlaplus/c/WzXGxFZwWLk/m/kRCkTLmTBAAJ

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,

    https://seldoc.eecs.yorku.ca/doku.php/tla/latex,

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:

    \documentclass[11pt,a4paper,fleqn]{article}
    \usepackage{tlatex}
    \usepackage{color}
    \definecolor{boxshade}{gray}{.9}\setboolean{shading}{true}
    \let\implies\relax

    \usepackage{hyperref}

    \begin{document}
    \begin{tla}
    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
    \end{tla}

    \begin{tlatex}
    \@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}%
    \end{tlatex}

    \end{document}

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?