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!
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?
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.
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.
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!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.
Auxon gave a talk at TLAconf this year. They’re using it for safety-critical industrial applications.
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.
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.
Hi @nickpsecurity, I shall check it out. Thanks for pointing me to it.
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
Hey @hwayne, thanks! Will check it out.