Commit 0cb42b19 authored by Hugo Moreau's avatar Hugo Moreau Committed by Etienne Renault
Browse files

Bench: Evaluating transpile time

parent 0ce9d269
......@@ -7,11 +7,11 @@ OUTPUT_BB=benchs-bb-${NBTHREADS}.csv
OUTPUT_REACH=benchs-reach-${REACHTHREADS}.csv
OUTPUT_LTL=benchs-ltl-${NBTHREADS}.csv
LTLFILES=RERS/2016-Problem1-ltl.go RERS/2016-Problem2-ltl.go RERS/2016-Problem4-ltl.go RERS/2016-Problem5-ltl.go RERS/2016-Problem7-ltl.go RERS/2017-Problem1-ltl.go RERS/2017-Problem2-ltl.go RERS/2017-Problem4-ltl.go RERS/2017-Problem5-ltl.go RERS/2017-Problem7-ltl.go RERS/2018-Problem1-ltl.go RERS/2018-Problem2-ltl.go RERS/2018-Problem4-ltl.go RERS/2018-Problem5-ltl.go RERS/2018-Problem7-ltl.go RERS/2019-Problem1-ltl.go RERS/2019-Problem2-ltl.go RERS/2019-Problem4-ltl.go RERS/2019-Problem5-ltl.go RERS/2019-Problem7-ltl.go RERS/2020-Problem1-ltl.go RERS/2020-Problem2-ltl.go RERS/2020-Problem4-ltl.go RERS/2020-Problem5-ltl.go RERS/2020-Problem7-ltl.go
LTLFILES=RERS/2016-Problem1-ltl.go RERS/2016-Problem2-ltl.go RERS/2016-Problem4-ltl.go RERS/2016-Problem5-ltl.go RERS/2016-Problem7-ltl.go RERS/2017-Problem1-ltl.go RERS/2017-Problem2-ltl.go RERS/2017-Problem4-ltl.go RERS/2017-Problem5-ltl.go RERS/2017-Problem7-ltl.go RERS/2018-Problem1-ltl.go RERS/2018-Problem2-ltl.go RERS/2018-Problem4-ltl.go RERS/2018-Problem5-ltl.go RERS/2018-Problem7-ltl.go RERS/2019-Problem1-ltl.go RERS/2019-Problem2-ltl.go RERS/2019-Problem4-ltl.go RERS/2019-Problem5-ltl.go RERS/2019-Problem7-ltl.go RERS/2020-Problem1-ltl.go RERS/2020-Problem2-ltl.go RERS/2020-Problem4-ltl.go RERS/2020-Problem5-ltl.go RERS/2020-Problem7-ltl.go
LTLDIR=${LTLFILES:RERS/%.go=%}
LTLOUTPUT=${LTLDIR:%=%/${OUTPUT_LTL}}
REACHFILES=RERS/2016-Problem10-reach.go RERS/2016-Problem11-reach.go RERS/2016-Problem12-reach.go RERS/2016-Problem14-reach.go RERS/2016-Problem15-reach.go RERS/2017-Problem10-reach.go RERS/2017-Problem11-reach.go RERS/2017-Problem12-reach.go RERS/2017-Problem14-reach.go RERS/2017-Problem15-reach.go RERS/2018-Problem10-reach.go RERS/2018-Problem11-reach.go RERS/2019-Problem11-reach.go RERS/2019-Problem12-reach.go RERS/2019-Problem14-reach.go RERS/2019-Problem15-reach.go
REACHFILES=RERS/2016-Problem10-reach.go RERS/2016-Problem11-reach.go RERS/2016-Problem12-reach.go RERS/2016-Problem14-reach.go RERS/2016-Problem15-reach.go RERS/2017-Problem10-reach.go RERS/2017-Problem11-reach.go RERS/2017-Problem12-reach.go RERS/2017-Problem14-reach.go RERS/2017-Problem15-reach.go RERS/2018-Problem10-reach.go RERS/2018-Problem11-reach.go RERS/2019-Problem11-reach.go RERS/2019-Problem12-reach.go RERS/2019-Problem14-reach.go RERS/2019-Problem15-reach.go
REACHDIR=${REACHFILES:RERS/%.go=%}
REACHOUTPUT=${REACHDIR:%=%/${OUTPUT_REACH}}
......@@ -37,7 +37,7 @@ ${LTLOUTPUT}: %-ltl/${OUTPUT_LTL}: RERS/%-ltl.go.formulae.txt RERS/%-ltl.go %-lt
%-ltl/output/go2pins-mc: %-ltl
@if [ ! -f $@ ]; then\
echo Building RERS/$<.go output;\
${GO2PINS} -f -o $</output -rers RERS/$<.go > /dev/null 2>&1;\
./build.sh ${GO2PINS} $<;\
echo End of building RERS/$<.go, use $@;\
fi
......@@ -58,7 +58,7 @@ ${REACHOUTPUT}: %-reach/${OUTPUT_REACH}: RERS/%-reach.go %-reach/output/go2pins-
%-reach/output/go2pins-mc: %-reach
@if [ ! -f $@ ]; then\
echo Building RERS/$<.go output;\
${GO2PINS} -f -o $</output -rers RERS/$<.go > /dev/null 2>&1;\
./build.sh ${GO2PINS} $<;\
echo End of building RERS/$<.go, use $@;\
fi
......
# /bin/zsh
go2pins=$1
file=$2
transpile="$file"/transpile.tmp
kripke="$file"/kripke.tmp
kripkestate="$kripke".state
/usr/bin/time -o "$transpile" -v $go2pins -f -o "$file"/output -rers RERS/"$file".go > /dev/null 2>&1
TRANSPILE_TIME=$(grep "User time" $transpile | awk '{print $4}')
TRANSPILE_MEMORY=$(grep "Maximum resident" $transpile | awk '{print $6}')
/usr/bin/time -o "$kripke" -v ./"$file"/output/go2pins-mc -kripke-size > $kripkestate
ST=$(cat $kripkestate | awk -F',' '{print $2}')
TR=$(cat $kripkestate | awk -F',' '{print $3}')
U_TIME=$(grep "User time" $kripke | awk '{print $4}')
MEMORY=$(grep "Maximum resident" $kripke | awk '{print $6}')
echo "file,transpile_time, transpile_memory, states, transitions, time, memory" > "$file"/global.csv
echo RERS/"$file".go,$TRANSPILE_TIME, $TRANSPILE_MEMORY,$ST,$TR, $U_TIME, $MEMORY >> "$file"/global.csv
rm $kripke $kripkestate $transpile
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment