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    $v[$num] = [split /,/];
13#    print $v[$num]->[48], " ",  $#{$v[$num]}, "\n";
14#    if ($#{$v[$num]} != 49)
15#    {
16#	pop $v[$num];
17#	push $v[$num], '-', '-';
18#   }
19#    print $v[$num]->[48], " ",  $#{$v[$num]}, "\n";
20
21    ++$num;
22}
23
24sub dratcong($$)
25{
26    my ($a, $b) = @_;
27    return 0 if ($a =~ /.*CONG/ && $b =~ /.*CONG/);
28    return $a cmp $b;
29}
30
31sub mycmp()
32{
33    my $v = dratcong($b->[2], $a->[2]);
34    return $v if $v;
35    my $n1 = lc $a->[0];
36    $n1 =~ s/\W//g;
37    my $n2 = lc $b->[0];
38    $n2 =~ s/\W//g;
39    return $n1 cmp $n2 || $a->[0] cmp $b->[0] || $b->[2] cmp $a->[2];;
40}
41
42my @w = sort mycmp @v;
43
44print "\\documentclass{standalone}\n
45\\usepackage{amsmath}
46\\usepackage{colortbl}
47\\definecolor{mygray}{gray}{0.75} % 1 = white, 0 = black
48\\definecolor{lightgray}{gray}{0.7} % 1 = white, 0 = black
49\\def\\E{\\cellcolor{mygray}}
50\\def\\P{\\cellcolor{red}}
51\\def\\PP{\\cellcolor{yellow}}
52\\def\\F{\\mathsf{F}} % in future
53\\def\\G{\\mathsf{G}} % globally
54\\def\\X{\\mathsf{X}} % next
55\\DeclareMathOperator{\\W}{\\mathbin{\\mathsf{W}}} % weak until
56\\DeclareMathOperator{\\M}{\\mathbin{\\mathsf{M}}} % strong release
57\\DeclareMathOperator{\\U}{\\mathbin{\\mathsf{U}}} % until
58\\DeclareMathOperator{\\R}{\\mathbin{\\mathsf{R}}} % release
59";
60
61print "\\begin{document}\n";
62print "\\begin{tabular}{lrcr|r|rrrr|rrr|rr|rrr|rrr|rrrr}";
63print "\\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";
64print "\\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";
65print "&&&&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";
66print "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";
67
68sub nonnull($)
69{
70    return 1 if $_[0] == 0;
71    return $_[0];
72}
73
74sub getlastsuccesful($$)
75{
76    my ($n,$type) = @_;
77    open LOG, "<$n.$type.satlog" or return "";
78    my $min = "";
79    while (my $line = <LOG>)
80    {
81	my @f = split(/,/, $line);
82	$min = $f[2] if $f[2] ne '';
83    }
84    $min = ", \$\\le\$$min" if $min ne "";
85    return $min;
86}
87
88
89my $lasttype = '';
90my $linenum = 0;
91foreach my $tab (@w)
92{
93    sub val($)
94    {
95	my ($n) = @_;
96	my $v = $tab->[$n];
97	return 0+'inf' if !defined($v) || $v =~ /\s*-\s*/;
98	return $v;
99    }
100
101    if (dratcong($lasttype, $tab->[2]))
102    {
103	print "\\hline\n";
104	$linenum = 0;
105    }
106    $lasttype = $tab->[2];
107    if ($linenum++ % 4 == 0)
108    {
109	print "\\arrayrulecolor{lightgray}\\hline\\arrayrulecolor{black}";
110    }
111
112    my $n = $tab->[52];
113    my $f = $tab->[0];
114    $f =~ s/\&/\\land /g;
115    $f =~ s/\|/\\lor /g;
116    $f =~ s/!/\\bar /g;
117    $f =~ s/<->/\\leftrightarrow /g;
118    $f =~ s/->/\\rightarrow /g;
119    $f =~ s/[XRWMGFU]/\\$& /g;
120    print "\$$f\$\t& ";
121    print "$tab->[1] & ";
122    if ($tab->[2] =~ /trad/) { print "T & "; }
123    elsif ($tab->[2] =~ /TCONG/) { print "P & "; }
124    elsif ($tab->[2] =~ /DRA/) { print "R & "; }
125    elsif ($tab->[2] =~ /WDBA/) { print "W & "; }
126    else { print "$tab->[2]& "; }
127    # If one of the automata is not deterministic highlight the "Complete" column.
128    print "{\\P}" if val(8) == 0 || val(17) == 0 || val(26) == 0 || val(35) == 0  || val(44) == 0;
129    print "$tab->[9] & ";
130
131    if ($tab->[51] =~ m:\s*n/a\s*:) #  DRA
132    {
133	print "&";
134	$tab->[51] = 0+'inf';
135    }
136    else
137    {
138	# Remove sink state if not complete.
139	my $st = $tab->[51] - 1 + $tab->[9] || 1;
140	print "$st & ";
141    }
142
143    print "$tab->[3] & "; # states
144    print "$tab->[5] & "; # transitions
145    print "$tab->[6] & "; # acc
146    printf("%.2f &", $tab->[10]);
147
148    if ($tab->[12] =~ /\s*-\s*/)  # DBA
149    {
150	print "- & - & - &";
151	$tab->[12] = 0+'inf';
152    }
153    elsif ($tab->[12] =~ /\s*!\s*/)  # DBA
154    {
155	print "! & ! & ! &";
156	$tab->[12] = 0+'inf';
157    }
158    else
159    {
160	print "$tab->[12] & "; # states
161	print "$tab->[14] & "; # transitions
162	printf("%.2f &", $tab->[19]);
163    }
164
165    if ($tab->[48] =~ /\s*-\s*/) #  DBAminimizer
166    {
167	print "\\multicolumn{2}{c|}{(killed)}&";
168	$tab->[48] = 0+'inf';
169    }
170    elsif ($tab->[48] =~ m:\s*n/a\s*:) #  DBAminimizer
171    {
172	print " & &";
173	$tab->[48] = 0+'inf';
174    }
175    else
176    {
177	# Remove sink state if not complete.
178	my $st = $tab->[48] - 1 + $tab->[9] || 1;
179	print "{\\E}" if ($st < $tab->[12]);
180	print "{\\P}" if ($st > $tab->[12]);
181	print "$st & "; # states
182	printf("%.2f &", $tab->[49]);
183    }
184
185    if ($tab->[21] =~ /\s*-\s*/) #  minDBA
186    {
187	my $s = getlastsuccesful($n, "DBA");
188	print "\\multicolumn{3}{c|}{(killed$s)}&";
189	$tab->[21] = 0+'inf';
190    }
191    elsif ($tab->[21] =~ /\s*!\s*/) #  minDBA
192    {
193	my $s = getlastsuccesful($n, "DBA");
194	print "\\multicolumn{3}{c|}{(intmax$s)}&";
195	$tab->[21] = 0+'inf';
196    }
197    else
198    {
199	print "{\\E}" if ($tab->[21] < $tab->[12]);
200	print "{\\P}" if ($tab->[21] > $tab->[12]);
201	print "$tab->[21] & "; # states
202	print "$tab->[23] & "; # transitions
203	printf("%.2f &", $tab->[28]);
204    }
205
206    if ($tab->[39] =~ /\s*-\s*/) # min DTBA
207    {
208	my $s = getlastsuccesful($n, "DTBA");
209	print "\\multicolumn{3}{c|}{(killed$s)}&";
210	$tab->[39] = 0+'inf';
211    }
212    elsif ($tab->[39] =~ /\s*!\s*/) # min DTBA
213    {
214	my $s = getlastsuccesful($n, "DTBA");
215	print "\\multicolumn{3}{c|}{(intmax$s)}&";
216	$tab->[39] = 0+'inf';
217    }
218    else
219    {
220	print "{\\E}" if ($tab->[39] < $tab->[3]);
221	print "{\\P}" if ($tab->[39] > $tab->[3] * nonnull($tab->[6])) or ($tab->[39] > $tab->[12]);
222	print "\\textbf" if ($tab->[39] < $tab->[21]);
223	print "{$tab->[39]} & "; # states
224	print "$tab->[41] & "; # transitions
225	printf("%.2f &", $tab->[46]);
226    }
227
228    if ($tab->[30] =~ /\s*-\s*/)   # minTGBA
229    {
230	my $s = getlastsuccesful($n, "DTGBA");
231	print "\\multicolumn{4}{c}{(killed$s)}";
232	$tab->[30] = 0+'inf';
233    }
234    elsif ($tab->[30] =~ /\s*!\s*/)   # minTGBA
235    {
236	my $s = getlastsuccesful($n, "DTGBA");
237	print "\\multicolumn{4}{c}{(intmax$s)}";
238	$tab->[30] = 0+'inf';
239    }
240    else
241    {
242	print "{\\E}" if ($tab->[30] < $tab->[3]);
243	print "{\\P}" if ($tab->[30] > $tab->[3]) or ($tab->[30] > $tab->[12]) or ($tab->[30] > $tab->[21]) or ($tab->[30] > $tab->[39]);
244	print "{\\PP}" if ($tab->[21] ne 'inf' && $tab->[30] * ($tab->[33] + 1) < $tab->[21]);
245	print "\\textbf" if ($tab->[30] < $tab->[39]);
246	print "{$tab->[30]} & "; # states
247	print "$tab->[32] & "; # transitions
248	print "\\textbf" if ($tab->[33] > $tab->[6]);
249	print "{$tab->[33]} & "; # acc
250	printf("%.2f ", $tab->[37]);
251    }
252
253    print "\\\\\n";
254}
255print "\\end{tabular}\n";
256print "\\end{document}\n";
257