1. 43
    1. 13

      I am absolutely delighted that you found TLA+ so useful! If you want a “very large” discount on a Practical TLA+ PDF, please let me know and I’ll make it happen :)

      (Same goes for everyone else- I care much, much more about people learning TLA+ than I care about making money off the book.)

      EDIT: oh, one small request: when you mention Alloy, you link to http://alloy.lcs.mit.edu/alloy/. Could I ask you to change it to http://alloytools.org/? The MIT link is deprecated, and we’re in the process of moving stuff over to the new site. You’re not the first person to make this mistake this week, and I just sent a message to the core team bringing up the problem. Redirect is now in place!

      1. 3

        Thanks. I don’t have a need for a discount. What I’m currently missing is a good excuse to introduce it at work. Do you know of any users in automotive or other safety-critical industries?

        Link for Alloy is changed.

        1. 7

          Auxon gave a talk at TLAconf this year. They’re using it for safety-critical industrial applications.

    2. 2

      I have to present the Raft algorithm to my team at work in a few weeks’ time. Wondering how TLA+ can be used to illustrate the scenarios. I am aware that the algorithm is model checked with TLA+ already, but that might be too complex for pedagogic purposes.

      1. 3

        You might also like to read Murat Buffalo’s TLA+ articles. He keeps both specing and analyzing interesting protocols in TLA+. The resulting write-ups are great. I’d say look for simpler ones like two-phase commit first, though.

        1. 2

          Hi @nickpsecurity, I shall check it out. Thanks for pointing me to it.

      2. 3

        At one point Ongaro was working on his own (now defunct) specification language, and made an interactive raft demo in it: https://runway.systems/?model=github.com/ongardie/runway-model-raft

        1. 2

          Hey @hwayne, thanks! Will check it out.