<div dir="ltr">Hi folks,<div><br></div><div>I've recently been re-living my misspent university days learning about modelling complex systems and model-checking. In particular, I've been reading about TLA+ (Temporal Logic of Actions) [0], a language conceived by Leslie Lamport, and playing with the TLA+Toolbox. The TLA+Toolbox is an Eclipse-based IDE for defining specifications and checking models against them.</div><div><br></div><div>I have snapped the TLA+Toolbox application; the snap is called "tlaplus". If you're interested in this area at all, I can recommend the TLA+ Hyperbook [1] (or what I've read of it so far, anyway). Please let me know of any problems you encounter using the snap. I know for one thing that the hyperlinks from the IDE do not work.</div><div><br></div><div>Cheers,</div><div>Andrew</div><div><br></div><div>[0] <a href="https://research.microsoft.com/en-us/um/people/lamport/tla/tla.html">https://research.microsoft.com/en-us/um/people/lamport/tla/tla.html</a></div><div>[1] <a href="https://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html">https://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html</a></div></div>