-
-
Notifications
You must be signed in to change notification settings - Fork 38
/
apalache-mc
executable file
·69 lines (59 loc) · 2.02 KB
/
apalache-mc
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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
#!/usr/bin/env bash
#
# Run the APALACHE model checker
#
# Igor Konnov, 2018-2019
DIR=`dirname $0`
DIR=`cd "$DIR/.."; pwd`
echo "# Tool home: $DIR"
# try to find either a release jar, or a local build
DISTS=`mktemp /tmp/apalache-dists.XXXX`
find >$DISTS "$DIR" "$DIR/mod-distribution/target/" \
-maxdepth 1 -name "apalache-pkg-*-full.jar"
case `cat $DISTS | wc -l | sed 's/[[:space:]]*//g'` in
1)
JAR=`head -n 1 $DISTS`
echo "# Package: $JAR"
;;
0)
echo "ERROR: Distribution jar not found. Did you run mvn package?"
exit 1
;;
*)
echo "Found multiple apalache packages:"
cat $DISTS
echo ""
echo "To resolve this, run:"
echo " mvn clean && mvn package"
exit 1
;;
esac
rm -f "$DISTS"
# an additional lookup list for the TLA+ modules
TLA_LIB="$DIR/src/tla"
# This is a temporary solution for handling TLA_PATH via a Java variable.
# See apalache/#187.
# Once tlaplus/#490,#493 are released, remove this workaround.
(test -z "$TLA_PATH" && TLA_PATH="$TLA_LIB") || TLA_PATH="TLA_LIB:$TLA_PATH"
# set LD_LIBRARY_PATH to find z3 libraries
export LD_LIBRARY_PATH="$DIR/3rdparty/lib:${LD_LIBRARY_PATH}"
# 1. The maximum heap size, Z3 will use much more as a native library.
# 2. Duplicating LD_LIBRARY_PATH, tell JVM to find the third-party libraries.
JVM_ARGS="-Xmx4096m -Djava.library.path=$DIR/3rdparty/lib "
# uncomment to track memory usage with: jcmd <pid> VM.native_memory summary
#JVM_ARGS="${JVM_ARGS} -XX:NativeMemoryTracking=summary"
JVM_ARGS="$JVM_ARGS -DTLA-Library=$TLA_LIB"
echo "# JVM args: $JVM_ARGS"
echo "#"
# a trap for SIGINT and SIGTERM
sigterm() {
echo "Premature termination requested. Killing apalache-mc (pid $child)" 1>&2
trap - SIGTERM SIGINT # unregister to avoid recursion below
# send termination to the child process
kill SIGTERM $child 2>/dev/null
}
trap sigterm SIGTERM SIGINT
# run java in the background in order to react to SIGTERM
java $JVM_ARGS -jar "$JAR" "$@" &
child=$!
wait "$child"