tlaplus

As stated in the other thread, TLAPM does not yet support checking proofs involving real numbers.

If you're using this for writing proofs over it, you'll probably make the function a constant

I've been thinking about this a little more. For arbitrary actions A and B, we also have (see

Thanks Stephan! Ach of course, I thought it was some transformation involving the ¬ but in fact it

I'm exploring formal methods for verifying a data ingestion pipeline. I'm particularly

It's hard to make general models of this sort to build on top of because what you actually care

The book A Science of Concurrent Programs will be published by Cambridge University Press. A copy of

Hi, please note the recent and ongoing discussion related to the approach in this Github PR: https://

I don't care about the probabilities, I just want to express that false positives are possible to

It is not the only way. There is the age-old design decision analogous to the choice between an array

I think it would be quite confusing to say that REACHABLE specifies an invariant. Indeed, one can

I actually just found out about this parser the other day after Chris Newcombe mentioned it. Is it

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