[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. |