Much more verbose statistics.

diff --git a/helm/software/matita/bench_summary.py b/helm/software/matita/bench_summary.py
index 64f3ad39dd4123a21cf63956efe832849ecdaae3..32df4b0177c25298e13d20f2cb566086b1970af9 100755 (executable)
--- a/helm/software/matita/bench_summary.py
+++ b/helm/software/matita/bench_summary.py
@@ -2,12 +2,10 @@
 import sys
 
 stats = {}
+stats['total'] = []
 stats['precise'] = []
 stats['imprecise'] = []
-stats['total'] = 0
-stats['spurious'] = {'tot': 0, 'max': 0, 'names': []}
-stats['half-mistakes'] = []
-stats['mistakes'] = []
+stats['false-positives'] = []
 stats['undetected'] = []
 
 for line in open(sys.argv[1]):
@@ -19,60 +17,59 @@ for line in open(sys.argv[1]):
     if cols[1] != 'KO':
         print "Warning: outcome of %s is %s, skipping it" % (name, cols[1])
         continue
-    stats['total'] += 1
     expected_error = cols[2]
     real_errors = cols[3].split(',')
     spurious_errors = cols[4].split(',')
 
-    if [expected_error] == real_errors:
+    stats['total'].append((name,real_errors))
+    if set([expected_error]) == set(real_errors):
         if expected_error in spurious_errors:
-            stats['half-mistakes'].append(name)
+            stats['false-positives'].append((name,real_errors))
         else:
-            stats['precise'].append(name)
-            stats['spurious']['max'] = max(len(spurious_errors), stats['spurious']['max'])
-            stats['spurious']['tot'] += len(spurious_errors)
+            stats['precise'].append((name,real_errors))
     elif expected_error in real_errors:
         if expected_error in spurious_errors:
-            stats['half-mistakes'].append(name)
+            stats['false-positives'].append((name,real_errors))
         else:
-            stats['imprecise'].append(name)
+            stats['imprecise'].append((name,real_errors))
     else:
         if expected_error in spurious_errors:
-            stats['mistakes'].append(name)
+            stats['false-positives'].append((name,real_errors))
         else:
-            stats['undetected'].append(name)
+            stats['undetected'].append((name,real_errors))
 
-for field in ['undetected', 'imprecise', 'mistakes', 'half-mistakes']:
+for field in ['undetected', 'imprecise', 'false-positives']:
     print "===================="
     print "%s:" % field
-    for name in stats[field]:
+    for name,_ in stats[field]:
         print "  %s" % name
 
-def get_stat(field):
-    global stats
-    return (stat, float(stat) / stats['total'] * 100)
+def average(l):
+    if not(len(l)):
+        return "N/A"
+    else:
+        return "%6.1f" % (reduce(lambda acc,x: acc+x,l,0)/float(len(l)))
+
+def mymax(l):
+    if not(len(l)):
+        return 0
+    else:
+        return max(l)
 
 def format_stat(field):
     global stats
-    if isinstance(stats[field], int):
-        stat = stats[field]
-    else:
-        stat = len(stats[field])
-    return r'%-15s & %6d & %6.1f\%% \\' % (field, stat,
-            float(stat) / stats['total'] * 100)
+    lista = stats[field]
+    errors = map(lambda x: len(x[1]),lista)
+    locations = map(lambda x: len(set(x[1])),lista)
+    return r'%-15s & %6d & %6s & %6d & %6s & %6d & %6.1f\%% \\' % \
+            (field, len(lista), average(locations),mymax(locations),
+            average(errors),mymax(errors),float(len(lista)) /
+            len(stats['total']) * 100)
 
 print "\n"
 print format_stat('precise')
 print format_stat('imprecise')
-print format_stat('half-mistakes')
-print format_stat('mistakes')
+print format_stat('false-positives')
 print format_stat('undetected')
 print r'\hline'
 print format_stat('total')
-print r'\\'
-print r'%-15s & %6.1f & \\' % ('spurious average',
-        float(stats['spurious']['tot']) / len(stats['precise']))
-print r'%-15s & %6d & \\' % ('spurious max',
-        float(stats['spurious']['max']))
-print r'\hline'
-