Commit 77c63c67 authored by Etienne Renault's avatar Etienne Renault
Browse files

benchs: rework the whole benchmark to be homogeneous

- The benchmark now accept TIMEOUT=10s to fix the maximum
running time of each test.
- The output is the same, whatever the experience considered
- The logs file are now displayed with then \cr\n

* benchs/run-ltl-bb.sh,
benchs/run-ltl.sh,
benchs/run-reach-bb.sh,
benchs/run-reach.sh: Here.
parent c192aff8
...@@ -26,43 +26,51 @@ fi ...@@ -26,43 +26,51 @@ fi
blackbox() { blackbox() {
echo $1 > $formulatmp echo $1 > $formulatmp
/usr/bin/time -o "$transpile" -v ../go2pins -f -o "$dir"/blackbox -blackbox-fn="auto" -rers -formulae $formulatmp $model > /dev/null 2>&1 ../go2pins -f -o "$dir"/blackbox -blackbox-fn="auto" -rers -formulae $formulatmp $model >> "$logdir"/formula."$i".bb."log" 2>&1
TRANSPILE_TIME=$(grep "User time" $transpile | awk '{print $4}') TRANSPILE_TIME=$(grep "transpilation time:" "$logdir"/formula."$i".bb."log" | awk '{print $3}')
TRANSPILE_MEMORY=$(grep "Maximum resident" $transpile | awk '{print $6}') COMPILE_TIME=$(grep "compilation time:" "$logdir"/formula."$i".bb."log" | awk '{print $3}')
./"$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=$(basename -- "$model")
filename="${filename%.*}" filename="${filename%.*}"
# Compute LTSmin Spot resolution time # Compute LTSmin Spot resolution time
LTSMIN_F=$(echo $1 | sed 's/"//g') LTSMIN_F=$(echo $formula | sed 's/"//g')
start=$(date +%s.%N) start=$(date +%s.%N)
RESL=$(./"$dir"/blackbox/go2pins-mc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin 2>&1) timeout $TIMEOUT ./"$dir"/blackbox/go2pins-mc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin > "$logdir"/formula."$i".bb."log".tmp 2>&1
end=$(date +%s.%N) end=$(date +%s.%N)
ltsmin_timeblackbox=$(python -c "print ('%.3f' % (${end} - ${start}))") ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo $(date --iso-8601=ns) $RESL >> "$logdir"/formula."$i".bb."log" echo $(date --iso-8601=ns) >> "$logdir"/formula."$i".bb."log"
cat "$logdir"/formula."$i".bb."log".tmp 2>&1 >> "$logdir"/formula."$i".bb."log"
echo >> "$logdir"/formula."$i".bb."log"
start=$(date +%s.%N) start=$(date +%s.%N)
RESS=$(./"$dir"/blackbox/go2pins-mc -ltl "$1" -nb-threads $NBTHREADS -backend spot 2>&1) timeout $TIMEOUT ./"$dir"/blackbox/go2pins-mc -ltl "$formula" -nb-threads $NBTHREADS -backend spot > "$logdir"/formula."$i".bb."log".tmp 2>&1
end=$(date +%s.%N) end=$(date +%s.%N)
spot_timeblackbox=$(python -c "print ('%.3f' % (${end} - ${start}))") spot_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo $(date --iso-8601=ns) $RESS >> "$logdir"/formula."$i".bb."log" echo $(date --iso-8601=ns) >> "$logdir"/formula."$i".bb."log"
cat "$logdir"/formula."$i".bb."log".tmp 2>&1 >> "$logdir"/formula."$i".bb."log"
echo >> "$logdir"/formula."$i".bb."log"
statusbb=$(cat "$logdir"/formula."$i".bb."log" | grep "not_empty")
status=$(cat "$logdir"/formula."$i"."log" | grep "an accepting run exists") if [ -z "$statusbb" ]; then
if [ -z "$status" ]; then statusbb="EMPTY"
status="EMPTY"
else else
status="NOTEMPTY" statusbb="NOTEMPTY"
fi fi
ltsmin_st=$(cat "$logdir"/formula."$i".bb."log" | grep dve2lts-mc |grep Explored| tail -n 1 |awk '{print $5}')
echo $model,$status,$TRANSPILE_TIME, $TRANSPILE_MEMORY, $ST, $TR, $spot_timeblackbox, $ltsmin_timeblackbox >> "$tmpfile" ltsmin_tr=$(cat "$logdir"/formula."$i".bb."log" | grep dve2lts-mc |grep Explored| tail -n 1 |awk '{print $7}')
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" spot_st=$(cat "$logdir"/formula."$i".bb."log" | grep '^#' | awk -F',' '{print $6}')
spot_tr=$(cat "$logdir"/formula."$i".bb."log" | grep '^#' | awk -F',' '{print $7}')
echo " [formulae $i] $statusbb spot:$spot_time ($spot_st st,$spot_tr tr),ltsmin:$ltsmin_time ($ltsmin_st st,$ltsmin_tr tr) $bb"
echo "$model,$statusbb,$spot_time,$ltsmin_time,$spot_st,$spot_tr,$ltsmin_st,$ltsmin_tr,$formula">> $tmpfile
echo $(date --iso-8601=ns) "$model,$statusbb,$spot_time,$ltsmin_time,$spot_st,$spot_tr,$ltsmin_st,$ltsmin_tr,$formula">> "$logdir"/formula."$i".bb."log"
rm "$logdir"/formula."$i".bb."log".tmp
} }
while read -r formula while read -r formula
......
...@@ -18,7 +18,7 @@ fi ...@@ -18,7 +18,7 @@ fi
tmpfile="$save".tmp tmpfile="$save".tmp
if [ ! -f "$tmpfile" ]; then if [ ! -f "$tmpfile" ]; then
echo "model,isempty,spottime,ltsmintime,formulae" > $tmpfile echo "model,isempty,spottime,ltsmintime,spotst,spottr,ltsminst,ltsmintr,formulae" > $tmpfile
fi fi
...@@ -39,30 +39,39 @@ do ...@@ -39,30 +39,39 @@ do
# Compute LTSmin Spot resolution time # Compute LTSmin Spot resolution time
LTSMIN_F=$(echo $formula | sed 's/"//g') LTSMIN_F=$(echo $formula | sed 's/"//g')
start=$(date +%s.%N) start=$(date +%s.%N)
RESL=$(./$go2pinsmc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin 2>&1) timeout $TIMEOUT ./$go2pinsmc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin > "$logdir"/formula."$i"."log".tmp 2>&1
end=$(date +%s.%N) end=$(date +%s.%N)
ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))") ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo $(date --iso-8601=ns) $RESL >> "$logdir"/formula."$i"."log" echo $(date --iso-8601=ns) >> "$logdir"/formula."$i"."log"
cat "$logdir"/formula."$i"."log".tmp 2>&1 >> "$logdir"/formula."$i"."log"
echo >> "$logdir"/formula."$i"."log"
start=$(date +%s.%N) start=$(date +%s.%N)
RESS=$(./$go2pinsmc -ltl "$formula" -nb-threads $NBTHREADS -backend spot 2>&1) timeout $TIMEOUT ./$go2pinsmc -ltl "$formula" -nb-threads $NBTHREADS -backend spot > "$logdir"/formula."$i"."log".tmp 2>&1
end=$(date +%s.%N) end=$(date +%s.%N)
spot_time=$(python -c "print ('%.3f' % (${end} - ${start}))") spot_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo $(date --iso-8601=ns) $RESS >> "$logdir"/formula."$i"."log" echo $(date --iso-8601=ns) >> "$logdir"/formula."$i"."log"
cat "$logdir"/formula."$i"."log".tmp 2>&1 >> "$logdir"/formula."$i"."log"
echo >> "$logdir"/formula."$i"."log"
echo " [formulae $i] spot:$spot_time,ltsmin:$ltsmin_time $bb" status=$(cat "$logdir"/formula."$i"."log" | grep "not_empty")
status=$(cat "$logdir"/formula."$i"."log" | grep "an accepting run exists")
if [ -z "$status" ]; then if [ -z "$status" ]; then
status="EMPTY" status="EMPTY"
else else
status="NOTEMPTY" status="NOTEMPTY"
fi fi
ltsmin_st=$(cat "$logdir"/formula."$i"."log" | grep dve2lts-mc |grep Explored| tail -n 1 |awk '{print $5}')
echo "$model,$status,$spot_time,$ltsmin_time,$formula">> $tmpfile ltsmin_tr=$(cat "$logdir"/formula."$i"."log" | grep dve2lts-mc |grep Explored| tail -n 1 |awk '{print $7}')
echo $(date --iso-8601=ns) "$model,$status,$spot_time,$ltsmin_time,$formula">> "$logdir"/formula."$i"."log"
spot_st=$(cat "$logdir"/formula."$i"."log" | grep '^#' | awk -F',' '{print $6}')
spot_tr=$(cat "$logdir"/formula."$i"."log" | grep '^#' | awk -F',' '{print $7}')
echo " [formulae $i] $status spot:$spot_time ($spot_st st,$spot_tr tr),ltsmin:$ltsmin_time ($ltsmin_st st,$ltsmin_tr tr) $bb"
echo "$model,$status,$spot_time,$ltsmin_time,$spot_st,$spot_tr,$ltsmin_st,$ltsmin_tr,$formula">> $tmpfile
echo $(date --iso-8601=ns) "$model,$status,$spot_time,$ltsmin_time,$spot_st,$spot_tr,$ltsmin_st,$ltsmin_tr,$formula">> "$logdir"/formula."$i"."log"
rm "$logdir"/formula."$i"."log".tmp
i=$((i+1)) i=$((i+1))
done < $formulae done < $formulae
......
...@@ -41,57 +41,61 @@ do ...@@ -41,57 +41,61 @@ do
fi; fi;
echo $formula > $formulatmp echo $formula > $formulatmp
/usr/bin/time -o "$transpile" -v ../go2pins -f -o "$dir"/blackbox -blackbox-fn="auto" -rers -formulae $formulatmp $model > /dev/null 2>&1 ../go2pins -f -o "$dir"/blackbox -blackbox-fn="auto" -rers -formulae $formulatmp $model >> "$logdir"/formula."$i".bb."log" 2>&1
TRANSPILE_TIME=$(grep "User time" $transpile | awk '{print $4}') TRANSPILE_TIME=$(grep "transpilation time:" "$logdir"/formula."$i".bb."log" | awk '{print $3}')
TRANSPILE_MEMORY=$(grep "Maximum resident" $transpile | awk '{print $6}') COMPILE_TIME=$(grep "compilation time:" "$logdir"/formula."$i".bb."log" | awk '{print $3}')
./"$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=$(basename -- "$model")
filename="${filename%.*}" filename="${filename%.*}"
# Compute LTSmin and Spot resolution time # Compute LTSmin Spot resolution time
LTSMIN_F=$(echo $formula | sed 's/"//g') LTSMIN_F=$(echo $formula | sed 's/"//g')
start=$(date +%s.%N) start=$(date +%s.%N)
RESL=$(./"$dir"/blackbox/go2pins-mc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin 2>&1) timeout $TIMEOUT ./"$dir"/blackbox/go2pins-mc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin > "$logdir"/formula."$i".bb."log".tmp 2>&1
echo $(date --iso-8601=ns) $RESL >> "$logdir"/formula."$i".bb."log"
end=$(date +%s.%N) end=$(date +%s.%N)
ltsmin_timeblackbox=$(python -c "print ('%.3f' % (${end} - ${start}))") ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo $(date --iso-8601=ns) >> "$logdir"/formula."$i".bb."log"
cat "$logdir"/formula."$i".bb."log".tmp 2>&1 >> "$logdir"/formula."$i".bb."log"
echo >> "$logdir"/formula."$i".bb."log"
start=$(date +%s.%N) start=$(date +%s.%N)
RESS=$(./"$dir"/blackbox/go2pins-mc -ltl "$formula" -nb-threads $NBTHREADS -backend spot 2>&1) timeout $TIMEOUT ./"$dir"/blackbox/go2pins-mc -ltl "$formula" -nb-threads $NBTHREADS -backend spot > "$logdir"/formula."$i".bb."log".tmp 2>&1
end=$(date +%s.%N) end=$(date +%s.%N)
spot_timeblackbox=$(python -c "print ('%.3f' % (${end} - ${start}))") spot_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo $(date --iso-8601=ns) $RESS >> "$logdir"/formula."$i".bb."log" echo $(date --iso-8601=ns) >> "$logdir"/formula."$i".bb."log"
cat "$logdir"/formula."$i".bb."log".tmp 2>&1 >> "$logdir"/formula."$i".bb."log"
echo >> "$logdir"/formula."$i".bb."log"
echo " [formulae $i] blackbox: spot:$spot_timeblackbox, ltsmin:$ltsmin_timeblackbox, states: $ST, transitions: $TR" mystatus=$(cat "$logdir"/formula."$i".bb."log" | grep "not_empty")
if [ -z "$mystatus" ]; then
mystatus="EMPTY"
else
mystatus="NOTEMPTY"
fi
ltsmin_st=$(cat "$logdir"/formula."$i".bb."log" | grep dve2lts-mc |grep Explored| tail -n 1 |awk '{print $4}')
ltsmin_tr=$(cat "$logdir"/formula."$i".bb."log" | grep dve2lts-mc |grep Explored| tail -n 1 |awk '{print $6}')
if [ "$status" == "EMPTY" ]; then spot_st=$(cat "$logdir"/formula."$i".bb."log" | grep '^#' | awk -F',' '{print $6}')
TMP=$(echo $RESS | grep "no accepting run found") spot_tr=$(cat "$logdir"/formula."$i".bb."log" | grep '^#' | awk -F',' '{print $7}')
echo " [formulae $i] $mystatus spot:$spot_time ($spot_st st,$spot_tr tr),ltsmin:$ltsmin_time ($ltsmin_st st,$ltsmin_tr tr) $bb"
if [ "$TMP" != "" ]; then
echo " Checking for Correctness: OK"
else
echo " Checking for Correctness: KO"
echo FAIL: $model $2
exit 1
fi
else
TMP=$(echo $RESS | grep "an accepting run exists")
if [ "$TMP" != "" ]; then
echo " Checking for Correctness: OK"
else
echo " Checking for Correctness: KO"
echo FAIL: $model $2
exit 1
fi
if [ "$status" = "$mystatus" ]; then
echo " Checking for Correctness: OK"
else
echo " Checking for Correctness: KO"
echo FAIL: $model $formula
exit 1
fi fi
echo "$model,$mystatus,$spot_time,$ltsmin_time,$spot_st,$spot_tr,$ltsmin_st,$ltsmin_tr,$formula">> $tmpfile
echo $(date --iso-8601=ns) "$model,$mystatus,$spot_time,$ltsmin_time,$spot_st,$spot_tr,$ltsmin_st,$ltsmin_tr,$formula">> "$logdir"/formula."$i".bb."log"
rm "$logdir"/formula."$i".bb."log".tmp
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)) i=$((i+1))
done < $model.formulae.txt done < $model.formulae.txt
......
...@@ -36,45 +36,56 @@ do ...@@ -36,45 +36,56 @@ do
continue continue
fi; fi;
# Compute LTSmin and Spot resolution time
filename=$(basename -- "$model")
filename="${filename%.*}"
# Compute LTSmin Spot resolution time
LTSMIN_F=$(echo $formula | sed 's/"//g') LTSMIN_F=$(echo $formula | sed 's/"//g')
start=$(date +%s.%N) start=$(date +%s.%N)
RESL=$(./$go2pinsmc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin 2>&1) timeout $TIMEOUT ./$go2pinsmc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin > "$logdir"/formula."$i"."log".tmp 2>&1
end=$(date +%s.%N) end=$(date +%s.%N)
ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))") ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo $(date --iso-8601=ns) $RESL >> "$logdir"/formula."$i"."log" echo $(date --iso-8601=ns) >> "$logdir"/formula."$i"."log"
cat "$logdir"/formula."$i"."log".tmp 2>&1 >> "$logdir"/formula."$i"."log"
echo >> "$logdir"/formula."$i"."log"
start=$(date +%s.%N) start=$(date +%s.%N)
RESS=$(./$go2pinsmc -ltl "$formula" -nb-threads $NBTHREADS -backend spot 2>&1) timeout $TIMEOUT ./$go2pinsmc -ltl "$formula" -nb-threads $NBTHREADS -backend spot > "$logdir"/formula."$i"."log".tmp 2>&1
end=$(date +%s.%N) end=$(date +%s.%N)
spot_time=$(python -c "print ('%.3f' % (${end} - ${start}))") spot_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo $(date --iso-8601=ns) $RESS >> "$logdir"/ormula."$i"."log" echo $(date --iso-8601=ns) >> "$logdir"/formula."$i"."log"
cat "$logdir"/formula."$i"."log".tmp 2>&1 >> "$logdir"/formula."$i"."log"
echo >> "$logdir"/formula."$i"."log"
mystatus=$(cat "$logdir"/formula."$i"."log" | grep "not_empty")
if [ -z "$mystatus" ]; then
mystatus="EMPTY"
else
mystatus="NOTEMPTY"
fi
ltsmin_st=$(cat "$logdir"/formula."$i"."log" | grep dve2lts-mc |grep Explored| tail -n 1 |awk '{print $3}')
ltsmin_tr=$(cat "$logdir"/formula."$i"."log" | grep dve2lts-mc |grep Explored| tail -n 1 |awk '{print $5}')
echo " [formulae $i] spot:$spot_time,ltsmin:$ltsmin_time" spot_st=$(cat "$logdir"/formula."$i"."log" | grep '^#' | awk -F',' '{print $6}')
spot_tr=$(cat "$logdir"/formula."$i"."log" | grep '^#' | awk -F',' '{print $7}')
if [ "$status" == "EMPTY" ]; then echo " [formulae $i] $mystatus spot:$spot_time ($spot_st st,$spot_tr tr),ltsmin:$ltsmin_time ($ltsmin_st st,$ltsmin_tr tr) $bb"
TMP=$(echo $RESS | grep "no accepting run found")
if [ "$TMP" != "" ]; then
echo " Checking for Correctness: OK"
else
echo " Checking for Correctness: KO"
echo FAIL: $model $formula
exit 1
fi
else
TMP=$(echo $RESS | grep "an accepting run exists")
if [ "$TMP" != "" ]; then
echo " Checking for Correctness: OK"
else
echo " Checking for Correctness: KO"
echo FAIL: $model $formula
exit 1
fi
if [ "$status" = "$mystatus" ]; then
echo " Checking for Correctness: OK"
else
echo " Checking for Correctness: KO"
echo FAIL: $model $formula
exit 1
fi fi
echo "$model,$mystatus,$spot_time,$ltsmin_time,$spot_st,$spot_tr,$ltsmin_st,$ltsmin_tr,$formula">> $tmpfile
echo $(date --iso-8601=ns) "$model,$mystatus,$spot_time,$ltsmin_time,$spot_st,$spot_tr,$ltsmin_st,$ltsmin_tr,$formula">> "$logdir"/formula."$i"."log"
rm "$logdir"/formula."$i"."log".tmp
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)) i=$((i+1))
done < $model.formulae.txt 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