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. */
20 /* extern void free(void *); */
22 static char *PsPre
[] = {
24 "%%%%PageOrder: Ascend",
25 "%%%%DocumentData: Clean7Bit",
26 "%%%%Orientation: Portrait",
27 "%%%%DocumentNeededResources: font Courier-Bold",
44 " dup length dict begin",
45 " {1 index /FID ne {def} {pop pop} ifelse} forall",
46 " /Encoding ISOLatin1Encoding def",
49 " /Temporary exch definefont",
56 " .5 lt {0} {1} ifelse",
72 " dup lineLength gt {/lineLength exch def} {pop} ifelse",
75 " 0 0 moveto (TXygqPZ) false charpath",
76 " pathbbox dup /baseline exch def",
77 " exch pop exch sub /height exch def pop",
80 " lineLength xoffset mul",
81 " strings length 1 sub spacing mul height add yoffset mul translate",
82 " justify lineLength mul baseline neg translate",
84 " dup stringwidth pop",
85 " justify neg mul 0 moveto",
90 " char 0 3 -1 roll put",
93 " char true charpath clip StippleText",
95 " char stringwidth translate",
100 " 0 spacing neg translate",
106 "%%%%IncludeResource: font Courier-Bold",
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 */
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;
132 extern int ntrail
, s_trail
, pno
, depth
;
133 extern Symbol
*oFname
;
134 extern void exit(int);
136 void spitbox(int, int, int, char *);
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");
156 fprintf(pfd
, "%%%%Page: %d %d\n", pspno
, pspno
);
159 for (i
= TotSteps
-1; i
>= 0; i
--)
160 { if (!I
[i
]) continue;
161 spitbox(i
, RH
, -PH
, I
[i
]);
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));
174 fprintf(pfd
, "%f %f scale\n", Scaler
, Scaler
);
179 { char snap
[256]; FILE *fd
;
181 sprintf(snap
, "%s.ps", oFname
?oFname
->name
:"msc");
182 if (!(pfd
= fopen(snap
, "w")))
183 fatal("cannot create file '%s'", snap
);
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
);
193 sprintf(snap
, "%s%d.trail", oFname
?oFname
->name
:"msc", ntrail
);
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);
202 while (fgets(snap
, 256, fd
)) TotSteps
++;
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));
218 fprintf(pfd
, "%%%%Trailer\n");
219 fprintf(pfd
, "end\n");
220 fprintf(pfd
, "%%%%Pages: %d\n", pspno
);
221 fprintf(pfd
, "%%%%EOF\n");
223 /* stderr, in case user redirected output */
224 fprintf(stderr
, "spin: wrote %d pages into '%s.ps'\n",
225 pspno
, oFname
?oFname
->name
:"msc");
230 psline(int x0
, int iy0
, int x1
, int iy1
, float r
, float g
, float b
, int w
)
234 if (y1
> y0
) y1
-= MH
;
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");
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");
261 for (i
= p
; i
>= 0; i
--)
263 { psline(i
, 0, i
, MH
-1, (float) (0.4), (float) (0.4), (float) (1.0), 1);
269 putarrow(int from
, int to
)
276 { int y
= MH
-(i
*HH
)%MH
;
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");
293 spitbox(int x
, int dx
, int y
, char *s
)
294 { float r
,g
,b
, bw
; int a
; char d
[256];
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.);
305 case 'B': r
= (float) 0.2; g
= (float) 0.2; b
= (float) 1.;
307 case 'G': r
= (float) 0.2; g
= (float) 1.; b
= (float) 0.2;
310 default : r
= (float) 1.; g
= (float) 0.2; b
= (float) 0.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.;
319 { r
= (float) 1.; g
= (float) 1.; b
= (float) 0.;
321 && sscanf(s
, "%d:%250s", &a
, d
) == 2 /* was &d */
322 && a
>= 0 && a
< TotSteps
)
324 || strlen(I
[a
]) <= strlen(s
))
325 I
[a
] = emalloc((int) strlen(s
)+1);
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");
340 { int i
, lasti
=0; float nmh
;
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
;
348 for (i
= TotSteps
-1; i
>= 0; i
--)
349 { if (!I
[i
]) continue;
350 spitbox(i
, 0, 0, I
[i
]);
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 */
360 int topop
= (reali
)/MH
; topop
*= MH
;
361 reali
-= topop
; realt
-= topop
;
363 if (M
[i
] == M
[T
[i
]] && reali
== realt
)
364 /* an rv handshake */
365 psline( M
[lasti
], reali
+2-3*HH
/2,
367 (float) 1.,(float) 0.,(float) 0., 2);
371 (float) 1.,(float) 0.,(float) 0., 2);
373 if (realt
>= MH
) T
[T
[i
]] = -i
;
375 } else if (T
[i
] < 0) /* arrow from prev page */
376 { int reali
= (-T
[i
])*HH
;
378 int topop
= (realt
)/MH
; topop
*= MH
;
379 reali
-= topop
; realt
-= topop
;
381 psline( M
[-T
[i
]], reali
,
383 (float) 1., (float) 0., (float) 0., 2);
386 { spitbox(M
[i
], 0, i
, L
[i
]);
391 fprintf(pfd
, "showpage\nrestore\n");
397 if (ldepth
>= TotSteps
)
398 { fprintf(stderr
, "max length of %d steps exceeded - ps file truncated\n",
403 if (x
> maxx
) maxx
= x
;
407 pstext(int x
, char *s
)
408 { char *tmp
= emalloc((int) strlen(s
)+1);
415 if (depth
>= TotSteps
|| ldepth
>= TotSteps
)
416 { fprintf(stderr
, "max nr of %d steps exceeded\n",
418 fatal("aborting", (char *) 0);
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);
439 for (i
= 0; i
<= pid
; i
++)
442 fprintf(fd
, "%s", s
);
This page took 0.108209 seconds and 4 git commands to generate.