[SERVER-43588] Select and update TLA+ specs for trace checking Created: 24/Sep/19 Updated: 29/Oct/23 Resolved: 13/Jan/20 |
|
| Status: | Closed |
| Project: | Core Server |
| Component/s: | Replication |
| Affects Version/s: | None |
| Fix Version/s: | 4.3.3 |
| Type: | New Feature | Priority: | Major - P3 |
| Reporter: | A. Jesse Jiryu Davis | Assignee: | A. Jesse Jiryu Davis |
| Resolution: | Fixed | Votes: | 0 |
| Labels: | None | ||
| Remaining Estimate: | Not Specified | ||
| Time Spent: | Not Specified | ||
| Original Estimate: | Not Specified | ||
| Issue Links: |
|
||||||||
| Backwards Compatibility: | Fully Compatible | ||||||||
| Participants: | |||||||||
| Description |
|
Among TLA+ specs that the Replication Team has already written, select some to test against our actual implementation. Selection criteria:
See a list of possible specs (not exhaustive) in the Scope doc for this project. |
| Comments |
| Comment by A. Jesse Jiryu Davis [ 13/Jan/20 ] |
|
We selected RaftMongo only, see |