diff options
Diffstat (limited to 'src/mongo/db/repl/tla_plus/model-check.sh')
| -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" |