tlaplus

Not to say that this behavior is up to spec, but TLC is quite happy to evaluate expressions like 1 \

On 7/26/21 4:31 AM, Andrew Helwer wrote: > However this then caused TLC to output a novel (to me)

Tried to check this proof as well. But I'm getting the following error when using tlapm from the

If you're mechanically translating policy lists to TLA+ to check them, it might not be the most

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