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...@xxxxxxxxxxxxxxxx <tla...@xxxxxxxxxxxxxxxx> on behalf of sadjad tala <sadjadta...@xxxxxxxxx>
Sent: 30 September 2020 11:15
To: tlaplus <tla...@xxxxxxxxxxxxxxxx>
Subject: [tlaplus] Raft Spec Checking problemHello,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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ba3fac42-9887-4223-8349-15d338a66281n%40googlegroups.com.