Improved file structure

6 files changed, 265 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..1407935
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+cloud-auth
diff --git a/archiver b/archiver
new file mode 100755
index 0000000..1c0bc79
--- /dev/null
+++ b/archiver
@@ -0,0 +1,65 @@
+#!/bin/bash
+
+RESULTS_PATH=$1
+
+main() {
+    if [ $# -eq 0 ]; then
+        help; exit 1
+    fi
+
+    case "$1" in
+        -h|--help)
+            help; exit ;;
+    esac
+
+    if [[ ! -d "$RESULTS_PATH" ]]; then
+        echo "error: invalid results path"
+        exit 1
+    fi
+
+    aggregate_files 
+}
+
+aggregate_files() {
+    OUTPUT=""
+    HEADER_INSERTED=false
+
+    while IFS= read -r -d '' ENTRY
+    do
+        if [ $HEADER_INSERTED == true ]; then
+            FILE=$(tail -n +2 "$ENTRY")
+        else 
+            FILE=$(cat "$ENTRY")
+        fi
+
+        OUTPUT+="$FILE\n"
+        HEADER_INSERTED=true
+    done <   <(find "$RESULTS_PATH" -maxdepth 1 -type f -print0)
+
+    HEADER=$(echo -e "$OUTPUT" | head -n 1)
+    ALL_ROWS=$(echo -e "$OUTPUT" | tail -n +2 | sort -t$'\t' -k6,6 -n) 
+    STRATS=$(echo -e "$ALL_ROWS" | awk -F '\t' '{print $5}' | sort | uniq)
+
+    OUTPUT=""
+    while read -r STRAT; do
+        [ -z "$STRAT" ] && continue
+        ROWS=$(echo -e "$ALL_ROWS" | grep -P "\t$STRAT\t")
+        OUTPUT+="$ROWS\n"
+    done <<< "$STRATS"
+
+    OUTPUT=$(echo -e "$HEADER\n$OUTPUT" | head -n -1)
+    echo -e "$OUTPUT" > "$RESULTS_PATH/data.csv"
+}
+
+help() {
+cat << EOF
+usage: $0 RESULTS-DIR
+
+Aggregate data from search stragey benchmark
+
+Options:
+  -h, --help            Show this message
+EOF
+}
+
+main "$@"
diff --git a/cloud-upload b/cloud-upload
new file mode 100755
index 0000000..3f0a454
--- /dev/null
+++ b/cloud-upload
@@ -0,0 +1,12 @@
+#!/bin/bash
+
+PREFIX=$(dirname "$0")
+CLOUD_AUTH=$(<"$PREFIX/cloud-auth")
+UPLOAD_PATH="https://cloud.adast.xyz/public.php/webdav/uploads"
+
+if [ -f "$1" ]; then
+    FILE=$(basename "$1")
+    curl -T "$1" -u "$CLOUD_AUTH" "$UPLOAD_PATH/$FILE"
+else 
+    echo "error: invalid file $1"
+fi
diff --git a/run-model b/run-model
new file mode 100755
index 0000000..fe8aea8
--- /dev/null
+++ b/run-model
@@ -0,0 +1,83 @@
+#!/bin/bash
+#SBATCH --mem=15000
+#SBATCH --output=/dev/null
+#SBATCH --exclude=naples01,dhabi01,rome01
+
+TIME_CMD="/usr/bin/time -f \"@@@%M@@@\" "
+
+# THIS SCRIPT IS NOT INTENDED TO BE RUN MANUALLY, LOOK AT 'start' SCRIPT
+
+main () {
+    BINARY=$1
+    TIME_LIMIT=$2 # in seconds per query
+    STRAT_STR="$3"
+    MODEL_PATH="$4"
+    RESULT_PATH="$5"
+
+    lscpu > "$RESULT_PATH.hardwareinfo"                    
+
+    DATE=$(date -u +"%d/%m/%Y %H.%M.%S")
+    OUTPUT="model\tquery\tsolved\tresult\tstrategy\ttime\tdate\ttime-limit\tmemory\texit-code\tformula\ttimed-out\terror-msg\tdiscoveredStates\texploredStates\texpandedStates\tmaxTokens\tsearchTime"
+
+    MODEL=$(basename "$MODEL_PATH")
+
+    deserialize_array STRAT_STR STRATEGIES '|'
+
+    for STRAT in "${STRATEGIES[@]}"; do
+        for QUERY in $(seq 16); do
+            START_TIME=$(date +%s.%N)
+            TMP=$($TIME_CMD timeout $TIME_LIMIT $BINARY -n -x $QUERY -s $STRAT $MODEL_PATH/model.pnml $MODEL_PATH/ReachabilityCardinality.xml 2>&1)
+            RETVAL=$?
+
+            ERROR_MSG=""
+            if [[ "$RETVAL" -ne 0 ]]; then
+                ERROR_MSG=$(echo "$TMP" | tr -d '\n' | sed 's|\t|   |g')
+            fi
+
+            END_TIME=$(date +%s.%N)
+            TIME=$(echo "$END_TIME - $START_TIME" | bc -l)
+            if [[ $TIME =~ ^[.] ]]; then
+                TIME="0$TIME"
+            fi 
+
+            MEM_USED=$(grep -oP "(?<=@@@).*(?=@@@)" <<< "$TMP")
+
+            TIMED_OUT="FALSE"
+            if grep -qm 1 'Command exited with non-zero status 124' <<< "$TMP"; then
+                TIMED_OUT="TRUE"
+            fi
+
+            FORMULA="FALSE"
+            if grep -qm 1 'FORMULA' <<< "$TMP"; then
+                FORMULA="TRUE"
+            fi
+
+            SOLVED="FALSE"
+            if grep -qm 1 'was solved' <<< "$TMP"; then
+                SOLVED="TRUE"
+            fi 
+
+            RESULT="NULL"
+            if grep -qm 1 'Query is satisfied.' <<< "$TMP"; then
+                RESULT="TRUE"
+            elif grep -qm 1 'Query is NOT satisfied.' <<< "$TMP"; then
+                RESULT="FALSE"
+            fi 
+
+            DISCOVERED_STATES=$(echo "$TMP" | grep -m 1 'discovered states:' | grep -Eo '[0-9]+$')
+            EXPLORED_STATES=$(echo "$TMP" | grep -m 1 'explored states:' | grep -Eo '[0-9]+$')
+            EXPANDED_STATES=$(echo "$TMP" | grep -m 1 'expanded states:' | grep -Eo '[0-9]+$')
+            MAX_TOKENS=$(echo "$TMP" | grep -m 1 'max tokens:' | grep -Eo '[0-9]+$')
+            SEARCH_TIME=$(echo "$TMP" | grep -m 1 'search time taken:' | grep -Eo "[0-9]+\.[0-9]+")
+            OUTPUT+="\n$MODEL\t$QUERY\t$SOLVED\t$RESULT\t$STRAT\t$TIME\t$DATE\t$TIME_LIMIT\t$MEM_USED\t$RETVAL\t$FORMULA\t$TIMED_OUT\t$ERROR_MSG\t$DISCOVERED_STATES\t$EXPLORED_STATES\t$EXPANDED_STATES\t$MAX_TOKENS\t$SEARCH_TIME"
+        done
+    done
+
+    echo -e "$OUTPUT" > "$RESULT_PATH"
+}
+
+deserialize_array() {
+    IFS="${3:-$'\x01'}" read -r -a "${2}" <<<"${!1}" # -a => split on IFS
+}
+
+main "$@"
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 "$@"
diff --git a/update-binary b/update-binary
new file mode 100755
index 0000000..9713994
--- /dev/null
+++ b/update-binary
@@ -0,0 +1,9 @@
+#!/bin/bash
+
+PREFIX=$(dirname "$0")
+CLOUD_AUTH=$(<"$PREFIX/cloud-auth")
+BIN_PATH="https://cloud.adast.xyz/public.php/webdav/uploads"
+BIN_NAME="verifypn-linux64"
+
+curl -u "$CLOUD_AUTH" -s "$BIN_PATH/$BIN_NAME" --output "$PREFIX/$BIN_NAME"
+chmod +x "$PREFIX/$BIN_NAME"