Apologies for the deletion, google groups has been acting up and deleting random replies for years now. I usually deal with it by sending replies through email, not the google groups web interface. That way if the message gets deleted I can find it in my sent folder and re-send it.Andrew Helwer--On Wed, Sep 24, 2025 at 6:45 PM 'dvnh87' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:It looks like my previous reply was deleted? Here it is again:Thank you, the links should be fixed now:For edits, can you make a pull request?--The “All model sources can be found here.”
Link does not appear to work?!
Is this the correct place to send minor edits?
Thanks
Dave
From: 'Jskri' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx>
Sent: 23 September 2025 12:31
To: tlaplus <tlaplus@xxxxxxxxxxxxxxxx>
Subject: [tlaplus] Feedback on TLA+ tutorial and proofs
Hello,
Some time ago, I wrote a (long) tutorial on TLA+ intended for engineers.
It is very proof-oriented, using a “correct by construction” approach, as presented by J-R. Abrial, the author of Event-B. The idea is to start with a very abstract model and refine it as many times as necessary until you arrive at a version that can be easily translated into code. For each model, the invariants (safety) and refinement are proven.
The tutorial therefore covers these different concepts, but also how to break down a model into sub-models, and finally how to verify that the implementation (the code) complies with the model.
The approach is illustrated by several examples and finishes by a client-server system, implemented in C++20 / ZeroMQ.
There is nothing new in this work, but I have tried to present what I have learned here and there in a way that I hope is coherent. I also feel that there are not many introductions to proof with TLA+.
The PDF is here: https://github.com/jskri/modeling-with-tla/releases/download/v0.1/modeling-with-tla-v0.1.pdf
(the TLA+ specifications and C++ sources are in the repository)
I am interested in any constructive feedback.
Thanks!
--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/646a785a-88eb-46b5-a691-ff9992c3ace1n%40googlegroups.com.--You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/TXK5vZ762vI/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/014501dc2c82%2469f33770%243dd9a650%24%40gmail.com.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/UVEyCLHyWXVXB0klrNd6OfNH3DLwlCqCYloYKHYQ09a1FpTecKui8zXF6BUX0Vhfu3j0WXhy2ZZFoihvNY9DXjK3Porl_NqD4NWKStR9evg%3D%40protonmail.com.
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/TXK5vZ762vI/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CABj%3DxUXhQuKB_KwZYapadnywpgFXPL2vYjCN7d73i9C%3DW9ge5g%40mail.gmail.com.