I am convinced. Completely sold on TLA+. You’ll see a lot more posts on TLA+ here. This one is on how to set up your ubuntu machine for TLA+ development.
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.
-Dorg.eclipse.swt.browser.DefaultType=mozilla
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!