tlaplus

On 29 Sep 2022, at 11:16 pm, Gareth Smith <anythingwithawire@gmail.com> wrote: > I haven

Its difficult to see what's going on in this example. Can you reduce it to a smaller example that

Hello Andreas, apologies for the late reply. In response to your original question, TLAPS is not

Thanks, done. That was my instinct but I got the impression from the readme on GH that I should start

Usually in the config, you specify the specification to check using the SPECIFICATION statement.

Good catch. That did fix the problem. Thanks a lot. aman On Thursday, September 22, 2022 at 2:38:08

Hi Kareem, I found some useful patterns in the book "specifiying systems" by Leslie Lamport

Dear inevity, what primarily proposed was to look what the PlusCal transpiler makes from your code.

You might find inspiration on how to model various consistency levels The cosmos db specs is just for

Thank you very much for your prompt reply. On Thu, 1 Sep 2022, 18:05 Stephan Merz, <stephan.merz@

Yes I'm sorry I knew that, I'm embarrassed to see that I wrote that. I need to check what I

Is this conference ever held in some city other than St Louis? And is it possible to virtually attend

Cool! Thanks On Monday, 29 August 2022 at 19:11:22 UTC+5:30 isaacd...@gmail.com wrote: Hello Anand,

Ok - I just found the errata sheet and it already mentions that correction. Sorry for the noise. On

I am implementing the Raft protocol in Rust, reading the specification given by the original author.

In formulas Q x \in S : F (where Q is either \A or \E), S has to be a set. See also section 1.3 of

Hello, I am new to TLA+/TLC and I am trying the HourClock example from Leslie Lamport's

Oops, what a silly thing. my bad. On Friday, 12 August 2022 at 12:10:59 UTC+5:30 Stephan Merz wrote:

Arrghhh ... I checked, my OCaml version is called "4.11.1+default-unsafe-string" [1], and I

Oh, thank you, I'm definitely looking forwad to trying Apalache. (As a personal bonus, I

Thank you, Hillel. This clarifies it for me. Thank you all for the help! Timi On Wednesday, 3 August

Haha, sorry for the lack of context in that statement - I should have said "use for infinite

Typo on my part; apologies. It is now working. Sean > On Jul 18, 2022, at 1:24 PM, Sean Peisert

In order to add to Andrew's reply: the ENABLED operator does not refer to any specification S,

The bogus error message has been corrected as part of https://github.com/tlaplus/tlaplus/issues/742

The parser update has been rolled out (modulo some frontend caching) and you should be able to see

Hi Leo, at this point, we do not have an End-Of-Life policy. However, the TLA+ tools are open-source

Should be noted that TLC doesn't support variable hiding in that way, so if you're only

In case anyone else reads this thread, the closest thing to memoization while model checking is the

No, partial order reduction is currently not implemented for TLC, but it could be an interesting