From 490431782825d9d032d301fa2ea9665fa2f87b7e Mon Sep 17 00:00:00 2001 From: "Adam M. Stück" Date: Fri, 16 Dec 2022 21:35:38 +0100 Subject: Simplified some data parsing in 'run_model' --- run-model | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'run-model') 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 -- cgit v1.2.3-70-g09d2