tlaplus

Thank you, Leslie! That is helpful On Thursday, June 24, 2021 at 8:28:20 PM UTC+3 Leslie Lamport

On 18.06.21 19:47, migu...@ciencias.unam.mx wrote: > > Hello all! > I'm getting back

One interesting thing Leslie talks about a lot in Real Time (and somewhat mentioned in the other

A friendly reminder that the CfP for the TLA+ conference ends in 14 days on July 1st. Please send

Is correctReceive ever enabled in the counter-example? The await condition in receiveData clearly

In your Init formula, constrain the initial state of variables representing the configuration to only

Hunnn, thanks, Markus o/ Everyday is day to learn something about TLC. On Thu, Jun 10, 2021, 1:32 AM

yeah. I just realized that ALWAYS actually has the same MANY as "Infinitely Many/Often" On

I don't know if people realize that TLC can handle: VARIABLES x, y, a, b, c foo == <<x, y

Trivial answer: TLAPS can prove TRUE /\ Next => TRUE' for any formula Next. More seriously, I

Awesome. Yeah. The reason why I sent to our group is: I am not confident enough about my

On 04.06.21 23:40, Jinkun Geng wrote: > I am running tlc2.TLC in command line, on a 64-core Linux

Very encouraging. When I was a PhD student, it was Lamport's paper(The Clock One) that

Thanks a lot guys! For someone who interested here is the complete spec that verifies successor

Process algebras have non-observable (\tau) actions that are discarded by weak bisimulation etc.,

I misspoke: even the implication [](\E x : F) => \EE x : []F is not valid in general, but it is

Thanks a lot! воскресенье, 30 мая 2021 г. в 16:26:29 UTC+3, Afonso Fernandes: Hello, There is a tool

Hey Jefferson, You're very welcome! I'm glad you got things working properly. Best, Isaac On

Oh thanks! It really helps. Now the only issue is Java heap out of memory, maybe I should decrease

en. Our TLC is not a gcc *compiler*. So, it is our responsibility to make sure any WF or/and SF

On 18.05.21 10:34, Markus Kuppe wrote: > Can you please open an issue as a place to discuss

Trying to wrap my head around how exactly this subexpression works. From page 14 of the TLA+ 2

Hi! Have you looked at page 6 in https://lamport.azurewebsites.net/tla/summary.pdf? Karolis On Sun,

Thanks Andrew, interesting post! Karolis On Wed, May 5, 2021 at 10:09 PM Andrew Helwer <andrew.

Ah, I see my mistake. I was assuming that simple temporal formulas included invariants, which it

Hello, TLC will be able to handle your second spec if you restrict the choice of y' to a finite

Here is some documentation for the SANY stand-alone parser: The switches for the sany parser are: -s

Thanks again! I'm afraid that my learning style is to dive straight in and ask questions when I

On 27.04.21 23:49, myzh...@gmail.com wrote: > The attachment is too large (TE.tla, 2.1M and MC_TE.

Hello, Good question. I assumed that was one of the points of providing the seed and fp, but never