-
Type: Improvement
-
Resolution: Unresolved
-
Priority: Major - P3
-
None
-
Affects Version/s: None
-
Component/s: Replication
-
Replication
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.
- depends on
-
SERVER-44458 Productionize RaftMongo TLA+ spec
- Closed
-
SERVER-44851 Update TLA+ model of heartbeat safe reconfig
- Closed