...

diff --git a/helm/software/matita/bench_summary.py b/helm/software/matita/bench_summary.py
new file mode 100755 (executable)
index 0000000..d16f9a2
--- /dev/null
+++ b/helm/software/matita/bench_summary.py
@@ -0,0 +1,63 @@
+#!/usr/bin/python
+import sys
+
+stats = {}
+stats['precise'] = []
+stats['imprecise'] = []
+stats['total'] = 0
+stats['spurious'] = {'tot': 0, 'max': 0, 'names': []}
+stats['half-mistakes'] = []
+stats['mistakes'] = []
+stats['undetected'] = []
+
+for line in open(sys.argv[1]):
+    if line[0] == '#':
+        continue
+    cols = line.split('|')
+    name = cols[0]
+    if cols[1] != 'KO':
+        print >> sys.stderr, "Warning: outcome is %s" % 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:
+        if expected_error in spurious_errors:
+            stats['half-mistakes'].append(name)
+        else:
+            stats['precise'].append(name)
+            stats['spurious']['max'] = max(len(spurious_errors), stats['spurious']['max'])
+            stats['spurious']['tot'] += len(spurious_errors)
+    elif expected_error in real_errors:
+        if expected_error in spurious_errors:
+            stats['half-mistakes'].append(name)
+        else:
+            stats['imprecise'].append(name)
+    else:
+        if expected_error in spurious_errors:
+            stats['mistakes'].append(name)
+        else:
+            stats['undetected'].append(name)
+
+for field in ['undetected', 'imprecise', 'mistakes', 'half-mistakes']:
+    print "===================="
+    print "%s:" % field
+    for name in stats[field]:
+        print "  %s" % name
+print "\n"
+print 'precise:\t%3d' % len(stats['precise'])
+print 'imprecise:\t%3d' % len(stats['imprecise'])
+print 'half-mistakes:\t%3d' % len(stats['half-mistakes'])
+print 'mistakes:\t%3d' % len(stats['mistakes'])
+print 'undetected:\t%3d' % len(stats['undetected'])
+print 'TOTAL:\t\t%3d' % stats['total'], "\n"
+
+print 'average spurious errors no: ', float(stats['spurious']['tot']) / len(stats['precise'])
+
+#for field, value in stats.iteritems():
+#    if field == 'spurious':
+#        value['avg'] = float(value['tot']) / stats['precise']
+#    print "%s: %s" % (field, value)
+