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