1#!/usr/bin/perl -w
2
3use strict;
4
5my $num = 0;
6my @v = ();
7while (<>)
8{
9    # 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
10    chomp;
11    next if /.*realizable.*/;
12    next unless /WDBA/;
13    $v[$num] = [split /,/];
14    ++$num;
15}
16
17sub dratcong($$)
18{
19    my ($a, $b) = @_;
20    return 0 if ($a =~ /.*CONG/ && $b =~ /.*CONG/);
21    return $a cmp $b;
22}
23
24sub mycmp()
25{
26    my $v = dratcong($b->[2], $a->[2]);
27    return $v if $v;
28    my $n1 = lc $a->[0];
29    $n1 =~ s/\W//g;
30    my $n2 = lc $b->[0];
31    $n2 =~ s/\W//g;
32    return $n1 cmp $n2 || $a->[0] cmp $b->[0] || $b->[2] cmp $a->[2];;
33}
34
35my @w = sort mycmp @v;
36
37print "\\documentclass{standalone}\n
38\\usepackage{amsmath}
39\\usepackage{colortbl}
40\\usepackage{booktabs}
41\\definecolor{mygray}{gray}{0.75} % 1 = white, 0 = black
42\\definecolor{lightgray}{gray}{0.7} % 1 = white, 0 = black
43\\def\\E{\\cellcolor{mygray}}
44\\def\\P{\\cellcolor{red}}
45\\def\\PP{\\cellcolor{yellow}}
46\\def\\F{\\mathsf{F}} % in future
47\\def\\G{\\mathsf{G}} % globally
48\\def\\X{\\mathsf{X}} % next
49\\DeclareMathOperator{\\W}{\\mathbin{\\mathsf{W}}} % weak until
50\\DeclareMathOperator{\\M}{\\mathbin{\\mathsf{M}}} % strong release
51\\DeclareMathOperator{\\U}{\\mathbin{\\mathsf{U}}} % until
52\\DeclareMathOperator{\\R}{\\mathbin{\\mathsf{R}}} % release
53";
54
55print "\\begin{document}\n";
56print "\\begin{tabular}{lc|c|rr|c|r}";
57print "&& \\multicolumn{1}{c|}{minDBA} & trad & +SAT & DRA & {DBA\\footnotesize m..zer} \\\\\n";
58print " & C. & \$|Q|\$ & time & time & \$|Q|\$ & time \\\\\n";
59print "\\midrule\n";
60
61sub nonnull($)
62{
63    return 1 if $_[0] == 0;
64    return $_[0];
65}
66
67sub getlastsuccesful($$)
68{
69    my ($n,$type) = @_;
70    open LOG, "<$n.$type.satlog" or return "";
71    my $min = "";
72    while (my $line = <LOG>)
73    {
74	my @f = split(/,/, $line);
75	$min = $f[2] if $f[2] ne '';
76    }
77    $min = ", \$\\le\$$min" if $min ne "";
78    return $min;
79}
80
81
82
83my $lasttype = '';
84my $linenum = 0;
85foreach my $tab (@w)
86{
87    sub val($)
88    {
89	my ($n) = @_;
90	my $v = $tab->[$n];
91	return 0+'inf' if !defined($v) || $v =~ /\s*-\s*/;
92	return $v;
93    }
94
95    $lasttype = $tab->[2];
96    if ($linenum++ % 4 == 0)
97    {
98	# print "\\arrayrulecolor{lightgray}\\hline\\arrayrulecolor{black}";
99    }
100
101    my $n = $tab->[52];
102    my $f = $tab->[0];
103    $f =~ s/\&/\\land /g;
104    $f =~ s/\|/\\lor /g;
105    $f =~ s/!/\\bar /g;
106    $f =~ s/<->/\\leftrightarrow /g;
107    $f =~ s/->/\\rightarrow /g;
108    $f =~ s/[XRWMGFU]/\\$& /g;
109    print "\$$f\$\t& ";
110    # If one of the automata is not deterministic highlight the "Complete" column.
111    print "{\\P}" if val(8) == 0 || val(17) == 0 || val(26) == 0 || val(35) == 0  || val(44) == 0;
112    print "$tab->[9] & ";
113
114    # print "$tab->[3] & "; # states
115    # print "$tab->[5] & "; # transitions
116    # print "$tab->[6] & "; # acc
117    # printf("%.2f &", $tab->[10]);
118
119    if ($tab->[12] =~ /\s*-\s*/)  # DBA
120    {
121	print "- & - &";
122	$tab->[12] = 0+'inf';
123    }
124    elsif ($tab->[12] =~ /\s*!\s*/)  # DBA
125    {
126	print "! & ! &";
127	$tab->[12] = 0+'inf';
128    }
129    else
130    {
131	print "$tab->[12] & "; # states
132	# print "$tab->[14] & "; # transitions
133	printf("%.2f &", $tab->[19]);
134    }
135
136    if ($tab->[21] =~ /\s*-\s*/) #  minDBA
137    {
138        my $s = getlastsuccesful($n, "DBA");
139	print "\\multicolumn{1}{c|}{(killed$s)}&";
140	$tab->[21] = 0+'inf';
141    }
142    elsif ($tab->[21] =~ /\s*!\s*/) #  minDBA
143    {
144        my $s = getlastsuccesful($n, "DBA");
145	print "\\multicolumn{1}{c|}{(intmax$s)}&";
146	$tab->[21] = 0+'inf';
147    }
148    else
149    {
150	printf("%.2f &", $tab->[28]);
151    }
152
153    if ($tab->[51] =~ m:\s*n/a\s*:) #  DRA
154    {
155	print "&";
156	$tab->[51] = 0+'inf';
157    }
158    else
159    {
160	# Remove sink state if not complete.
161	my $st = $tab->[51] - 1 + $tab->[9] || 1;
162	print "\\textbf" if ($st > $tab->[12]);
163	print "{$st} & ";
164    }
165
166    if ($tab->[48] =~ /\s*-\s*/) #  DBAminimizer
167    {
168	print "\\multicolumn{1}{c}{(killed)}&";
169	$tab->[48] = 0+'inf';
170    }
171    elsif ($tab->[48] =~ m:\s*n/a\s*:) #  DBAminimizer
172    {
173	print " &";
174	$tab->[48] = 0+'inf';
175    }
176    else
177    {
178	# Remove sink state if not complete.
179	my $st = $tab->[48] - 1 + $tab->[9] || 1;
180	print "{\\E}" if ($st < $tab->[12]);
181	print "{\\P}" if ($st > $tab->[12]);
182	printf("%.2f", $tab->[49]);
183    }
184
185    print "\\\\\n";
186}
187print "\\end{tabular}\n";
188print "\\end{document}\n";
189