BinyuHuang-nju commented on pull request #1690: URL: https://github.com/apache/zookeeper/pull/1690#issuecomment-832752514
@Vanlightly Hi! Since I previously thought that infinite state space is normal, I didn't pay much attention to how to constrain state space. Thanks for your reminder, I think I can modify spec ZabWithQTest.tla, to try to let models be run completely. I added global variables electionNum, totalRestartNum to restrain state space and try to run models to completion. I let electionNum < MaxElectionNum in Election, let totalRestartNum < MaxTotalRestartNum in Restart and RecoveryAfterRestart, and let Len(history[i]) < MaxTransactionNum in ClientRequest. When I set 2 servers, MaxElectionNum = 2, MaxTotalRestartNum = 3, MaxTransactionNum = 2, the model was run completely in 1 minute, and reached a diameter of 47 with 2518479 states. In this case, it is normal that actions involving election and restart and some low-probability actions such as BecomeFollower will not be traversed. So this time We may be able to run the model completely when the scale is not very large. I will try this way with bigger values like 3 servers, and tell you results tomorrow if it can be run completely. And I will push new spec here immediately. But, in principle state space is infinite in this spec using model checking. This way in spec makes my verification more like a testing, not model checking. I think it is a trade-off between verification of Zab correctness and model checking. -- 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]
