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