[SERVER-45415] Factor RaftMongo.tla with MongoReplReconfig.tla Created: 08/Jan/20  Updated: 06/Dec/22

Status: Backlog
Project: Core Server
Component/s: Replication
Affects Version/s: None
Fix Version/s: None

Type: Improvement Priority: Major - P3
Reporter: A. Jesse Jiryu Davis Assignee: Backlog - Replication Team
Resolution: Unresolved Votes: 0
Labels: former-quick-wins
Remaining Estimate: Not Specified
Time Spent: Not Specified
Original Estimate: Not Specified

Issue Links:
Depends
depends on SERVER-44458 Productionize RaftMongo TLA+ spec Closed
depends on SERVER-44851 Update TLA+ model of heartbeat safe r... Closed
Assigned Teams:
Replication
Participants:

 Description   

These two TLA+ specs are actively developed, they are both adapted from siyuan.zhou's original RaftMongo.tla in his personal repository. They have divergent copies of many shared chunks of TLA+ code. Although Leslie Lamport advises against factoring TLA+, we should consider it.


Generated at Thu Feb 08 05:08:43 UTC 2024 using Jira 9.7.1#970001-sha1:2222b88b221c4928ef0de3161136cc90c8356a66.