Ever checked the https://lamport.azurewebsites.net/tla/practical-tla.html?

[leiless]

Hi, Hillel. I loved your Learn TLA+ tutorial, and I was so fascinated by the second version of the book.

As I go through the TLA+ website, I found that Lamport already said something about your book https://lamport.azurewebsites.net/tla/practical-tla.html.

I guess there is some overlapping in the content between the book and this tutorial, more or less.

And if you haven't checked it yet, I guess you may look at it, you might find something useful. :-D

[leiless]

The LearnTLA Web Site This web site, written and maintained by Hillel Wayne, is a beginning course in PlusCal. It covers just about all of PlusCal's programming-like constructs, but not all of the TLA+ mathematical operators that can be used in PlusCal expressions. There are currently a number of minor problems with this course, plus one major one. A PlusCal algorithm can be written in either of two syntaxes; the book uses the P syntax, while most engineers will prefer the C syntax. I hope these problems will eventually be corrected. https://lamport.azurewebsites.net/tla/learning.html

Hope this will be helpful to the version 2.

[hwayne]

Yup, that was the comments he had for version one. This was before I wrote practical tla+ and version two of Learntla. I I know a lot of the critique was factual errors, which I think I've corrected, but I should go back and triple check them.