Commit b9f2a12f authored by Etienne Renault's avatar Etienne Renault

benchs: restore transpilation

* benchs/run-benchmark.sh: Here.
parent 42f56cbf
Pipeline #24493 passed with stage
in 2 minutes and 23 seconds
......@@ -85,46 +85,46 @@ echo "model,isempty,spottime,ltsmintime,formulae" > $OUTPUT_LTL
echo First, we transpile only once every model. This may take some time.
i=0
# for model in $LTLFILES; do
# echo -e "==> Processing $model"
# 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
# done
# 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%.*}"
# # Compute Spot resolution time
# LTSMIN_F=$(echo $formulae | sed 's/"//g')
# start=$(date +%s.%N)
# RESL=$($filename/go2pins-mc -ltl "$LTSMIN_F" -backend ltsmin 2>&1)
# end=$(date +%s.%N)
# ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
# start=$(date +%s.%N)
# RESS=$($filename/go2pins-mc -ltl "$formulae" 2>&1)
# end=$(date +%s.%N)
# 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
for model in $LTLFILES; do
echo -e "==> Processing $model"
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
done
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%.*}"
# Compute Spot resolution time
LTSMIN_F=$(echo $formulae | sed 's/"//g')
start=$(date +%s.%N)
RESL=$($filename/go2pins-mc -ltl "$LTSMIN_F" -backend ltsmin 2>&1)
end=$(date +%s.%N)
ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
start=$(date +%s.%N)
RESS=$($filename/go2pins-mc -ltl "$formulae" 2>&1)
end=$(date +%s.%N)
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
......
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