tlaplus

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

You can get distinct state counts with a JVM system property and a small amount of TLA+. Step 1:

Hello Pierre-Louis, thanks for sharing the spec, here are a few comments: - The operators ValidPath

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

Hi all, I've implemented a feature in TLC to accept an EXPECT statement in model files. This lets

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

After checking in with the actual experts, I realized there's a different link to share re: TLA+

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

Thanks, Stephan! Wow, after all these years parsing TLA+ I am still learning about new corners of the

The list of presentations accepted for the Community Meeting is now online at https://conf.tlapl.us/

It is really cool when you demo'd it to us during the outreach meeting. It is even accessible on

My question was not clear. Suppose one is writing a user or technical guide for TLA. For absolute

Hi Hank Wang, You can find the TLA+ specifications from the book in the examples repository [1]. The

Now that I'm more familiar with how SANY works I might be able to answer this in greater detail.

Hi everyone, we'd like to invite the TLA+ community to check out and contribute to a new

For a discussion about functions vs. operators, see section 6.4 of Specifying Systems. As I should

Thank you very much, Stephan, Indeed it looks like I was thinking too much like a programmer, your