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 #ifdef PC 15 #include "y_tab.h" 16 #else 17 #include "y.tab.h" 18 #endif 19 20 static int indent = 1; 21 22 extern ProcList *rdy; 23 void repro_seq(Sequence *); 24 25 void 26 doindent(void) 27 { int i; 28 for (i = 0; i < indent; i++) 29 printf(" "); 30 } 31 32 void 33 repro_sub(Element *e) 34 { 35 doindent(); 36 switch (e->n->ntyp) { 37 case D_STEP: 38 printf("d_step {\n"); 39 break; 40 case ATOMIC: 41 printf("atomic {\n"); 42 break; 43 case NON_ATOMIC: 44 printf(" {\n"); 45 break; 46 } 47 indent++; 48 repro_seq(e->n->sl->this); 49 indent--; 50 51 doindent(); 52 printf(" };\n"); 53 } 54 55 void 56 repro_seq(Sequence *s) 57 { Element *e; 58 Symbol *v; 59 SeqList *h; 60 61 for (e = s->frst; e; e = e->nxt) 62 { 63 v = has_lab(e, 0); 64 if (v) printf("%s:\n", v->name); 65 66 if (e->n->ntyp == UNLESS) 67 { printf("/* normal */ {\n"); 68 repro_seq(e->n->sl->this); 69 doindent(); 70 printf("} unless {\n"); 71 repro_seq(e->n->sl->nxt->this); 72 doindent(); 73 printf("}; /* end unless */\n"); 74 } else if (e->sub) 75 { 76 switch (e->n->ntyp) { 77 case DO: doindent(); printf("do\n"); indent++; break; 78 case IF: doindent(); printf("if\n"); indent++; break; 79 } 80 81 for (h = e->sub; h; h = h->nxt) 82 { indent--; doindent(); indent++; printf("::\n"); 83 repro_seq(h->this); 84 printf("\n"); 85 } 86 87 switch (e->n->ntyp) { 88 case DO: indent--; doindent(); printf("od;\n"); break; 89 case IF: indent--; doindent(); printf("fi;\n"); break; 90 } 91 } else 92 { if (e->n->ntyp == ATOMIC 93 || e->n->ntyp == D_STEP 94 || e->n->ntyp == NON_ATOMIC) 95 repro_sub(e); 96 else if (e->n->ntyp != '.' 97 && e->n->ntyp != '@' 98 && e->n->ntyp != BREAK) 99 { 100 doindent(); 101 if (e->n->ntyp == C_CODE) 102 { printf("c_code "); 103 plunk_inline(stdout, e->n->sym->name, 1); 104 } else if (e->n->ntyp == 'c' 105 && e->n->lft->ntyp == C_EXPR) 106 { printf("c_expr { "); 107 plunk_expr(stdout, e->n->lft->sym->name); 108 printf("} ->\n"); 109 } else 110 { comment(stdout, e->n, 0); 111 printf(";\n"); 112 } } 113 } 114 if (e == s->last) 115 break; 116 } 117 } 118 119 void 120 repro_proc(ProcList *p) 121 { 122 if (!p) return; 123 if (p->nxt) repro_proc(p->nxt); 124 125 if (p->det) printf("D"); /* deterministic */ 126 printf("proctype %s()", p->n->name); 127 if (p->prov) 128 { printf(" provided "); 129 comment(stdout, p->prov, 0); 130 } 131 printf("\n{\n"); 132 repro_seq(p->s); 133 printf("}\n"); 134 } 135 136 void 137 repro_src(void) 138 { 139 repro_proc(rdy); 140 } 141