Skip to content

GitLab

Commit 282677c7 authored by Hugo Moreau's avatar Hugo Moreau
Browse files

Benchmark: Basic LTL and REACH Makefile 

By invoking the make command in benchs, you can now generate a benchmark
for basic LTL and REACH RERS files.

 * benchs/Makefile,
   benchs/run-ltl.sh,
   benchs/run-reach.sh: Here.
parent 664550b9
Pipeline #27196 passed with stage
in 2 minutes and 25 seconds
Hide whitespace changes
Inline Side-by-side
benchs/Makefile 0 → 100644
View file @ 282677c7
GO2PINS=../go2pins
NBTHREADS?=1
OUTPUT=benchs-${NBTHREADS}.csv
OUTPUT_BB=benchs-bb-${NBTHREADS}.csv
OUTPUT_REACH=benchs-reach-${NBTHREADS}.csv
OUTPUT_LTL=benchs-ltl-${NBTHREADS}.csv
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
LTLDIR=${LTLFILES:RERS/%.go=%}
LTLOUTPUT=${LTLDIR:%=%/${OUTPUT_LTL}}
REACHFILES=RERS/2016-Problem10-reach.go RERS/2016-Problem11-reach.go RERS/2016-Problem12-reach.go RERS/2016-Problem14-reach.go RERS/2016-Problem15-reach.go RERS/2017-Problem10-reach.go RERS/2017-Problem11-reach.go RERS/2017-Problem12-reach.go RERS/2017-Problem14-reach.go RERS/2017-Problem15-reach.go RERS/2018-Problem10-reach.go RERS/2018-Problem11-reach.go RERS/2019-Problem11-reach.go RERS/2019-Problem12-reach.go RERS/2019-Problem14-reach.go RERS/2019-Problem15-reach.go
REACHDIR=${REACHFILES:RERS/%.go=%}
REACHOUTPUT=${REACHDIR:%=%/${OUTPUT_REACH}}
all: ${OUTPUT_LTL} ${OUTPUT_REACH}
@echo "Benchs is over using ${NBTHREADS} thread(s):"
@#echo -e "\t- All values: ${OUTPUT}"
@#echo -e "\t- Blackbox evaluations: ${OUTPUT_BB}"
@echo -e "\t- Reachability evaluations: ${OUTPUT_REACH}"
@echo -e "\t- LTL evaluations: ${OUTPUT_LTL}"
${OUTPUT_LTL}: ${LTLOUTPUT}
@echo "model,isempty,spottime,ltsmintime,formulae" > $@
@tail -q -n +2 $< >> $@
${LTLOUTPUT}: %-ltl/${OUTPUT_LTL}: RERS/%-ltl.go.formulae.txt RERS/%-ltl.go %-ltl/output/go2pins-mc
@echo Processing $<
@./run-ltl.sh $@ $^ ${NBTHREADS}
@echo End of processing $<
%-ltl/output/go2pins-mc: %-ltl
@if [ ! -f $@ ]; then\
echo Building RERS/$<.go output;\
${GO2PINS} -f -o $</output -rers RERS/$<.go > /dev/null 2>&1;\
echo End of building RERS/$<.go, use $@;\
fi
%-ltl:
@mkdir $@
${OUTPUT_REACH}: ${REACHOUTPUT}
@echo "model,isempty,spottime,ltsmintime,formulae" > $@
@tail -q -n +2 $< >> $@
${REACHOUTPUT}: %-reach/${OUTPUT_REACH}: RERS/%-reach.go %-reach/output/go2pins-mc
@echo Processing $<.formulae.txt if it exists
@./run-reach.sh $@ $^ ${NBTHREADS}
@echo End of processing $<
%-reach/output/go2pins-mc: %-reach
@if [ ! -f $@ ]; then\
echo Building RERS/$<.go output;\
${GO2PINS} -f -o $</output -rers RERS/$<.go > /dev/null 2>&1;\
echo End of building RERS/$<.go, use $@;\
fi
%-reach:
@mkdir $@
clean:
rm -rf ${LTLDIR} ${REACHDIR}
distclean:
rm -rf ${OUTPUT} ${OUTPUT_LTL} ${OUTPUT_REACH} ${OUTPUT_BB}
.PRECIOUS: ${LTLDIR} ${REACHDIR}
.PHONY: all clean
benchs/run-ltl.sh 0 → 100755
View file @ 282677c7
# /bin/zsh
i=0
save=$1
formulae=$2
model=$3
go2pins=$4
NBTHREADS=$5
if [ -f "$save" ]; then
exit 0
fi
tmpfile="$save".tmp
if [ ! -f "$tmpfile" ]; then
echo "model,isempty,spottime,ltsmintime,formulae" > $tmpfile
fi
while read -r formula
do
# Detect the number of lines and skip already computed formulae
LOC=$(wc -l $tmpfile | awk '{print $1}' )
tmp=$((i+2))
if [ "$tmp" -lt "$LOC" ]; then
echo " [SKIP] formulae $i"
i=$((i+1))
continue
fi;
filename=$(basename -- "$model")
filename="${filename%.*}"
# Compute LTSmin Spot resolution time
LTSMIN_F=$(echo $formula | sed 's/"//g')
start=$(date +%s.%N)
RESL=$(./$go2pins -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin 2>&1)
end=$(date +%s.%N)
ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
start=$(date +%s.%N)
RESS=$(./$go2pins -ltl "$formula" -nb-threads $NBTHREADS -backend spot 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,$formula">> $tmpfile
i=$((i+1))
done < $formulae
cp $tmpfile $save
rm $tmpfile
benchs/run-reach.sh 0 → 100755
View file @ 282677c7
# /bin/zsh
i=0
save=$1
model=$2
go2pins=$3
NBTHREADS=$4
if [ ! -f "$model.formulae.txt" ]; then
echo "No specifications for $model" > $save
exit 0
fi
if [ -f "$save" ]; then
exit 0
fi
tmpfile="$save".tmp
if [ ! -f "$tmpfile" ]; then
echo "model,isempty,spottime,ltsmintime,formulae" > $tmpfile
fi;
while read -r status formula
do
# Detect the number of lines and skip already computed formulae
LOC=$(wc -l $tmpfile | awk '{print $1}' )
tmp=$((i+2))
if [ "$tmp" -lt "$LOC" ]; then
echo " [SKIP] formulae $i"
i=$((i+1))
continue
fi;
# Compute LTSmin and Spot resolution time
LTSMIN_F=$(echo $formula | sed 's/"//g')
start=$(date +%s.%N)
RESL=$(./$go2pins -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin 2>&1)
end=$(date +%s.%N)
ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
start=$(date +%s.%N)
RESS=$(./$go2pins -ltl "$formula" -nb-threads $NBTHREADS -backend spot 2>&1)
end=$(date +%s.%N)
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 $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
fi
echo "$model,$status,$spot_time,$ltsmin_time,$formulae">> $tmpfile
i=$((i+1))
done < $model.formulae.txt
cp $tmpfile $save
rm $tmpfile
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