55ee18b96a
* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Record statistics about intermediate automata if SPOT_SATLOG is set to some filename, and display intermediate automata if SPOT_SATSHOW is set. * bench/dtgbasat/stat.sh, bench/dtgbasat/stats.sh, bench/dtgbasat/tabl.pl, bench/dtgbasat/tabl1.pl, bench/dtgbasat/tabl2.pl, bench/dtgbasat/tabl3.pl, bench/dtgbasat/tabl4.pl: Gather these extra statistics.
107 lines
4.1 KiB
Bash
Executable file
107 lines
4.1 KiB
Bash
Executable file
#!/bin/sh
|
|
|
|
ltlfilt=../../src/bin/ltlfilt
|
|
ltl2tgba=../../src/bin/ltl2tgba
|
|
dstar2tgba=../../src/bin/dstar2tgba
|
|
timeout='timeout -sKILL 2h'
|
|
stats=--stats="%s, %e, %t, %a, %c, %d, %p, %r"
|
|
empty='-, -, -, -, -, -, -, -'
|
|
tomany='!, !, !, !, !, !, !, !'
|
|
dbamin=${DBA_MINIMIZER-/home/adl/projs/dbaminimizer/minimize.py}
|
|
|
|
get_stats()
|
|
{
|
|
type=$1
|
|
shift
|
|
SPOT_SATLOG=$n.$type.satlog $timeout "$@" "$stats" > stdin.$$ 2>stderr.$$
|
|
if grep -q 'INT_MAX' stderr.$$; then
|
|
# Too many SAT-clause?
|
|
echo "$tomany"
|
|
else
|
|
tmp=`cat stdin.$$`
|
|
echo ${tmp:-$empty}
|
|
fi
|
|
rm -f stdin.$$ stderr.$$
|
|
}
|
|
|
|
get_dbamin_stats()
|
|
{
|
|
tmp=`./rundbamin.pl $timeout $dbamin "$@"`
|
|
mye='-, -'
|
|
echo ${tmp:-$mye}
|
|
}
|
|
|
|
n=$1
|
|
f=$2
|
|
type=$3
|
|
accmax=$4
|
|
|
|
case $type in
|
|
*WDBA*)
|
|
echo "$f, $accmax, $type..." 1>&2
|
|
input=`get_stats BA $ltl2tgba "$f" -BD`
|
|
dba=$input
|
|
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA..." 1>&2
|
|
mindba=`get_stats DBA $ltl2tgba "$f" -BD -x 'sat-minimize=-1'`
|
|
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA..." 1>&2
|
|
mindtgba=`get_stats DTGBA $ltl2tgba "$f" -D -x 'sat-minimize=-1'`
|
|
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA..." 1>&2
|
|
mindtba=`get_stats DTBA $ltl2tgba "$f" -D -x 'sat-minimize=-1,sat-acc=1'`
|
|
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA, $mindtba, dbaminimizer..." 1>&2
|
|
$ltlfilt --remove-wm -f "$f" -l |
|
|
ltl2dstar --ltl2nba=spin:$ltl2tgba@-sD - dra.$$
|
|
dbamin=`get_dbamin_stats dra.$$`
|
|
dra=`sed -n 's/States: \(.*\)/\1/p' dra.$$`
|
|
rm dra.$$
|
|
;;
|
|
*TCONG*|*trad*) # Not in WDBA
|
|
echo "$f, $accmax, $type..." 1>&2
|
|
input=`get_stats TBA $ltl2tgba "$f" -D -x '!wdba-minimize,tba-det'`
|
|
echo "$f, $accmax, $type, $input, DBA, ..." 1>&2
|
|
dba=`get_stats BA $ltl2tgba "$f" -BD -x '!wdba-minimize,tba-det'`
|
|
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA..." 1>&2
|
|
mindba=`get_stats DBA $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize'`
|
|
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA..." 1>&2
|
|
mindtgba=`get_stats DTGBA $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize'`
|
|
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA..." 1>&2
|
|
mindtba=`get_stats DTBA $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize,sat-acc=1'`
|
|
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA, $mindtba, dbaminimizer..." 1>&2
|
|
case $type in
|
|
*TCONG*) dbamin="n/a, n/a" dra="n/a";;
|
|
*trad*)
|
|
$ltlfilt --remove-wm -f "$f" -l |
|
|
ltl2dstar --ltl2nba=spin:$ltl2tgba@-sD - dra.$$
|
|
dbamin=`get_dbamin_stats dra.$$`
|
|
dra=`sed -n 's/States: \(.*\)/\1/p' dra.$$`
|
|
rm dra.$$
|
|
;;
|
|
esac
|
|
;;
|
|
*DRA*)
|
|
echo "$f, $accmax, $type... " 1>&2
|
|
$ltlfilt --remove-wm -f "$f" -l |
|
|
ltl2dstar --ltl2nba=spin:$ltl2tgba@-sD - dra.$$
|
|
input=`get_stats TBA $dstar2tgba dra.$$ -D -x '!wdba-minimize'`
|
|
echo "$f, $accmax, $type, $input, DBA, ... " 1>&2
|
|
dba=`get_stats BA $dstar2tgba dra.$$ -BD -x '!wdba-minimize'`
|
|
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA... " 1>&2
|
|
mindba=`get_stats DBA $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize'`
|
|
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA..." 1>&2
|
|
mindtgba=`get_stats DTGBA $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-acc='$accmax`
|
|
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA..." 1>&2
|
|
mindtba=`get_stats DTBA $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-acc=1'`
|
|
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA, $mindtba, dbaminimizer..." 1>&2
|
|
dbamin=`get_dbamin_stats dra.$$`
|
|
dra=`sed -n 's/States: \(.*\)/\1/p' dra.$$`
|
|
rm -f dra.$$
|
|
;;
|
|
*not*)
|
|
exit 0
|
|
;;
|
|
*)
|
|
echo "SHOULD NOT HAPPEND"
|
|
exit 2
|
|
;;
|
|
esac
|
|
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA, $mindtba, dbaminimizer, $dbamin, DRA, $dra, $n" 1>&2
|
|
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA, $mindtba, dbaminimizer, $dbamin, DRA, $dra, $n"
|