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 } 137