TLA Toolbox is a pretty decent IDE for TLA+, built on top of eclipse. On my machine, the ToolBox jvm process kept crashing. Adding the following line to toobox/toolbox.ini fixed this. For more details, refer this eclipse bug.
The ASCII to PDF export (LaTex) would fail unless you have pdflatex installed.
sudo apt-get install texlive-latex-base
As for running the Model Checket, I prefer to use the TLA+ tools from the cli. Make sure to add the tla2tools.jar to your classpath and you should be good to go!