/***** 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 *);voiddoindent(void){	int i;	for (i = 0; i < indent; i++)		printf("   ");}voidrepro_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");}voidrepro_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;	}}voidrepro_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");}voidrepro_src(void){	repro_proc(rdy);}