[tlaplus] Embedding TLA typeset rules in a Latex document

Hi,

I have been trying to embed TLA typeset formulas in a Latex document. I have gone through the instructions for downloading and installing the tools at https://lamport.azurewebsites.net/tla/standalone-tools.html?back-link=tools.html#tlatex?unhideBut@EQhide-tlatex@AMPunhideDiv@EQtlatex

I am using Windows. The instructions in the page includes the following -

"Let's suppose that your folder is c:\user\myfolder . This will create a subfolder of myfolder named tla that has three subfolders, each containing one of the tools. You must then add c:\user\myfolder\tla to your CLASSPATH variable."

However, after extracting thetla2tools.jar file, instead of a folder named tla with three subfolders, three separate folders for each tool called tla2sany, tla2tex and tlc2 were created, along with some other folders.

I tried adding tla2latex to my CLASSPATH and then running the following in the directory where my tex file is present (as described in https://lamport.azurewebsites.net/tla/texinfo.txt):

java tla2tex.TeX My_file.tex

I also tried the above by adding the tla2latex folder to my Path variable in windows.

However, it seems that the tla2tex folder does not have any class named tla2tex.TeX.

I will appreciate any help regarding this. If there is some other way to embed tla+ into a latex document, that will be helpful as well.

Thanks