mirrors/mongodb
mirrors/mongodb
0
0
Fork 0
mirror of https://github.com/mongodb/mongo.git synced 2024-12-01 09:32:32 +01:00
Code Issues Releases Activity

SERVER-48045 Use Java 11 for TLA+ model-checking

Browse Source
This commit is contained in:
A. Jesse Jiryu Davis 2020-05-08 16:16:30 -04:00 committed by Evergreen Agent
parent 49cc63fbb3
commit dc47e87ce7
2 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/mongo/db/repl/tla_plus/download-tlc.sh
View File

@ -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

3
src/mongo/db/repl/tla_plus/model-check.sh
View File

@ -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"