[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] TLA+ / PlusCalc Cookbook ?



Hi Kareem,

I found some useful patterns in the book "specifiying systems" by Leslie Lamport.
You can downolad it here https://www.microsoft.com/en-us/research/publication/specifying-systems-the-tla-language-and-tools-for-hardware-and-software-engineers/

A lot of examples are also here: https://github.com/tlaplus/Examples
You may also look at different branches of the git, especially when it comes to liveness proofs.

Patterns from TLAPS are here:
https://members.loria.fr/SMerz/talks/argentina2005/MerzTLA+Logic.pdf
With references to more.

Kind regards
Andreas

hwa...@xxxxxxxxx schrieb am Mittwoch, 21. September 2022 um 04:54:00 UTC+2:
I've been working on it for learntla, but it's gonna be a while before most of the patterns I know are up. Here's what I have so far: https://learntla.com/topics/index.html

On Tue, Sep 20, 2022 at 7:08 PM Jones Martins <jone...@xxxxxxxxx> wrote:
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

[1]: https://apalache.informal.systems/docs/idiomatic/index.html
[2]: https://learntla.com/topics/tips.html
[3]: https://github.com/tlaplus/Examples

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,

Kareem


On 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.

--
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.

--
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/36fb032b-ab32-42a3-a571-e740bca6d921n%40googlegroups.com.