[SERVER-81460] Write TLA+ spec to verify the new design Created: 26/Sep/23 Updated: 09/Nov/23 Resolved: 09/Nov/23 |
|
| Status: | Closed |
| Project: | Core Server |
| Component/s: | None |
| Affects Version/s: | None |
| Fix Version/s: | 7.3.0-rc0 |
| Type: | Task | Priority: | Major - P3 |
| Reporter: | Wenbin Zhu | Assignee: | Jiawei Yang |
| Resolution: | Fixed | Votes: | 0 |
| Labels: | None | ||
| Remaining Estimate: | Not Specified | ||
| Time Spent: | Not Specified | ||
| Original Estimate: | Not Specified | ||
| Assigned Teams: |
Replication
|
| Backwards Compatibility: | Fully Compatible |
| Sprint: | Repl 2023-10-02, Repl 2023-10-16, Repl 2023-10-30, Repl 2023-11-13 |
| Participants: |
| Description |
|
We should first investigate the current TLA+ specs and figure out what invariants we need to update and what new invariants we want to add. |
| Comments |
| Comment by Githook User [ 09/Nov/23 ] |
|
Author: {'name': 'Jiawei Yang', 'email': 'jiawei.yang@mongodb.com', 'username': 'YoungYang0820'}Message: |