Re: [tlaplus] TLA+ / PlusCalc Cookbook ?

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,

Kareem

On Mon, Sep 19, 2022 at 7:01 AM 'Sam Bacha' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:

Specifying Systems, accept no substitute:

https://lamport.azurewebsites.net/tla/book-02-08-08.pdf

On Sun, Sep 18, 2022 at 3:59 PM Kareem Shehata <kareem@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+unsubscribe@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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABNQDasZTNrZH38%3DexFfMoe6OciTheL_cOojowSscKg72S8ykg%40mail.gmail.com.