I experimented with TLA, and the graphical toolbox didn't seem to work or match the tutorial. Kinda disappointing: I wanted to use TLA, and I'm otherwise a big fan of Lamport's work, from the utilitarian Latex to the intellectually satisfying paper on time, clocks, and distributed systems.