Commit 6d6c6eb5 authored by Hugo Moreau's avatar Hugo Moreau
Browse files

Bench: Logging actions

A new log directory is now generated when bench is in progress,
containing all log files, named with this pattern,
`formula.<FORMULA NB>.[bb.].log`.
parent 2cf1e2d5
Pipeline #27384 passed with stage
in 2 minutes and 25 seconds
......@@ -68,7 +68,7 @@ ${LTLOUTPUT}: %-ltl/${OUTPUT_LTL}: RERS/%-ltl.go.formulae.txt RERS/%-ltl.go %-lt
fi
%-ltl:
@mkdir $@
@mkdir $@ $@/log
${REACHBB}: %-reach/${OUTPUT_BB}: RERS/%-reach.go %-reach
@echo Processing blackbox $< if it exists
......@@ -81,7 +81,7 @@ ${OUTPUT_REACH}: ${REACHOUTPUT}
tail -q -n +2 $< >> $@;\
fi
${REACHOUTPUT}: %-reach/${OUTPUT_REACH}: RERS/%-reach.go %-reach/output/go2pins-mc
${REACHOUTPUT}: %-reach/${OUTPUT_REACH}: RERS/%-reach.go %-reach/output/go2pins-mc %-reach
@echo Processing $<.formulae.txt if it exists
@./run-reach.sh $@ $^ ${REACHTHREADS}
@echo End of processing $<
......@@ -94,7 +94,7 @@ ${REACHOUTPUT}: %-reach/${OUTPUT_REACH}: RERS/%-reach.go %-reach/output/go2pins-
fi
%-reach:
@mkdir $@
@mkdir $@ $@/log
clean:
rm -rf ${LTLDIR} ${REACHDIR}
......
......@@ -7,6 +7,8 @@ model=$3
dir=$4
NBTHREADS=$5
logdir="$dir"/log
if [ -f "$save" ]; then
exit 0
fi
......@@ -30,6 +32,7 @@ blackbox() {
./"$dir"/blackbox/go2pins-mc -kripke-size > $kripkestate
ST=$(cat $kripkestate | grep "states" | grep -o "[0-9]\+")
TR=$(cat $kripkestate | grep "transitions" | grep -o "[0-9]\+")
echo $(date --iso-8601=ns) $ST, $TR, $formula >> "$logdir"/formula."$i".bb."log"
filename=$(basename -- "$model")
filename="${filename%.*}"
......@@ -40,13 +43,16 @@ blackbox() {
RESL=$(./"$dir"/blackbox/go2pins-mc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin 2>&1)
end=$(date +%s.%N)
ltsmin_timeblackbox=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo $(date --iso-8601=ns) $RESL >> "$logdir"/formula."$i".bb."log"
start=$(date +%s.%N)
RESS=$(./"$dir"/blackbox/go2pins-mc -ltl "$1" -nb-threads $NBTHREADS -backend spot 2>&1)
end=$(date +%s.%N)
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"
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"
}
......
......@@ -8,6 +8,8 @@ go2pinsmc=$4
dir=$5
NBTHREADS=$6
logdir="$dir"/log
if [ -f "$save" ]; then
exit 0
......@@ -40,16 +42,19 @@ do
RESL=$(./$go2pinsmc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin 2>&1)
end=$(date +%s.%N)
ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo $(date --iso-8601=ns) $RESL >> "$logdir"/formula."$i"."log"
start=$(date +%s.%N)
RESS=$(./$go2pinsmc -ltl "$formula" -nb-threads $NBTHREADS -backend spot 2>&1)
end=$(date +%s.%N)
spot_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo $(date --iso-8601=ns) $RESS >> "$logdir"/formula."$i"."log"
echo " [formulae $i] spot:$spot_time,ltsmin:$ltsmin_time $bb"
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))
done < $formulae
......
......@@ -6,6 +6,8 @@ model=$2
dir=$3
NBTHREADS=$4
logdir="$dir"/log
if [ ! -f "$model.formulae.txt" ]; then
echo "No specifications for $model" > $save
......@@ -45,6 +47,7 @@ do
./"$dir"/blackbox/go2pins-mc -kripke-size > $kripkestate
ST=$(cat $kripkestate | grep "states" | grep -o "[0-9]\+")
TR=$(cat $kripkestate | grep "transitions" | grep -o "[0-9]\+")
echo $(date --iso-8601=ns) $ST, $TR, $formula >> "$logdir"/formula."$i".bb."log"
filename=$(basename -- "$model")
filename="${filename%.*}"
......@@ -53,12 +56,14 @@ do
LTSMIN_F=$(echo $formula | sed 's/"//g')
start=$(date +%s.%N)
RESL=$(./"$dir"/blackbox/go2pins-mc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin 2>&1)
echo $(date --iso-8601=ns) $RESL >> "$logdir"/formula."$i".bb."log"
end=$(date +%s.%N)
ltsmin_timeblackbox=$(python -c "print ('%.3f' % (${end} - ${start}))")
start=$(date +%s.%N)
RESS=$(./"$dir"/blackbox/go2pins-mc -ltl "$formula" -nb-threads $NBTHREADS -backend spot 2>&1)
end=$(date +%s.%N)
spot_timeblackbox=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo $(date --iso-8601=ns) $RESS >> "$logdir"/formula."$i".bb."log"
echo " [formulae $i] blackbox: spot:$spot_timeblackbox, ltsmin:$ltsmin_timeblackbox, states: $ST, transitions: $TR"
......@@ -86,6 +91,7 @@ do
fi
echo $model,$status,$TRANSPILE_TIME, $TRANSPILE_MEMORY, $ST, $TR, $spot_timeblackbox, $ltsmin_timeblackbox >> "$tmpfile"
echo $(date --iso-8601=ns) "$model,$status,$spot_time,$ltsmin_time,$formula" >> "$logdir"/formula."$i".bb."log"
i=$((i+1))
done < $model.formulae.txt
......
......@@ -4,7 +4,10 @@ i=0
save=$1
model=$2
go2pinsmc=$3
NBTHREADS=$4
dir=$4
NBTHREADS=$5
logdir="$dir"/log
if [ ! -f "$model.formulae.txt" ]; then
......@@ -39,11 +42,12 @@ do
RESL=$(./$go2pinsmc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin 2>&1)
end=$(date +%s.%N)
ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo $(date --iso-8601=ns) $RESL >> "$logdir"/formula."$i"."log"
start=$(date +%s.%N)
RESS=$(./$go2pinsmc -ltl "$formula" -nb-threads $NBTHREADS -backend spot 2>&1)
end=$(date +%s.%N)
spot_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo $(date --iso-8601=ns) $RESS >> "$logdir"/ormula."$i"."log"
echo " [formulae $i] spot:$spot_time,ltsmin:$ltsmin_time"
......@@ -69,7 +73,8 @@ do
fi
echo "$model,$status,$spot_time,$ltsmin_time,$formulae">> $tmpfile
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))
done < $model.formulae.txt
......
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