Subversion Repositories planix.SVN

/***** spin: ps_msc.c *****/

/* Copyright (c) 1997-2003 by Lucent Technologies, Bell Laboratories.     */

/* All Rights Reserved.  This software is for educational purposes only.  */

/* No guarantee whatsoever is expressed or implied by the distribution of */

/* this code.  Permission is given to distribute this code provided that  */

/* this introductory message is not removed and no monies are exchanged.  */

/* Software written by Gerard J. Holzmann.  For tool documentation see:   */

/*             http://spinroot.com/                                       */

/* Send all bug-reports and/or questions to: bugs@spinroot.com            */

/* The Postscript generation code below was written by Gerard J. Holzmann */

/* in June 1997. Parts of the prolog template are based on similar boiler */

/* plate in the Tcl/Tk distribution. This code is used to support Spin's  */

/* option -M for generating a Postscript file from a simulation run.      */

#include "spin.h"

#include "version.h"

/* extern void free(void *); */

static char *PsPre[] = {

	"%%%%Pages: (atend)",

	"%%%%PageOrder: Ascend",

	"%%%%DocumentData: Clean7Bit",

	"%%%%Orientation: Portrait",

	"%%%%DocumentNeededResources: font Courier-Bold",

	"%%%%EndComments",

	"",

	"%%%%BeginProlog",

	"50 dict begin",

	"",

	"/baseline 0 def",

	"/height 0 def",

	"/justify 0 def",

	"/lineLength 0 def",

	"/spacing 0 def",

	"/stipple 0 def",

	"/strings 0 def",

	"/xoffset 0 def",

	"/yoffset 0 def",

	"",

	"/ISOEncode {",

	"    dup length dict begin",

	"	{1 index /FID ne {def} {pop pop} ifelse} forall",

	"	/Encoding ISOLatin1Encoding def",

	"	currentdict",

	"    end",

	"    /Temporary exch definefont",

	"} bind def",

	"",

	"/AdjustColor {",

	"    CL 2 lt {",

	"	currentgray",

	"	CL 0 eq {",

	"	    .5 lt {0} {1} ifelse",

	"	} if",

	"	setgray",

	"    } if",

	"} bind def",

	"",

	"/DrawText {",

	"    /stipple exch def",

	"    /justify exch def",

	"    /yoffset exch def",

	"    /xoffset exch def",

	"    /spacing exch def",

	"    /strings exch def",

	"    /lineLength 0 def",

	"    strings {",

	"	stringwidth pop",

	"	dup lineLength gt {/lineLength exch def} {pop} ifelse",

	"	newpath",

	"    } forall",

	"    0 0 moveto (TXygqPZ) false charpath",

	"    pathbbox dup /baseline exch def",

	"    exch pop exch sub /height exch def pop",

	"    newpath",

	"    translate",

	"    lineLength xoffset mul",

	"    strings length 1 sub spacing mul height add yoffset mul translate",

	"    justify lineLength mul baseline neg translate",

	"    strings {",

	"	dup stringwidth pop",

	"	justify neg mul 0 moveto",

	"	stipple {",

	"	    gsave",

	"	    /char (X) def",

	"	    {",

	"		char 0 3 -1 roll put",

	"		currentpoint",

	"		gsave",

	"		char true charpath clip StippleText",

	"		grestore",

	"		char stringwidth translate",

	"		moveto",

	"	    } forall",

	"	    grestore",

	"	} {show} ifelse",

	"	0 spacing neg translate",

	"    } forall",

	"} bind def",

	"%%%%EndProlog",

	"%%%%BeginSetup",

	"/CL 2 def",

	"%%%%IncludeResource: font Courier-Bold",

	"%%%%EndSetup",

	0,

};

static int MH  = 600;	/* page height - can be scaled */

static int oMH = 600;	/* page height - not scaled */

#define MW	500	/* page width */

#define LH	100	/* bottom margin */

#define RH	100	/* right margin */

#define WW	 50	/* distance between process lines */

#define HH	  8	/* vertical distance between steps */

#define PH	 14	/* height of process-tag headers */

static FILE	*pfd;

static char	**I;		/* initial procs */

static int	*D,*R;		/* maps between depth and ldepth */

static short	*M;		/* x location of each box at index y */

