# HG changeset patch # User nipkow # Date 1252054730 -7200 # Node ID bfe7573a239b89da6c9f31a11206f40efc2ccf6f # Parent a579bc82e932a1ced905418a7a19ffd6f6fa0ec7 tuned output diff -r a579bc82e932 -r bfe7573a239b src/HOL/Mirabelle/lib/scripts/report.pl --- a/src/HOL/Mirabelle/lib/scripts/report.pl Thu Sep 03 22:48:18 2009 +0200 +++ b/src/HOL/Mirabelle/lib/scripts/report.pl Fri Sep 04 10:58:50 2009 +0200 @@ -18,7 +18,7 @@ my $metis_calls = 0; my $metis_succeeded = 0; -my $metis_time_out = 0; +my $metis_timeout = 0; my $metis_time = 0; foreach (@lines) { @@ -40,7 +40,7 @@ $metis_time += $1; } if (m/^metis \(sledgehammer\): time out/) { - $metis_time_out++; + $metis_timeout++; } } @@ -57,8 +57,8 @@ my $time = $sh_time / 1000; my $avg_time = $time / $sh_succeeded; print FILE "Total number of sledgehammer calls: $sh_calls\n"; - print FILE "Number of successful sledgehammer calls: $sh_succeeded\n"; - printf FILE "Percentage of successful sledgehammer calls: %.0f%%\n", $percent; + print FILE "Number of successful sledgehammer calls: $sh_succeeded\n"; + printf FILE "Success rate: %.0f%%\n", $percent; printf FILE "Total time for successful sledgehammer calls: %.3f seconds\n", $time; printf FILE "Average time for successful sledgehammer calls: %.3f seconds\n\n", $avg_time; } @@ -67,10 +67,12 @@ my $percent = $metis_succeeded / $metis_calls * 100; my $time = $metis_time / 1000; my $avg_time = $time / $metis_succeeded; + my $metis_exc = $sh_succeeded - $metis_succeeded - $metis_timeout; print FILE "Total number of metis calls: $metis_calls\n"; print FILE "Number of successful metis calls: $metis_succeeded\n"; - print FILE "Number of metis time outs: $metis_time_out\n"; - printf FILE "Percentage of successful metis calls: %.0f%%\n", $percent; + print FILE "Number of metis timeouts: $metis_timeout\n"; + print FILE "Number of metis exceptions: $metis_exc\n"; + printf FILE "Success rate: %.0f%%\n", $percent; printf FILE "Total time for successful metis calls: %.3f seconds\n", $time; printf FILE "Average time for successful metis calls: %.3f seconds\n", $avg_time; }