BinyuHuang-nju edited a comment on pull request #1690: URL: https://github.com/apache/zookeeper/pull/1690#issuecomment-832510959
@Vanlightly Sorry, I didn't make it clear that I didn't do complete running. Actually, It is almost impossible to traverse all states due to state space explosion, and this is a disadvantage of "model checking". So it is very normal when you see the model cannot stop. We can assume situations when a server halts and restarts for multiple times, or re-elect a leader for multiple times but not increase epoch because the last round of elections ended before the prospective leader broadcasts NEWEPOCH. So in principle, there are infinite large state spaces when running models. On the other hand, there are a lot of repetitive actions like restart, re-election happen continuously, which make state space expand rapidly. And the experience imparted to me by the senior’s work like Parallel Raft, TPaxos shows that it is quite normal that models cannot be run completely. So in actual, I run it for a long time to judge whether there's invariant violation or not. Also, I have run models with excluding the restart situation(modify "currentEpoch[i] < 0" in Restart and RecoveryAfterRestart), and the result will produce a lot of actions we care more about. Until now, the results appears good. I think you could have a try if you have enough time. -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. For queries about this service, please contact Infrastructure at: [email protected]
