In Victoria university Wellington New Zealand I am teaching 23 students in a 400 level course on applied formal methods. This year is the first year using TLA+, previous years used Spark Ada and Event B.
Personally there is a lot about TLA+ that I like. But, of course, a lot of frustrations. Certainly the PlusCal extension is essential for the students to be able to do much in a single course. I will have a better idea how easy it was for the students to cope with at the end of the course, or at the end of next years course. Finding easy high level strategies for applying TLA+ and strategies for debugging TLA+ specs has consumed a lot of time. But, hopefully next year I will be more able to help the students in these areas.
kind regards david
On Friday, 26 April 2019 07:57:56 UTC+12, markos...@xxxxxxxxxxxxxx wrote:
Dear All,
Hillel Wayne made me aware of Murat Demirbas using TLA+/PlusCal as part of teaching distributed algorithms. I imagine it can be used in many more courses and would like to hear of experiences. For example, does someone have experience using it in an analysis of algorithms course? Any other course?
Thanks and best regards,
Marko