[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: SERVER-81460 Add new TLA+ spec for Raft with timestamp
Branch: master
https://github.com/mongodb/mongo/commit/3f978bb7298a6f692a3198a5ce1c4a9d58f4753b

Generated at Thu Feb 08 06:46:34 UTC 2024 using Jira 9.7.1#970001-sha1:2222b88b221c4928ef0de3161136cc90c8356a66.