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