Commit 55ee18b9 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

sat-minimize: more statistics.

* 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.
parent 1319ec0b
......@@ -11,7 +11,9 @@ dbamin=${DBA_MINIMIZER-/home/adl/projs/dbaminimizer/minimize.py}
get_stats()
{
$timeout "$@" "$stats" > stdin.$$ 2>stderr.$$
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"
......@@ -29,22 +31,22 @@ get_dbamin_stats()
echo ${tmp:-$mye}
}
f=$1
type=$2
accmax=$3
n=$1
f=$2
type=$3
accmax=$4
case $type in
*WDBA*)
echo "$f, $accmax, $type..." 1>&2
input=`get_stats $ltl2tgba "$f" -BD`
input=`get_stats BA $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'`
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 $ltl2tgba "$f" -D -x 'sat-minimize=-1'`
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 $ltl2tgba "$f" -D -x 'sat-minimize=-1,sat-acc=1'`
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.$$
......@@ -54,15 +56,15 @@ case $type in
;;
*TCONG*|*trad*) # Not in WDBA
echo "$f, $accmax, $type..." 1>&2
input=`get_stats $ltl2tgba "$f" -D -x '!wdba-minimize,tba-det'`
input=`get_stats TBA $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'`
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 $ltl2tgba "$f" -BD -x '!wdba-minimize,sat-minimize'`
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 $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize'`
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 $ltl2tgba "$f" -D -x '!wdba-minimize,sat-minimize,sat-acc=1'`
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";;
......@@ -79,15 +81,15 @@ case $type in
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'`
input=`get_stats TBA $dstar2tgba dra.$$ -D -x '!wdba-minimize'`
echo "$f, $accmax, $type, $input, DBA, ... " 1>&2
dba=`get_stats $dstar2tgba dra.$$ -BD -x '!wdba-minimize'`
dba=`get_stats BA $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'`
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 $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-acc='$accmax`
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 $dstar2tgba dra.$$ -D -x '!wdba-minimize,sat-acc=1'`
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.$$`
......@@ -101,5 +103,5 @@ case $type in
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"
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"
......@@ -17,15 +17,15 @@ while IFS=, read f type accmax accmin; do
case $type in
*TCONG*)
echo "$n.log:; ./stat.sh '$f' $type $accmax >\$@" >> stats.tmp
echo "$n.log:; ./stat.sh $n '$f' $type $accmax >\$@" >> stats.tmp
all="$all $n.log"
n=`expr $n + 1`
echo "$n.log:; ./stat.sh '$f' DRA-CONG $accmax >\$@" >> stats.tmp
echo "$n.log:; ./stat.sh $n '$f' DRA-CONG $accmax >\$@" >> stats.tmp
all="$all $n.log"
n=`expr $n + 1`
;;
*)
echo "$n.log:; ./stat.sh '$f' $type $accmax >\$@" >> stats.tmp
echo "$n.log:; ./stat.sh $n '$f' $type $accmax >\$@" >> stats.tmp
all="$all $n.log"
n=`expr $n + 1`
;;
......
......@@ -60,7 +60,7 @@ print "\\documentclass{standalone}\n
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{type} shows how the initial det. aut. 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";
......@@ -71,6 +71,20 @@ sub nonnull($)
return $_[0];
}
sub getlastsuccesful($$)
{
my ($n,$type) = @_;
open LOG, "<$n.$type.satlog" or return "";
my $min = "";
while (my $line = <LOG>)
{
my @f = split(/,/, $line);
$min = $f[1] if $f[1] ne '';
}
$min = ", \$\\le\$$min" if $min ne "";
return $min;
}
my $lasttype = '';
my $linenum = 0;
......@@ -95,6 +109,7 @@ foreach my $tab (@w)
print "\\arrayrulecolor{lightgray}\\hline\\arrayrulecolor{black}";
}
my $n = $tab->[52];
my $f = $tab->[0];
$f =~ s/\&/\\land /g;
$f =~ s/\|/\\lor /g;
......@@ -169,12 +184,14 @@ foreach my $tab (@w)
if ($tab->[21] =~ /\s*-\s*/) # minDBA
{
print "\\multicolumn{3}{c|}{(killed)}&";
my $s = getlastsuccesful($n, "DBA");
print "\\multicolumn{3}{c|}{(killed$s)}&";
$tab->[21] = 0+'inf';
}
elsif ($tab->[21] =~ /\s*!\s*/) # minDBA
{
print "\\multicolumn{3}{c|}{(intmax)}&";
my $s = getlastsuccesful($n, "DBA");
print "\\multicolumn{3}{c|}{(intmax$s)}&";
$tab->[21] = 0+'inf';
}
else
......@@ -188,12 +205,14 @@ foreach my $tab (@w)
if ($tab->[39] =~ /\s*-\s*/) # min DTBA
{
print "\\multicolumn{3}{c|}{(killed)}&";
my $s = getlastsuccesful($n, "DTBA");
print "\\multicolumn{3}{c|}{(killed$s)}&";
$tab->[39] = 0+'inf';
}
elsif ($tab->[39] =~ /\s*!\s*/) # min DTBA
{
print "\\multicolumn{3}{c|}{(intmax)}&";
my $s = getlastsuccesful($n, "DTBA");
print "\\multicolumn{3}{c|}{(intmax$s)}&";
$tab->[39] = 0+'inf';
}
else
......@@ -208,12 +227,14 @@ foreach my $tab (@w)
if ($tab->[30] =~ /\s*-\s*/) # minTGBA
{
print "\\multicolumn{4}{c}{(killed)}";
my $s = getlastsuccesful($n, "DTGBA");
print "\\multicolumn{4}{c}{(killed$s)}";
$tab->[30] = 0+'inf';
}
elsif ($tab->[30] =~ /\s*!\s*/) # minTGBA
{
print "\\multicolumn{4}{c}{(intmax)}";
my $s = getlastsuccesful($n, "DTGBA");
print "\\multicolumn{4}{c}{(intmax$s)}";
$tab->[30] = 0+'inf';
}
else
......
......@@ -64,6 +64,21 @@ sub nonnull($)
return $_[0];
}
sub getlastsuccesful($$)
{
my ($n,$type) = @_;
open LOG, "<$n.$type.satlog" or return "";
my $min = "";
while (my $line = <LOG>)
{
my @f = split(/,/, $line);
$min = $f[1] if $f[1] ne '';
}
$min = ", \$\\le\$$min" if $min ne "";
return $min;
}
my $lasttype = '';
my $linenum = 0;
......@@ -83,6 +98,7 @@ foreach my $tab (@w)
# print "\\arrayrulecolor{lightgray}\\hline\\arrayrulecolor{black}";
}
my $n = $tab->[52];
my $f = $tab->[0];
$f =~ s/\&/\\land /g;
$f =~ s/\|/\\lor /g;
......@@ -119,12 +135,14 @@ foreach my $tab (@w)
if ($tab->[21] =~ /\s*-\s*/) # minDBA
{
print "\\multicolumn{1}{c|}{(killed)}&";
my $s = getlastsuccesful($n, "DBA");
print "\\multicolumn{1}{c|}{(killed$s)}&";
$tab->[21] = 0+'inf';
}
elsif ($tab->[21] =~ /\s*!\s*/) # minDBA
{
print "\\multicolumn{1}{c|}{(\$>\$INTMAX)}&";
my $s = getlastsuccesful($n, "DBA");
print "\\multicolumn{1}{c|}{(intmax$s)}&";
$tab->[21] = 0+'inf';
}
else
......
......@@ -83,6 +83,21 @@ sub nonnull($)
return $_[0];
}
sub getlastsuccesful($$)
{
my ($n,$type) = @_;
open LOG, "<$n.$type.satlog" or return "";
my $min = "";
while (my $line = <LOG>)
{
my @f = split(/,/, $line);
$min = $f[1] if $f[1] ne '';
}
$min = ", \$\\le\$$min" if $min ne "";
return $min;
}
my $lasttype = '';
my $linenum = 0;
......@@ -107,6 +122,7 @@ foreach my $tab (@w)
# print "\\arrayrulecolor{lightgray}\\hline\\arrayrulecolor{black}";
}
my $n = $tab->[52];
my $f = $tab->[0];
$f =~ s/\&/\\land /g;
$f =~ s/\|/\\lor /g;
......@@ -178,12 +194,14 @@ foreach my $tab (@w)
if ($tab->[21] =~ /\s*-\s*/) # minDBA
{
print "\\multicolumn{1}{c|}{(killed)}&";
my $s = getlastsuccesful($n, "DBA");
print "\\multicolumn{1}{c|}{(killed$s)}&";
$tab->[21] = 0+'inf';
}
elsif ($tab->[21] =~ /\s*!\s*/) # minDBA
{
print "\\multicolumn{1}{c|}{(INTMAX)}&";
my $s = getlastsuccesful($n, "DBA");
print "\\multicolumn{1}{c|}{(intmax$s)}&";
$tab->[21] = 0+'inf';
}
else
......@@ -198,12 +216,14 @@ foreach my $tab (@w)
if ($tab->[39] =~ /\s*-\s*/) # min DTBA
{
print "\\multicolumn{2}{c|}{(killed)}&";
my $s = getlastsuccesful($n, "DTBA");
print "\\multicolumn{2}{c|}{(killed$s)}&";
$tab->[39] = 0+'inf';
}
elsif ($tab->[39] =~ /\s*!\s*/) # min DTBA
{
print "\\multicolumn{2}{c|}{(INTMAX)}&";
my $s = getlastsuccesful($n, "DTBA");
print "\\multicolumn{2}{c|}{(intmax$s)}&";
$tab->[39] = 0+'inf';
}
else
......@@ -218,12 +238,14 @@ foreach my $tab (@w)
if ($tab->[30] =~ /\s*-\s*/) # minTGBA
{
print "\\multicolumn{3}{c}{(killed)}";
my $s = getlastsuccesful($n, "DTGBA");
print "\\multicolumn{3}{c}{(killed$s)}";
$tab->[30] = 0+'inf';
}
elsif ($tab->[30] =~ /\s*!\s*/) # minTGBA
{
print "\\multicolumn{3}{c}{(INTMAX)}";
my $s = getlastsuccesful($n, "DTGBA");
print "\\multicolumn{3}{c}{(intmax$s)}";
$tab->[30] = 0+'inf';
}
else
......
......@@ -85,6 +85,21 @@ sub nonnull($)
return $_[0];
}
sub getlastsuccesful($$)
{
my ($n,$type) = @_;
open LOG, "<$n.$type.satlog" or return "";
my $min = "";
while (my $line = <LOG>)
{
my @f = split(/,/, $line);
$min = $f[1] if $f[1] ne '';
}
$min = ", \$\\le\$$min" if $min ne "";
return $min;
}
my $lasttype = '';
my $linenum = 0;
......@@ -109,6 +124,7 @@ foreach my $tab (@w)
# print "\\arrayrulecolor{lightgray}\\hline\\arrayrulecolor{black}";
}
my $n = $tab->[52];
my $f = $tab->[0];
$f =~ s/\&/\\land /g;
$f =~ s/\|/\\lor /g;
......@@ -179,12 +195,14 @@ foreach my $tab (@w)
if ($tab->[21] =~ /\s*-\s*/) # minDBA
{
print "\\multicolumn{2}{c|}{(killed)}&";
my $s = getlastsuccesful($n, "DBA");
print "\\multicolumn{2}{c|}{(killed$s)}&";
$tab->[21] = 0+'inf';
}
elsif ($tab->[21] =~ /\s*!\s*/) # minDBA
{
print "\\multicolumn{2}{c|}{(intmax)}&";
my $s = getlastsuccesful($n, "DBA");
print "\\multicolumn{2}{c|}{(intmax$s)}&";
$tab->[21] = 0+'inf';
}
else
......@@ -199,12 +217,14 @@ foreach my $tab (@w)
if ($tab->[39] =~ /\s*-\s*/) # min DTBA
{
print "\\multicolumn{2}{c|}{(killed)}&";
my $s = getlastsuccesful($n, "DTBA");
print "\\multicolumn{2}{c|}{(killed$s)}&";
$tab->[39] = 0+'inf';
}
elsif ($tab->[39] =~ /\s*!\s*/) # min DTBA
{
print "\\multicolumn{2}{c|}{(intmax)}&";
my $s = getlastsuccesful($n, "DTBA");
print "\\multicolumn{2}{c|}{(intmax$s)}&";
$tab->[39] = 0+'inf';
}
else
......@@ -219,12 +239,14 @@ foreach my $tab (@w)
if ($tab->[30] =~ /\s*-\s*/) # minTGBA
{
print "\\multicolumn{3}{c}{(killed)}";
my $s = getlastsuccesful($n, "DTGBA");
print "\\multicolumn{3}{c}{(killed$s)}";
$tab->[30] = 0+'inf';
}
elsif ($tab->[30] =~ /\s*!\s*/) # minTGBA
{
print "\\multicolumn{3}{c}{(intmax)}";
my $s = getlastsuccesful($n, "DTGBA");
print "\\multicolumn{3}{c}{(intmax$s)}";
$tab->[30] = 0+'inf';
}
else
......
......@@ -84,6 +84,21 @@ sub nonnull($)
return $_[0];
}
sub getlastsuccesful($$)
{
my ($n,$type) = @_;
open LOG, "<$n.$type.satlog" or return "";
my $min = "";
while (my $line = <LOG>)
{
my @f = split(/,/, $line);
$min = $f[1] if $f[1] ne '';
}
$min = ", \$\\le\$$min" if $min ne "";
return $min;
}
my $lasttype = '';
my $linenum = 0;
......@@ -104,6 +119,7 @@ foreach my $tab (@w)
}
++$linenum;
my $n = $tab->[52];
my $f = $tab->[0];
next if length($f) > 60;
$f =~ s/\&/\\land /g;
......@@ -181,12 +197,14 @@ foreach my $tab (@w)
if ($tab->[21] =~ /\s*-\s*/) # minDBA
{
print "\\multicolumn{2}{c|}{(killed)}&";
my $s = getlastsuccesful($n, "DBA");
print "\\multicolumn{2}{c|}{(killed$s)}&";
$tab->[21] = 0+'inf';
}
elsif ($tab->[21] =~ /\s*!\s*/) # minDBA
{
print "\\multicolumn{2}{c|}{(intmax)}&";
my $s = getlastsuccesful($n, "DBA");
print "\\multicolumn{2}{c|}{(intmax$s)}&";
$tab->[21] = 0+'inf';
}
else
......@@ -201,12 +219,14 @@ foreach my $tab (@w)
if ($tab->[39] =~ /\s*-\s*/) # min DTBA
{
print "\\multicolumn{2}{c|}{(killed)}&";
my $s = getlastsuccesful($n, "DTBA");
print "\\multicolumn{2}{c|}{(killed$s)}&";
$tab->[39] = 0+'inf';
}
elsif ($tab->[39] =~ /\s*!\s*/) # min DTBA
{
print "\\multicolumn{2}{c|}{(intmax)}&";
my $s = getlastsuccesful($n, "DTBA");
print "\\multicolumn{2}{c|}{(intmax$s)}&";
$tab->[39] = 0+'inf';
}
else
......@@ -221,12 +241,14 @@ foreach my $tab (@w)
if ($tab->[30] =~ /\s*-\s*/) # minTGBA
{
print "\\multicolumn{3}{c}{(killed)}";
my $s = getlastsuccesful($n, "DTGBA");
print "\\multicolumn{3}{c}{(killed$s)}";
$tab->[30] = 0+'inf';
}
elsif ($tab->[30] =~ /\s*!\s*/) # minTGBA
{
print "\\multicolumn{3}{c}{(intmax)}";
my $s = getlastsuccesful($n, "DTGBA");
print "\\multicolumn{3}{c}{(intmax$s)}";
$tab->[30] = 0+'inf';
}
else
......
......@@ -29,6 +29,8 @@
#include "ltlast/constant.hh"
#include "stats.hh"
#include "misc/satsolver.hh"
#include "misc/timer.hh"
#include "dotty.hh"
// If you set the SPOT_TMPKEEP environment variable the temporary
// file used to communicate with the sat solver will be left in
......@@ -320,9 +322,11 @@ namespace spot
}
};
typedef std::pair<int, int> sat_stats;
static
void dtba_to_sat(std::ostream& out, const tgba* ref, dict& d,
bool state_based)
sat_stats dtba_to_sat(std::ostream& out, const tgba* ref,
dict& d, bool state_based)
{
clause_counter nclauses;
int ref_size = 0;
......@@ -354,7 +358,7 @@ namespace spot
if (d.cand_size == 0)
{
out << "p cnf 1 2\n-1 0\n1 0\n";
return;
return std::make_pair(1, 2);
}
// An empty line for the header
......@@ -667,6 +671,7 @@ namespace spot
}
out.seekp(0);
out << "p cnf " << d.nvars << " " << nclauses.nb_clauses();
return std::make_pair(d.nvars, nclauses.nb_clauses());
}
static tgba_explicit_number*
......@@ -813,13 +818,46 @@ namespace spot
satsolver solver;
satsolver::solution_pair solution;
dtba_to_sat(solver(), a, d, state_based);
timer_map t;
t.start("encode");
sat_stats s = dtba_to_sat(solver(), a, d, state_based);
t.stop("encode");
t.start("solve");
solution = solver.get_solution();
t.stop("solve");
tgba_explicit_number* res = 0;
if (!solution.second.empty())
res = sat_build(solution.second, d, a, state_based);
static const char* log = getenv("SPOT_SATLOG");
if (log)
{
std::fstream out(log,
std::ios_base::app | std::ios_base::out);
out.exceptions(std::ifstream::failbit | std::ifstream::badbit);
const timer& te = t.timer("encode");
const timer& ts = t.timer("solve");
out << target_state_number << ',';
if (res)
{
tgba_sub_statistics st = sub_stats_reachable(res);
out << st.states << ',' << st.transitions
<< ',' << st.sub_transitions;
}
else
{
out << ",,";
}
out << ','
<< s.first << ',' << s.second << ','
<< te.utime() << ',' << te.stime() << ','
<< ts.utime() << ',' << ts.stime() << '\n';
}
static const char* show = getenv("SPOT_SATSHOW");
if (show && res)
dotty_reachable(std::cout, res);
trace << "dtba_sat_synthetize(...) = " << res << "\n";
return res;
}
......
......@@ -30,7 +30,9 @@
#include "stats.hh"
#include "ltlenv/defaultenv.hh"
#include "misc/satsolver.hh"
#include "misc/timer.hh"
#include "isweakscc.hh"
#include "dotty.hh"
// If you set the SPOT_TMPKEEP environment variable the temporary
// file used to communicate with the sat solver will be left in
......@@ -465,9 +467,11 @@ namespace spot
}
};
typedef std::pair<int, int> sat_stats;
static
void dtgba_to_sat(std::ostream& out, const tgba* ref, dict& d,
bool state_based)
sat_stats dtgba_to_sat(std::ostream& out, const tgba* ref,
dict& d, bool state_based)
{
clause_counter nclauses;
int ref_size = 0;
......@@ -499,7 +503,7 @@ namespace spot
if (d.cand_size == 0)
{
out << "p cnf 1 2\n-1 0\n1 0\n";
return;
return std::make_pair(1, 2);
}
// An empty line for the header
......@@ -839,6 +843,7 @@ namespace spot
}
out.seekp(0);
out << "p cnf " << d.nvars << " " << nclauses.nb_clauses();
return std::make_pair(d.nvars, nclauses.nb_clauses());
}
static tgba_explicit_number*
......@@ -960,13 +965,46 @@ namespace spot
satsolver solver;
satsolver::solution_pair solution;
dtgba_to_sat(solver(), a, d, state_based);
timer_map t;