[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: teaching TLA

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