[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: |
|
||||||||||||
| 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. |