diff options
| author | A. Jesse Jiryu Davis <jesse@mongodb.com> | 2020-05-08 16:16:30 -0400 |
|---|---|---|
| committer | Evergreen Agent <no-reply@evergreen.mongodb.com> | 2020-05-08 20:28:48 +0000 |
| commit | dc47e87ce770fd14af1d781edc54b4723fe53802 (patch) | |
| tree | 19fcf4e785ee08d83da5598d6557f35ed63008e2 /src/mongo/db | |
| parent | 49cc63fbb37f8a51f845c8d35bdb2f9c11219dab (diff) | |
| download | mongo-dc47e87ce770fd14af1d781edc54b4723fe53802.tar.gz | |
SERVER-48045 Use Java 11 for TLA+ model-checking
Diffstat (limited to 'src/mongo/db')
| -rwxr-xr-x | src/mongo/db/repl/tla_plus/download-tlc.sh | 2 | ||||
| -rwxr-xr-x | src/mongo/db/repl/tla_plus/model-check.sh | 3 |
2 files changed, 3 insertions, 2 deletions
diff --git a/src/mongo/db/repl/tla_plus/download-tlc.sh b/src/mongo/db/repl/tla_plus/download-tlc.sh index 8828a17b08a..b63944a7231 100755 --- a/src/mongo/db/repl/tla_plus/download-tlc.sh +++ b/src/mongo/db/repl/tla_plus/download-tlc.sh @@ -3,4 +3,4 @@ # Downloads TLC, which is the model-checker for the TLA+ formal specifications in this directory. echo "Downloading tla2tools.jar" -curl -fLO tla.msr-inria.inria.fr/tlatoolbox/dist/tla2tools.jar +curl -fLO https://github.com/tlaplus/tlaplus/releases/download/v1.7.0/tla2tools.jar diff --git a/src/mongo/db/repl/tla_plus/model-check.sh b/src/mongo/db/repl/tla_plus/model-check.sh index 526134fd8fd..44a6be2ba08 100755 --- a/src/mongo/db/repl/tla_plus/model-check.sh +++ b/src/mongo/db/repl/tla_plus/model-check.sh @@ -31,5 +31,6 @@ elif ! WORKERS=$(sysctl -n hw.logicalcpu); then fi cd "$1" +# Requires Java 11. # Defer liveness checks to the end with -lncheck, for speed. -java -XX:+UseParallelGC -cp ../tla2tools.jar tlc2.TLC -lncheck final -workers "$WORKERS" "$TLA_FILE" +/opt/java/jdk11/bin/java -XX:+UseParallelGC -cp ../tla2tools.jar tlc2.TLC -lncheck final -workers "$WORKERS" "$TLA_FILE" |