Skip to Content

Announcing: Learn TLA+

Posted on

tl;dr: online TLA+ manual/advanced techniques/examples here.

TLA+ is a tool for testing abstract software designs. I first stumbled on it in 2016 and found it so useful I wrote a free online guide to help others learn it. Then I decided the guide wasn’t good enough and wrote Practical TLA+ in 2018. Then I decided the book wasn’t good enough and needed a second edition.

Just kidding! Book’s never getting a second edition, because it costs $26 and no matter how good I make it, it’s never going to have the reach of a free resource. So instead I took all the teaching lessons I learned over the past four years and turned them on rewriting the online guide from scratch.

Six months and 40,000 words later, the Learn TLA+ rewrite is now online! While I’m nowhere near done writing, the guide’s now complete enough to be a useful TLA+ resource, for beginners and experts alike.

What’s Different?

The old verison of learntla was about getting people up and running as fast as possible. The new version does that too, but as only one part of the full site. Even so, the core’s now heavily expanded:

  • I reorganized the teaching order to introduce more “programming-like” concepts earlier.
  • It now covers writing temporal properties, action properties, pure TLA+ specs, and modules.
  • Specs are now shown iteratively, as a progressive series of changes from a base spec. Each spec also comes with a state space “fingerprint” you can use to keep in sync with the guide.
  • There’s now lots of internal references, a search page, and a proper index.

The new version is also meant to be a resource for experienced practitioners, too. So there’s now a special topics section, with articles on

  • General tips
  • Using TLA+ from the CLI
  • Auxiliary variables
  • State machine patterns

I have more topics planned, that’s just what I got done by the end of June. Finally, I’m writing a bunch of examples that cover various specification domains, how to get around problems, operator design, etc.

(There’s also a lot of backend changes I made to maintain the site better. This shouldn’t affect your reading experience, but it makes it easier for me to add and maintain content. I put the details in an Appendix if you’re interested in reading it.)

The Work to be Done

I’ll say upfront that Learn TLA+ isn’t anywhere near complete. First of all, this is the first time other people are seeing the new content. In writing you have to constantly revise what you do. I expect there will be significant changes as people start reading it and providing feedback. If you have any comments or critiques, please share them all at the Github repo!

Second, I scoped the initial release to six months and had to cut a lot of planned content. There aren’t any exercises, and I still need to write many of the topics and examples.

Finally, as mentioned, this is dynamic. I’ll be making lots of improvements over time. You can read what I plan to do over at the roadmap.

I hope you enjoy!

Appendix A: What about Practical TLA+?

Don’t bother. There’s some specifications in the book that won’t be put in Learn TLA+ for legal reasons, but otherwise I’m aiming to make learntla a strictly-better resource. It already covers a host of things not in PT, like action properties, strong fairness, and advanced operators. Plus, learntla is free!

Appendix B: Backend Changes

These are changes users aren’t likely to see but help me maintain the site better. I’m including them in case people are interested (or want to repeat them). All of the code is here.

Autobuild

I deployed the old version of learntla with a custom script that I never remembered to run. The new version uses a GitHub action to build on every push to master.

Sphinx

In the past five years I’ve developed fairly strong opinions on how to document well, especially on the importance of extensibility. Hugo, which powered the old version of learntla, is poorly-suited to serious documentation projects. I migrated the site to Sphinx. Sphinx has a steeper learning curve, but is a much better choice for documentation overall. Here’s just three reasons why:

  1. Internal referencing. Sphinx has a native tag for path-independent internal references. This meant I could move content around without having to rewrite any of the referencing hyperlinks. Hugo has a similar ref shortcode but it’s far too limited to be useful.

  2. Programmability. Sphinx creates an intermediate doctree representation you can transform before it renders out into html. The format isn’t well documented but with some experimentation I was able to make a lot of useful customizations.

  3. Extensibility. Sphinx lets you create custom text elements that’s treated as first-class markup syntax, as opposed to as a preprocessor for a markdown doc. Sphinx uses this to add a bunch of useful features, such as automatic indexes and toggleable TODO blocks. But I also added a few of my own, like spec. That’s what powers the user-facing autodiffs.

More tooling

One lesson I’ve learned the hard way is that keeping lots of assets in sync is an absolute nightmare. So this version has a lot more software managing that for me. In particular, I built a pipeline for handling spec assets. I have several XML spec templates that represent “sequences of iterations” on a spec. A python script unpacks the template into a set of .tla files. After I put in appropriate metadata, a second script cleans up each spec into a “presentable” form, loads the metadata into the appropriate files, and places the asset in the appropriate path. Then I can just write

.. spec:: spec/version/4
  :diff: spec/version/3

And that automatically renders the diff between the two specs in the guide.

Because all of the specs are reproducibly built from a template, I can modify version 1 of the spec and automatically propagate the changes to versions 2-4. The benefits of this approach were enormous and now I can’t imagine working without it. Plus, I can finally say I found a good use for XML.