Commit 983feb52 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Add benchmark for our DTGBA SAT-minimization.

* bench/dtgbasat/: New directory.
* bench/Makefile.am: New file.
* configure.ac, README: Adjust.
parent 3076c3da
......@@ -188,6 +188,7 @@ doc/ Documentation for libspot.
userdoc/ HTML documentation about the command-line tools.
spot.html/ HTML reference manual for the library.
bench/ Benchmarks for ...
dtgbasat/ ... SAT-based minimization of DTGBA,
emptchk/ ... emptiness-check algorithms,
ltl2tgba/ ... LTL-to-Büchi translation algorithms,
ltlcounter/ ... translation of a class of LTL formulae,
......
......@@ -20,4 +20,4 @@
## along with this program. If not, see <http://www.gnu.org/licenses/>.
SUBDIRS = emptchk ltl2tgba scc-stats split-product ltlcounter \
ltlclasses wdba spin13
ltlclasses wdba spin13 dtgbasat
## Copyright (C) 2013 Laboratoire de Recherche et Développement de
## l'Epita (LRDE).
##
## This file is part of Spot, a model checking library.
##
## Spot is free software; you can redistribute it and/or modify it
## under the terms of the GNU General Public License as published by
## the Free Software Foundation; either version 3 of the License, or
## (at your option) any later version.
##
## Spot is distributed in the hope that it will be useful, but WITHOUT
## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
## License for more details.
##
## You should have received a copy of the GNU General Public License
## along with this program. If not, see <http://www.gnu.org/licenses/>.
EXTRA_DIST = formulas prepare.sh rundbamin.pl stat.sh stats.sh tabl.pl \
tabl1.pl tabl2.pl tabl3.pl tabl4.pl
These are the benchmark for our submission to VMCAI'14.
To reproduce, follow these instructions:
1) Compile Spot and install if it is not already done.
2) Compile Glucose from https://www.lri.fr/~simon/?page=glucose
and make sure the 'glucose' binary is in your PATH.
3) Compile ltl2dstar from http://www.ltl2dstar.de/ and
make sure the 'ltl2dstar' binary is in your path.
4) Compile DBAminimizer from
http://www.react.uni-saarland.de/tools/dbaminimizer
and define the path to minimize.py with
% export DBA_MINIMIZER=$HOME/dbaminimizer/minimize.py
5) Then make sure you are in this directory:
% cd bench/dtgbasat/
6) Classify the set of formulas with
% ./prepare.sh
This will read the formulas from file "formulas" and output a file
"info.ltl", in which each formula is associated to a class (the ①,
②, ②, and ④ of the paper), and a number of acceptance conditions
(the "m" of the paper).
7) Build a makefile to run all experiments
% ./stats.sh
8) You may optionally change the directory that contains temporary
files with
% export TMPDIR=someplace
(These temporary files can be several GB large.)
Note that runtime will be limited to 2h, but memory is not bounded.
You should set such a limit with "ulimit" if you like. For instance
% ulimit -v 41943040
9) Actually run all experiments
% make -j4 stat.mk
This will build a CSV file called "all.log".
10) You may generate LaTeX code for the tables with the scripts:
- tabl.pl: Full data.
- tabl1.pl, tabl2.pl, tabl3.pl, tabl4.pl: Partial tables as shown
in the paper.
All these script takes the CSV file all.log as first argument, and
output LaTeX to their standard output.
For more instruction about how to use ltl2tgba and dstar2tgba to
compute minimal DTGBA or DTBA, please read doc/userdoc/satmin.html
# Formulas from Gasier et al., "Rabinizer: Small deterministic
# automata for LTL(F,G)" (ATVA'12)
G(a | Fb)
FGa | FGb | GFc
F(a | b)
GF(a | b)
G(a | Fa)
G(a | b | c)
G(a | F(b | c))
Fa | Gb
G(a | F(b & c))
FGa | GFb
GF(a | b) & GF(b | c)
FF(a & G!a) | (GG!a & Fa)
GFa & FGb
(GFa & FGb) | (FG!a & GF!b)
FGa & GFa
G(Fa & Fb)
Fa & F!a
G(b | GFa) & G(c | GF!a) | Gb | Gc
G(b | FGa) & G(c | FG!a) | Gb | Gc
F(b & FGa) | F(c & FG!a) & Fb & Fc
F(b & GFa) | F(c & GF!a) & Fb & Fc
GFa -> GFb
(GFa -> GFb) & (GFc -> GFd)
GF(Fa | GFb | FG(a | b))
FG(Fa | GFb | FG(a | b))
FG(Fa | GFb | FG(a | b) | FGb)
# formulas from DBA minimizer
XXa
GF(a -> XXXb)
F(p & XF(q & XF(r & XFs)))
F(q & X(p U r))
F(p & X(q & XFr))
p U (q & X(r U s))
G(a -> Fb) & G(c -> Fd)
GFa & GFb
GFa | GFb | GFc
GFa
a U b U c U d
G(a -> Fb) & Gc
(Ga -> Fb) & (G!a -> F!b)
p U (q & X(r & F(s & XF(u & XF(v & XFw)))))
G(a -> Fb) & G(b -> Fc)
G(a -> Fb) & G(!a -> F!b)
GFp && GFq && GF r && GF u
GF(a <-> XXXb)
G(p -> q U r)
GF(a <-> XXb)
G!c & G(a -> Fb) & G(b -> Fc)
G(a -> XXXb)
G(a -> Fb)
G(a U b U !a U !b)
(p U q U r) || (q U r U p) || (r U p U q)
# Some random formulas that are determinizable with tba-det
X((a M F((!c & !b) | (c & b))) W (G!c U b))
X(((a & b) R (!a U !c)) R b)
XXG(Fa U Xb)
(!a M !b) W F!c
(b & Fa & GFc) R a
(a R (b W a)) W G(!a M (c | b))
(Fa W b) R (Fc | !a)
X(G(!a M !b) | G(a | G!a))
Fa W Gb
Ga | GFb
a M G(F!b | X!a)
G!a R XFb
XF(!a | GFb)
G(F!a U !a) U Xa
(a | G(a M !b)) W Fc
Fa W Xb
X(a R ((!b & F!c) M X!a))
XG!a R Fb
GFc | (a & Fb)
X(a R (Fb R F!b))
G(Xa M Fa)
X(Gb | GFa)
X(Gc | XG((b & Ga) | (!b & F!a)))
Ga R Fb
G(a U (b | X((!c & !a) | (a & c))))
XG((G!a & F!b) | (Fa & (a | Gb)))
(a U X!a) | XG(!b & XFc)
X(G!a | GFa)
G(G!a | F!c | G!b)
# Some random formulas that should only be determinizable via dstar2tgba
# Generated with
# randltl -n -1 a b c |
# ltlfilt --remove-wm -r -u --size-min=3 --size-max=15 --syntactic-recurrence |
# ltlfilt -v --obligation |
# ../../src/bin/ltl2tgba -F - -x tba-det -D --stats='%d,%f' |
# grep 0, | head -n 30
X(Fc W b) R Fa
!b & ((Fa U b) W Xc)
G(F!c | (Fb U a))
(c R (b R Fa)) W XGb
X((Fb & XFa) R XFc)
(Ga R (F!c U b)) W b
X(!b | G(b & !a)) R F(c & Fa)
G(Fc | Ga | XXF!b)
G(F(!a & Fa) U (b U Xc))
G(F!c U X(Xb & F!b))
G(XXFa U (b | a | Fc))
G(c | F!a | (b U Xb))
G(a U X(a | (F!b U Xc)))
XF!a R F(b | (!a & F!c))
(c & Xc) R ((!b | XFc) U a)
G(Gb | (b & c) | F(!a & XXa))
G(X(Fc & Xa) M Fb)
X(!c & Fc) R (c M Fa)
G(Ga | X(Fc U (b | X!b)))
G(XXFb U (c | (!c & F!a)))
((Fc U b) R Fa) W X!a
G(a | X(a R (GFb | (Fc U a))))
(F!c R F!b) W G!a
(Fb & !b) R (!a R XFc)
F(Fb & c) W Xa
G(G!c | ((Fb U a) U c))
(Fa & XXb) R Fc
Gc R (F!a & (b U a))
(c R Fa) U X!b
GF(b & XXXFc)
# Extra ones
G(F(a & F(b & Fc)))
(GFa & GFb) | (GFc & GFd)
#!/bin/sh
ltlfilt=../../src/bin/ltlfilt
ltl2tgba=../../src/bin/ltl2tgba
dstar2tgba=../../src/bin/dstar2tgba
# Rename all formulas using a b c... suppress duplicates.
$ltlfilt -q --relabel=abc -u formulas > nodups.ltl
while read f; do
acc=`$ltl2tgba "$f" --low -a --stats="%a"`
acc2=`$ltl2tgba "$f" -D --stats="%a"`
if $ltlfilt -f "$f" --obligation >/dev/null; then
echo "$f, WDBA, $acc, $acc2"
elif test `$ltl2tgba "$f" -D --stats="%d"` = 1; then
echo "$f, trad, $acc, $acc2"
elif test `$ltl2tgba "$f" -x tba-det -D --stats="%d"` = 1; then
echo "$f, TCONG, $acc, $acc2"
elif test `$ltlfilt --remove-wm -f "$f" -l | ltl2dstar --ltl2nba=spin:$ltl2tgba@-sD - - | $dstar2tgba -D --low --stats="%d"` = 1; then
echo "$f, DRA, $acc, $acc2"
else
echo "$f, not DBA-realizable, $acc, $acc2"
fi
done < nodups.ltl | tee info.ltl
#!/usr/bin/perl -w
use strict;
use Time::HiRes;
my $start = Time::HiRes::gettimeofday();
my $res = `@ARGV` || die;
my $end = Time::HiRes::gettimeofday();
if ($res =~ /States:\s*(\d+)\w*$/som)
{
printf("%d, %f\n", $1, $end - $start);
}
else
{
printf("-, -\n");
}
#!/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()
{
$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}
}
f=$1
type=$2
accmax=$3
case $type in
*WDBA*)
echo "$f, $accmax, $type..." 1>&2
input=`get_stats $ltl2tgba "$f" -BD`
dba=$input
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA..." 1>&2
mindba=`get_stats $ltl2tgba "$f" -BD -x 'sat-minimize=-1'`
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA..." 1>&2
mindtgba=`get_stats $ltl2tgba "$f" -D -x 'sat-minimize=-1'`
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA..." 1>&2
mindtba=`get_stats $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 $ltl2tgba "$f" -D -x '!wdba-minimize,tba-det'`
echo "$f, $accmax, $type, $input, DBA, ..." 1>&2
dba=`get_stats $ltl2tgba "$f" -BD -x '!wdba-minimize,tba-det'`
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA..." 1>&2
mindba=`get_stats $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize'`
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA..." 1>&2
mindtgba=`get_stats $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 $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 $dstar2tgba dra.$$ -D -x '!wdba-minimize'`
echo "$f, $accmax, $type, $input, DBA, ... " 1>&2
dba=`get_stats $dstar2tgba dra.$$ -BD -x '!wdba-minimize'`
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA... " 1>&2
mindba=`get_stats $dstar2tgba dra.$$ -BD -x '!wdba-minimize,sat-minimize'`
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA..." 1>&2
mindtgba=`get_stats $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 $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" 1>&2
echo "$f, $accmax, $type, $input, DBA, $dba, minDBA, $mindba, minDTGBA, $mindtgba, minDTBA, $mindtba, dbaminimizer, $dbamin, DRA, $dra"
#!/bin/sh
ltlfilt=../../src/bin/ltlfilt
ltl2tgba=../../src/bin/ltl2tgba
dstar2tgba=../../src/bin/dstar2tgba
timeout='timeout -sKILL 1h'
stats=--stats="%s, %e, %t, %a, %c, %d, %p, %r"
empty='-, -, -, -, -, -, -, -'
rm -f stats.mk stats.tmp
n=1
all=
while IFS=, read f type accmax accmin; do
unset IFS
case $type in
*TCONG*)
echo "$n.log:; ./stat.sh '$f' $type $accmax >\$@" >> stats.tmp
all="$all $n.log"
n=`expr $n + 1`
echo "$n.log:; ./stat.sh '$f' DRA-CONG $accmax >\$@" >> stats.tmp
all="$all $n.log"
n=`expr $n + 1`
;;
*)
echo "$n.log:; ./stat.sh '$f' $type $accmax >\$@" >> stats.tmp
all="$all $n.log"
n=`expr $n + 1`
;;
esac
done < info.ltl
cat > stats.mk <<EOF
ALL = $all
all.log: \$(ALL)
cat \$(ALL) >\$@
EOF
cat stats.tmp >> stats.mk
echo "Now, run something like: make -j8 -f stats.mk"
#!/usr/bin/perl -w
use strict;
my $num = 0;
my @v = ();
while (<>)
{
# G(a | Fb), 1, trad, 2, 4, 8, 1, 1, 1, 1, 0.00165238, DBA, 2, 4, 8, 1, 1, 1, 1, 0.00197852, minDBA, 2, 4, 8, 1, 1, 1, 1, 0.00821457, minDTGBA, 2, 4, 8, 1, 1, 1, 1, 0.0081701
chomp;
next if /.*realizable.*/;
$v[$num] = [split /,/];
# print $v[$num]->[48], " ", $#{$v[$num]}, "\n";
# if ($#{$v[$num]} != 49)
# {
# pop $v[$num];
# push $v[$num], '-', '-';
# }
# print $v[$num]->[48], " ", $#{$v[$num]}, "\n";
++$num;
}
sub dratcong($$)
{
my ($a, $b) = @_;
return 0 if ($a =~ /.*CONG/ && $b =~ /.*CONG/);
return $a cmp $b;
}
sub mycmp()
{
my $v = dratcong($b->[2], $a->[2]);
return $v if $v;
my $n1 = lc $a->[0];
$n1 =~ s/\W//g;
my $n2 = lc $b->[0];
$n2 =~ s/\W//g;
return $n1 cmp $n2 || $a->[0] cmp $b->[0] || $b->[2] cmp $a->[2];;
}
my @w = sort mycmp @v;
print "\\documentclass{standalone}\n
\\usepackage{amsmath}
\\usepackage{colortbl}
\\definecolor{mygray}{gray}{0.75} % 1 = white, 0 = black
\\definecolor{lightgray}{gray}{0.7} % 1 = white, 0 = black
\\def\\E{\\cellcolor{mygray}}
\\def\\P{\\cellcolor{red}}
\\def\\PP{\\cellcolor{yellow}}
\\def\\F{\\mathsf{F}} % in future
\\def\\G{\\mathsf{G}} % globally
\\def\\X{\\mathsf{X}} % next
\\DeclareMathOperator{\\W}{\\mathbin{\\mathsf{W}}} % weak until
\\DeclareMathOperator{\\M}{\\mathbin{\\mathsf{M}}} % strong release
\\DeclareMathOperator{\\U}{\\mathbin{\\mathsf{U}}} % until
\\DeclareMathOperator{\\R}{\\mathbin{\\mathsf{R}}} % release
";
print "\\begin{document}\n";
print "\\begin{tabular}{lrcr|r|rrrr|rrr|rr|rrr|rrr|rrrr}";
print "\\multicolumn{24}{l}{Column \\textbf{type} shows how the initial deterministic automaton was obtained: T = translation produces DTGBA; W = WDBA minimization works; P = powerset construction transforms TBA to DTBA; R = DRA to DBA.}\\\\\n";
print "\\multicolumn{24}{l}{Column \\textbf{C.} tells whether the output automaton is complete: rejecting sink states are always omitted (add 1 state when C=0 if you want the size of the complete automaton).}\\\\\n";
print "&&&&DRA&\\multicolumn{4}{|c}{DTGBA} & \\multicolumn{3}{|c}{DBA} & \\multicolumn{2}{|c}{DBA\\footnotesize minimizer}& \\multicolumn{3}{|c}{min DBA} & \\multicolumn{3}{|c}{minDTBA} & \\multicolumn{4}{|c}{minDTGBA}\\\\\n";
print "formula & \$m\$ & type & C. & st. & st. & tr. & acc. & time & st. & tr. & time & st. & time & st. & tr. & time & st. & tr. & time & st. & tr. & acc. & time \\\\\n";
sub nonnull($)
{
return 1 if $_[0] == 0;
return $_[0];
}
my $lasttype = '';
my $linenum = 0;
foreach my $tab (@w)
{
sub val($)
{
my ($n) = @_;
my $v = $tab->[$n];
return 0+'inf' if !defined($v) || $v =~ /\s*-\s*/;
return $v;
}
if (dratcong($lasttype, $tab->[2]))
{
print "\\hline\n";
$linenum = 0;
}
$lasttype = $tab->[2];
if ($linenum++ % 4 == 0)
{
print "\\arrayrulecolor{lightgray}\\hline\\arrayrulecolor{black}";
}
my $f = $tab->[0];
$f =~ s/\&/\\land /g;
$f =~ s/\|/\\lor /g;
$f =~ s/!/\\bar /g;
$f =~ s/<->/\\leftrightarrow /g;
$f =~ s/->/\\rightarrow /g;
$f =~ s/[XRWMGFU]/\\$& /g;
print "\$$f\$\t& ";
print "$tab->[1] & ";
if ($tab->[2] =~ /trad/) { print "T & "; }
elsif ($tab->[2] =~ /TCONG/) { print "P & "; }
elsif ($tab->[2] =~ /DRA/) { print "R & "; }
elsif ($tab->[2] =~ /WDBA/) { print "W & "; }
else { print "$tab->[2]& "; }
# If one of the automata is not deterministic highlight the "Complete" column.
print "{\\P}" if val(8) == 0 || val(17) == 0 || val(26) == 0 || val(35) == 0 || val(44) == 0;
print "$tab->[9] & ";
if ($tab->[51] =~ m:\s*n/a\s*:) # DRA
{
print "&";
$tab->[51] = 0+'inf';
}
else
{
# Remove sink state if not complete.
my $st = $tab->[51] - 1 + $tab->[9] || 1;
print "$st & ";
}
print "$tab->[3] & "; # states
print "$tab->[5] & "; # transitions
print "$tab->[6] & "; # acc
printf("%.2f &", $tab->[10]);
if ($tab->[12] =~ /\s*-\s*/) # DBA
{
print "- & - & - &";
$tab->[12] = 0+'inf';
}
elsif ($tab->[12] =~ /\s*!\s*/) # DBA
{
print "! & ! & ! &";
$tab->[12] = 0+'inf';
}
else
{
print "$tab->[12] & "; # states
print "$tab->[14] & "; # transitions
printf("%.2f &", $tab->[19]);
}
if ($tab->[48] =~ /\s*-\s*/) # DBAminimizer
{
print "\\multicolumn{2}{c|}{(killed)}&";
$tab->[48] = 0+'inf';
}
elsif ($tab->[48] =~ m:\s*n/a\s*:) # DBAminimizer
{
print " & &";
$tab->[48] = 0+'inf';
}
else
{
# Remove sink state if not complete.
my $st = $tab->[48] - 1 + $tab->[9] || 1;
print "{\\E}" if ($st < $tab->[12]);
print "{\\P}" if ($st > $tab->[12]);
print "$st & "; # states
printf("%.2f &", $tab->[49]);
}
if ($tab->[21] =~ /\s*-\s*/) # minDBA
{
print "\\multicolumn{3}{c|}{(killed)}&";
$tab->[21] = 0+'inf';
}
elsif ($tab->[21] =~ /\s*!\s*/) # minDBA
{
print "\\multicolumn{3}{c|}{(intmax)}&";
$tab->[21] = 0+'inf';
}
else
{
print "{\\E}" if ($tab->[21] < $tab->[12]);
print "{\\P}" if ($tab->[21] > $tab->[12]);
print "$tab->[21] & "; # states
print "$tab->[23] & "; # transitions
printf("%.2f &", $tab->[28]);
}
if ($tab->[39] =~ /\s*-\s*/) # min DTBA
{
print "\\multicolumn{3}{c|}{(killed)}&";
$tab->[39] = 0+'inf';