File: create_plot.awk

package info (click to toggle)
eprover 2.6%2Bds-3
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 21,288 kB
  • sloc: ansic: 331,111; csh: 12,026; python: 10,178; awk: 5,825; makefile: 461; sh: 389
file content (103 lines) | stat: -rwxr-xr-x 1,895 bytes parent folder | download | duplicates (2)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
#!/opt/local/bin/gawk -f

# Usage: create_plot.awk max [<file>...<file>]
#
# Copyright 1998 Stephan Schulz, schulz@informatik.tu-muenchen.de
#

function done_in_time(times, limit,               i, res)
{
   res = 0;

   for(i in times)
   {
      if((0+times[i])<=(0+limit))
      {
	 res++;
      }
   }
   return res;
}

function compute_distrib(times, file,   i)
{
   print "# new file" > file;
   for(i=0; i<=max_time; i+=(max_time/300))
   {
      print done_in_time(times,i) >> file; 
   }
   print "\n\n" >> file;
}


BEGIN{
   if(!ARGV[1] )
   {
      print "Usage: create_plot.awk max [<file>...[<file>]]";
      exit(1);
   }
   max_time = ARGV[1];
   ARGV[1] = "";
   if(!ARGV[2])
   {
      ARGV[2] = "-";
      ARGC++;
   }   
   proc_arg = 0;
   fileno = 0;
   counter = 0;
   plot = "set key bottom\nset term postscript eps monochrome \"Times-Roman\"\nplot ";
   sep = "";
   last_file = "";
   title["protokoll_CW21"] = "1";
   title["protokoll_FFRW21mix"] = "2";
   title["protokoll_TSM36c"] = "3"
   title["protokoll_TSM32"] = "3"
}

# Skipping comments

/^#/{
 next;
}

# Process all non-empty lines

/[A-Za-z0-9]+/{
   if(ARGIND != proc_arg)
   {
      if(fileno)
      {
	 compute_distrib(times, "plotfile" fileno);
	 delete times;
	 first = 0;
	 plot = plot sep "\"plotfile" fileno "\" title \"" title[last_file] "\"";
	 sep = ",";
	 counter = 0;
      }
      proc_arg = ARGIND;
      last_file = ARGV[proc_arg];
      fileno++;
   }
   else if($2!="F")
   {
      times[counter++] = $3;
   }
}


END{
   compute_distrib(times, "plotfile" fileno);
   plot = plot sep "\"plotfile" fileno "\" title \"" title[last_file] "\"";
   print "set data style lines" | "gnuplot";
   print "set yrange [0:]" | "gnuplot";
   print plot | "gnuplot";
   print "Press return to continue" >> "/dev/stderr";
   getline < "/dev/stdin"; 
   close("gnuplot");
   system("rm plotfile*");
}