Subversion Repositories planix.SVN

Rev

Rev 2 | Details | Compare with Previous | Last modification | View Log | RSS feed

Rev Author Line No. Line
2 - 1 
/***** tl_spin: tl_rewrt.c *****/
2 
 
3 
/* Copyright (c) 1995-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 
/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
13 
/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.   */
14 
 
15 
#include "tl.h"
16 
 
17 
extern int	tl_verbose;
18 
 
19 
static Node	*can = ZN;
20 
 
21 
void
22 
ini_rewrt(void)
23 
{
24 
	can = ZN;
25 
}
26 
 
27 
Node *
28 
right_linked(Node *n)
29 
{
30 
	if (!n) return n;
31 
 
32 
	if (n->ntyp == AND || n->ntyp == OR)
33 
		while (n->lft && n->lft->ntyp == n->ntyp)
34 
		{	Node *tmp = n->lft;
35 
			n->lft = tmp->rgt;
36 
			tmp->rgt = n;
37 
			n = tmp;
38 
		}
39 
 
40 
	n->lft = right_linked(n->lft);
41 
	n->rgt = right_linked(n->rgt);
42 
 
43 
	return n;
44 
}
45 
 
46 
Node *
47 
canonical(Node *n)
48 
{	Node *m;	/* assumes input is right_linked */
49 
 
50 
	if (!n) return n;
51 
	if ((m = in_cache(n)) != ZN)
52 
		return m;
53 
 
54 
	n->rgt = canonical(n->rgt);
55 
	n->lft = canonical(n->lft);
56 
 
57 
	return cached(n);
58 
}
59 
 
60 
Node *
61 
push_negation(Node *n)
62 
{	Node *m;
63 
 
64 
	Assert(n->ntyp == NOT, n->ntyp);
65 
 
66 
	switch (n->lft->ntyp) {
67 
	case TRUE:
68 
		Debug("!true => false\n");
69 
		releasenode(0, n->lft);
70 
		n->lft = ZN;
71 
		n->ntyp = FALSE;
72 
		break;
73 
	case FALSE:
74 
		Debug("!false => true\n");
75 
		releasenode(0, n->lft);
76 
		n->lft = ZN;
77 
		n->ntyp = TRUE;
78 
		break;
79 
	case NOT:
80 
		Debug("!!p => p\n");
81 
		m = n->lft->lft;
82 
		releasenode(0, n->lft);
83 
		n->lft = ZN;
84 
		releasenode(0, n);
85 
		n = m;
86 
		break;
87 
	case V_OPER:
88 
		Debug("!(p V q) => (!p U !q)\n");
89 
		n->ntyp = U_OPER;
90 
		goto same;
91 
	case U_OPER:
92 
		Debug("!(p U q) => (!p V !q)\n");
93 
		n->ntyp = V_OPER;
94 
		goto same;
95 
#ifdef NXT
96 
	case NEXT:
97 
		Debug("!X -> X!\n");
98 
		n->ntyp = NEXT;
99 
		n->lft->ntyp = NOT;
100 
		n->lft = push_negation(n->lft);
101 
		break;
102 
#endif
103 
	case  AND:
104 
		Debug("!(p && q) => !p || !q\n");
105 
		n->ntyp = OR;
106 
		goto same;
107 
	case  OR:
108 
		Debug("!(p || q) => !p && !q\n");
109 
		n->ntyp = AND;
110 
 
111 
same:		m = n->lft->rgt;
112 
		n->lft->rgt = ZN;
113 
 
114 
		n->rgt = Not(m);
115 
		n->lft->ntyp = NOT;
116 
		m = n->lft;
117 
		n->lft = push_negation(m);
118 
		break;
119 
	}
120 
 
121 
	return rewrite(n);
122 
}
123 
 
124 
static void
125 
addcan(int tok, Node *n)
126 
{	Node	*m, *prev = ZN;
127 
	Node	**ptr;
128 
	Node	*N;
129 
	Symbol	*s, *t; int cmp;
130 
 
131 
	if (!n) return;
132 
 
133 
	if (n->ntyp == tok)
134 
	{	addcan(tok, n->rgt);
135 
		addcan(tok, n->lft);
136 
		return;
137 
	}
138 
 
139 
	N = dupnode(n);
140 
	if (!can)
141 
	{	can = N;
142 
		return;
143 
	}
144 
 
145 
	s = DoDump(N);
146 
	if (can->ntyp != tok)	/* only one element in list so far */
147 
	{	ptr = &can;
148 
		goto insert;
149 
	}
150 
 
151 
	/* there are at least 2 elements in list */
152 
	prev = ZN;
153 
	for (m = can; m->ntyp == tok && m->rgt; prev = m, m = m->rgt)
154 
	{	t = DoDump(m->lft);
155 
		if (t != ZS)
156 
			cmp = strcmp(s->name, t->name);
157 
		else
158 
			cmp = 0;
159 
		if (cmp == 0)	/* duplicate */
160 
			return;
161 
		if (cmp < 0)
162 
		{	if (!prev)
163 
			{	can = tl_nn(tok, N, can);
164 
				return;
165 
			} else
166 
			{	ptr = &(prev->rgt);
167 
				goto insert;
168 
	}	}	}
169 
 
170 
	/* new entry goes at the end of the list */
171 
	ptr = &(prev->rgt);
172 
insert:
173 
	t = DoDump(*ptr);
174 
	cmp = strcmp(s->name, t->name);
175 
	if (cmp == 0)	/* duplicate */
176 
		return;
177 
	if (cmp < 0)
178 
		*ptr = tl_nn(tok, N, *ptr);
179 
	else
180 
		*ptr = tl_nn(tok, *ptr, N);
181 
}
182 
 
