diff options
| author | A. Jesse Jiryu Davis <jesse@mongodb.com> | 2020-05-11 22:35:28 -0400 |
|---|---|---|
| committer | Evergreen Agent <no-reply@evergreen.mongodb.com> | 2020-05-12 18:45:59 +0000 |
| commit | 4317089d3206e16a623bd38f68e950f6b276f65c (patch) | |
| tree | 9d490cf68246e095036c1d2ee4556d9cefda8a12 /src | |
| parent | 26008265842c4282c94f1723d83d2b1659cace2d (diff) | |
| download | mongo-4317089d3206e16a623bd38f68e950f6b276f65c.tar.gz | |
SERVER-48045 Set Java path tla_plus.yml suite config
Diffstat (limited to 'src')
| -rwxr-xr-x | src/mongo/db/repl/tla_plus/model-check.sh | 15 |
1 files changed, 13 insertions, 2 deletions
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" |