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, 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 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 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 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 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 270 putarrow(int from, int to) 271 { 272 T[D[from]] = D[to]; 273 } 274 275 void 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 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 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 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 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 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