I get to teach part of a course on distributed algorithms to 4th year students, and I have been trying to use PlusCal / TLC. The experience has been mixed: our students haven't had any previous exposure to formal verification, and I don't have time to properly introduce the language. As a result, students had to cope with the difficulties of distributed algorithms and a language that is significantly different from anything they'd seen before. This year I switched to DistAlgo [1], a domain-specific language embedded in Python. The students liked it much better: the base language is familiar, so they can focus on the distributed aspects. For me, the main drawback is that there is no way to explore all possible executions of the program. I've resorted to introducing a dose of randomization in order to explore more interleavings, but obviously this is no match for model checking. There appears to have been a project of generating TLA+ specs from DistAlgo programs, but it doesn't seem to be active anymore.Stephan[1] https://github.com/DistAlgo/distalgo On 30 Apr 2019, at 17:50, Jonathan Ostroff <jonathan...@xxxxxxxxx> wrote:Hi:This year, I used TLA+/TLC (not Pluscal) in a component of a 4th year course on Requirements Engineering (5 weeks of a 12 week term) for software engineering and computer engineering students. This group provides a lot of help that has made it possible to teach the material. I’ll be teaching it again in the Fall. It’s a valuable tool for helping students formulate and test specifications above the code level. TLA+ has extremely powerful expressions, nondeterminism, a convenient way to describe atomicity, and model checking (safety and liveness). It is this combination of features that makes TLA+ a powerful tool from the point of view of an engineer designing complex systems that are safe and fit for purpose.RegardsJonathan(Lassonde School of Engineering, York University, Toronto.)On Apr 30, 2019, at 12:28 AM, david streader <davidis...@xxxxxxxxx> wrote:HIIn 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...@googlemail.com 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--
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 tla...@googlegroups.com .
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus .
For more options, visit https://groups.google.com/d/optout .
--
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 tla...@googlegroups.com .
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus .
For more options, visit https://groups.google.com/d/optout .