0b55f123 |
1 | /***** spin: ps_msc.c *****/ |
2 | |
3 | /* Copyright (c) 1997-2003 by Lucent Technologies, Bell Laboratories. */ |
4 | /* All Rights Reserved. This software is for educational purposes only. */ |
5 | /* No guarantee whatsoever is expressed or implied by the distribution of */ |
6 | /* this code. Permission is given to distribute this code provided that */ |
7 | /* this introductory message is not removed and no monies are exchanged. */ |
8 | /* Software written by Gerard J. Holzmann. For tool documentation see: */ |
9 | /* http://spinroot.com/ */ |
10 | /* Send all bug-reports and/or questions to: bugs@spinroot.com */ |
11 | |
12 | /* The Postscript generation code below was written by Gerard J. Holzmann */ |
13 | /* in June 1997. Parts of the prolog template are based on similar boiler */ |
14 | /* plate in the Tcl/Tk distribution. This code is used to support Spin's */ |
15 | /* option -M for generating a Postscript file from a simulation run. */ |
16 | |
17 | #include "spin.h" |
18 | #include "version.h" |
19 | |
20 | /* extern void free(void *); */ |
21 | |
22 | static char *PsPre[] = { |
23 | "%%%%Pages: (atend)", |
24 | "%%%%PageOrder: Ascend", |
25 | "%%%%DocumentData: Clean7Bit", |
26 | "%%%%Orientation: Portrait", |
27 | "%%%%DocumentNeededResources: font Courier-Bold", |
28 | "%%%%EndComments", |
29 | "", |
30 | "%%%%BeginProlog", |
31 | "50 dict begin", |
32 | "", |
33 | "/baseline 0 def", |
34 | "/height 0 def", |
35 | "/justify 0 def", |
36 | "/lineLength 0 def", |
37 | "/spacing 0 def", |
38 | "/stipple 0 def", |
39 | "/strings 0 def", |
40 | "/xoffset 0 def", |
41 | "/yoffset 0 def", |
42 | "", |
43 | "/ISOEncode {", |
44 | " dup length dict begin", |
45 | " {1 index /FID ne {def} {pop pop} ifelse} forall", |
46 | " /Encoding ISOLatin1Encoding def", |
47 | " currentdict", |
48 | " end", |
49 | " /Temporary exch definefont", |
50 | "} bind def", |
51 | "", |
52 | "/AdjustColor {", |
53 | " CL 2 lt {", |
54 | " currentgray", |
55 | " CL 0 eq {", |
56 | " .5 lt {0} {1} ifelse", |
57 | " } if", |
58 | " setgray", |
59 | " } if", |
60 | "} bind def", |
61 | "", |
62 | "/DrawText {", |
63 | " /stipple exch def", |
64 | " /justify exch def", |
65 | " /yoffset exch def", |
66 | " /xoffset exch def", |
67 | " /spacing exch def", |
68 | " /strings exch def", |
69 | " /lineLength 0 def", |
70 | " strings {", |
71 | " stringwidth pop", |
72 | " dup lineLength gt {/lineLength exch def} {pop} ifelse", |
73 | " newpath", |
74 | " } forall", |
75 | " 0 0 moveto (TXygqPZ) false charpath", |
76 | " pathbbox dup /baseline exch def", |
77 | " exch pop exch sub /height exch def pop", |
78 | " newpath", |
79 | " translate", |
80 | " lineLength xoffset mul", |
81 | " strings length 1 sub spacing mul height add yoffset mul translate", |
82 | " justify lineLength mul baseline neg translate", |
83 | " strings {", |
84 | " dup stringwidth pop", |
85 | " justify neg mul 0 moveto", |
86 | " stipple {", |
87 | " gsave", |
88 | " /char (X) def", |
89 | " {", |
90 | " char 0 3 -1 roll put", |
91 | " currentpoint", |
92 | " gsave", |
93 | " char true charpath clip StippleText", |
94 | " grestore", |
95 | " char stringwidth translate", |
96 | " moveto", |
97 | " } forall", |
98 | " grestore", |
99 | " } {show} ifelse", |
100 | " 0 spacing neg translate", |
101 | " } forall", |
102 | "} bind def", |
103 | "%%%%EndProlog", |
104 | "%%%%BeginSetup", |
105 | "/CL 2 def", |
106 | "%%%%IncludeResource: font Courier-Bold", |
107 | "%%%%EndSetup", |
108 | 0, |
109 | }; |
110 | |
111 | static int MH = 600; /* page height - can be scaled */ |
112 | static int oMH = 600; /* page height - not scaled */ |
113 | #define MW 500 /* page width */ |
114 | #define LH 100 /* bottom margin */ |
115 | #define RH 100 /* right margin */ |
116 | #define WW 50 /* distance between process lines */ |
117 | #define HH 8 /* vertical distance between steps */ |
118 | #define PH 14 /* height of process-tag headers */ |
119 | |
120 | static FILE *pfd; |
121 | static char **I; /* initial procs */ |
122 | static int *D,*R; /* maps between depth and ldepth */ |
123 | static short *M; /* x location of each box at index y */ |
124 | static short *T; /* y index of match for each box at index y */ |
125 | static char **L; /* text labels */ |
126 | static char *ProcLine; /* active processes */ |
127 | static int pspno = 0; /* postscript page */ |
128 | static int ldepth = 1; |
129 | static int maxx, TotSteps = 2*4096; /* max nr of steps, about 40 pages */ |
130 | static float Scaler = (float) 1.0; |
131 | |
132 | extern int ntrail, s_trail, pno, depth; |
133 | extern Symbol *oFname; |
134 | extern void exit(int); |
135 | void putpages(void); |
136 | void spitbox(int, int, int, char *); |
137 | |
138 | void |
139 | putlegend(void) |
140 | { |
141 | fprintf(pfd, "gsave\n"); |
142 | fprintf(pfd, "/Courier-Bold findfont 8 scalefont "); |
143 | fprintf(pfd, "ISOEncode setfont\n"); |
144 | fprintf(pfd, "0.000 0.000 0.000 setrgbcolor AdjustColor\n"); |
145 | fprintf(pfd, "%d %d [\n", MW/2, LH+oMH+ 5*HH); |
146 | fprintf(pfd, " (%s -- %s -- MSC -- %d)\n] 10 -0.5 0.5 0 ", |
147 | SpinVersion, oFname?oFname->name:"", pspno); |
148 | fprintf(pfd, "false DrawText\ngrestore\n"); |
149 | } |
150 | |
151 | void |
152 | startpage(void) |
153 | { int i; |
154 | |
155 | pspno++; |
156 | fprintf(pfd, "%%%%Page: %d %d\n", pspno, pspno); |
157 | putlegend(); |
158 | |
159 | for (i = TotSteps-1; i >= 0; i--) |
160 | { if (!I[i]) continue; |
161 | spitbox(i, RH, -PH, I[i]); |
162 | } |
163 | |
164 | fprintf(pfd, "save\n"); |
165 | fprintf(pfd, "10 %d moveto\n", LH+oMH+5); |
166 | fprintf(pfd, "%d %d lineto\n", RH+MW, LH+oMH+5); |
167 | fprintf(pfd, "%d %d lineto\n", RH+MW, LH); |
168 | fprintf(pfd, "10 %d lineto\n", LH); |
169 | fprintf(pfd, "closepath clip newpath\n"); |
170 | fprintf(pfd, "%f %f translate\n", |
171 | (float) RH, (float) LH); |
172 | memset(ProcLine, 0, 256*sizeof(char)); |
173 | if (Scaler != 1.0) |
174 | fprintf(pfd, "%f %f scale\n", Scaler, Scaler); |
175 | } |
176 | |
177 | void |
178 | putprelude(void) |
179 | { char snap[256]; FILE *fd; |
180 | |
181 | sprintf(snap, "%s.ps", oFname?oFname->name:"msc"); |
182 | if (!(pfd = fopen(snap, "w"))) |
183 | fatal("cannot create file '%s'", snap); |
184 | |
185 | fprintf(pfd, "%%!PS-Adobe-2.0\n"); |
186 | fprintf(pfd, "%%%%Creator: %s\n", SpinVersion); |
187 | fprintf(pfd, "%%%%Title: MSC %s\n", oFname?oFname->name:"--"); |
188 | fprintf(pfd, "%%%%BoundingBox: 119 154 494 638\n"); |
189 | ntimes(pfd, 0, 1, PsPre); |
190 | |
191 | if (s_trail) |
192 | { if (ntrail) |
193 | sprintf(snap, "%s%d.trail", oFname?oFname->name:"msc", ntrail); |
194 | else |
195 | sprintf(snap, "%s.trail", oFname?oFname->name:"msc"); |
196 | if (!(fd = fopen(snap, "r"))) |
197 | { snap[strlen(snap)-2] = '\0'; |
198 | if (!(fd = fopen(snap, "r"))) |
199 | fatal("cannot open trail file", (char *) 0); |
200 | } |
201 | TotSteps = 1; |
202 | while (fgets(snap, 256, fd)) TotSteps++; |
203 | fclose(fd); |
204 | } |
205 | R = (int *) emalloc(TotSteps * sizeof(int)); |
206 | D = (int *) emalloc(TotSteps * sizeof(int)); |
207 | M = (short *) emalloc(TotSteps * sizeof(short)); |
208 | T = (short *) emalloc(TotSteps * sizeof(short)); |
209 | L = (char **) emalloc(TotSteps * sizeof(char *)); |
210 | I = (char **) emalloc(TotSteps * sizeof(char *)); |
211 | ProcLine = (char *) emalloc(1024 * sizeof(char)); |
212 | startpage(); |
213 | } |
214 | |
215 | void |
216 | putpostlude(void) |
217 | { putpages(); |
218 | fprintf(pfd, "%%%%Trailer\n"); |
219 | fprintf(pfd, "end\n"); |
220 | fprintf(pfd, "%%%%Pages: %d\n", pspno); |
221 | fprintf(pfd, "%%%%EOF\n"); |
222 | fclose(pfd); |
223 | /* stderr, in case user redirected output */ |
224 | fprintf(stderr, "spin: wrote %d pages into '%s.ps'\n", |
225 | pspno, oFname?oFname->name:"msc"); |
226 | exit(0); |
227 | } |
228 | |
229 | void |
230 | psline(int x0, int iy0, int x1, int iy1, float r, float g, float b, int w) |
231 | { int y0 = MH-iy0; |
232 | int y1 = MH-iy1; |
233 | |
234 | if (y1 > y0) y1 -= MH; |
235 | |
236 | fprintf(pfd, "gsave\n"); |
237 | fprintf(pfd, "%d %d moveto\n", x0*WW, y0); |
238 | fprintf(pfd, "%d %d lineto\n", x1*WW, y1); |
239 | fprintf(pfd, "%d setlinewidth\n", w); |
240 | fprintf(pfd, "0 setlinecap\n"); |
241 | fprintf(pfd, "1 setlinejoin\n"); |
242 | fprintf(pfd, "%f %f %f setrgbcolor AdjustColor\n", r,g,b); |
243 | fprintf(pfd, "stroke\ngrestore\n"); |
244 | } |
245 | |
246 | void |
247 | colbox(int x, int y, int w, int h, float r, float g, float b) |
248 | { fprintf(pfd, "%d %d moveto\n", x - w, y-h); |
249 | fprintf(pfd, "%d %d lineto\n", x + w, y-h); |
250 | fprintf(pfd, "%d %d lineto\n", x + w, y+h); |
251 | fprintf(pfd, "%d %d lineto\n", x - w, y+h); |
252 | fprintf(pfd, "%d %d lineto\n", x - w, y-h); |
253 | fprintf(pfd, "%f %f %f setrgbcolor AdjustColor\n", r,g,b); |
254 | fprintf(pfd, "closepath fill\n"); |
255 | } |
256 | |
257 | void |
258 | putgrid(int p) |
259 | { int i; |
260 | |
261 | for (i = p ; i >= 0; i--) |
262 | { if (!ProcLine[i]) |
263 | { psline(i, 0, i, MH-1, (float) (0.4), (float) (0.4), (float) (1.0), 1); |
264 | ProcLine[i] = 1; |
265 | } } |
266 | } |
267 | |
268 | void |
269 | putarrow(int from, int to) |
270 | { |
271 | T[D[from]] = D[to]; |
272 | } |
273 | |
274 | void |
275 | stepnumber(int i) |
276 | { int y = MH-(i*HH)%MH; |
277 | |
278 | fprintf(pfd, "gsave\n"); |
279 | fprintf(pfd, "/Courier-Bold findfont 6 scalefont "); |
280 | fprintf(pfd, "ISOEncode setfont\n"); |
281 | fprintf(pfd, "0.000 0.000 0.000 setrgbcolor AdjustColor\n"); |
282 | fprintf(pfd, "%d %d [\n", -40, y); |
283 | fprintf(pfd, " (%d)\n] 10 -0.5 0.5 0 ", R[i]); |
284 | fprintf(pfd, "false DrawText\ngrestore\n"); |
285 | fprintf(pfd, "%d %d moveto\n", -20, y); |
286 | fprintf(pfd, "%d %d lineto\n", M[i]*WW, y); |
287 | fprintf(pfd, "1 setlinewidth\n0 setlinecap\n1 setlinejoin\n"); |
288 | fprintf(pfd, "0.92 0.92 0.92 setrgbcolor AdjustColor\n"); |
289 | fprintf(pfd, "stroke\n"); |
290 | } |
291 | |
292 | void |
293 | spitbox(int x, int dx, int y, char *s) |
294 | { float r,g,b, bw; int a; char d[256]; |
295 | |
296 | if (!dx) |
297 | { stepnumber(y); |
298 | putgrid(x); |
299 | } |
300 | bw = (float)2.7*(float)strlen(s); |
301 | colbox(x*WW+dx, MH-(y*HH)%MH, (int) (bw+1.0), |
302 | 5, (float) 0.,(float) 0.,(float) 0.); |
303 | if (s[0] == '~') |
304 | { switch (s[1]) { |
305 | case 'B': r = (float) 0.2; g = (float) 0.2; b = (float) 1.; |
306 | break; |
307 | case 'G': r = (float) 0.2; g = (float) 1.; b = (float) 0.2; |
308 | break; |
309 | case 'R': |
310 | default : r = (float) 1.; g = (float) 0.2; b = (float) 0.2; |
311 | break; |
312 | } |
313 | s += 2; |
314 | } else if (strchr(s, '!')) |
315 | { r = (float) 1.; g = (float) 1.; b = (float) 1.; |
316 | } else if (strchr(s, '?')) |
317 | { r = (float) 0.; g = (float) 1.; b = (float) 1.; |
318 | } else |
319 | { r = (float) 1.; g = (float) 1.; b = (float) 0.; |
320 | if (!dx |
321 | && sscanf(s, "%d:%250s", &a, d) == 2 /* was &d */ |
322 | && a >= 0 && a < TotSteps) |
323 | { if (!I[a] |
324 | || strlen(I[a]) <= strlen(s)) |
325 | I[a] = emalloc((int) strlen(s)+1); |
326 | strcpy(I[a], s); |
327 | } } |
328 | colbox(x*WW+dx, MH-(y*HH)%MH, (int) bw, 4, r,g,b); |
329 | fprintf(pfd, "gsave\n"); |
330 | fprintf(pfd, "/Courier-Bold findfont 8 scalefont "); |
331 | fprintf(pfd, "ISOEncode setfont\n"); |
332 | fprintf(pfd, "0.000 0.000 0.000 setrgbcolor AdjustColor\n"); |
333 | fprintf(pfd, "%d %d [\n", x*WW+dx, MH-(y*HH)%MH); |
334 | fprintf(pfd, " (%s)\n] 10 -0.5 0.5 0 ", s); |
335 | fprintf(pfd, "false DrawText\ngrestore\n"); |
336 | } |
337 | |
338 | void |
339 | putpages(void) |
340 | { int i, lasti=0; float nmh; |
341 | |
342 | if (maxx*WW > MW-RH/2) |
343 | { Scaler = (float) (MW-RH/2) / (float) (maxx*WW); |
344 | fprintf(pfd, "%f %f scale\n", Scaler, Scaler); |
345 | nmh = (float) MH; nmh /= Scaler; MH = (int) nmh; |
346 | } |
347 | |
348 | for (i = TotSteps-1; i >= 0; i--) |
349 | { if (!I[i]) continue; |
350 | spitbox(i, 0, 0, I[i]); |
351 | } |
352 | if (ldepth >= TotSteps) ldepth = TotSteps-1; |
353 | for (i = 0; i <= ldepth; i++) |
354 | { if (!M[i] && !L[i]) continue; /* no box here */ |
355 | if (6+i*HH >= MH*pspno) |
356 | { fprintf(pfd, "showpage\nrestore\n"); startpage(); } |
357 | if (T[i] > 0) /* red arrow */ |
358 | { int reali = i*HH; |
359 | int realt = T[i]*HH; |
360 | int topop = (reali)/MH; topop *= MH; |
361 | reali -= topop; realt -= topop; |
362 | |
363 | if (M[i] == M[T[i]] && reali == realt) |
364 | /* an rv handshake */ |
365 | psline( M[lasti], reali+2-3*HH/2, |
366 | M[i], reali, |
367 | (float) 1.,(float) 0.,(float) 0., 2); |
368 | else |
369 | psline( M[i], reali, |
370 | M[T[i]], realt, |
371 | (float) 1.,(float) 0.,(float) 0., 2); |
372 | |
373 | if (realt >= MH) T[T[i]] = -i; |
374 | |
375 | } else if (T[i] < 0) /* arrow from prev page */ |
376 | { int reali = (-T[i])*HH; |
377 | int realt = i*HH; |
378 | int topop = (realt)/MH; topop *= MH; |
379 | reali -= topop; realt -= topop; |
380 | |
381 | psline( M[-T[i]], reali, |
382 | M[i], realt, |
383 | (float) 1., (float) 0., (float) 0., 2); |
384 | } |
385 | if (L[i]) |
386 | { spitbox(M[i], 0, i, L[i]); |
387 | /* free(L[i]); */ |
388 | lasti = i; |
389 | } |
390 | } |
391 | fprintf(pfd, "showpage\nrestore\n"); |
392 | } |
393 | |
394 | void |
395 | putbox(int x) |
396 | { |
397 | if (ldepth >= TotSteps) |
398 | { fprintf(stderr, "max length of %d steps exceeded - ps file truncated\n", |
399 | TotSteps); |
400 | putpostlude(); |
401 | } |
402 | M[ldepth] = x; |
403 | if (x > maxx) maxx = x; |
404 | } |
405 | |
406 | void |
407 | pstext(int x, char *s) |
408 | { char *tmp = emalloc((int) strlen(s)+1); |
409 | |
410 | strcpy(tmp, s); |
411 | if (depth == 0) |
412 | I[x] = tmp; |
413 | else |
414 | { putbox(x); |
415 | if (depth >= TotSteps || ldepth >= TotSteps) |
416 | { fprintf(stderr, "max nr of %d steps exceeded\n", |
417 | TotSteps); |
418 | fatal("aborting", (char *) 0); |
419 | } |
420 | |
421 | D[depth] = ldepth; |
422 | R[ldepth] = depth; |
423 | L[ldepth] = tmp; |
424 | ldepth += 2; |
425 | } |
426 | } |
427 | |
428 | void |
429 | dotag(FILE *fd, char *s) |
430 | { extern int columns, notabs; extern RunList *X; |
431 | int i = (!strncmp(s, "MSC: ", 5))?5:0; |
432 | int pid = s_trail ? pno : (X?X->pid:0); |
433 | |
434 | if (columns == 2) |
435 | pstext(pid, &s[i]); |
436 | else |
437 | { if (!notabs) |
438 | { printf(" "); |
439 | for (i = 0; i <= pid; i++) |
440 | printf(" "); |
441 | } |
442 | fprintf(fd, "%s", s); |
443 | fflush(fd); |
444 | } |
445 | } |