Commit 4eafb090 authored by Hugo Moreau's avatar Hugo Moreau
Browse files

Bench: LTL blackbox

parent 65c5bf7b
Pipeline #27333 passed with stage
in 2 minutes and 24 seconds
......@@ -11,12 +11,13 @@ LTLFILES=RERS/2016-Problem1-ltl.go RERS/2016-Problem2-ltl.go RERS/2016-Problem4-
LTLDIR=${LTLFILES:RERS/%.go=%}
LTLOUTPUT=${LTLDIR:%=%/${OUTPUT_LTL}}
LTLGLOBAL=${LTLDIR:%=%/global.csv}
LTLBB=${LTLDIR:%=%/${OUTPUT_BB}}
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}}
REACHGLOBAL=${REACHDIR:%=%/global.csv}
REACHBB=${REACHDIR:%=%/${OUTPUT_BB}}
all: ${OUTPUT_LTL} ${OUTPUT_REACH} ${OUTPUT}
@echo "Benchs is over using ${NBTHREADS} thread(s):"
......@@ -31,13 +32,26 @@ ${OUTPUT}: ${LTLGLOBAL} ${REACHGLOBAL}
tail -q -n +2 $^ >> $@;\
fi
${LTLGLOBAL}: ${LTLOUTPUT}
${REACHGLOBAL}: ${REACHGLOBAL}
blackbox: ${OUTPUT_BB}
${OUTPUT_BB}: ${LTLBB}
@echo "model,transpile_time,transpile_memory,states,transitions,blackbox_spot_time,blackbox_ltsmin_time" > $@
@ if [ -f $< ]; then\
tail -q -n +2 $< >> $@;\
fi
${LTLBB}: ${LTLOUTPUT}
${OUTPUT_LTL}: ${LTLOUTPUT}
@echo "model,isempty,spottime,ltsmintime,formulae" > $@
@if [ -f $< ]; then\
tail -q -n +2 $< >> $@;\
fi
${LTLOUTPUT}: %-ltl/${OUTPUT_LTL}: RERS/%-ltl.go.formulae.txt RERS/%-ltl.go %-ltl/output/go2pins-mc
${LTLOUTPUT}: %-ltl/${OUTPUT_LTL}: RERS/%-ltl.go.formulae.txt RERS/%-ltl.go %-ltl/output/go2pins-mc %-ltl
@echo Processing $<
@./run-ltl.sh $@ $^ ${NBTHREADS}
@echo End of processing $<
......
......@@ -5,8 +5,8 @@ save=$1
formulae=$2
model=$3
go2pinsmc=$4
NBTHREADS=$5
dir=$5
NBTHREADS=$6
if [ -f "$save" ]; then
......@@ -19,6 +19,46 @@ if [ ! -f "$tmpfile" ]; then
echo "model,isempty,spottime,ltsmintime,formulae" > $tmpfile
fi
blackboxcsv="$dir"/blackbox.csv
formulatmp="$dir"/formula.tmp
tmpblackboxcsv="$blackboxcsv".tmp
transpile="$dir"/transpile.tmp
kripke="$dir"/kripke.tmp
kripkestate="$kripke".state
if [ ! -f "$tmpblackboxcsv" ]; then
echo "model,transpile_time,transpile_memory,states,transitions,blackbox_spot_time,blackbox_ltsmin_time" > $tmpblackboxcsv
fi
blackbox() {
echo $1 > $formulatmp
/usr/bin/time -o "$transpile" -v ../go2pins -f -o "$dir"/blackbox -blackbox-fn="auto" -formulae $formulatmp $model > /dev/null 2>&1
TRANSPILE_TIME=$(grep "User time" $transpile | awk '{print $4}')
TRANSPILE_MEMORY=$(grep "Maximum resident" $transpile | awk '{print $6}')
./"$dir"/blackbox/go2pins-mc -kripke-size > $kripkestate
ST=$(cat $kripkestate | awk -F',' '{print $2}')
TR=$(cat $kripkestate | awk -F',' '{print $3}')
filename=$(basename -- "$model")
filename="${filename%.*}"
# Compute LTSmin Spot resolution time
LTSMIN_F=$(echo $formula | sed 's/"//g')
start=$(date +%s.%N)
RESL=$(./"$dir"/blackbox/go2pins-mc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin 2>&1)
end=$(date +%s.%N)
ltsmin_timeblackbox=$(python -c "print ('%.3f' % (${end} - ${start}))")
start=$(date +%s.%N)
RESS=$(./"$dir"/blackbox/go2pins-mc -ltl "$1" -nb-threads $NBTHREADS -backend spot 2>&1)
end=$(date +%s.%N)
spot_timeblackbox=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo $model, $TRANSPILE_TIME, $TRANSPILE_MEMORY, $ST, $TR, $spot_timeblackbox, $ltsmin_timeblackbox >> "$tmpblackboxcsv"
echo "(blackbox: spot:$spot_timeblackbox, ltsmin:$ltsmin_timeblackbox)"
}
while read -r formula
do
# Detect the number of lines and skip already computed formulae
......@@ -45,7 +85,8 @@ do
end=$(date +%s.%N)
spot_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo " [formulae $i] spot:$spot_time,ltsmin:$ltsmin_time"
bb=$(blackbox $formula)
echo " [formulae $i] spot:$spot_time,ltsmin:$ltsmin_time $bb"
echo "$model,$status,$spot_time,$ltsmin_time,$formula">> $tmpfile
......@@ -53,4 +94,5 @@ do
done < $formulae
cp $tmpfile $save
rm $tmpfile
cp $tmpblackboxcsv $blackbox
rm $tmpfile $tmpblackboxcsv
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