Re:Introduction to TLA+ Model Checking in the Command Line
by aseipp on Friday January 18, 2019 @03:13PM
(#18942592)
I think it's mostly just sticker shock. Downloading another thing, and it's a bit spoiling these days when most toolsets have some amount of cross-editor support. You can do similar things in various language modes in VS Code, after all (plotting/fancy rendering/cloud APIs).
There don't seem to be many developers working on TLA+ outside of Microsoft Research though, so I think their work is probably better spent elsewhere than just recreating the Toolbox in other editors. It's not that bad. Maybe in a year or two if TLA+ continues growing in popularity someone will help hash out an alternative.
In a prior project one of our developers checked their models in the Toolbox originally and then we just ran them in CI from the command line, which also worked fine and made it easier if people wanted to run/edit them "by hand" in vim or something.
- It shows you the ASCII and pretty printed spec side-by-side.
- It plots TLC data as it runs and presents live coverage data in a nice way. Soon it will also show TLC performance profiles as color maps. (https://twitter.com/lemmster/status/1082787089140183040)
- It makes running TLC in the cloud (single-node or distributed) very easy. (https://tla.msr-inria.inria.fr/tlatoolbox/doc/cloudtlc/)
- I don't know of any other way of using TLAPS. (https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T...)
Then again, I'm really not a fan of either vim or emacs, despite having used the latter as my main editor for some years. I think this may be because I value tools that present more information in a convenient way that allows me to inspect and analyze my text over tools that allow editing more quickly (when I write code, I spend 80% of my time in Sourcetrail and only use the editor to punch-in characters), but I don't know.