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