tlaplus

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

The program is online at https://conf.tlapl.us/2025-etaps/. Participants will be required to register

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

2nd Call for Papers CONCUR 2025 https://conferences.au.dk/confest2025/concur CONCUR 2025 is the 36th

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

Thank you. Do you know if there is a downloadable copy of video6v2.mp4? I couldn't find it in the

Hi Karolis, I don't know if there is an answer to your question because I wouldn't know how

We could do that; github only allows the latest release to be a full release, not a pre-release,

CONFEST 2025 - Call for Workshops https://conferences.au.dk/confest2025 CONFEST 2025 will be held in

We were able to find a minimal example demonstrating the differences: ---- MODULE testgenerate ----

Hi Andrew, the problem is certainly decidable for finite-state systems. In automata-theoretic terms,