-
Type:
New Feature
-
Resolution: Fixed
-
Priority:
Major - P3
-
Affects Version/s: None
-
Component/s: Replication
-
Labels:None
-
Fully Compatible
-
Repl 2020-02-10, Repl 2020-03-23, Repl 2020-04-06, Repl 2020-04-20
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.
- causes
-
SERVER-47503 Invalid batchtime setting on tla_plus task
-
- Closed
-
- related to
-
SERVER-46789 Make TLC wrapper script cross-platform
-
- Closed
-
-
-
- Closed
-