tla+ specification of raft study

[qujihan]

Regarding the several files in the tla/consensus directory, can anyone explain the difference? If I want to learn how the tla+ of raft is implemented, which file is better?

[lemmy]

ccfraft.tla is the main specification.

[achamayou]

@qujihan

MCccfraft and MCccfraftAtomicReconfig and MCccfraftWithReconfig are Model Checking ccfraft.tla with slightly different space constraints.

SIMccfraft runs TLC on ccfraft.tla in simulation model, stochastically exploring the state space.

Traceccfraft validates traces produced by the implementation against ccfraft.tla.

[qujihan]

Thank you very much for your answer. I also want to ask a question. I saw that 500+G disk space is required under the issue of ongardie. I would like to ask, if I run it, how much disk space will it occupy?