1#!/sw/bin/gawk -f
2
3# Usage: eauswert.awk <result_file>
4#
5# Copyright 1998 Stephan Schulz, schulz@informatik.tu-muenchen.de
6#
7# Read a protocol file (as e.g. written by distribute_eprover.awk)
8# and summarize it, reporting successes, timeouts, out-of
9# memory-failures and potential bugs.
10#
11
12BEGIN{
13  ttime = 0.0;
14  if(!ARGV[2])
15  {
16    proc_limit = int(1000000); /* Large enough */
17  }
18  else
19  {
20    proc_limit = ARGV[2];
21    sub("0*", "" , proc_limit);
22    proc_limit = int(proc_limit);
23  }
24
25  if(!ARGV[3])
26  {
27     timelimit = 1000000.0; /* Large enough */
28  }
29  else
30  {
31    timelimit = ARGV[3];
32    sub("0*", "" , timelimit);
33    timelimit = float(timelimit);
34  }
35  succ = 0;
36  total = 0;
37  bugs = 0;
38  nomem = 0;
39  incomplete=0;
40  ARGC=2;
41
42  if(ARGV[1]=="-")
43    {
44      ARGV[1]="";
45    }
46
47  if(ARGV[1])
48    {
49      test1 = getline < ARGV[1];
50      close(ARGV[1]);
51      if(test1 == -1)
52	{
53	  if(!index(ARGV[1],"PROTOCOL"))
54	    {
55	      if(substr(ARGV[1], length(ARGV[1]))!="/")
56		{
57		  ARGV[1] = ARGV[1] "/";
58		}
59	      ARGV[1] = ARGV[1] "PROTOCOL";
60	    }
61	}
62    }
63}
64
65
66function float(x)
67{
68   return 0.0+x+0.0;
69}
70
71!(/^#/) && !(/^%/){
72   if((total < proc_limit))
73   {
74      total++;
75      if(($2 == "F")||((float($3))>= timelimit))
76      {
77	 if($4 == "unknown")
78	 {
79	    bugs++;
80	 }
81	 if($4 == "maxmem" && ((float($3)) < timelimit))
82	 {
83	    nomem++;
84	 }
85	 if($4 == "incomplete" && ((float($3)) < timelimit))
86	 {
87	    incomplete++;
88	 }
89      }
90      else
91      {
92	 /* if(($2 == "N")) */
93	 {
94	    succ++;
95	    ttime+=$3;
96	 }
97      }
98   }
99}
100
101END{
102  printf "Total : %4d S/F/I/N/B: %5d/%5d/%3d/%3d/%3d Time: %f\n",
103         total, succ, total-succ, incomplete, nomem, bugs, ttime;
104}
105