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

benchs: include correctness specification

* benchs/run-benchmark.sh: Here.
parent 01d90331
......@@ -44,7 +44,76 @@ FILES="RERS/2016-Problem10-reach.go \
OUTPUT=benchs.csv
OUTPUT_BB=benchs-bb.csv
OUTPUT_REACH=benchs-reach.csv
echo "##################################"
echo "==> Benchmark for Reachability"
echo "##################################"
echo
echo "model,isempty,spottime,ltsmintime,formulae" > $OUTPUT_REACH
i=0
for model in $FILES; do
if [ ! -f "$model.formulae.txt" ]; then
# No full specification for this model
continue
fi
echo -e "==> Processing $model"
while read -r status formulae
do
rers_inputs=$(cat $model | grep 'var inputs \[\]int' | \
sed 's/var inputs \[\]int = \[\]int{//g' | \
sed 's/}//g' | sed 's/ *//g' | sed 's/,/;/g')
filename=$(basename -- "$model")
filename="${filename%.*}"
../go2pins -f -o $filename -rers "$rers_inputs" $model > /dev/null 2>&1
# Compute Spot resolution time
LTSMIN_F=$(echo $formulae | sed 's/"//g')
start=$(date +%s)
RESL=$($filename/go2pins-mc -ltl "$LTSMIN_F" -backend ltsmin 2>&1)
end=$(date +%s)
ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
start=$(date +%s)
RESS=$($filename/go2pins-mc -ltl "$formulae" 2>&1)
end=$(date +%s)
spot_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo " [formulae $i] spot:$spot_time,ltsmin:$ltsmin_time"
if [ "$status" == "EMPTY" ]; then
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 $formulae
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 $formulae
exit 1
fi
fi
echo "$model,$status,$spot_time,$ltsmin_time,$formulae">> $OUTPUT_REACH
i=$((i+1))
done < $model.formulae.txt
done
echo
echo file : $(pwd)/$OUTPUT_REACH contains the CSV of reachability evaluation
echo "##################################"
......
Markdown is supported
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