# HG changeset patch # User nipkow # Date 1251982202 -7200 # Node ID 52b4f2f54e466e7513bf38569284905271ebc1a8 # Parent eb82ed858b8481993a87ff1eb8b82136b353196d# Parent 173fd51d06c92ea910aac3e01f1116bec679bd7f merged diff -r eb82ed858b84 -r 52b4f2f54e46 src/HOL/Mirabelle/lib/scripts/report.pl --- a/src/HOL/Mirabelle/lib/scripts/report.pl Thu Sep 03 14:40:52 2009 +0200 +++ b/src/HOL/Mirabelle/lib/scripts/report.pl Thu Sep 03 14:50:02 2009 +0200 @@ -18,6 +18,7 @@ my $metis_calls = 0; my $metis_succeeded = 0; +my $metis_time_out = 0; my $metis_time = 0; foreach (@lines) { @@ -38,6 +39,9 @@ $metis_succeeded++; $metis_time += $1; } + if (m/^metis \(sledgehammer\): time out/) { + $metis_time_out++; + } } open(FILE, ">>$log_file") || die "Cannot open file '$log_file'"; @@ -51,19 +55,24 @@ if ($sh_calls > 0) { my $percent = $sh_succeeded / $sh_calls * 100; my $time = $sh_time / 1000; + my $avg_time = $sh_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 "Total time for successful sledgehammer calls: $time seconds\n\n"; + print FILE "Total time for successful sledgehammer calls: $time seconds\n"; + print FILE "Average time for successful sledgehammer calls: $avg_time seconds\n\n"; } if ($metis_calls > 0) { my $percent = $metis_succeeded / $metis_calls * 100; my $time = $metis_time / 1000; + my $avg_time = $time / $metis_succeeded; 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 "Total time for successful metis calls: $time seconds\n"; + print FILE "Average time for successful metis calls: $avg_time seconds\n"; } close(FILE);