static short	*T;		/* y index of match for each box at index y */

static char	**L;		/* text labels */

static char	*ProcLine;	/* active processes */

static int	pspno = 0;	/* postscript page */

static int	ldepth = 1;

static int	maxx, TotSteps = 2*4096; /* max nr of steps, about 40 pages */

static float	Scaler = (float) 1.0;

extern int	ntrail, s_trail, pno, depth;

extern Symbol	*oFname;

extern void	exit(int);

void putpages(void);

void spitbox(int, int, int, char *);

void

putlegend(void)

{

	fprintf(pfd, "gsave\n");

	fprintf(pfd, "/Courier-Bold findfont 8 scalefont ");

	fprintf(pfd, "ISOEncode setfont\n");

	fprintf(pfd, "0.000 0.000 0.000 setrgbcolor AdjustColor\n");

	fprintf(pfd, "%d %d [\n", MW/2, LH+oMH+ 5*HH);

	fprintf(pfd, "    (%s -- %s -- MSC -- %d)\n] 10 -0.5 0.5 0 ",

		SpinVersion, oFname?oFname->name:"", pspno);

	fprintf(pfd, "false DrawText\ngrestore\n");

}

void

startpage(void)

{	int i;

	pspno++;

	fprintf(pfd, "%%%%Page: %d %d\n", pspno, pspno);

	putlegend();

	for (i = TotSteps-1; i >= 0; i--)

	{	if (!I[i]) continue;

		spitbox(i, RH, -PH, I[i]);

	}

	fprintf(pfd, "save\n");

	fprintf(pfd, "10 %d moveto\n", LH+oMH+5);

	fprintf(pfd, "%d %d lineto\n", RH+MW, LH+oMH+5);

	fprintf(pfd, "%d %d lineto\n", RH+MW, LH);

	fprintf(pfd, "10 %d lineto\n", LH);

	fprintf(pfd, "closepath clip newpath\n");

	fprintf(pfd, "%f %f translate\n",

		(float) RH, (float) LH);

	memset(ProcLine, 0, 256*sizeof(char));

	if (Scaler != 1.0)

		fprintf(pfd, "%f %f scale\n", Scaler, Scaler);

}

void

putprelude(void)

{	char snap[256]; FILE *fd;

	sprintf(snap, "%s.ps", oFname?oFname->name:"msc");

	if (!(pfd = fopen(snap, MFLAGS)))

		fatal("cannot create file '%s'", snap);

	fprintf(pfd, "%%!PS-Adobe-2.0\n");

	fprintf(pfd, "%%%%Creator: %s\n", SpinVersion);

	fprintf(pfd, "%%%%Title: MSC %s\n", oFname?oFname->name:"--");

	fprintf(pfd, "%%%%BoundingBox: 119 154 494 638\n");

	ntimes(pfd, 0, 1, PsPre);

	if (s_trail)

	{	if (ntrail)

		sprintf(snap, "%s%d.trail", oFname?oFname->name:"msc", ntrail);

		else

		sprintf(snap, "%s.trail", oFname?oFname->name:"msc");

		if (!(fd = fopen(snap, "r")))

		{	snap[strlen(snap)-2] = '\0';

			if (!(fd = fopen(snap, "r")))

				fatal("cannot open trail file", (char *) 0);

		}

		TotSteps = 1;

		while (fgets(snap, 256, fd)) TotSteps++;

		fclose(fd);

	}

	TotSteps += 10;

	R = (int   *) emalloc(TotSteps * sizeof(int));

	D = (int   *) emalloc(TotSteps * sizeof(int));

	M = (short *) emalloc(TotSteps * sizeof(short));

	T = (short *) emalloc(TotSteps * sizeof(short));

	L = (char **) emalloc(TotSteps * sizeof(char *));

	I = (char **) emalloc(TotSteps * sizeof(char *));

	ProcLine = (char *) emalloc(1024 * sizeof(char));

	startpage();

}

void

putpostlude(void)

{	putpages();

	fprintf(pfd, "%%%%Trailer\n");

	fprintf(pfd, "end\n");

	fprintf(pfd, "%%%%Pages: %d\n", pspno);

	fprintf(pfd, "%%%%EOF\n");

	fclose(pfd);

	/* stderr, in case user redirected output */

	fprintf(stderr, "spin: wrote %d pages into '%s.ps'\n",

		pspno, oFname?oFname->name:"msc");

	exit(0);

}

