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