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
doindent(void)22 doindent(void)
23 { int i;
24 for (i = 0; i < indent; i++)
25 printf(" ");
26 }
27
28 void
repro_sub(Element * e)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
repro_seq(Sequence * s)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
repro_proc(ProcList * p)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
repro_src(void)133 repro_src(void)
134 {
135 repro_proc(rdy);
136 }
137