void

psline(int x0, int iy0, int x1, int iy1, float r, float g, float b, int w)

{	int y0 = MH-iy0;

	int y1 = MH-iy1;

	if (y1 > y0) y1 -= MH;

	fprintf(pfd, "gsave\n");

	fprintf(pfd, "%d %d moveto\n", x0*WW, y0);

	fprintf(pfd, "%d %d lineto\n", x1*WW, y1);

	fprintf(pfd, "%d setlinewidth\n", w);

	fprintf(pfd, "0 setlinecap\n");

	fprintf(pfd, "1 setlinejoin\n");

	fprintf(pfd, "%f %f %f setrgbcolor AdjustColor\n", r,g,b);

	fprintf(pfd, "stroke\ngrestore\n");

}

void

colbox(int x, int y, int w, int h, float r, float g, float b)

{	fprintf(pfd, "%d %d moveto\n", x - w, y-h);

	fprintf(pfd, "%d %d lineto\n", x + w, y-h);

	fprintf(pfd, "%d %d lineto\n", x + w, y+h);

	fprintf(pfd, "%d %d lineto\n", x - w, y+h);

	fprintf(pfd, "%d %d lineto\n", x - w, y-h);

	fprintf(pfd, "%f %f %f setrgbcolor AdjustColor\n", r,g,b);

	fprintf(pfd, "closepath fill\n");

}

void

putgrid(int p)

{	int i;

	for (i = p ; i >= 0; i--)

	{	if (!ProcLine[i])

		{	psline(i, 0, i, MH-1, (float) (0.4), (float) (0.4), (float) (1.0), 1);

			ProcLine[i] = 1;

	}	}

}

void

putarrow(int from, int to)

{

	T[D[from]] = D[to];

}

void

stepnumber(int i)

{	int y = MH-(i*HH)%MH;

	fprintf(pfd, "gsave\n");

	fprintf(pfd, "/Courier-Bold findfont 6 scalefont ");

	fprintf(pfd, "ISOEncode setfont\n");

	fprintf(pfd, "0.000 0.000 0.000 setrgbcolor AdjustColor\n");

	fprintf(pfd, "%d %d [\n", -40, y);

	fprintf(pfd, "    (%d)\n] 10 -0.5 0.5 0 ", R[i]);

	fprintf(pfd, "false DrawText\ngrestore\n");

	fprintf(pfd, "%d %d moveto\n", -20, y);

	fprintf(pfd, "%d %d lineto\n", M[i]*WW, y);

	fprintf(pfd, "1 setlinewidth\n0 setlinecap\n1 setlinejoin\n");

	fprintf(pfd, "0.92 0.92 0.92 setrgbcolor AdjustColor\n");

	fprintf(pfd, "stroke\n");

}

void

spitbox(int x, int dx, int y, char *s)

{	float r,g,b, bw; int a; char d[256];

	if (!dx)

	{	stepnumber(y);

		putgrid(x);

	}

	bw = (float)2.7*(float)strlen(s);

	colbox(x*WW+dx, MH-(y*HH)%MH, (int) (bw+1.0),

		5, (float) 0.,(float) 0.,(float) 0.);

	if (s[0] == '~')

	{	switch (s[1]) {

		case 'B': r = (float) 0.2; g = (float) 0.2; b = (float) 1.;

			  break;

		case 'G': r = (float) 0.2; g = (float) 1.; b = (float) 0.2;

			  break;

		case 'R':

		default : r = (float) 1.; g = (float) 0.2; b = (float) 0.2;

			  break;

		}

		s += 2;

	} else if (strchr(s, '!'))

	{	r = (float) 1.; g = (float) 1.; b = (float) 1.;

	} else if (strchr(s, '?'))

	{	r = (float) 0.; g = (float) 1.; b = (float) 1.;

	} else

	{	r = (float) 1.; g = (float) 1.; b = (float) 0.;

		if (!dx

		&&  sscanf(s, "%d:%250s", &a, d) == 2	/* was &d */

		&&  a >= 0 && a < TotSteps)

		{	if (!I[a]

			||  strlen(I[a]) <= strlen(s))

				I[a] = emalloc((int) strlen(s)+1);

			strcpy(I[a], s);

	}	}

	colbox(x*WW+dx, MH-(y*HH)%MH, (int) bw, 4, r,g,b);

	fprintf(pfd, "gsave\n");

	fprintf(pfd, "/Courier-Bold findfont 8 scalefont ");

	fprintf(pfd, "ISOEncode setfont\n");

	fprintf(pfd, "0.000 0.000 0.000 setrgbcolor AdjustColor\n");

	fprintf(pfd, "%d %d [\n", x*WW+dx, MH-(y*HH)%MH);

	fprintf(pfd, "    (%s)\n] 10 -0.5 0.5 0 ", s);

	fprintf(pfd, "false DrawText\ngrestore\n");

}

