tlaplus

> it's possible they could be defined over a non-abelian group where this leads to unexpected

Hello Stephan, thanks a lot for your quick answer. I appreciate your patients and time to ramp up

Again, it seems to me that the assumption runningTask # “” can be removed because it is redundant

Thanks again @Stephen for your comprehensive answer. This is much more detailed than I had expected.

The TLA+ Foundation is accepting proposals for grant funding to support projects that advance the

Hello, Regarding point 2 and in particular for the Raft spec. The original spec is just hard to model

Early registration is ending on April 1st so it is good to book within the next few days if you want

Final Call for Papers CONCUR 2025 https://conferences.au.dk/confest2025/concur This is the final CFP

Got it. It worked. Much appreciated On Friday, March 21, 2025 at 11:37:06 AM UTC-4 Hillel Wayne wrote

You're absolutely right. Thank you for pointing that out! I've corrected it, and I was able

Hello! This is mainly a question for Markus Kuppe and Jack Vanlightly, but I'll ask in public for

Yup! Thank you! Works fine Spec == Init /\ [][Next]_vars /\ SF_vars(initial /\ pc'["Job

Thanks for your help! That works! On Tuesday, 18 March 2025 at 03:14:57 UTC+8 Hillel Wayne wrote:

March TLA+ development update: a bad month for tuple-except expressions, another formal methods use

Hello Team, I'm trying to seek help in generating the TLA+ specification for the blockchain. I

We've enabled GitHub Discussions as a place for everyone to propose agenda items in advance of

I touched on this topic in a blog post I wrote a while back called "TLA+ is more than a DSL for

Your specification makes heavy use of recursive operators, which cause TLC to require a large stack

Okay I actually just managed to figure it out approximately one minute after sending this message.

Dear TLA+ community, I have implemented the changes to include model values in transition labels in

Hi, I took a close look at FixedPointMult.tla, and it looks like you have indeed discovered a bug in

Done: https://github.com/hwayne/learntla-v2/issues/91 On Tuesday, 11 February 2025 at 17:42:10 UTC+1

For anyone who has interest in this I added answer here: https://www.reddit.com/r/compsci/comments/

Hello Mamoun, just to clarify the context of your question: you refer to the TLA+ Proof System: TLC

Just installed it yesterday. You need to have Rosetta installed - to support the current x86-64 build

Thanks, Hillel, for the feedback! I appreciate it. I didn't include PRISM examples directly in

I have the commands in emacs lisp and would like to see how one might typically write them in TLA+.

Hi everyone, we are moving the monthly TLA+ Community calls from Microsoft Teams to Zoom. You can

Hey. When running -simulate with default -depth 100 on single core mean length is 100 as expected (I

One alternative way of thinking about it is that scope/contexts aren't real, only things