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
putlegend(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
startpage(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
putprelude(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, MFLAGS)))
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 TotSteps += 10;
206 R = (int *) emalloc(TotSteps * sizeof(int));
207 D = (int *) emalloc(TotSteps * sizeof(int));
208 M = (short *) emalloc(TotSteps * sizeof(short));
209 T = (short *) emalloc(TotSteps * sizeof(short));
210 L = (char **) emalloc(TotSteps * sizeof(char *));
211 I = (char **) emalloc(TotSteps * sizeof(char *));
212 ProcLine = (char *) emalloc(1024 * sizeof(char));
213 startpage();
214 }
215
216 void
putpostlude(void)217 putpostlude(void)
218 { putpages();
219 fprintf(pfd, "%%%%Trailer\n");
220 fprintf(pfd, "end\n");
221 fprintf(pfd, "%%%%Pages: %d\n", pspno);
222 fprintf(pfd, "%%%%EOF\n");
223 fclose(pfd);
224 /* stderr, in case user redirected output */
225 fprintf(stderr, "spin: wrote %d pages into '%s.ps'\n",
226 pspno, oFname?oFname->name:"msc");
227 exit(0);
228 }
229
230 void
psline(int x0,int iy0,int x1,int iy1,float r,float g,float b,int w)231 psline(int x0, int iy0, int x1, int iy1, float r, float g, float b, int w)
232 { int y0 = MH-iy0;
233 int y1 = MH-iy1;
234
235 if (y1 > y0) y1 -= MH;
236
237 fprintf(pfd, "gsave\n");
238 fprintf(pfd, "%d %d moveto\n", x0*WW, y0);
239 fprintf(pfd, "%d %d lineto\n", x1*WW, y1);
240 fprintf(pfd, "%d setlinewidth\n", w);
241 fprintf(pfd, "0 setlinecap\n");
242 fprintf(pfd, "1 setlinejoin\n");
243 fprintf(pfd, "%f %f %f setrgbcolor AdjustColor\n", r,g,b);
244 fprintf(pfd, "stroke\ngrestore\n");
245 }
246
247 void
colbox(int x,int y,int w,int h,float r,float g,float b)248 colbox(int x, int y, int w, int h, float r, float g, float b)
249 { fprintf(pfd, "%d %d moveto\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, "%d %d lineto\n", x - w, y-h);
254 fprintf(pfd, "%f %f %f setrgbcolor AdjustColor\n", r,g,b);
255 fprintf(pfd, "closepath fill\n");
256 }
257
258 void
putgrid(int p)259 putgrid(int p)
260 { int i;
261
262 for (i = p ; i >= 0; i--)
263 { if (!ProcLine[i])
264 { psline(i, 0, i, MH-1, (float) (0.4), (float) (0.4), (float) (1.0), 1);
265 ProcLine[i] = 1;
266 } }
267 }
268
269 void
putarrow(int from,int to)270 putarrow(int from, int to)
271 {
272 T[D[from]] = D[to];
273 }
274
275 void
stepnumber(int i)276 stepnumber(int i)
277 { int y = MH-(i*HH)%MH;
278
279 fprintf(pfd, "gsave\n");
280 fprintf(pfd, "/Courier-Bold findfont 6 scalefont ");
281 fprintf(pfd, "ISOEncode setfont\n");
282 fprintf(pfd, "0.000 0.000 0.000 setrgbcolor AdjustColor\n");
283 fprintf(pfd, "%d %d [\n", -40, y);
284 fprintf(pfd, " (%d)\n] 10 -0.5 0.5 0 ", R[i]);
285 fprintf(pfd, "false DrawText\ngrestore\n");
286 fprintf(pfd, "%d %d moveto\n", -20, y);
287 fprintf(pfd, "%d %d lineto\n", M[i]*WW, y);
288 fprintf(pfd, "1 setlinewidth\n0 setlinecap\n1 setlinejoin\n");
289 fprintf(pfd, "0.92 0.92 0.92 setrgbcolor AdjustColor\n");
290 fprintf(pfd, "stroke\n");
291 }
292
293 void
spitbox(int x,int dx,int y,char * s)294 spitbox(int x, int dx, int y, char *s)
295 { float r,g,b, bw; int a; char d[256];
296
297 if (!dx)
298 { stepnumber(y);
299 putgrid(x);
300 }
301 bw = (float)2.7*(float)strlen(s);
302 colbox(x*WW+dx, MH-(y*HH)%MH, (int) (bw+1.0),
303 5, (float) 0.,(float) 0.,(float) 0.);
304 if (s[0] == '~')
305 { switch (s[1]) {
306 case 'B': r = (float) 0.2; g = (float) 0.2; b = (float) 1.;
307 break;
308 case 'G': r = (float) 0.2; g = (float) 1.; b = (float) 0.2;
309 break;
310 case 'R':
311 default : r = (float) 1.; g = (float) 0.2; b = (float) 0.2;
312 break;
313 }
314 s += 2;
315 } else if (strchr(s, '!'))
316 { r = (float) 1.; g = (float) 1.; b = (float) 1.;
317 } else if (strchr(s, '?'))
318 { r = (float) 0.; g = (float) 1.; b = (float) 1.;
319 } else
320 { r = (float) 1.; g = (float) 1.; b = (float) 0.;
321 if (!dx
322 && sscanf(s, "%d:%250s", &a, d) == 2 /* was &d */
323 && a >= 0 && a < TotSteps)
324 { if (!I[a]
325 || strlen(I[a]) <= strlen(s))
326 I[a] = emalloc((int) strlen(s)+1);
327 strcpy(I[a], s);
328 } }
329 colbox(x*WW+dx, MH-(y*HH)%MH, (int) bw, 4, r,g,b);
330 fprintf(pfd, "gsave\n");
331 fprintf(pfd, "/Courier-Bold findfont 8 scalefont ");
332 fprintf(pfd, "ISOEncode setfont\n");
333 fprintf(pfd, "0.000 0.000 0.000 setrgbcolor AdjustColor\n");
334 fprintf(pfd, "%d %d [\n", x*WW+dx, MH-(y*HH)%MH);
335 fprintf(pfd, " (%s)\n] 10 -0.5 0.5 0 ", s);
336 fprintf(pfd, "false DrawText\ngrestore\n");
337 }
338
339 void
putpages(void)340 putpages(void)
341 { int i, lasti=0; float nmh;
342
343 if (maxx*WW > MW-RH/2)
344 { Scaler = (float) (MW-RH/2) / (float) (maxx*WW);
345 fprintf(pfd, "%f %f scale\n", Scaler, Scaler);
346 nmh = (float) MH; nmh /= Scaler; MH = (int) nmh;
347 }
348
349 for (i = TotSteps-1; i >= 0; i--)
350 { if (!I[i]) continue;
351 spitbox(i, 0, 0, I[i]);
352 }
353 if (ldepth >= TotSteps) ldepth = TotSteps-1;
354 for (i = 0; i <= ldepth; i++)
355 { if (!M[i] && !L[i]) continue; /* no box here */
356 if (6+i*HH >= MH*pspno)
357 { fprintf(pfd, "showpage\nrestore\n"); startpage(); }
358 if (T[i] > 0) /* red arrow */
359 { int reali = i*HH;
360 int realt = T[i]*HH;
361 int topop = (reali)/MH; topop *= MH;
362 reali -= topop; realt -= topop;
363
364 if (M[i] == M[T[i]] && reali == realt)
365 /* an rv handshake */
366 psline( M[lasti], reali+2-3*HH/2,
367 M[i], reali,
368 (float) 1.,(float) 0.,(float) 0., 2);
369 else
370 psline( M[i], reali,
371 M[T[i]], realt,
372 (float) 1.,(float) 0.,(float) 0., 2);
373
374 if (realt >= MH) T[T[i]] = -i;
375
376 } else if (T[i] < 0) /* arrow from prev page */
377 { int reali = (-T[i])*HH;
378 int realt = i*HH;
379 int topop = (realt)/MH; topop *= MH;
380 reali -= topop; realt -= topop;
381
382 psline( M[-T[i]], reali,
383 M[i], realt,
384 (float) 1., (float) 0., (float) 0., 2);
385 }
386 if (L[i])
387 { spitbox(M[i], 0, i, L[i]);
388 /* free(L[i]); */
389 lasti = i;
390 }
391 }
392 fprintf(pfd, "showpage\nrestore\n");
393 }
394
395 void
putbox(int x)396 putbox(int x)
397 {
398 if (ldepth >= TotSteps)
399 { fprintf(stderr, "max length of %d steps exceeded - ps file truncated\n",
400 TotSteps);
401 putpostlude();
402 }
403 M[ldepth] = x;
404 if (x > maxx) maxx = x;
405 }
406
407 void
pstext(int x,char * s)408 pstext(int x, char *s)
409 { char *tmp = emalloc((int) strlen(s)+1);
410
411 strcpy(tmp, s);
412 if (depth == 0)
413 I[x] = tmp;
414 else
415 { putbox(x);
416 if (depth >= TotSteps || ldepth >= TotSteps)
417 { fprintf(stderr, "max nr of %d steps exceeded\n",
418 TotSteps);
419 fatal("aborting", (char *) 0);
420 }
421
422 D[depth] = ldepth;
423 R[ldepth] = depth;
424 L[ldepth] = tmp;
425 ldepth += 2;
426 }
427 }
428
429 void
dotag(FILE * fd,char * s)430 dotag(FILE *fd, char *s)
431 { extern int columns, notabs; extern RunList *X;
432 int i = (!strncmp(s, "MSC: ", 5))?5:0;
433 int pid = s_trail ? pno : (X?X->pid:0);
434
435 if (columns == 2)
436 pstext(pid, &s[i]);
437 else
438 { if (!notabs)
439 { printf(" ");
440 for (i = 0; i <= pid; i++)
441 printf(" ");
442 }
443 fprintf(fd, "%s", s);
444 fflush(fd);
445 }
446 }
447