If you run the pretty-printer from the Toolbox on a module M in a spec S, you will find in the directory S.toolbox a file M.tex from which LaTeX created the pdf file M.pdf. If you copy the body of that M.tex file into your thesis and add the appropriate subset of the preamble of M.tex, it might work. Otherwise, you'll have to copy the TLA+ formulas and the PlusCal code from your specs into separate tla and pcal environments, and copy any comments into the main text of your document.
The only other alternative is finding the source of the tla2tex.TLA java program and modifying it to do what you want. But I expect that, like me, you have more important things to do.
Leslie
On Sunday, November 8, 2015 at 11:58:30 AM UTC-8, Stephan Rehfeld wrote:
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