Hi Kareem,There's a few idiomatic TLA+ tips in the Apalache documentation[1] and in the Learn TLA website[2].The Examples repository[2] on Github contains many advanced examples, including those used in industry.If I understand you correctly, you're looking for something closer to design patterns in TLA+ -- in the sense that it's generic enough to be applicable in many situations? I'm not sure this kind of resource is available.Best,Jones--On Tuesday, 20 September 2022 at 01:06:50 UTC-3 s...@xxxxxxxxxxxxxxxxxxx wrote:I have not seen anything like that however here is a list of repos with TLA proofs used in production systems:On Mon, Sep 19, 2022 at 8:55 PM Kareem Shehata <kar...@xxxxxxxxxx> wrote:Specifying Systems seems like a great guide for how to think in TLA+, but not a catalog of best practices. What I'm really looking for is a set of patterns based on experiences. Yes, I can probably go through all of Specifying Systems and then write my own way of doing semi-synchronous specs, but why not catalog "here's the best way we've found to do this"?Thanks,KareemOn Mon, Sep 19, 2022 at 7:01 AM 'Sam Bacha' via tlaplus <tla...@xxxxxxxxxxxxxxxx> wrote:Specifying Systems, accept no substitute:--On Sun, Sep 18, 2022 at 3:59 PM Kareem Shehata <kar...@xxxxxxxxxx> wrote:Hey everyone!I'm a PhD student studying distributed systems at National University of Singapore and I'm just getting started with TLA+. I was wondering if there was a "cookbook" or any kind of reference for best practices? I've seen plenty of example specs for different systems, but, for example, nothing that explains the right way to set up synchronous message queues or semi-synchronous systems. Other examples: byzantine fault tolerance, digital signatures.Thanks!Kareem--
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/158c7a50-ea83-43c8-b80c-6c88e59f927fn%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/DANnssZ4Fuw/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABNQDasZTNrZH38%3DexFfMoe6OciTheL_cOojowSscKg72S8ykg%40mail.gmail.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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CALaKtAJeaCYvnq-Nff2i31HZn5GSUFFZdXt0%2BFchAYHD72%3DtsA%40mail.gmail.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 on the web visit https://groups.google.com/d/msgid/tlaplus/d004fa4d-f393-4e60-8b04-2430426af50cn%40googlegroups.com.