Practice questions and answers for TLA+

[David Ajaba]

Hi Everyone, I'm new here. 😅 So please, pardon my question if this question has been asked before. And please, if it has been asked, please kindly leave a link to the question please.

But, as you may have guessed, I'm new to TLA+ and I'm trying to find my way around it to better understand the formal language and proceed to designing Distributed Systems using my new found knowledge. But I'd like to practice what I've learned before building an real world systems, because I'm in this in between state of "I understand, but I'm not sure I fully understand". Please are there any resources to practice questions and answers I can use to jump right in and attempt to solve challenges (hopefully beginner friendly), break things and learn on the go?

By the way, I recommend https://www.youtube.com/playlist?list=PLWAv2Etpa7AOAwkreYImYt0gIpOdWQevD to learn TLA+ from Dr. Leslie Lamport himself.

[Ryan Worsley]

Not exactly what you're looking for, but Jack and Murat's blogs both have interesting TLA exercises you can do and follow along with. I'm sure others here will have some fine links to undergraduate courses with exercises though.

[Daniel]

Hi David,

have you checked out the awesome-tlaplus repo? It contains a list of university lectures using TLA+. Some of them contain exercises which you could do :)

Generally, distributed systems lectures often contain classic problems. Some of them are the two generals problem, leading to the byzantine generals problem, the river crossing puzzle, or the dining philosophers problem. 

You could try to model those in TLA+. Specs already exist online for all of them, so it's easy to compare your spec to others.

[David Ajaba]

Thank you so much Ryan Worsley, this was really helpful. I'll check them out.

[David Ajaba]

Thank you Daniel, the awesome-tlaplus repo is amazing. I've found my next steps in my TLA+ plus journey along with the blogs from Ryan. Wish me luck! 🤩