1 /***** spin: ps_msc.c *****/
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 */
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. */
21 extern void free(void *);
24 static char *PsPre[] = {
26 "%%%%PageOrder: Ascend",
27 "%%%%DocumentData: Clean7Bit",
28 "%%%%Orientation: Portrait",
29 "%%%%DocumentNeededResources: font Courier-Bold",
46 " dup length dict begin",
47 " {1 index /FID ne {def} {pop pop} ifelse} forall",
48 " /Encoding ISOLatin1Encoding def",
51 " /Temporary exch definefont",
58 " .5 lt {0} {1} ifelse",
74 " dup lineLength gt {/lineLength exch def} {pop} ifelse",
77 " 0 0 moveto (TXygqPZ) false charpath",
78 " pathbbox dup /baseline exch def",
79 " exch pop exch sub /height exch def pop",
82 " lineLength xoffset mul",
83 " strings length 1 sub spacing mul height add yoffset mul translate",
84 " justify lineLength mul baseline neg translate",
86 " dup stringwidth pop",
87 " justify neg mul 0 moveto",
92 " char 0 3 -1 roll put",
95 " char true charpath clip StippleText",
97 " char stringwidth translate",
102 " 0 spacing neg translate",
108 "%%%%IncludeResource: font Courier-Bold",
113 int MH = 600; /* page height - can be scaled */
114 int oMH = 600; /* page height - not scaled */
115 #define MW 500 /* page width */
116 #define LH 100 /* bottom margin */
117 #define RH 100 /* right margin */
118 #define WW 50 /* distance between process lines */
119 #define HH 8 /* vertical distance between steps */
120 #define PH 14 /* height of process-tag headers */
123 static char **I; /* initial procs */
124 static int *D,*R; /* maps between depth and ldepth */
125 static short *M; /* x location of each box at index y */
126 static short *T; /* y index of match for each box at index y */
127 static char **L; /* text labels */
128 static char *ProcLine; /* active processes */
129 static int pspno = 0; /* postscript page */
130 static int ldepth = 1;
131 static int maxx, TotSteps = 2*4096; /* max nr of steps, about 40 pages */
132 static float Scaler = (float) 1.0;
134 extern int ntrail, s_trail, pno, depth;
135 extern Symbol *oFname;
136 extern void exit(int);
138 void spitbox(int, int, int, char *);
143 fprintf(pfd, "gsave\n");
144 fprintf(pfd, "/Courier-Bold findfont 8 scalefont ");
145 fprintf(pfd, "ISOEncode setfont\n");
146 fprintf(pfd, "0.000 0.000 0.000 setrgbcolor AdjustColor\n");
147 fprintf(pfd, "%d %d [\n", MW/2, LH+oMH+ 5*HH);
148 fprintf(pfd, " (%s -- %s -- MSC -- %d)\n] 10 -0.5 0.5 0 ",
149 Version, oFname?oFname->name:"", pspno);
150 fprintf(pfd, "false DrawText\ngrestore\n");
158 fprintf(pfd, "%%%%Page: %d %d\n", pspno, pspno);
161 for (i = TotSteps-1; i >= 0; i--)
162 { if (!I[i]) continue;
163 spitbox(i, RH, -PH, I[i]);
166 fprintf(pfd, "save\n");
167 fprintf(pfd, "10 %d moveto\n", LH+oMH+5);
168 fprintf(pfd, "%d %d lineto\n", RH+MW, LH+oMH+5);
169 fprintf(pfd, "%d %d lineto\n", RH+MW, LH);
170 fprintf(pfd, "10 %d lineto\n", LH);
171 fprintf(pfd, "closepath clip newpath\n");
172 fprintf(pfd, "%f %f translate\n",
173 (float) RH, (float) LH);
174 memset(ProcLine, 0, 256*sizeof(char));
176 fprintf(pfd, "%f %f scale\n", Scaler, Scaler);
181 { char snap[256]; FILE *fd;
183 sprintf(snap, "%s.ps", oFname?oFname->name:"msc");
184 if (!(pfd = fopen(snap, "w")))
185 fatal("cannot create file '%s'", snap);
187 fprintf(pfd, "%%!PS-Adobe-2.0\n");
188 fprintf(pfd, "%%%%Creator: %s\n", Version);
189 fprintf(pfd, "%%%%Title: MSC %s\n", oFname?oFname->name:"--");
190 fprintf(pfd, "%%%%BoundingBox: 119 154 494 638\n");
191 ntimes(pfd, 0, 1, PsPre);
195 sprintf(snap, "%s%d.trail", oFname?oFname->name:"msc", ntrail);
197 sprintf(snap, "%s.trail", oFname?oFname->name:"msc");
198 if (!(fd = fopen(snap, "r")))
199 { snap[strlen(snap)-2] = '\0';
200 if (!(fd = fopen(snap, "r")))
201 fatal("cannot open trail file", (char *) 0);
204 while (fgets(snap, 256, fd)) TotSteps++;
207 R = (int *) emalloc(TotSteps * sizeof(int));
208 D = (int *) emalloc(TotSteps * sizeof(int));
209 M = (short *) emalloc(TotSteps * sizeof(short));
210 T = (short *) emalloc(TotSteps * sizeof(short));
211 L = (char **) emalloc(TotSteps * sizeof(char *));
212 I = (char **) emalloc(TotSteps * sizeof(char *));
213 ProcLine = (char *) emalloc(1024 * sizeof(char));
220 fprintf(pfd, "%%%%Trailer\n");
221 fprintf(pfd, "end\n");
222 fprintf(pfd, "%%%%Pages: %d\n", pspno);
223 fprintf(pfd, "%%%%EOF\n");
225 /* stderr, in case user redirected output */
226 fprintf(stderr, "spin: wrote %d pages into '%s.ps'\n",
227 pspno, oFname?oFname->name:"msc");
231 psline(int x0, int iy0, int x1, int iy1, float r, float g, float b, int w)
235 if (y1 > y0) y1 -= MH;
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");
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");
262 for (i = p ; i >= 0; i--)
264 { psline(i,0, i,MH-1,
265 (float) 0.4, (float) 0.4, (float) 1.0, 1);
271 putarrow(int from, int to)
278 { int y = MH-(i*HH)%MH;
280 fprintf(pfd, "gsave\n");
281 fprintf(pfd, "/Courier-Bold findfont 6 scalefont ");
282 fprintf(pfd, "ISOEncode setfont\n");
283 fprintf(pfd, "0.000 0.000 0.000 setrgbcolor AdjustColor\n");
284 fprintf(pfd, "%d %d [\n", -40, y);
285 fprintf(pfd, " (%d)\n] 10 -0.5 0.5 0 ", R[i]);
286 fprintf(pfd, "false DrawText\ngrestore\n");
287 fprintf(pfd, "%d %d moveto\n", -20, y);
288 fprintf(pfd, "%d %d lineto\n", M[i]*WW, y);
289 fprintf(pfd, "1 setlinewidth\n0 setlinecap\n1 setlinejoin\n");
290 fprintf(pfd, "0.92 0.92 0.92 setrgbcolor AdjustColor\n");
291 fprintf(pfd, "stroke\n");
295 spitbox(int x, int dx, int y, char *s)
296 { float r,g,b, bw; int a; char d[256];
302 bw = (float)2.7*(float)strlen(s);
303 colbox(x*WW+dx, MH-(y*HH)%MH, (int) (bw+1.0),
304 5, (float) 0.,(float) 0.,(float) 0.);
307 case 'B': r = (float) 0.2; g = (float) 0.2; b = (float) 1.;
309 case 'G': r = (float) 0.2; g = (float) 1.; b = (float) 0.2;
312 default : r = (float) 1.; g = (float) 0.2; b = (float) 0.2;
316 } else if (strchr(s, '!'))
317 { r = (float) 1.; g = (float) 1.; b = (float) 1.;
318 } else if (strchr(s, '?'))
319 { r = (float) 0.; g = (float) 1.; b = (float) 1.;
321 { r = (float) 1.; g = (float) 1.; b = (float) 0.;
323 && sscanf(s, "%d:%s", &a, d) == 2 /* was &d */
324 && a >= 0 && a < TotSteps)
326 || strlen(I[a]) <= strlen(s))
327 I[a] = emalloc((int) strlen(s)+1);
330 colbox(x*WW+dx, MH-(y*HH)%MH, (int) bw, 4, r,g,b);
331 fprintf(pfd, "gsave\n");
332 fprintf(pfd, "/Courier-Bold findfont 8 scalefont ");
333 fprintf(pfd, "ISOEncode setfont\n");
334 fprintf(pfd, "0.000 0.000 0.000 setrgbcolor AdjustColor\n");
335 fprintf(pfd, "%d %d [\n", x*WW+dx, MH-(y*HH)%MH);
336 fprintf(pfd, " (%s)\n] 10 -0.5 0.5 0 ", s);
337 fprintf(pfd, "false DrawText\ngrestore\n");
342 { int i, lasti=0; float nmh;
344 if (maxx*WW > MW-RH/2)
345 { Scaler = (float) (MW-RH/2) / (float) (maxx*WW);
346 fprintf(pfd, "%f %f scale\n", Scaler, Scaler);
347 nmh = (float) MH; nmh /= Scaler; MH = (int) nmh;
350 for (i = TotSteps-1; i >= 0; i--)
351 { if (!I[i]) continue;
352 spitbox(i, 0, 0, I[i]);
354 if (ldepth >= TotSteps) ldepth = TotSteps-1;
355 for (i = 0; i <= ldepth; i++)
356 { if (!M[i] && !L[i]) continue; /* no box here */
357 if (6+i*HH >= MH*pspno)
358 { fprintf(pfd, "showpage\nrestore\n"); startpage(); }
359 if (T[i] > 0) /* red arrow */
362 int topop = (reali)/MH; topop *= MH;
363 reali -= topop; realt -= topop;
365 if (M[i] == M[T[i]] && reali == realt)
366 /* an rv handshake */
367 psline( M[lasti], reali+2-3*HH/2,
369 (float) 1.,(float) 0.,(float) 0., 2);
373 (float) 1.,(float) 0.,(float) 0., 2);
375 if (realt >= MH) T[T[i]] = -i;
377 } else if (T[i] < 0) /* arrow from prev page */
378 { int reali = (-T[i])*HH;
380 int topop = (realt)/MH; topop *= MH;
381 reali -= topop; realt -= topop;
383 psline( M[-T[i]], reali,
385 (float) 1., (float) 0., (float) 0., 2);
388 { spitbox(M[i], 0, i, L[i]);
393 fprintf(pfd, "showpage\nrestore\n");
399 if (ldepth >= TotSteps)
401 fprintf(stderr, "max length of %d steps exceeded\n",
403 fatal("postscript file truncated", (char *) 0);
406 if (x > maxx) maxx = x;
410 pstext(int x, char *s)
411 { char *tmp = emalloc((int) strlen(s)+1);
418 if (depth >= TotSteps || ldepth >= TotSteps)
419 { fprintf(stderr, "max nr of %d steps exceeded\n",
421 fatal("aborting", (char *) 0);
432 dotag(FILE *fd, char *s)
433 { extern int columns, notabs; extern RunList *X;
434 int i = (!strncmp(s, "MSC: ", 5))?5:0;
435 int pid = s_trail ? pno : (X?X->pid:0);
442 for (i = 0; i <= pid; i++)
445 fprintf(fd, "%s", s);