blob: d751859c6b4f77aaab3b030636a8de6b8ad40da7 (
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
|
#!/bin/bash
#SBATCH --mem=15000
#SBATCH --output=/dev/null
#SBATCH --partition=naples
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"
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 "$@"
|
