tlaplus

Can we tweak it so the main page shows it as the latest release? Currently, it still shows an old

Hi all, Recently, I tried to extract some parts of my proofs on relations to a separate module and

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

Hello all, As part of work funded by the TLA+ Foundation I have written up a newsletter on various

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

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

Following the long discussion at the last community meeting about unifying the TLA+ parsers I opened

Hi Anthony, The specification [2] that you pointed to is an extension of [1], which enumerates

Hi Abhishek, Yes, that's the bug in the spec that made TLC runs into stuttering state. Thanks.

Thanks Igor; I'm interested in these temporal properties that must be treated differently in

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

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