[lttv.git] / trunk / verif / Spin / Src5.1.6 / reprosrc.c

/***** spin: reprosrc.c *****/

/* Copyright (c) 2002-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            */

#include <stdio.h>
#include "spin.h"
#include "y.tab.h"

static int indent = 1;

extern ProcList	*rdy;
void repro_seq(Sequence *);

void
doindent(void)
{	int i;
	for (i = 0; i < indent; i++)
		printf("   ");
}

void
repro_sub(Element *e)
{
	doindent();
	switch (e->n->ntyp) {
	case D_STEP:
		printf("d_step {\n");
		break;
	case ATOMIC:
		printf("atomic {\n");
		break;
	case NON_ATOMIC:
		printf(" {\n");
		break;
	}
	indent++;
	repro_seq(e->n->sl->this);
	indent--;

	doindent();
	printf(" };\n");
}

void
repro_seq(Sequence *s)
{	Element *e;
	Symbol *v;
	SeqList *h;

	for (e = s->frst; e; e = e->nxt)
	{
		v = has_lab(e, 0);
		if (v) printf("%s:\n", v->name);

		if (e->n->ntyp == UNLESS)
		{	printf("/* normal */ {\n");
			repro_seq(e->n->sl->this);
			doindent();
			printf("} unless {\n");
			repro_seq(e->n->sl->nxt->this);
			doindent();
			printf("}; /* end unless */\n");
		} else if (e->sub)
		{
			switch (e->n->ntyp) {
			case DO: doindent(); printf("do\n"); indent++; break;
			case IF: doindent(); printf("if\n"); indent++; break;
			}

			for (h = e->sub; h; h = h->nxt)
			{	indent--; doindent(); indent++; printf("::\n");
				repro_seq(h->this);
				printf("\n");
			}

			switch (e->n->ntyp) {
			case DO: indent--; doindent(); printf("od;\n"); break;
			case IF: indent--; doindent(); printf("fi;\n"); break;
			}
		} else
		{	if (e->n->ntyp == ATOMIC
			||  e->n->ntyp == D_STEP
			||  e->n->ntyp == NON_ATOMIC)
				repro_sub(e);
			else if (e->n->ntyp != '.'
			     &&  e->n->ntyp != '@'
			     &&  e->n->ntyp != BREAK)
			{
				doindent();
				if (e->n->ntyp == C_CODE)
				{	printf("c_code ");
					plunk_inline(stdout, e->n->sym->name, 1);
				} else if (e->n->ntyp == 'c'
				       &&  e->n->lft->ntyp == C_EXPR)
				{	printf("c_expr { ");
					plunk_expr(stdout, e->n->lft->sym->name);
					printf("} ->\n");
				} else
				{	comment(stdout, e->n, 0);
					printf(";\n");
			}	}
		}
		if (e == s->last)
			break;
	}
}

void
repro_proc(ProcList *p)
{
	if (!p) return;
	if (p->nxt) repro_proc(p->nxt);

	if (p->det) printf("D");	/* deterministic */
	printf("proctype %s()", p->n->name);
	if (p->prov)
	{	printf(" provided ");
		comment(stdout, p->prov, 0);
	}
	printf("\n{\n");
	repro_seq(p->s);
	printf("}\n");
}

void
repro_src(void)
{
	repro_proc(rdy);
}
Commit	Line	Data
0b55f123	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);
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	}