diff options
-rw-r--r-- | buildscripts/resmokeconfig/suites/tla_plus.yml | 3 | ||||
-rw-r--r-- | buildscripts/resmokelib/testing/testcases/tla_plus_test.py | 12 | ||||
-rwxr-xr-x | src/mongo/db/repl/tla_plus/model-check.sh | 15 |
3 files changed, 25 insertions, 5 deletions
diff --git a/buildscripts/resmokeconfig/suites/tla_plus.yml b/buildscripts/resmokeconfig/suites/tla_plus.yml index 249d0dd9870..6ce813f6c84 100644 --- a/buildscripts/resmokeconfig/suites/tla_plus.yml +++ b/buildscripts/resmokeconfig/suites/tla_plus.yml @@ -5,4 +5,5 @@ selector: - src/mongo/db/repl/tla_plus/**/*.cfg executor: - config: {} + config: + java_binary: /opt/java/jdk11/bin/java diff --git a/buildscripts/resmokelib/testing/testcases/tla_plus_test.py b/buildscripts/resmokelib/testing/testcases/tla_plus_test.py index a8c8f28bfcc..504d428fbf2 100644 --- a/buildscripts/resmokelib/testing/testcases/tla_plus_test.py +++ b/buildscripts/resmokelib/testing/testcases/tla_plus_test.py @@ -11,11 +11,13 @@ class TLAPlusTestCase(interface.ProcessTestCase): REGISTERED_NAME = "tla_plus_test" - def __init__(self, logger, model_config_file): + def __init__(self, logger, model_config_file, java_binary=None): """Initialize the TLAPlusTestCase with a TLA+ model config file. model_config_file is the full path to a file like src/mongo/db/repl/tla_plus/MongoReplReconfig/MCMongoReplReconfig.cfg. + + java_binary is the full path to the "java" program, or None. """ message = f"Path '{model_config_file}' doesn't" \ f" match **/<SpecName>/MC<SpecName>.cfg" @@ -30,8 +32,14 @@ class TLAPlusTestCase(interface.ProcessTestCase): if not specname or filename != f'MC{specname}.cfg': raise ValueError(message) + self.java_binary = java_binary + interface.ProcessTestCase.__init__(self, logger, "TLA+ test", specname) def _make_process(self): + process_kwargs = {"cwd": self.working_dir} + if self.java_binary is not None: + process_kwargs["env_vars"] = {"JAVA_BINARY": self.java_binary} + return core.programs.generic_program(self.logger, ["sh", "model-check.sh", self.test_name], - process_kwargs={"cwd": self.working_dir}) + process_kwargs=process_kwargs) diff --git a/src/mongo/db/repl/tla_plus/model-check.sh b/src/mongo/db/repl/tla_plus/model-check.sh index 44a6be2ba08..031d300f6f2 100755 --- a/src/mongo/db/repl/tla_plus/model-check.sh +++ b/src/mongo/db/repl/tla_plus/model-check.sh @@ -1,5 +1,11 @@ #!/bin/sh +# Execute TLC, the TLA+ model-checker, on a TLA+ specification and model config. Call like: +# +# ./model-check.sh RaftMongo +# +# Requires Java 11. You can set the JAVA_BINARY environment variable to the full path to java. + if [ "$#" -ne 1 ]; then echo "Usage: $0 SPEC_DIRECTORY" >&2 exit 1 @@ -23,6 +29,12 @@ if ! [ -f "$1/$TLA_FILE" ]; then exit 1 fi +if [ -z "$JAVA_BINARY" ]; then + JAVA_BINARY=java +else + echo "Using java binary [$JAVA_BINARY]" +fi + # Count CPUs. Linux has cpuinfo, Mac has sysctl, otherwise use a default. if [ -e "/proc/cpuinfo" ]; then WORKERS=$(grep -c processor /proc/cpuinfo) @@ -31,6 +43,5 @@ elif ! WORKERS=$(sysctl -n hw.logicalcpu); then fi cd "$1" -# Requires Java 11. # Defer liveness checks to the end with -lncheck, for speed. -/opt/java/jdk11/bin/java -XX:+UseParallelGC -cp ../tla2tools.jar tlc2.TLC -lncheck final -workers "$WORKERS" "$TLA_FILE" +"$JAVA_BINARY" -XX:+UseParallelGC -cp ../tla2tools.jar tlc2.TLC -lncheck final -workers "$WORKERS" "$TLA_FILE" |