[SERVER-45416] TLA+ specs are not continuously tested Created: 08/Jan/20  Updated: 29/Oct/23  Resolved: 06/Apr/20

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

Type: New Feature Priority: Major - P3
Reporter: A. Jesse Jiryu Davis Assignee: A. Jesse Jiryu Davis
Resolution: Fixed Votes: 0
Labels: None
Remaining Estimate: Not Specified
Time Spent: Not Specified
Original Estimate: Not Specified

Issue Links:
Problem/Incident
causes SERVER-47503 Invalid batchtime setting on tla_plus... Closed
Related
related to SERVER-46789 Make TLC wrapper script cross-platform Closed
related to SERVER-48226 Improve TLA+ CI Closed
Backwards Compatibility: Fully Compatible
Sprint: Repl 2020-02-10, Repl 2020-03-23, Repl 2020-04-06, Repl 2020-04-20
Participants:

 Description   

The Replication team has several TLA+ specs in the server repository. Currently there is little or no guidance for how to run the model-checker ("TLC") on these specs, and we do not test continuously that these specs would pass the model-checker.

Proposed solution: commit model checker config files to git, install TLC on an Evergreen build image, and create an Evergreen task to run TLC on all the specs.



 Comments   
Comment by Githook User [ 06/Apr/20 ]

Author:

{'name': 'A. Jesse Jiryu Davis', 'email': 'jesse@mongodb.com', 'username': 'ajdavis'}

Message: SERVER-45416 Model-check TLA+ specs in Evergreen
Branch: master
https://github.com/mongodb/mongo/commit/6018c34bd232d565d18ba8ee5b97509b374ac3ed

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