Commit 0b70b79e authored by Hugo Moreau's avatar Hugo Moreau Committed by Etienne Renault
Browse files

Bench: building blackbox separately

To preserve a nice workflow and tracking more efficiently when Makefile
can possibly fail. The current workflow is LTL files, Reach files, LTL
files blackboxed, Reach files blackboxed.
parent 57f35423
......@@ -37,13 +37,16 @@ ${REACHGLOBAL}: ${REACHGLOBAL}
blackbox: ${OUTPUT_BB}
${OUTPUT_BB}: ${LTLBB}
@echo "model,transpile_time,transpile_memory,states,transitions,blackbox_spot_time,blackbox_ltsmin_time" > $@
${OUTPUT_BB}: ${LTLBB} ${REACHBB}
@echo "model,isempty,transpile_time,transpile_memory,states,transitions,blackbox_spot_time,blackbox_ltsmin_time" > $@
@if [ ! -z $< ]; then\
tail -q -n +2 $< >> $@;\
fi
${LTLBB}: ${LTLOUTPUT}
${LTLBB}: %-ltl/${OUTPUT_BB}: RERS/%-ltl.go.formulae.txt RERS/%-ltl.go %-ltl
@echo Processing blackbox $<
@./run-ltl-bb.sh $@ $^ ${NBTHREADS}
@echo End of Processing blackbox
${OUTPUT_LTL}: ${LTLOUTPUT}
@echo "model,isempty,spottime,ltsmintime,formulae" > $@
......@@ -67,6 +70,11 @@ ${LTLOUTPUT}: %-ltl/${OUTPUT_LTL}: RERS/%-ltl.go.formulae.txt RERS/%-ltl.go %-lt
%-ltl:
@mkdir $@
${REACHBB}: %-reach/${OUTPUT_BB}: RERS/%-reach.go %-reach
@echo Processing blackbox $< if it exists
@./run-reach-bb.sh $@ $^ ${NBTHREADS}
@echo End of Processing blackbox
${OUTPUT_REACH}: ${REACHOUTPUT}
@echo "model,isempty,spottime,ltsmintime,formulae" > $@
@if [ ! -z $< ]; then\
......
#!/bin/zsh
i=0
save=$1
formulae=$2
model=$3
dir=$4
NBTHREADS=$5
if [ -f "$save" ]; then
exit 0
fi
tmpfile="$save".tmp
formulatmp="$dir"/formula.tmp
transpile="$dir"/transpile.tmp
kripke="$dir"/kripke.tmp
kripkestate="$kripke".state
if [ ! -f "$tmpfile" ]; then
echo "model,isempty,transpile_time,transpile_memory,states,transitions,blackbox_spot_time,blackbox_ltsmin_time" > $tmpfile
fi
blackbox() {
echo $1 > $formulatmp
/usr/bin/time -o "$transpile" -v ../go2pins -f -o "$dir"/blackbox -blackbox-fn="auto" -rers -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 | grep "states" | grep -o "[0-9]\+")
TR=$(cat $kripkestate | grep "transitions" | grep -o "[0-9]\+")
filename=$(basename -- "$model")
filename="${filename%.*}"
# Compute LTSmin Spot resolution time
LTSMIN_F=$(echo $1 | 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 >> "$tmpfile"
echo " [formulae $i] blackbox: spot:$spot_timeblackbox, ltsmin:$ltsmin_timeblackbox, states: $ST, transitions: $TR"
}
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;
blackbox $formula
i=$((i+1))
done < $formulae
cp $tmpfile $save
rm $tmpfile
......@@ -19,45 +19,6 @@ 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
......@@ -85,7 +46,6 @@ do
end=$(date +%s.%N)
spot_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
bb=$(blackbox $formula)
echo " [formulae $i] spot:$spot_time,ltsmin:$ltsmin_time $bb"
......@@ -94,5 +54,4 @@ do
done < $formulae
cp $tmpfile $save
cp $tmpblackboxcsv $blackbox
rm $tmpfile $tmpblackboxcsv
rm $tmpfile
# /bin/zsh
i=0
save=$1
model=$2
dir=$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
formulatmp="$dir"/formula.tmp
transpile="$dir"/transpile.tmp
kripke="$dir"/kripke.tmp
kripkestate="$kripke".state
if [ ! -f "$tmpfile" ]; then
echo "model,isempty,transpile_time,transpile_memory,states,transitions,blackbox_spot_time,blackbox_ltsmin_time" > $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;
echo $formula > $formulatmp
/usr/bin/time -o "$transpile" -v ../go2pins -f -o "$dir"/blackbox -blackbox-fn="auto" -rers -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 | grep "states" | grep -o "[0-9]\+")
TR=$(cat $kripkestate | grep "transitions" | grep -o "[0-9]\+")
filename=$(basename -- "$model")
filename="${filename%.*}"
# Compute LTSmin and 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 "$formula" -nb-threads $NBTHREADS -backend spot 2>&1)
end=$(date +%s.%N)
spot_timeblackbox=$(python -c "print ('%.3f' % (${end} - ${start}))")
echo " [formulae $i] blackbox: spot:$spot_timeblackbox, ltsmin:$ltsmin_timeblackbox, states: $ST, transitions: $TR"
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 $2
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 $2
exit 1
fi
fi
echo $model,$status,$TRANSPILE_TIME, $TRANSPILE_MEMORY, $ST, $TR, $spot_timeblackbox, $ltsmin_timeblackbox >> "$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