You'll miss a lot on this web site unless you enable Javascript
in your browser.
The TLA+ Video Course
A series of video lectures on TLA+ that assumes only a basic understanding
of programming concepts.
Most beginners will find this the best way to learn TLA+.
However, it does not discuss PlusCal. Useful TLA+ operators
not described in the videos are explained here.
The PlusCal Tutorial
This
is a 14-session tutorial that teaches how to write and check algorithms
in PlusCal. It assumes only a basic understanding of programming
concepts.
Here is some additional material about PlusCal. Hillel Wayne's Web Site and Book [show]
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.
Practical TLA+ This links to a web page about a book by Hillel Wayne that provides a good complete course on PlusCal. The page contains a link to the book and my detailed comments on it. The PlusCal Manual [show]
PlusCal has two syntaxes: a C-syntax similar to that of C-based
languages like C# and Java, and a P-syntax similar to that of
older languages like Pascal. Most users will prefer the
C-syntax.
There are
versions of the manual for both:
C-Version P-Version Papers About PlusCal [show]The TLA+ Book
A book titled Specifying Systems
that you can download. It contains a complete description
of TLA+ and the TLC model checker as of 2002 when it was published,
which was before the Toolbox was developed. There have been
changes to the TLA+ language since then--the major ones being the
addition of recursive operator definitions and of
constructs for writing proofs. All the changes are
described
here.
A 7-page "cheat sheet"
extracted from the book
summarizes the TLA+ language and definitions from its standard
modules.
A Book About TLA
A final draft of a book titled A Science of Concurrent
Programs about TLA, the logic underlying the TLA+ language.
It is for computer scientists and for users of TLA+ who want to
understand its mathematical foundation and the rationale that
underlies the language.
The TLA+ Hyperbook
This is a hypertext book that I intended to be the way to learn TLA+
and PlusCal, until I realized that people don't read anymore and I made
the video course. It's unfinished, but it still provides a good
introduction to TLA+, PlusCal, and the TLAPS proof system.
|
|||