Using tlatext to typeset TLA+ Module that contain PlusCal specification

[Stephan Rehfeld <stephan...@xxxxxxxxx>]

Hi,

I'm currently using PlusCal to specify some algorithms in my PhD Thesis. I want to include the complete Module that contains the algorithm in the appendix. Producing a PDF using the Toolbox works fine but can't be used in my LaTeX document. Using tlatex and the tla and ppcal envionemnts works fine, as long as the TLA+ parts and PlusCal parts are not within the same environment. The translation process fails, if I just copy my complete module into a tla environment. The PlusCal specification in the comment is not recognized.

Is there any possibility to create a type setted version using tlatex, such as procued by the Toolbox?

Regards,

Stephan