Details
-
New Feature
-
Resolution: Won't Fix
-
Major - P3
-
None
-
None
-
None
Description
I updated RaftMongo.tla in SERVER-44458 to include a LearnTermViaHeartbeat action. This is necessary to bring the spec close enough to the implementation for trace checking to succeed. The action represents a node "i" processing heartbeat metadata from node "j" and updating its view of the current term. Add trace logging somewhere around ReplicationCoordinatorImpl::processReplSetMetadata for this action.