[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Raft Spec Checking problem
i'll check that too, thanks
On Wednesday, September 30, 2020 at 1:28:54 PM UTC+3:30 Jack Vanlightly wrote:
If I remember correctly, the message sending in that spec is a bit broken. It uses a function for the messages with message -> counter. Sending increments the counter and receiving should decrement the counter, but there are no checks on the value of the counter,
meaning that a message can be received infinitely and the counter go negative.
That might cause excess running time. I would fix that issue and see if it helps.
I run the raft protocol specification from Diego Ongaro's Ph.D. dissertation. Now I use a server and run thread on 6 core with 25Gb ram. After 3 hours, it still keeps running.
How can I estimate how long will it take for a complex spec. is there any Variants or Liveness property that may help? does anyone got any suggestion?
Thanks a lot.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/cc9efe5b-a535-497e-87e0-7ab49c6b9152n%40googlegroups.com.