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