Commit 42f56cbf authored by Etienne Renault's avatar Etienne Renault

benchs: update scripts

parent 060775de
Pipeline #24491 passed with stage
in 2 minutes and 12 seconds
......@@ -83,47 +83,55 @@ echo
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"
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.%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
echo "##################################"
echo "==> Benchmark for Reachability"
echo "==> Benchmark for Reachability / Correctness"
echo "##################################"
echo
......@@ -136,9 +144,7 @@ for model in $FILES; do
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')
......@@ -147,6 +153,10 @@ for model in $FILES; do
../go2pins -f -o $filename -rers "$rers_inputs" $model > /dev/null 2>&1
echo -e "==> Processing $model"
while read -r status formulae
do
# Compute Spot resolution time
LTSMIN_F=$(echo $formulae | sed 's/"//g')
start=$(date +%s.%N)
......@@ -164,6 +174,7 @@ for model in $FILES; do
if [ "$status" == "EMPTY" ]; then
TMP=$(echo $RESS | grep "no accepting run found")
if [ "$TMP" != "" ]; then
echo " Checking for Correctness: OK"
else
......
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