1 /***** spin: reprosrc.c *****/
4 * This file is part of the public release of Spin. It is subject to the
5 * terms in the LICENSE file that is included in this source directory.
6 * Tool documentation is available at http://spinroot.com
14 static int indent = 1;
16 extern YYSTYPE yylval;
18 static void repro_seq(Sequence *);
23 for (i = 0; i < indent; i++)
43 repro_seq(e->n->sl->this);
51 repro_seq(Sequence *s)
56 for (e = s->frst; e; e = e->nxt)
59 if (v) printf("%s:\n", v->name);
61 if (e->n->ntyp == UNLESS)
62 { printf("/* normal */ {\n");
63 repro_seq(e->n->sl->this);
65 printf("} unless {\n");
66 repro_seq(e->n->sl->nxt->this);
68 printf("}; /* end unless */\n");
72 case DO: doindent(); printf("do\n"); indent++; break;
73 case IF: doindent(); printf("if\n"); indent++; break;
76 for (h = e->sub; h; h = h->nxt)
77 { indent--; doindent(); indent++; printf("::\n");
83 case DO: indent--; doindent(); printf("od;\n"); break;
84 case IF: indent--; doindent(); printf("fi;\n"); break;
87 { if (e->n->ntyp == ATOMIC
88 || e->n->ntyp == D_STEP
89 || e->n->ntyp == NON_ATOMIC)
91 else if (e->n->ntyp != '.'
93 && e->n->ntyp != BREAK)
96 if (e->n->ntyp == C_CODE)
98 plunk_inline(stdout, e->n->sym->name, 1, 1);
99 } else if (e->n->ntyp == 'c'
100 && e->n->lft->ntyp == C_EXPR)
101 { printf("c_expr { ");
102 plunk_expr(stdout, e->n->lft->sym->name);
105 { comment(stdout, e->n, 0);
115 repro_proc(ProcList *p)
118 if (p->nxt) repro_proc(p->nxt);
120 if (p->det) printf("D"); /* deterministic */
121 printf("proctype %s()", p->n->name);
123 { printf(" provided ");
124 comment(stdout, p->prov, 0);
138 static int in_c_decl;
139 static int in_c_code;
148 default: if (n > 0 && n < 256)
149 sprintf(mtxt, "%c", n);
151 sprintf(mtxt, "<%d?>", n);
154 case '(': strcpy(mtxt, "("); in_decl++; break;
155 case ')': strcpy(mtxt, ")"); in_decl--; break;
156 case '{': strcpy(mtxt, "{"); break;
157 case '}': strcpy(mtxt, "}"); break;
158 case '\t': sprintf(mtxt, "\\t"); break;
159 case '\f': sprintf(mtxt, "\\f"); break;
160 case '\n': sprintf(mtxt, "\\n"); break;
161 case '\r': sprintf(mtxt, "\\r"); break;
162 case 'c': sprintf(mtxt, "condition"); break;
163 case 's': sprintf(mtxt, "send"); break;
164 case 'r': sprintf(mtxt, "recv"); break;
165 case 'R': sprintf(mtxt, "recv poll"); break;
166 case '@': sprintf(mtxt, "@"); break;
167 case '?': sprintf(mtxt, "(x->y:z)"); break;
168 case NEXT: sprintf(mtxt, "X"); break;
169 case ALWAYS: sprintf(mtxt, "[]"); break;
170 case EVENTUALLY: sprintf(mtxt, "<>"); break;
171 case IMPLIES: sprintf(mtxt, "->"); break;
172 case EQUIV: sprintf(mtxt, "<->"); break;
173 case UNTIL: sprintf(mtxt, "U"); break;
174 case WEAK_UNTIL: sprintf(mtxt, "W"); break;
175 case IN: sprintf(mtxt, "in"); break;
176 case ACTIVE: sprintf(mtxt, "active"); break;
177 case AND: sprintf(mtxt, "&&"); break;
178 case ARROW: sprintf(mtxt, "->"); break;
179 case ASGN: sprintf(mtxt, "="); break;
180 case ASSERT: sprintf(mtxt, "assert"); break;
181 case ATOMIC: sprintf(mtxt, "atomic"); break;
182 case BREAK: sprintf(mtxt, "break"); break;
183 case C_CODE: sprintf(mtxt, "c_code"); in_c_code++; break;
184 case C_DECL: sprintf(mtxt, "c_decl"); in_c_decl++; break;
185 case C_EXPR: sprintf(mtxt, "c_expr"); break;
186 case C_STATE: sprintf(mtxt, "c_state"); break;
187 case C_TRACK: sprintf(mtxt, "c_track"); break;
188 case CLAIM: sprintf(mtxt, "never"); break;
189 case CONST: sprintf(mtxt, "%d", yylval->val); break;
190 case DECR: sprintf(mtxt, "--"); break;
191 case D_STEP: sprintf(mtxt, "d_step"); break;
192 case D_PROCTYPE: sprintf(mtxt, "d_proctype"); break;
193 case DO: sprintf(mtxt, "do"); break;
194 case DOT: sprintf(mtxt, "."); break;
195 case ELSE: sprintf(mtxt, "else"); break;
196 case EMPTY: sprintf(mtxt, "empty"); break;
197 case ENABLED: sprintf(mtxt, "enabled"); break;
198 case EQ: sprintf(mtxt, "=="); break;
199 case EVAL: sprintf(mtxt, "eval"); break;
200 case FI: sprintf(mtxt, "fi"); break;
201 case FULL: sprintf(mtxt, "full"); break;
202 case GE: sprintf(mtxt, ">="); break;
203 case GET_P: sprintf(mtxt, "get_priority"); break;
204 case GOTO: sprintf(mtxt, "goto"); break;
205 case GT: sprintf(mtxt, ">"); break;
206 case HIDDEN: sprintf(mtxt, "hidden"); break;
207 case IF: sprintf(mtxt, "if"); break;
208 case INCR: sprintf(mtxt, "++"); break;
210 case INLINE: sprintf(mtxt, "inline"); break;
211 case INIT: sprintf(mtxt, "init"); break;
212 case ISLOCAL: sprintf(mtxt, "local"); break;
214 case LABEL: sprintf(mtxt, "<label-name>"); break;
216 case LE: sprintf(mtxt, "<="); break;
217 case LEN: sprintf(mtxt, "len"); break;
218 case LSHIFT: sprintf(mtxt, "<<"); break;
219 case LT: sprintf(mtxt, "<"); break;
220 case LTL: sprintf(mtxt, "ltl"); break;
222 case NAME: sprintf(mtxt, "%s", yylval->sym->name); break;
224 case XU: switch (yylval->val) {
225 case XR: sprintf(mtxt, "xr"); break;
226 case XS: sprintf(mtxt, "xs"); break;
227 default: sprintf(mtxt, "<?>"); break;
231 case TYPE: switch (yylval->val) {
232 case BIT: sprintf(mtxt, "bit"); break;
233 case BYTE: sprintf(mtxt, "byte"); break;
234 case CHAN: sprintf(mtxt, "chan"); in_decl++; break;
235 case INT: sprintf(mtxt, "int"); break;
236 case MTYPE: sprintf(mtxt, "mtype"); break;
237 case SHORT: sprintf(mtxt, "short"); break;
238 case UNSIGNED: sprintf(mtxt, "unsigned"); break;
239 default: sprintf(mtxt, "<unknown type>"); break;
243 case NE: sprintf(mtxt, "!="); break;
244 case NEG: sprintf(mtxt, "!"); break;
245 case NEMPTY: sprintf(mtxt, "nempty"); break;
246 case NFULL: sprintf(mtxt, "nfull"); break;
248 case NON_ATOMIC: sprintf(mtxt, "<sub-sequence>"); break;
250 case NONPROGRESS: sprintf(mtxt, "np_"); break;
251 case OD: sprintf(mtxt, "od"); break;
252 case OF: sprintf(mtxt, "of"); break;
253 case OR: sprintf(mtxt, "||"); break;
254 case O_SND: sprintf(mtxt, "!!"); break;
255 case PC_VAL: sprintf(mtxt, "pc_value"); break;
256 case PRINT: sprintf(mtxt, "printf"); break;
257 case PRINTM: sprintf(mtxt, "printm"); break;
258 case PRIORITY: sprintf(mtxt, "priority"); break;
259 case PROCTYPE: sprintf(mtxt, "proctype"); break;
260 case PROVIDED: sprintf(mtxt, "provided"); break;
261 case RCV: sprintf(mtxt, "?"); break;
262 case R_RCV: sprintf(mtxt, "??"); break;
263 case RSHIFT: sprintf(mtxt, ">>"); break;
264 case RUN: sprintf(mtxt, "run"); break;
265 case SEP: sprintf(mtxt, "::"); break;
266 case SEMI: sprintf(mtxt, ";"); break;
267 case SET_P: sprintf(mtxt, "set_priority"); break;
268 case SHOW: sprintf(mtxt, "show"); break;
269 case SND: sprintf(mtxt, "!"); break;
274 case STRING: sprintf(mtxt, "%s", yylval->sym->name); break;
276 case TRACE: sprintf(mtxt, "trace"); break;
277 case TIMEOUT: sprintf(mtxt, "timeout"); break;
278 case TYPEDEF: sprintf(mtxt, "typedef"); break;
279 case UMIN: sprintf(mtxt, "-"); break;
280 case UNLESS: sprintf(mtxt, "unless"); break;
288 if (strlen(b) == 0) return;
290 if (b[strlen(b)-1] != ':') /* label? */
291 { if (b[0] == ':' && b[1] == ':')
308 extern int lex(void);
318 while ((c = lex()) != EOF)
320 if ((lastc == IF || lastc == DO) && c != SEP)
321 { indent--; /* c_code if */
323 if (c == C_DECL || c == C_STATE
324 || c == C_TRACK || c == SEP
325 || c == DO || c == IF
326 || (c == TYPE && !in_decl))
327 { purge(buf); /* start on new line */
331 && lastc != OF && lastc != IN
332 && lastc != ATOMIC && lastc != D_STEP
333 && lastc != C_CODE && lastc != C_DECL && lastc != C_EXPR)
340 assert(strlen(yylval->sym->name) < sizeof(buf));
341 strcpy(buf, yylval->sym->name);
348 if (c != ':' && c != SEMI
349 && c != ',' && c != '('
350 && c != '#' && lastc != '#'
351 && c != ARROW && lastc != ARROW
352 && c != '.' && lastc != '.'
353 && c != '!' && lastc != '!'
354 && c != SND && lastc != SND
355 && c != RCV && lastc != RCV
356 && c != O_SND && lastc != O_SND
357 && c != R_RCV && lastc != R_RCV
358 && (c != ']' || lastc != '[')
359 && (c != '>' || lastc != '<')
360 && (c != GT || lastc != LT)
361 && c != '@' && lastc != '@'
362 && c != DO && c != OD && c != IF && c != FI
363 && c != SEP && strlen(buf) > 0)
366 if (c == '}' || c == OD || c == FI)
372 if (c == '{' || c == DO || c == IF)
377 if (c == '}' || c == BREAK || c == SEMI
378 || (c == ':' && lastc == NAME))