trunk/verif/Spin/Src5.1.6/ps_msc.c

   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 }