|
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: tlaplus@xxxxxxxxxxxxxxxx <tlaplus@xxxxxxxxxxxxxxxx> on behalf of sadjad tala <sadjadtalakoob74@xxxxxxxxx>
Sent: 30 September 2020 11:15 To: tlaplus <tlaplus@xxxxxxxxxxxxxxxx> Subject: [tlaplus] Raft Spec Checking problem 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.
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/ba3fac42-9887-4223-8349-15d338a66281n%40googlegroups.com. 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/DM6PR05MB4106B17F25A0AE5491782A52D7330%40DM6PR05MB4106.namprd05.prod.outlook.com. |