[SERVER-45157] Factor or reconcile RaftMongo.tla and RaftMongoWithRaftReconfig.tla Created: 14/Dec/19 Updated: 16/Dec/19 Resolved: 16/Dec/19 |
|
| Status: | Closed |
| 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: | A. Jesse Jiryu Davis |
| Resolution: | Won't Fix | Votes: | 0 |
| Labels: | None | ||
| Remaining Estimate: | Not Specified | ||
| Time Spent: | Not Specified | ||
| Original Estimate: | Not Specified | ||
| Participants: |
| Description |
|
We've imported two versions of RaftMongo.tla forĀ |
| Comments |
| Comment by A. Jesse Jiryu Davis [ 16/Dec/19 ] |
|
I misunderstood. RaftMongoWithRaftReconfig.tla is a historical artifact of an abandoned version of the Safe Reconfig protocol. It won't be trace-checked and it won't be further developed, so there's no need to factor it with RaftMongo.tla, which is a living document that will be continuously trace-checked. |