summaryrefslogtreecommitdiff
path: root/start
diff options
context:
space:
mode:
Diffstat (limited to 'start')
-rwxr-xr-xstart95
1 files changed, 95 insertions, 0 deletions
diff --git a/start b/start
new file mode 100755
index 0000000..596d81c
--- /dev/null
+++ b/start
@@ -0,0 +1,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 "$@"