183 
static void
184 
marknode(int tok, Node *m)
185 
{
186 
	if (m->ntyp != tok)
187 
	{	releasenode(0, m->rgt);
188 
		m->rgt = ZN;
189 
	}
190 
	m->ntyp = -1;
191 
}
192 
 
193 
Node *
194 
Canonical(Node *n)
195 
{	Node *m, *p, *k1, *k2, *prev, *dflt = ZN;
196 
	int tok;
197 
 
198 
	if (!n) return n;
199 
 
200 
	tok = n->ntyp;
201 
	if (tok != AND && tok != OR)
202 
		return n;
203 
 
204 
	can = ZN;
205 
	addcan(tok, n);
206 
#if 0
207 
	Debug("\nA0: "); Dump(can);
208 
	Debug("\nA1: "); Dump(n); Debug("\n");
209 
#endif
210 
	releasenode(1, n);
211 
 
212 
	/* mark redundant nodes */
213 
	if (tok == AND)
214 
	{	for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN)
215 
		{	k1 = (m->ntyp == AND) ? m->lft : m;
216 
			if (k1->ntyp == TRUE)
217 
			{	marknode(AND, m);
218 
				dflt = True;
219 
				continue;
220 
			}
221 
			if (k1->ntyp == FALSE)
222 
			{	releasenode(1, can);
223 
				can = False;
224 
				goto out;
225 
		}	}
226 
		for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN)
227 
		for (p = can; p; p = (p->ntyp == AND) ? p->rgt : ZN)
228 
		{	if (p == m
229 
			||  p->ntyp == -1
230 
			||  m->ntyp == -1)
231 
				continue;
232 
			k1 = (m->ntyp == AND) ? m->lft : m;
233 
			k2 = (p->ntyp == AND) ? p->lft : p;
234 
 
235 
			if (isequal(k1, k2))
236 
			{	marknode(AND, p);
237 
				continue;
238 
			}
239 
			if (anywhere(OR, k1, k2))
240 
			{	marknode(AND, p);
241 
				continue;
242 
			}
243 
	}	}
244 
	if (tok == OR)
245 
	{	for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN)
246 
		{	k1 = (m->ntyp == OR) ? m->lft : m;
247 
			if (k1->ntyp == FALSE)
248 
			{	marknode(OR, m);
249 
				dflt = False;
250 
				continue;
251 
			}
252 
			if (k1->ntyp == TRUE)
253 
			{	releasenode(1, can);
254 
				can = True;
255 
				goto out;
256 
		}	}
257 
		for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN)
258 
		for (p = can; p; p = (p->ntyp == OR) ? p->rgt : ZN)
259 
		{	if (p == m
260 
			||  p->ntyp == -1
261 
			||  m->ntyp == -1)
262 
				continue;
263 
			k1 = (m->ntyp == OR) ? m->lft : m;
264 
			k2 = (p->ntyp == OR) ? p->lft : p;
265 
 
266 
			if (isequal(k1, k2))
267 
			{	marknode(OR, p);
268 
				continue;
269 
			}
270 
			if (anywhere(AND, k1, k2))
271 
			{	marknode(OR, p);
272 
				continue;
273 
			}
274 
	}	}
275 
	for (m = can, prev = ZN; m; )	/* remove marked nodes */
276 
	{	if (m->ntyp == -1)
277 
		{	k2 = m->rgt;
278 
			releasenode(0, m);
279 
			if (!prev)
280 
			{	m = can = can->rgt;
281 
			} else
282 
			{	m = prev->rgt = k2;
283 
				/* if deleted the last node in a chain */
284 
				if (!prev->rgt && prev->lft
285 
				&&  (prev->ntyp == AND || prev->ntyp == OR))
286 
				{	k1 = prev->lft;
287 
					prev->ntyp = prev->lft->ntyp;
288 
					prev->sym = prev->lft->sym;
289 
					prev->rgt = prev->lft->rgt;
290 
					prev->lft = prev->lft->lft;
291 
					releasenode(0, k1);
292 
				}
293 
			}
294 
			continue;
295 
		}
296 
		prev = m;
297 
		m = m->rgt;
298 
	}
299 
out:
300 
#if 0
301 
	Debug("A2: "); Dump(can); Debug("\n");
302 
#endif
303 
	if (!can)
304 
	{	if (!dflt)
305 
			fatal("cannot happen, Canonical", (char *) 0);
306 
		return dflt;
307 
	}
308 
 
309 
	return can;
310 
}