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

benchs: log status

* benchs/run-ltl-bb.sh, benchs/run-ltl.sh: Here.
parent b32b86af
Pipeline #27416 passed with stage
in 2 minutes and 25 seconds
......@@ -51,7 +51,16 @@ blackbox() {
spot_timeblackbox=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo $(date --iso-8601=ns) $RESS >> "$logdir"/formula."$i".bb."log"
echo $model,,$TRANSPILE_TIME, $TRANSPILE_MEMORY, $ST, $TR, $spot_timeblackbox, $ltsmin_timeblackbox >> "$tmpfile"
status=$(cat "$logdir"/formula."$i"."log" | grep "an accepting run exists")
if [ -z "$status" ]; then
status="EMPTY"
else
status="NOTEMPTY"
fi
echo $model,$status,$TRANSPILE_TIME, $TRANSPILE_MEMORY, $ST, $TR, $spot_timeblackbox, $ltsmin_timeblackbox >> "$tmpfile"
echo $(date --iso-8601=ns) $model,,$TRANSPILE_TIME, $TRANSPILE_MEMORY, $ST, $TR, $spot_timeblackbox, $ltsmin_timeblackbox >> "$logdir"/formula."$i".bb."log"
echo " [formulae $i] blackbox: spot:$spot_timeblackbox, ltsmin:$ltsmin_timeblackbox, states: $ST, transitions: $TR"
}
......
......@@ -53,6 +53,14 @@ do
echo " [formulae $i] spot:$spot_time,ltsmin:$ltsmin_time $bb"
status=$(cat "$logdir"/formula."$i"."log" | grep "an accepting run exists")
if [ -z "$status" ]; then
status="EMPTY"
else
status="NOTEMPTY"
fi
echo "$model,$status,$spot_time,$ltsmin_time,$formula">> $tmpfile
echo $(date --iso-8601=ns) "$model,$status,$spot_time,$ltsmin_time,$formula">> "$logdir"/formula."$i"."log"
i=$((i+1))
......
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