There's a typo in the TLA+ spec for applying oplog entries independently from making them durable:
Restart(i) ==
/\ state' = [state EXCEPT ![i] = "Follwer"]
...
If restarting a node changes its state to "Follwer", that disables actions which check if its state is "Follower", which means model-checking isn't verifying what we want.
Also, model-checking could be much faster if you add Symmetry == Permutations(Server) to MCRaftMongoReplTimestamp.tla and add SYMMETRY Symmetry to MCRaftMongoReplTimestamp.cfg
- is caused by
-
SERVER-81460 Write TLA+ spec to verify the new design
- Closed