[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Ā SERVER-44458 andĀ SERVER-44340. They represent divergent branches of development from an earlier RaftMongo.tla. Let's determine whether to merge them, factor out a common TLA+ module they share, or something else.



 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.

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