Commit 85c0e480 authored by Etienne Renault's avatar Etienne Renault
Browse files

benchs: add part about LTL

*  benchs/run-benchmark.sh: Here.
parent a48adae0
Pipeline #24382 passed with stage
in 5 minutes and 35 seconds
......@@ -25,6 +25,34 @@
# category "Sequential Reachability Problems/data structures, hard" since
# they require complex array manipulation that are not yet supported by
# the Go2Pins tool.
LTLFILES="RERS/2016-Problem1-ltl.go \
RERS/2016-Problem2-ltl.go \
RERS/2016-Problem4-ltl.go \
RERS/2016-Problem5-ltl.go \
RERS/2016-Problem7-ltl.go \
RERS/2017-Problem1-ltl.go \
RERS/2017-Problem2-ltl.go \
RERS/2017-Problem4-ltl.go \
RERS/2017-Problem5-ltl.go \
RERS/2017-Problem7-ltl.go \
RERS/2018-Problem1-ltl.go \
RERS/2018-Problem2-ltl.go \
RERS/2018-Problem4-ltl.go \
RERS/2018-Problem5-ltl.go \
RERS/2018-Problem7-ltl.go \
RERS/2019-Problem1-ltl.go \
RERS/2019-Problem2-ltl.go \
RERS/2019-Problem4-ltl.go \
RERS/2019-Problem5-ltl.go \
RERS/2019-Problem7-ltl.go \
RERS/2020-Problem1-ltl.go \
RERS/2020-Problem2-ltl.go \
RERS/2020-Problem4-ltl.go \
RERS/2020-Problem5-ltl.go \
RERS/2020-Problem7-ltl.go "
FILES="RERS/2016-Problem10-reach.go \
RERS/2016-Problem11-reach.go \
RERS/2016-Problem12-reach.go \
......@@ -45,6 +73,54 @@ FILES="RERS/2016-Problem10-reach.go \
OUTPUT=benchs.csv
OUTPUT_BB=benchs-bb.csv
OUTPUT_REACH=benchs-reach.csv
OUTPUT_LTL=benchs-ltl.csv
echo "##################################"
echo "==> Benchmark for LTL evaluation"
echo "##################################"
echo
echo "model,isempty,spottime,ltsmintime,formulae" > $OUTPUT_LTL
i=0
for model in $LTLFILES; do
echo -e "==> Processing $model"
while read -r 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"
echo "$model,$status,$spot_time,$ltsmin_time,$formulae">> $OUTPUT_LTL
i=$((i+1))
done < $model.formulae.txt
done
echo
echo file : $(pwd)/$OUTPUT_LTL contains the CSV of LTL evaluation
echo "##################################"
echo "==> Benchmark for Reachability"
......
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