tlaplus

In https://lamport.azurewebsites.net/pubs/lamport-actions.pdf, Figure 5 mentions various rules of

Please check the definition of SameDiagonal. Diagonals lie on x+y = constant and xy = constant. -

Hi Anthony, Apalache's support for liveness is still experimental. There were not many people who

ABZ 2025, the 11th International Conference on Rigorous State Based Methods will be organized at the

A TLA+ Community Meeting will be organized as a satellite of ETAPS 2025 (https://www.etaps.org/2025/)

Hello all, If you have some spare cycles for non-code pull request reviewing I would love to get some

Stephan, About the comment Steps <1>1 and <1>2 appear to be definitions (in particular

I will add a note that I read further into the book and on page 109 it expands the proof a bit.

I currently want to define the Fourier Transform on a stochastic generated seismogram h(t). That is,

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

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>