Raft Spec Checking problem

[sadjad tala]

Hello, 

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. 

[Jack Vanlightly]

Hi,

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.

Jack

---

From: tla...@googlegroups.com <tla...@googlegroups.com> on behalf of sadjad tala <sadjadta...@gmail.com>
Sent: 30 September 2020 11:15
To: tlaplus <tla...@googlegroups.com>
Subject: [tlaplus] Raft Spec Checking problem

 

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ba3fac42-9887-4223-8349-15d338a66281n%40googlegroups.com.

[sadjad tala]

i'll check that too, thanks