Subversion Repositories planix.SVN

Rev

Rev 2 | Details | Compare with Previous | Last modification | View Log | RSS feed

Rev Author Line No. Line
2 - 1 
/***** spin: reprosrc.c *****/
2 
 
3 
/* Copyright (c) 2002-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 
#include <stdio.h>
13 
#include "spin.h"
14 
#include "y.tab.h"
15 
 
16 
static int indent = 1;
17 
 
18 
extern ProcList	*rdy;
19 
void repro_seq(Sequence *);
20 
 
21 
void
22 
doindent(void)
23 
{	int i;
24 
	for (i = 0; i < indent; i++)
25 
		printf("   ");
26 
}
27 
 
28 
void
29 
repro_sub(Element *e)
30 
{
31 
	doindent();
32 
	switch (e->n->ntyp) {
33 
	case D_STEP:
34 
		printf("d_step {\n");
35 
		break;
36 
	case ATOMIC:
37 
		printf("atomic {\n");
38 
		break;
39 
	case NON_ATOMIC:
40 
		printf(" {\n");
41 
		break;
42 
	}
43 
	indent++;
44 
	repro_seq(e->n->sl->this);
45 
	indent--;
46 
 
47 
	doindent();
48 
	printf(" };\n");
49 
}
50 
 
51 
void
52 
repro_seq(Sequence *s)
53 
{	Element *e;
54 
	Symbol *v;
55 
	SeqList *h;
56 
 
57 
	for (e = s->frst; e; e = e->nxt)
58 
	{
59 
		v = has_lab(e, 0);
60 
		if (v) printf("%s:\n", v->name);
61 
 
62 
		if (e->n->ntyp == UNLESS)
63 
		{	printf("/* normal */ {\n");
64 
			repro_seq(e->n->sl->this);
65 
			doindent();
66 
			printf("} unless {\n");
67 
			repro_seq(e->n->sl->nxt->this);
68 
			doindent();
69 
			printf("}; /* end unless */\n");
70 
		} else if (e->sub)
71 
		{
72 
			switch (e->n->ntyp) {
73 
			case DO: doindent(); printf("do\n"); indent++; break;
74 
			case IF: doindent(); printf("if\n"); indent++; break;
75 
			}
76 
 
77 
			for (h = e->sub; h; h = h->nxt)
78 
			{	indent--; doindent(); indent++; printf("::\n");
79 
				repro_seq(h->this);
80 
				printf("\n");
81 
			}
82 
 
83 
			switch (e->n->ntyp) {
84 
			case DO: indent--; doindent(); printf("od;\n"); break;
85 
			case IF: indent--; doindent(); printf("fi;\n"); break;
86 
			}
87 
		} else
88 
		{	if (e->n->ntyp == ATOMIC
89 
			||  e->n->ntyp == D_STEP
90 
			||  e->n->ntyp == NON_ATOMIC)
91 
				repro_sub(e);
92 
			else if (e->n->ntyp != '.'
93 
			     &&  e->n->ntyp != '@'
94 
			     &&  e->n->ntyp != BREAK)
95 
			{
96 
				doindent();
97 
				if (e->n->ntyp == C_CODE)
98 
				{	printf("c_code ");
99 
					plunk_inline(stdout, e->n->sym->name, 1, 1);
100 
				} else if (e->n->ntyp == 'c'
101 
				       &&  e->n->lft->ntyp == C_EXPR)
102 
				{	printf("c_expr { ");
103 
					plunk_expr(stdout, e->n->lft->sym->name);
104 
					printf("} ->\n");
105 
				} else
106 
				{	comment(stdout, e->n, 0);
107 
					printf(";\n");
108 
			}	}
109 
		}
110 
		if (e == s->last)
111 
			break;
112 
	}
113 
}
114 
 
115 
void
116 
repro_proc(ProcList *p)
117 
{
118 
	if (!p) return;
119 
	if (p->nxt) repro_proc(p->nxt);
120 
 
121 
	if (p->det) printf("D");	/* deterministic */
122 
	printf("proctype %s()", p->n->name);
123 
	if (p->prov)
124 
	{	printf(" provided ");
125 
		comment(stdout, p->prov, 0);
126 
	}
127 
	printf("\n{\n");
128 
	repro_seq(p->s);
129 
	printf("}\n");
130 
}
131 
 
132 
void
133 
repro_src(void)
134 
{
135 
	repro_proc(rdy);
136 
}