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.