I plan to incorporate next semester an introduction to TLA (and
temporal logic) into a graduate introductory course on formal logic
and program verification.
By the way there is a tool that is rarely mentionned and that I find very useful. It is java tlc2.Generator.
It generates traces of the designed algorithm. It is useful to grasp what happens.
Try: tlc2.Generator -d 150 -f spec-trace <name of your spec>
In my experience the learning curve of tlaplus is very long. There are many things to grasp:
a non classical logic, a representation of algorithms that is not standard, demonstrations
at a very formal level, several kinds of tools (tlc, pcal, tlaps). Tlaplus is also designed to work with
parallel algorithms.
And there are also pitfalls in the tools that make thinks still harder.
Maybe a mixture of TLC with Pcal may be a good beginning on a very simple algorithm (for instance
the generation of the addition table).
--
FL