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 #ifdef PC 21 extern void free(void *); 22 #endif 23 24 static char *PsPre[] = { 25 "%%%%Pages: (atend)", 26 "%%%%PageOrder: Ascend", 27 "%%%%DocumentData: Clean7Bit", 28 "%%%%Orientation: Portrait", 29 "%%%%DocumentNeededResources: font Courier-Bold", 30 "%%%%EndComments", 31 "", 32 "%%%%BeginProlog", 33 "50 dict begin", 34 "", 35 "/baseline 0 def", 36 "/height 0 def", 37 "/justify 0 def", 38 "/lineLength 0 def", 39 "/spacing 0 def", 40 "/stipple 0 def", 41 "/strings 0 def", 42 "/xoffset 0 def", 43 "/yoffset 0 def", 44 "", 45 "/ISOEncode {", 46 " dup length dict begin", 47 " {1 index /FID ne {def} {pop pop} ifelse} forall", 48 " /Encoding ISOLatin1Encoding def", 49 " currentdict", 50 " end", 51 " /Temporary exch definefont", 52 "} bind def", 53 "", 54 "/AdjustColor {", 55 " CL 2 lt {", 56 " currentgray", 57 " CL 0 eq {", 58 " .5 lt {0} {1} ifelse", 59 " } if", 60 " setgray", 61 " } if", 62 "} bind def", 63 "", 64 "/DrawText {", 65 " /stipple exch def", 66 " /justify exch def", 67 " /yoffset exch def", 68 " /xoffset exch def", 69 " /spacing exch def", 70 " /strings exch def", 71 " /lineLength 0 def", 72 " strings {", 73 " stringwidth pop", 74 " dup lineLength gt {/lineLength exch def} {pop} ifelse", 75 " newpath", 76 " } forall", 77 " 0 0 moveto (TXygqPZ) false charpath", 78 " pathbbox dup /baseline exch def", 79 " exch pop exch sub /height exch def pop", 80 " newpath", 81 " translate", 82 " lineLength xoffset mul", 83 " strings length 1 sub spacing mul height add yoffset mul translate", 84 " justify lineLength mul baseline neg translate", 85 " strings {", 86 " dup stringwidth pop", 87 " justify neg mul 0 moveto", 88 " stipple {", 89 " gsave", 90 " /char (X) def", 91 " {", 92 " char 0 3 -1 roll put", 93 " currentpoint", 94 " gsave", 95 " char true charpath clip StippleText", 96 " grestore", 97 " char stringwidth translate", 98 " moveto", 99 " } forall", 100 " grestore", 101 " } {show} ifelse", 102 " 0 spacing neg translate", 103 " } forall", 104 "} bind def", 105 "%%%%EndProlog", 106 "%%%%BeginSetup", 107 "/CL 2 def", 108 "%%%%IncludeResource: font Courier-Bold", 109 "%%%%EndSetup", 110 0, 111 }; 112 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 */ 121 122 static FILE *pfd; 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; 133 134 extern int ntrail, s_trail, pno, depth; 135 extern Symbol *oFname; 136 extern void exit(int); 137 void putpages(void); 138 void spitbox(int, int, int, char *); 139 140 void 141 putlegend(void) 142 { 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"); 151 } 152 153 void 154 startpage(void) 155 { int i; 156 157 pspno++; 158 fprintf(pfd, "%%%%Page: %d %d\n", pspno, pspno); 159 putlegend(); 160 161 for (i = TotSteps-1; i >= 0; i--) 162 { if (!I[i]) continue; 163 spitbox(i, RH, -PH, I[i]); 164 } 165 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)); 175 if (Scaler != 1.0) 176 fprintf(pfd, "%f %f scale\n", Scaler, Scaler); 177 } 178 179 void 180 putprelude(void) 181 { char snap[256]; FILE *fd; 182 183 sprintf(snap, "%s.ps", oFname?oFname->name:"msc"); 184 if (!(pfd = fopen(snap, "w"))) 185 fatal("cannot create file '%s'", snap); 186 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); 192 193 if (s_trail) 194 { if (ntrail) 195 sprintf(snap, "%s%d.trail", oFname?oFname->name:"msc", ntrail); 196 else 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); 202 } 203 TotSteps = 1; 204 while (fgets(snap, 256, fd)) TotSteps++; 205 fclose(fd); 206 } 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)); 214 startpage(); 215 } 216 217 void 218 putpostlude(void) 219 { putpages(); 220 fprintf(pfd, "%%%%Trailer\n"); 221 fprintf(pfd, "end\n"); 222 fprintf(pfd, "%%%%Pages: %d\n", pspno); 223 fprintf(pfd, "%%%%EOF\n"); 224 fclose(pfd); 225 /* stderr, in case user redirected output */ 226 fprintf(stderr, "spin: wrote %d pages into '%s.ps'\n", 227 pspno, oFname?oFname->name:"msc"); 228 exit(0); 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, 265 (float) 0.4, (float) 0.4, (float) 1.0, 1); 266 ProcLine[i] = 1; 267 } 268 } 269 270 void 271 putarrow(int from, int to) 272 { 273 T[D[from]] = D[to]; 274 } 275 276 void 277 stepnumber(int i) 278 { int y = MH-(i*HH)%MH; 279 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"); 292 } 293 294 void 295 spitbox(int x, int dx, int y, char *s) 296 { float r,g,b, bw; int a; char d[256]; 297 298 if (!dx) 299 { stepnumber(y); 300 putgrid(x); 301 } 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.); 305 if (s[0] == '~') 306 { switch (s[1]) { 307 case 'B': r = (float) 0.2; g = (float) 0.2; b = (float) 1.; 308 break; 309 case 'G': r = (float) 0.2; g = (float) 1.; b = (float) 0.2; 310 break; 311 case 'R': 312 default : r = (float) 1.; g = (float) 0.2; b = (float) 0.2; 313 break; 314 } 315 s += 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.; 320 } else 321 { r = (float) 1.; g = (float) 1.; b = (float) 0.; 322 if (!dx 323 && sscanf(s, "%d:%s", &a, d) == 2 /* was &d */ 324 && a >= 0 && a < TotSteps) 325 { if (!I[a] 326 || strlen(I[a]) <= strlen(s)) 327 I[a] = emalloc((int) strlen(s)+1); 328 strcpy(I[a], s); 329 } } 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"); 338 } 339 340 void 341 putpages(void) 342 { int i, lasti=0; float nmh; 343 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; 348 } 349 350 for (i = TotSteps-1; i >= 0; i--) 351 { if (!I[i]) continue; 352 spitbox(i, 0, 0, I[i]); 353 } 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 */ 360 { int reali = i*HH; 361 int realt = T[i]*HH; 362 int topop = (reali)/MH; topop *= MH; 363 reali -= topop; realt -= topop; 364 365 if (M[i] == M[T[i]] && reali == realt) 366 /* an rv handshake */ 367 psline( M[lasti], reali+2-3*HH/2, 368 M[i], reali, 369 (float) 1.,(float) 0.,(float) 0., 2); 370 else 371 psline( M[i], reali, 372 M[T[i]], realt, 373 (float) 1.,(float) 0.,(float) 0., 2); 374 375 if (realt >= MH) T[T[i]] = -i; 376 377 } else if (T[i] < 0) /* arrow from prev page */ 378 { int reali = (-T[i])*HH; 379 int realt = i*HH; 380 int topop = (realt)/MH; topop *= MH; 381 reali -= topop; realt -= topop; 382 383 psline( M[-T[i]], reali, 384 M[i], realt, 385 (float) 1., (float) 0., (float) 0., 2); 386 } 387 if (L[i]) 388 { spitbox(M[i], 0, i, L[i]); 389 free(L[i]); 390 lasti = i; 391 } 392 } 393 fprintf(pfd, "showpage\nrestore\n"); 394 } 395 396 void 397 putbox(int x) 398 { 399 if (ldepth >= TotSteps) 400 { putpostlude(); 401 fprintf(stderr, "max length of %d steps exceeded\n", 402 TotSteps); 403 fatal("postscript file truncated", (char *) 0); 404 } 405 M[ldepth] = x; 406 if (x > maxx) maxx = x; 407 } 408 409 void 410 pstext(int x, char *s) 411 { char *tmp = emalloc((int) strlen(s)+1); 412 413 strcpy(tmp, s); 414 if (depth == 0) 415 I[x] = tmp; 416 else 417 { putbox(x); 418 if (depth >= TotSteps || ldepth >= TotSteps) 419 { fprintf(stderr, "max nr of %d steps exceeded\n", 420 TotSteps); 421 fatal("aborting", (char *) 0); 422 } 423 424 D[depth] = ldepth; 425 R[ldepth] = depth; 426 L[ldepth] = tmp; 427 ldepth += 2; 428 } 429 } 430 431 void 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); 436 437 if (columns == 2) 438 pstext(pid, &s[i]); 439 else 440 { if (!notabs) 441 { printf(" "); 442 for (i = 0; i <= pid; i++) 443 printf(" "); 444 } 445 fprintf(fd, "%s", s); 446 fflush(fd); 447 } 448 } 449