A walkthrough tutorial of TLA+ and its tools: analyzing a blocking queue
1–7 of 7 posts
Re: A walkthrough tutorial of TLA+ and its tools: analyzing a blocking queue
#2This is the coolest demonstration of TLA+ I've seen to date. It takes you through specification, implementation, model-checking with TLC, visualization and animation, checking an inductive invariant, deductive proofs mechanically checked by TLAPS, refinement mapping and even model-based trace checking.
Re: A walkthrough tutorial of TLA+ and its tools: analyzing a blocking queue
#3If anyone is trying to learn TLA+, this site looks like a good one: https://learntla.com/ too
Re: A walkthrough tutorial of TLA+ and its tools: analyzing a blocking queue
#4This is the coolest demonstration of TLA+ I've seen to date. It takes you through specification, implementation, model-checking with TLC, visualization and animation, checking an inductive invariant, deductive proofs mechanically checked by TLAPS, refinement mapping and even model-based trace checking.
OT: I don't know if this level of rigor is employed by any major libraries. I know AWS has used it a great deal for their systems though notably recently[1]
[1] https://assets.amazon.science/c4/11/de2606884b63bf4d95190a3c...
Re: A walkthrough tutorial of TLA+ and its tools: analyzing a blocking queue
#5If anyone is trying to learn TLA+, this site looks like a good one: https://learntla.com/ too
Lamport lists various learning resources on his page: http://lamport.azurewebsites.net/tla/learning.html
Re: A walkthrough tutorial of TLA+ and its tools: analyzing a blocking queue
#6If anyone is trying to learn TLA+, this site looks like a good one: https://learntla.com/ too
OP is perhaps being a bit modest, but his own website https://pron.github.io/tlaplus is a fantastic resource.
Re: A walkthrough tutorial of TLA+ and its tools: analyzing a blocking queue
#7If anyone is trying to learn TLA+, this site looks like a good one: https://learntla.com/ too
I liked the Practical TLA+ book: