tlaplus

Perhaps the confusion is related to what TLC considers to be a stuttering step and what it considers

Thanks Calvin, I've updated the wiki's settings to disable the entity rewriting. Please let

Bisecting identified the breaking commit, which occurred in August 2021. I opened this issue in the

https://github.com/tlaplus/tlaplus/issues/272 On Monday, October 7, 2024 at 2:18:11 PM UTC-7 andrew..

My workaround is to fork a nested TLC for each configuration value from an outer “config spec".

That worked. Thanks! On Sun, Sep 29, 2024 at 9:49 PM Markus Kuppe <tlaplus-google-group@lemmster.

I wrote a blog post about how TLA⁺ is more than a DSL for breadth-first search - two other ways of

Currently nobody is really working on maintaining the toolbox GUI so if you would like it to work on

Hi Lucas, I've been using TLA+ for specifying front-end development on a couple projects now. I

> Another possible candidate for removal is the notation for binary, octal, and hexadecimal

<<A>>_v isn't a temporal formula (it's an action), but by page 91, ◇<<A>

Stephan, Yes, based on the thread here (https://github.com/tlaplus/tlaplus/issues/998) it is now

Hi, I am trying to port some of my TLA+ spec from Toolbox to VScode with TLA+ nightly plugin. When I

The base algorithm is described in the book "Temporal Verification of Reactive Systems” by Zohar

Thank you Stephan for your response. Le dimanche 4 août 2024 à 08:53:10 UTC+2, Stephan Merz a écrit :

> I'm still a bit puzzled as to why TLC hangs TLC does not memoize functions the way you might

The main code block of an algorithm must appear inside braces. See the PlusCal grammar in the manual

A preliminary program for the meeting is now online at https://conf.tlapl.us/2024-fm/, subject to

The link works now. aman On Thursday, July 18, 2024 at 9:28:31 PM UTC-4 Leslie Lamport wrote:

In your lemma, IdxSet is indeed under a quantifier and thus a constant, so your lemma is true. But in

Should TLC be able to check such a property? I suspect that the error is that TLC should report that

Note that TLC's simulation mode also supports the `-continue` parameter, which causes the

If anybody is looking for a fun project, there was recently a fairly severe bug in OpenSSH caused by

Hello to all, I am student of PhD in Pakistan. I have proposed the following algorithm to check pH at

Hi All, As part of my TLA+ learning, I wrote a spec for a Leetcode problem (https://leetcode.com/

Thanks for the tip Finn, i now better understand the approach. Cheers! /Lee On Thu, 20 Jun 2024, 23:

Hello Jack, You mentioned above that you worked with the new Kafka consumer group protocol from KIP

Hi Leslie, I'd like to provide a suggestion of including some of the concepts of your "

Wrote about it here: https://www.hillelwayne.com/post/composing-tla/. Thanks to Murat and Andrew for

Dear Leslie, Thank you for your feedback. Looks like their comparison is unfortunately missleading