#!/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 "$@"