SERVER-48045 Set Java path tla_plus.yml suite config

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"