teaching TLA

[Daniel Leivant]

I plan to incorporate next semester an introduction to TLA (and temporal logic) into a graduate introductory course on formal logic and program verification.
If anyone has any ideas, material, pointers, or experience to share, that would be tremendously helpful and greatly appreciated.

Thanks much in advance and best wishes  - Daniel

Daniel Leivant
Professor of computer science
and adjunct professor of mathematics
Indiana University Bloomington

[Stephan Merz]

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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/groups/opt_out.

[Friedrich Vogt]

Dear Daniel Leivant,

 

My experience shows that it is best to use Leslie’s hyperbook as the primary starting source and add (more!) theoretical background as appropriate for a possibly required understanding of related notations and/or concepts. Students tend to appreciate machine support for “thinking” quite a bit!

Another issue is the application background. The level of the “informal” understanding of the concepts of e. g. distributed systems is key before entering “formal” descriptions of it.

 

All the best

 

Fritz

[fl]

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

 

[fl]

 

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

 

 

 

Even better: the binary addition table (no loop).

 

--

FL 

[fl]

 

In my experience the learning curve of tlaplus is very long.

 

 

Let's be clear. I don't want to discourage anybody to use tlaplus. I think it's a very

valuable tool and that specifying an algorithm with it will always bring you

deep insights.

 

I also think that if you use a subset of tlaplus (let's say TLC + PCAL) you will

be able to use it very quickly.

 

I just want to avoid discouragement among those that are not aware that it is

a large piece of software that allows to do many things (specifying algorithms

but also digital systems, classical but also parallel algorithms, proving

everything, model checking).

 

I think tlaplus is a nice trip do to. But it's just like China, maybe, sometimes, you can

consider something a bit longer than a two-day round trip.

 

So maybe (I just say maybe -- I hope it will prudent enough) you may want to take

your time to get acquainted with it.

 

--

FL

[fl]

 

 

 

I think tlaplus is a nice trip do to. But it's just like China, maybe, sometimes, you can

consider something a bit longer than a two-day round trip.

 

 

You can also obviously have a two-day trip and then come back home, tell your trip

to some friends, think, go to the library to find information and understand

what you have seen,  and then go to China a second time  for one

month, come back home, think, go to France, come back home, think, go to China

for the third time with your wife this time, pay a visit the Tiananmen square.

 

After all it's a civilization that is several millennia old.

 

Well I stop. I feel I make my case worse.

 

--

FL

[Leslie Lamport]

I have no disagreement with what FL writes.  However, saying "TLA+ is
hard, but it's good for you" will needlessly scare away students.  Every
user of a non-trivial language just uses a subset.  I use a subset of
English.  Engineers can learn a subset of TLA+ that allows them
to use it in their work in two or three weeks.

 

I think it's usually better to start students using PlusCal rather
than TLA+.  However, they should know enough TLA+ to understand the
TLA+ translation of their PlusCal algorithms.  Computer people tend to
believe that languages have magical powers.  All you need to solve a
problem is to find the right language.  Believing in magic is not
conducive to proper thinking.  Students need to learn to think of
programs as specifying an initial states and next-state relations.
they use describe a program in terms of an initial predicate and
next-state relation.

 

Since Daniel is teaching about formal logic and program verification,
what is "usually better" may be best for his purposes.

 

Leslie

[fl]

 

> I have no disagreement with what FL writes.  However, saying "TLA+ is

> hard, but it's good for you" will needlessly scare away students. 

I apologize. I definitely don't want to frighten students. I swear I don't.

>  Students need to learn to think of

> programs as specifying an initial states and next-state relations.

> they use describe a program in terms of an initial predicate and

> next-state relation.

Well that's true: this is the most important idea in TLA+.

-- 

FL