blob: 596d81c3b520da53341f1dec8047c6f7f1f8f1c8 (
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
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
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
#!/bin/bash
# SETUP
TIME_LIMIT=300 # In seconds, per query
NUM_PROBLEMS=1350 # First n problems from models path (e.g. MCC2022/)
STRATEGIES=(
"RDFS --seed-offset 5760351"
"BestFS"
"DFS"
"BFS"
)
# DO NOT CHANGE THIS BELOW THIS POINT
PIPELINE_PATH=$(dirname "$0")
main() {
if [ $# -eq 0 ]; then
help; exit 1
fi
USE_SBATCH="false"
case "$1" in
-h|--help)
help
exit
;;
-s|--sbatch)
USE_SBATCH="true"
MODELS_PATH="$2"
OUTPUT_PATH="$3"
;;
*)
MODELS_PATH="$1"
OUTPUT_PATH="$2"
;;
esac
if [[ ! -d "$MODELS_PATH" ]]; then
echo "error: invalid models path"
exit 1
fi
OUTPUT_PATH="$OUTPUT_PATH/$(date -u +"%d-%m-%YT%H.%M.%S")"
mkdir -p "$OUTPUT_PATH/pipeline"
cp -r "$PIPELINE_PATH" "$OUTPUT_PATH"
start_jobs $USE_SBATCH "$MODELS_PATH"
}
start_jobs() {
USE_SBATCH=$1
MODELS_PATH=$2
STRAT_LEN=${#STRATEGIES[@]}
serialize_array STRATEGIES STRAT_STR "|"
ALL_MODELS=$(find "$MODELS_PATH" -type d -printf '%f\n' | tail -n+2 | sort | head -n "$NUM_PROBLEMS")
TOTAL_TIME_LIMIT=$(echo "($TIME_LIMIT * $STRAT_LEN * 16) / 60 + 1" | bc)
for MODEL in $ALL_MODELS; do
if [ "$USE_SBATCH" == "true" ]; then
sbatch --time "$TOTAL_TIME_LIMIT" "$PIPELINE_PATH/run-model" "$PIPELINE_PATH/verifypn-linux64" "$TIME_LIMIT" "$STRAT_STR" "$MODELS_PATH/$MODEL" "$OUTPUT_PATH/$MODEL.csv"
else
timeout "${TOTAL_TIME_LIMIT}m" "$PIPELINE_PATH/run-model" "$PIPELINE_PATH/verifypn-linux64" "$TIME_LIMIT" "$STRAT_STR" "$MODELS_PATH/$MODEL" "$OUTPUT_PATH/$MODEL.csv"
fi
done
}
serialize_array() {
declare -n _array="${1}" _str="${2}" # _array, _str => local reference vars
local IFS="${3:-$'\x01'}"
# shellcheck disable=SC2034 # Reference vars assumed used by caller
_str="${_array[*]}" # * => join on IFS
}
help() {
cat << EOF
usage: $0 [OPTIONS] MODELS-PATH OUTPUT-PATH
Run Tapaal/MCC search strategy benchmark.
Number of models to run, time limit and search strategies can be
configured in the top of this script.
Options:
-h, --help Show this message
-s, --sbatch Run on the cluster, instead of locally.
EOF
}
main "$@"
|
