tlaplus

Consider the following spec of a tree (extremely simplified, with only two possible node values):

Section 16.2.4 gives a syntactic definition of a valid TLA formula, which is defined inductively from

The program of TLA+ Conf is now up at http://conf.tlapl.us/2021/ Markus

Oh, I see. Thank you, Markus On Thursday, July 15, 2021 at 6:05:04 PM UTC+3 Markus Alexander Kuppe

Consider A == x /\ x' = FALSE B == ~x /\ x' = TRUE Then ENABLED A <=> ~(ENABLED B). H

I feel like the programmer in me understood fairness a lot better when I learned how liveness is

Sweet. Works like a charm. And page numbers fixed too! Now if only we could click and goto the page

So turns out the US holiday weekend made the deadline tricky for some people, so we're extending

On Jun 30, 2021, 11:23 AM -0700, Markus Kuppe <tlaplus-google-group@lemmster.de>, wrote: On 6/

Ah that makes perfect sense! I ended expanded the definition according to Specifying Systems (\A n \

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