[SERVER-78205] Remove TLA invariant for PriorityTicketHolder Created: 19/Jun/23  Updated: 29/Oct/23  Resolved: 20/Jun/23

Status: Closed
Project: Core Server
Component/s: None
Affects Version/s: None
Fix Version/s: 7.1.0-rc0

Type: Bug Priority: Major - P3
Reporter: Jordi Olivares Provencio Assignee: Jordi Olivares Provencio
Resolution: Fixed Votes: 0
Labels: None
Remaining Estimate: Not Specified
Time Spent: Not Specified
Original Estimate: Not Specified

Issue Links:
Depends
Backwards Compatibility: Fully Compatible
Operating System: ALL
Sprint: Execution EMEA Team 2023-06-26
Participants:
Linked BF Score: 20

 Description   

SERVER-74778 refactored the PriorityTicketHolder and as a result modified the TLA+ model. It removed one invariant but forgot to modify the configuration file. This is now causing the TLA+ model verification to fail.



 Comments   
Comment by Githook User [ 19/Jun/23 ]

Author:

{'name': 'Jordi Olivares Provencio', 'email': 'jordi.olivares-provencio@mongodb.com', 'username': 'jordiolivares'}

Message: SERVER-78205 Remove invariant from TLA model config for PriorityTicketHolder
Branch: master
https://github.com/mongodb/mongo/commit/9296d5c2366768f493048967e9341f6cce2653f4

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