tlaplus

Hi Ugur, thanks for your feedback. I have seen similar problems when checking long proofs in a single

Hi TLC usually computes the initial-state of a spec while performing model checking. Is it possible

In TLA+, the refinement that you want to prove is stated as RefinedSpec => \EE pc : GeneralSpec

My mistake! I thought the total number of states could be affected by thread interleaving in parallel

Note that it appears the num=X parameter is multiplied by the number of workers On Saturday, January

I tried to investigate this a little further and ended up writing a blog post. I'm sure I got

I see. I suggest you take a look at the chapter 5 in Leslie's book Specifying Systems, particular

We have already received a number of contributions to the Community Meeting, but a few more would be

After reading the Knuth-Yao spec that Ron Pressler & Markus Kuppe wrote (https://github.com/

On 1/19/23 7:32 AM, Andrew Helwer wrote: > This makes specs here considerably harder to read and

Yes sorry for some reason all the formatting was removed after I posted it and despite multiple

es sorry for some reason all the formatting was removed after I posted it. And the displayed post

Ah, cracked open specifying systems - so you can only have [][A]_v or <><<A>>_v

Hello, the first problem that I have with this module is that it instantiates module Consensus, which

This one works, thanks! M. Dátum: nedeľa 15. januára 2023, čas: 20:02:51 UTC+1, odosielateľ: Markus

Thanks a lot! El viernes, 13 de enero de 2023 a las 14:18:34 UTC+1, andrew...@gmail.com escribió:

Thank you very much,I'll try it now. :) 在2023年1月13日星期五 UTC+8 21:55:19<Stephan Merz> 写道： The

Besides the fingerprint set, TLC stores a state queue, a trace, and the liveness graph on disk, and,

I wrote a long blog post about my experience writing the tree-sitter grammar; it overlaps a fair bit

Got it, thanks! On Thursday, January 12, 2023 at 1:03:32 AM UTC-8 Stephan Merz wrote: TLC cannot

I read from **Specifying Systems** that: >> In the actual implementation, the nodes of the

Meeting Minutes January 10, 2023 Participants • Mamoun Filali • Martin Hornacek • Igor Konnov •

It's hard to say what a formal spec for a parser would even look like, other than an EBNF grammar

I'd read it as "WF sub count Tick". Also, if you really want to allow for these

Hi, When a model checker is run with the tla+ toolbox, it lists the number of states explored, and if

External link below since it's a little bit long: https://stackoverflow.com/questions/74912408/

Yes,that's exactly what I want,thank you. 在2022年12月22日星期四 UTC+8 23:57:08<Stephan Merz> 写道：

Thank you Markus. Your link led me to the solution written in Caveats Section. The picture attached:

Hello, a few quick comments on your spec: - all actions should determine the values of all state

with m = [t |-> "PROPOSE", v |-> input] do msgs := [p \in peers |-> msgs[p] \cup {