Details
-
Bug
-
Resolution: Fixed
-
Major - P3
-
None
-
None
-
None
-
Fully Compatible
-
ALL
-
Execution EMEA Team 2023-06-26
-
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.