[SERVER-45490] Internal retrospective on TLA+ Trace Checker paper Created: 10/Jan/20  Updated: 06/Dec/22  Resolved: 21/Feb/20

Status: Closed
Project: Core Server
Component/s: Replication
Affects Version/s: None
Fix Version/s: None

Type: Task Priority: Major - P3
Reporter: A. Jesse Jiryu Davis Assignee: Backlog - Replication Team
Resolution: Won't Do Votes: 0
Labels: None
Remaining Estimate: Not Specified
Time Spent: Not Specified
Original Estimate: Not Specified

Assigned Teams:
Replication
Participants:

 Description   

The public research paper will describe why we found model-based trace-checking impractical for RaftMongo.tla. Let's complement it with an internal retrospective on what we gained and spent on this project, and analyze the decision-making process that led us to start a research project that we had to abandon.



 Comments   
Comment by Judah Schvimer [ 21/Feb/20 ]

Contents of the paper cover everything we would want to say.

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