summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAdam M. Stück <adam@adast.xyz>2022-12-16 21:35:38 +0100
committerAdam M. Stück <adam@adast.xyz>2022-12-17 17:03:19 +0100
commit490431782825d9d032d301fa2ea9665fa2f87b7e (patch)
tree9212eaf223e1d943c3332bf76412da939b15bc31
parentae08f6fe70a1a525662905a6ded935c05bb053f1 (diff)
Simplified some data parsing in 'run_model'
-rwxr-xr-xrun-model10
1 files changed, 5 insertions, 5 deletions
diff --git a/run-model b/run-model
index d751859..4047a03 100755
--- a/run-model
+++ b/run-model
@@ -62,11 +62,11 @@ main () {
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]+")
+ DISCOVERED_STATES=$(echo "$TMP" | grep -m 1 'discovered states:' | awk '{print $3}')
+ EXPLORED_STATES=$(echo "$TMP" | grep -m 1 'explored states:' | awk '{print $3}')
+ EXPANDED_STATES=$(echo "$TMP" | grep -m 1 'expanded states:' | awk '{print $3}')
+ MAX_TOKENS=$(echo "$TMP" | grep -m 1 'max tokens:' | awk '{print $3}')
+ SEARCH_TIME=$(echo "$TMP" | grep -m 1 'search time taken:' | awk '{print $4}')
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