Dear Daniel Leivant, Leslie's hyperbook is an obvious source for many ideas for such a course, it is essentially a tutorial: http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html. I have occasionally given TLA courses at summer schools, and I'll send you a set of slides off-list. For a description that focuses more on the logic of TLA, you may find some material in http://www.loria.fr/~merz/papers/tla+logic2008.html. The TLA+ distribution comes with a set of a few examples for the use of the model checker. I'm not sure if these are part of the TLA+ Toolbox distribution of TLC, but they are (or at least used to be) part of the standalone (command-line) tools available from http://research.microsoft.com/en-us/um/people/lamport/tla/tools.html#downloading. Best regards, Stephan On 16 Dec 2013, at 18:04, Daniel Leivant <lei...@xxxxxxxxxxxxxx> wrote:
|