[SERVER-46789] Make TLC wrapper script cross-platform Created: 11/Mar/20  Updated: 29/Oct/23  Resolved: 12/Mar/20

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

Type: Improvement 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:
Related
is related to SERVER-45416 TLA+ specs are not continuously tested Closed
is related to SERVER-44458 Productionize RaftMongo TLA+ spec Closed
Backwards Compatibility: Fully Compatible
Sprint: Repl 2020-03-23
Participants:

 Description   

InĀ SERVER-44458 I introduced a command-line wrapper script for TLC, the TLA+ model-checker. The script is called model-check.sh. Its purpose is to make it easy for humans to run TLC with predefined model-checking parameters, and eventually to do the same in Evergreen (SERVER-45416).

For simplicity, the first version used a Linux-only method for determining the number of CPU cores. On other platforms the script would fail.

I've changed my mind, I think it would be nice to run this script on any platform.



 Comments   
Comment by Githook User [ 12/Mar/20 ]

Author:

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

Message: SERVER-46789 Make model-check.sh cross-platform
Branch: master
https://github.com/mongodb/mongo/commit/b71e22a2091af835b5f11dacc61fd1516ad94425

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