From 0173fd6562ae4bb8dbd50954e69e20dfe08c3f94 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Sat, 23 Sep 2023 15:17:11 +0100 Subject: [PATCH] benchmark generator --- experiments/drs_cell_signal/run.sh | 29 ++++++++++++++++++++++++++--- 1 file changed, 26 insertions(+), 3 deletions(-) diff --git a/experiments/drs_cell_signal/run.sh b/experiments/drs_cell_signal/run.sh index 955a3e4..2de5f20 100755 --- a/experiments/drs_cell_signal/run.sh +++ b/experiments/drs_cell_signal/run.sh @@ -32,8 +32,10 @@ then mkdir -p $outdir fi -ulimit -t 3600 -ulimit -v 2097152 +#ulimit -t 3600 +#ulimit -v 2097152 +ulimit -t 360 +ulimit -v 1000000 for a in $aut_values do @@ -49,17 +51,38 @@ do # Skip undesired values continue fi - + + bench_identifier="${benchname}_F${formname}_A${a}" + filename_base="${outdir}/${benchname}_F${formname}__x${x}_y${y}_z${z}_A${a}" outfile="${filename_base}.out" infile="${filename_base}.drs" + stopfile="DONE_${bench_identifier}" + + if [[ -e "$stopfile" ]] + then + echo "Time limit -- SKIPPING" + continue + fi + $input_generator $x $y $z $a > ${infile} $reactics $reactics_opts $formname $infile > ${outfile} 2>&1 exitcode=$? echo "ReactICS exit code: $exitcode" + result="$(tail -1 $outfile | grep -E '.*;.*;.*;.*'| sed "s/STAT/$n /")" + if [ "$result" = "" ] + then + echo "TIME LIMIT; marking as finished" + touch $stopfile + else + echo $result >> $outdir/summary_${bench_identifier}.txt + echo $result | sed 's/;/ /g' >> $outdir/${bench_identifier}.dat + echo $result + fi + done done done