void

putpages(void)

{	int i, lasti=0; float nmh;

	if (maxx*WW > MW-RH/2)

	{	Scaler = (float) (MW-RH/2) / (float) (maxx*WW);

		fprintf(pfd, "%f %f scale\n", Scaler, Scaler);

		nmh = (float) MH; nmh /= Scaler; MH = (int) nmh;

	}

	for (i = TotSteps-1; i >= 0; i--)

	{	if (!I[i]) continue;

		spitbox(i, 0, 0, I[i]);

	}

	if (ldepth >= TotSteps) ldepth = TotSteps-1;

	for (i = 0; i <= ldepth; i++)

	{	if (!M[i] && !L[i]) continue;	/* no box here */

		if (6+i*HH >= MH*pspno)

		{ fprintf(pfd, "showpage\nrestore\n"); startpage(); }

		if (T[i] > 0)	/* red arrow */

		{	int reali = i*HH;

			int realt = T[i]*HH;

			int topop = (reali)/MH; topop *= MH;

			reali -= topop;  realt -= topop;

			if (M[i] == M[T[i]] && reali == realt)

				/* an rv handshake */

				psline( M[lasti], reali+2-3*HH/2,

					M[i], reali,

					(float) 1.,(float) 0.,(float) 0., 2);

			else

				psline(	M[i],    reali,

					M[T[i]], realt,

					(float) 1.,(float) 0.,(float) 0., 2);

			if (realt >= MH) T[T[i]] = -i;

		} else if (T[i] < 0)	/* arrow from prev page */

		{	int reali = (-T[i])*HH;

			int realt = i*HH;

			int topop = (realt)/MH; topop *= MH;

			reali -= topop;  realt -= topop;

			psline(	M[-T[i]], reali,

				M[i],     realt,

				(float) 1., (float) 0., (float) 0., 2);

		}

		if (L[i])

		{	spitbox(M[i], 0, i, L[i]);

			/* free(L[i]); */

			lasti = i;

		}

	}

	fprintf(pfd, "showpage\nrestore\n");

}

void

putbox(int x)

{

	if (ldepth >= TotSteps)

	{	fprintf(stderr, "max length of %d steps exceeded - ps file truncated\n",

			TotSteps);

		putpostlude();

	}

	M[ldepth] = x;

	if (x > maxx) maxx = x;

}

void

pstext(int x, char *s)

{	char *tmp = emalloc((int) strlen(s)+1);

	strcpy(tmp, s);

	if (depth == 0)

		I[x] = tmp;

	else

	{	putbox(x);

		if (depth >= TotSteps || ldepth >= TotSteps)

		{	fprintf(stderr, "max nr of %d steps exceeded\n",

				TotSteps);

			fatal("aborting", (char *) 0);

		}

		D[depth] = ldepth;

		R[ldepth] = depth;

		L[ldepth] = tmp;

		ldepth += 2;

	}

}

void

dotag(FILE *fd, char *s)

{	extern int columns, notabs; extern RunList *X;

	int i = (!strncmp(s, "MSC: ", 5))?5:0;

	int pid = s_trail ? pno : (X?X->pid:0);

	if (columns == 2)

		pstext(pid, &s[i]);

	else

	{	if (!notabs)

		{	printf("  ");

			for (i = 0; i <= pid; i++)

				printf("    ");

		}

		fprintf(fd, "%s", s);

		fflush(fd);

	}

}