blob: cc53169ca28f86bbae9d76636f502c9997a384f3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
#!/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
fi
if ! [ -e "$1" ]; then
echo "Directory $1 not found" >&2
exit 1
fi
if ! [ -d "$1" ]; then
echo "$1 not a directory" >&2
exit 1
fi
if ! [ -f "tla2tools.jar" ]; then
echo "No tla2tools.jar, run download-tlc.sh first"
exit 1
fi
TLA_FILE="MC$1.tla"
if ! [ -f "$1/$TLA_FILE" ]; then
echo "$1/$TLA_FILE does not exist" >&2
exit 1
fi
if [ -z "$JAVA_BINARY" ]; then
JAVA_BINARY=java
else
echo "Using java binary [$JAVA_BINARY]"
fi
cd "$1"
# Defer liveness checks to the end with -lncheck, for speed.
"$JAVA_BINARY" -XX:+UseParallelGC -Dtlc2.tool.fp.FPSet.impl=tlc2.tool.fp.OffHeapDiskFPSet -Dutil.ExecutionStatisticsCollector.id=10f53a1c957c11ea94a033245b683b65 -cp ../tla2tools.jar tlc2.TLC -lncheck final -workers auto "$TLA_FILE"
|
