Commit df67e017 authored by Etienne Renault's avatar Etienne Renault
Browse files

benchs: log time for transpile + compile + LOC

Avoid systematic computation of the whole State Space
that can be too huge.

* benchs/build.sh: Here.
parent d154d355
......@@ -5,14 +5,23 @@ 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
$go2pins -f -o "$file"/output -rers RERS/"$file".go > "$transpile" 2>&1
TRANSPILE_TIME=$(grep "transpilation time:" $transpile | awk '{print $3}')
COMPILE_TIME=$(grep "compilation time:" $transpile | awk '{print $3}')
# Avoid this computation that may be really huge since not constrained
# by the property
# /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
LOC=$(wc -l RERS/"$file".go | awk '{print $1}')
echo "file,LOC,transpile_time,compile_time,total_time" > "$file"/global.csv
echo RERS/"$file".go,$LOC,$TRANSPILE_TIME,$COMPILE_TIME,$((TRANSPILE_TIME+COMPILE_TIME)) >> "$file"/global.csv
rm -f $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