blob: 0d4ba6be705c6861e45b94730446009c5523e33b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
/***** 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 *);
void
doindent(void)
{ int i;
for (i = 0; i < indent; i++)
printf(" ");
}
void
repro_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");
}
void
repro_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;
}
}
void
repro_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");
}
void
repro_src(void)
{
repro_proc(rdy);
}
|
