TLA+ / PlusCalc Cookbook ?

[Kareem Shehata]

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

[Sam Bacha]

Specifying Systems, accept no substitute:

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

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/158c7a50-ea83-43c8-b80c-6c88e59f927fn%40googlegroups.com.

[Kareem Shehata]

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

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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABNQDasZTNrZH38%3DexFfMoe6OciTheL_cOojowSscKg72S8ykg%40mail.gmail.com.

[Sam Bacha]

I have not seen anything like that however here is a list of repos with TLA proofs used in production systems:

https://github.com/sambacha?tab=repositories&q=Tla&type=&language=&sort=

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CALaKtAJeaCYvnq-Nff2i31HZn5GSUFFZdXt0%2BFchAYHD72%3DtsA%40mail.gmail.com.

[Jones Martins]

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

[Hillel Wayne]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d004fa4d-f393-4e60-8b04-2430426af50cn%40googlegroups.com.

[Andreas Recke]

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