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

[hwayne]

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

[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.