tlaplus

Yes, TLC always prints an estimate of the probability of hash collisions. If that estimate is high

I have realized that defining axioms with equivalence provides both axioms for a logic as well as

April 2025 update: creator of P specification language joins the board, a new TLA+ parser written in

For anyone else with the same questions, these guys did a machine checked proof of Vertical Paxos in

> 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

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:

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