From 4317089d3206e16a623bd38f68e950f6b276f65c Mon Sep 17 00:00:00 2001
From: "A. Jesse Jiryu Davis" <jesse@mongodb.com>
Date: Mon, 11 May 2020 22:35:28 -0400
Subject: SERVER-48045 Set Java path tla_plus.yml suite config

---
 src/mongo/db/repl/tla_plus/model-check.sh | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

(limited to 'src')

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"
-- 
cgit v1.2.1