tlaplus

Thank you to all who responded with your feedback. I somewhat arduously added unit tests for the

Hi Shane, Thank you for your response! If I have a correct understanding: BFS construction and

This is a quick note that the examples in: https://github.com/gshanemiller/tla-examples together with

The next Outreach Committee meeting [1] will take place tomorrow, May 19, at 8:00 AM Pacific Time.

There is also this somewhat classic blog post about package manager design, which is now old enough

It was a while ago, but I did read through it, and I thought it was worth it. One thing I took away

Hi all, Our monthly TLA+ Community Call is happening now. Please join us at https://zoom-lfx.platform

The videos of the presentations at the meeting in Torino are now online at https://www.youtube.com/

An interesting reference what others are discussing : https://github.com/rust-lang/leadership-council

Unless you want TLC!RandomElement to bias successor selection with a custom (rational) distribution,

You can post these questions to this mailing list. Andrew On Fri, May 1, 2026 at 11:31 AM 'TT

Links are stale (and [3] not even cited in the text), may you relink the insights? Chris Newcombe

Hi Stephan, Thanks again for your feedback and comments! Apologies for the delayed response. I wanted

Hi Petru, thank you for sharing, this is very interesting. I'd like to read your write-up

I'd love to, but I'm not sure how much time I can dedicate to it right now. I'm currently

I have something to contribute to the implementation question. I have done some experimentation with

There are no real differences between P and C PlusCal except for the start/end block syntax. I

Mr. Suckrow, Consider reading the pdf in https://github.com/gshanemiller/tla-examples. The RPC

Ah that is a good spot, I will have to update the XML Exporter documentation. Thanks! Andrew On Mon,

I managed to find my Network module prototype. It lives in the commit at the head of this branch,

Hi all, I wanted to share a small repo I've been working on: https://github.com/younes-io/agent-

That clears it up. Thank you Stephan On Sunday, March 29, 2026 at 8:54:08 AM UTC+2 Stephan Merz wrote

Andrew, Murat: Gents, thank you again for offering to review paper. Just to remind: https://github.

https://lamport.azurewebsites.net/tla/learning.html https://learntla.com/ Andrew On Fri, Mar 20, 2026

Hi Marta, If you'd like, we can set up a video call to chat about your interest in TLA+ and what

Using TLA+ to Fix a Very Difficult glibc Bug - Malte Skarupke - C++Now 2025 The glibc condition

Hi Filip, I am very glad to hear that. I am looking forward to your email and to collaborate with you

Thanks Markus. I reviewed the link and that is actually a cool feature and I would like to try it out

> I don't recall if you can put a `goto` inside a macro, Unfortunately you can't.

I agree with Hillel on the answer to the first question. I also agree on his second answer. Just to