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_buchi.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, tl_clutter, Total, Max_Red;
18 
extern char *claim_name;
19 
 
20 
FILE	*tl_out;	/* if standalone: = stdout; */
21 
 
22 
typedef struct Transition {
23 
	Symbol *name;
24 
	Node *cond;
25 
	int redundant, merged, marked;
26 
	struct Transition *nxt;
27 
} Transition;
28 
 
29 
typedef struct State {
30 
	Symbol	*name;
31 
	Transition *trans;
32 
	Graph	*colors;
33 
	unsigned char redundant;
34 
	unsigned char accepting;
35 
	unsigned char reachable;
36 
	struct State *nxt;
37 
} State;
38 
 
39 
static State *never = (State *) 0;
40 
static int hitsall;
41 
 
42 
void
43 
ini_buchi(void)
44 
{
45 
	never = (State *) 0;
46 
	hitsall = 0;
47 
}
48 
 
49 
static int
50 
sametrans(Transition *s, Transition *t)
51 
{
52 
	if (strcmp(s->name->name, t->name->name) != 0)
53 
		return 0;
54 
	return isequal(s->cond, t->cond);
55 
}
56 
 
57 
static Node *
58 
Prune(Node *p)
59 
{
60 
	if (p)
61 
	switch (p->ntyp) {
62 
	case PREDICATE:
63 
	case NOT:
64 
	case FALSE:
65 
	case TRUE:
66 
#ifdef NXT
67 
	case NEXT:
68 
#endif
69 
		return p;
70 
	case OR:
71 
		p->lft = Prune(p->lft);
72 
		if (!p->lft)
73 
		{	releasenode(1, p->rgt);
74 
			return ZN;
75 
		}
76 
		p->rgt = Prune(p->rgt);
77 
		if (!p->rgt)
78 
		{	releasenode(1, p->lft);
79 
			return ZN;
80 
		}
81 
		return p;
82 
	case AND:
83 
		p->lft = Prune(p->lft);
84 
		if (!p->lft)
85 
			return Prune(p->rgt);
86 
		p->rgt = Prune(p->rgt);
87 
		if (!p->rgt)
88 
			return p->lft;
89 
		return p;
90 
	}
91 
	releasenode(1, p);
92 
	return ZN;
93 
}
94 
 
95 
static State *
96 
findstate(char *nm)
97 
{	State *b;
98 
	for (b = never; b; b = b->nxt)
99 
		if (!strcmp(b->name->name, nm))
100 
			return b;
101 
	if (strcmp(nm, "accept_all"))
102 
	{	if (strncmp(nm, "accept", 6))
103 
		{	int i; char altnm[64];
104 
			for (i = 0; i < 64; i++)
105 
				if (nm[i] == '_')
106 
					break;
107 
			if (i >= 64)
108 
				Fatal("name too long %s", nm);
109 
			sprintf(altnm, "accept%s", &nm[i]);
110 
			return findstate(altnm);
111 
		}
112 
	/*	Fatal("buchi: no state %s", nm); */
113 
	}
114 
	return (State *) 0;
115 
}
116 
 
117 
static void
118 
Dfs(State *b)
119 
{	Transition *t;
120 
 
121 
	if (!b || b->reachable) return;
122 
	b->reachable = 1;
123 
 
124 
	if (b->redundant)
125 
		printf("/* redundant state %s */\n",
126 
			b->name->name);
127 
	for (t = b->trans; t; t = t->nxt)
128 
	{	if (!t->redundant)
129 
		{	Dfs(findstate(t->name->name));
130 
			if (!hitsall
131 
			&&  strcmp(t->name->name, "accept_all") == 0)
132 
				hitsall = 1;
133 
		}
134 
	}
135 
}
136 
 
137 
void
138 
retarget(char *from, char *to)
139 
{	State *b;
140 
	Transition *t;
141 
	Symbol *To = tl_lookup(to);
142 
 
143 
	if (tl_verbose) printf("replace %s with %s\n", from, to);
144 
 
145 
	for (b = never; b; b = b->nxt)
146 
	{	if (!strcmp(b->name->name, from))
147 
			b->redundant = 1;
148 
		else
149 
		for (t = b->trans; t; t = t->nxt)
150 
		{	if (!strcmp(t->name->name, from))
151 
				t->name = To;
152 
	}	}
153 
}
154 
 
155 
#ifdef NXT
156 
static Node *
157 
nonxt(Node *n)
158 
{
159 
	switch (n->ntyp) {
160 
	case U_OPER:
161 
	case V_OPER:
162 
	case NEXT:
163 
		return ZN;
164 
	case OR:
165 
		n->lft = nonxt(n->lft);
166 
		n->rgt = nonxt(n->rgt);
167 
		if (!n->lft || !n->rgt)
168 
			return True;
169 
		return n;
170 
	case AND:
171 
		n->lft = nonxt(n->lft);
172 
		n->rgt = nonxt(n->rgt);
173 
		if (!n->lft)
174 
		{	if (!n->rgt)
175 
				n = ZN;
176 
			else
177 
				n = n->rgt;
178 
		} else if (!n->rgt)
179 
			n = n->lft;
180 
		return n;
181 
	}
182 
	return n;
183 
}
184 
#endif
185 
 
186 
static Node *
187 
combination(Node *s, Node *t)
188 
{	Node *nc;
189 
#ifdef NXT
190 
	Node *a = nonxt(s);
191 
	Node *b = nonxt(t);
192 
 
193 
	if (tl_verbose)
194 
	{	printf("\tnonxtA: "); dump(a);
195 
		printf("\n\tnonxtB: "); dump(b);
196 
		printf("\n");
197 
	}
198 
	/* if there's only a X(f), its equivalent to true */
199 
	if (!a || !b)
200 
		nc = True;
201 
	else
202 
		nc = tl_nn(OR, a, b);
203 
#else
204 
	nc = tl_nn(OR, s, t);
205 
#endif
206 
	if (tl_verbose)
207 
	{	printf("\tcombo: "); dump(nc);
208 
		printf("\n");
209 
	}
210 
	return nc;
211 
}
212 
 
213 
Node *
214 
unclutter(Node *n, char *snm)
215 
{	Node *t, *s, *v, *u;
216 
	Symbol *w;
217 
 
218 
	/* check only simple cases like !q && q */
219 
	for (t = n; t; t = t->rgt)
220 
	{	if (t->rgt)
221 
		{	if (t->ntyp != AND || !t->lft)
222 
				return n;
223 
			if (t->lft->ntyp != PREDICATE
224 
#ifdef NXT
225 
			&&  t->lft->ntyp != NEXT
226 
#endif
227 
			&&  t->lft->ntyp != NOT)
228 
				return n;
229 
		} else
230 
		{	if (t->ntyp != PREDICATE
231 
#ifdef NXT
232 
			&&  t->ntyp != NEXT
233 
#endif
234 
			&&  t->ntyp != NOT)
235 
				return n;
236 
		}
237 
	}
238 
 
239 
	for (t = n; t; t = t->rgt)
240 
	{	if (t->rgt)
241 
			v = t->lft;
242 
		else
243 
			v = t;
244 
		if (v->ntyp == NOT
245 
		&&  v->lft->ntyp == PREDICATE)
246 
		{	w = v->lft->sym;
247 
			for (s = n; s; s = s->rgt)
248 
			{	if (s == t) continue;
249 
				if (s->rgt)
250 
					u = s->lft;
251 
				else
252 
					u = s;
253 
				if (u->ntyp == PREDICATE
254 
				&&  strcmp(u->sym->name, w->name) == 0)
255 
				{	if (tl_verbose)
256 
					{	printf("BINGO %s:\t", snm);
257 
						dump(n);
258 
						printf("\n");
259 
					}
260 
					return False;
261 
				}
262 
			}
263 
	}	}
264 
	return n;
265 
}
266 
 
267 
static void
268 
clutter(void)
269 
{	State *p;
270 
	Transition *s;
271 
 
272 
	for (p = never; p; p = p->nxt)
273 
	for (s = p->trans; s; s = s->nxt)
274 
	{	s->cond = unclutter(s->cond, p->name->name);
275 
		if (s->cond
276 
		&&  s->cond->ntyp == FALSE)
277 
		{	if (s != p->trans
278 
			||  s->nxt)
279 
				s->redundant = 1;
280 
		}
281 
	}
282 
}
283 
 
284 
static void
285 
showtrans(State *a)
286 
{	Transition *s;
287 
 
288 
	for (s = a->trans; s; s = s->nxt)
289 
	{	printf("%s ", s->name?s->name->name:"-");
290 
		dump(s->cond);
291 
		printf(" %d %d %d\n", s->redundant, s->merged, s->marked);
292 
	}
293 
}
294 
 
295 
static int
296 
mergetrans(void)
297 
{	State *b;
298 
	Transition *s, *t;
299 
	Node *nc; int cnt = 0;
300 
 
301 
	for (b = never; b; b = b->nxt)
302 
	{	if (!b->reachable) continue;
303 
 
304 
		for (s = b->trans; s; s = s->nxt)
305 
		{	if (s->redundant) continue;
306 
 
307 
			for (t = s->nxt; t; t = t->nxt)
308 
			if (!t->redundant
309 
			&&  !strcmp(s->name->name, t->name->name))
310 
			{	if (tl_verbose)
311 
				{	printf("===\nstate %s, trans to %s redundant\n",
312 
					b->name->name, s->name->name);
313 
					showtrans(b);
314 
					printf(" conditions ");
315 
					dump(s->cond); printf(" <-> ");
316 
					dump(t->cond); printf("\n");
317 
				}
318 
 
319 
				if (!s->cond) /* same as T */
320 
				{	releasenode(1, t->cond); /* T or t */
321 
					nc = True;
322 
				} else if (!t->cond)
323 
				{	releasenode(1, s->cond);
324 
					nc = True;
325 
				} else
326 
				{	nc = combination(s->cond, t->cond);
327 
				}
328 
				t->cond = rewrite(nc);
329 
				t->merged = 1;
330 
				s->redundant = 1;
331 
				cnt++;
332 
				break;
333 
	}	}	}
334 
	return cnt;
335 
}
336 
 
337 
static int
338 
all_trans_match(State *a, State *b)
339 
{	Transition *s, *t;
340 
	int found, result = 0;
341 
 
342 
	if (a->accepting != b->accepting)
343 
		goto done;
344 
 
345 
	for (s = a->trans; s; s = s->nxt)
346 
	{	if (s->redundant) continue;
347 
		found = 0;
348 
		for (t = b->trans; t; t = t->nxt)
349 
		{	if (t->redundant) continue;
350 
			if (sametrans(s, t))
351 
			{	found = 1;
352 
				t->marked = 1;
353 
				break;
354 
		}	}
355 
		if (!found)
356 
			goto done;
357 
	}
358 
	for (s = b->trans; s; s = s->nxt)
359 
	{	if (s->redundant || s->marked) continue;
360 
		found = 0;
361 
		for (t = a->trans; t; t = t->nxt)
362 
		{	if (t->redundant) continue;
363 
			if (sametrans(s, t))
364 
			{	found = 1;
365 
				break;
366 
		}	}
367 
		if (!found)
368 
			goto done;
369 
	}
370 
	result = 1;
371 
done:
372 
	for (s = b->trans; s; s = s->nxt)
373 
		s->marked = 0;
374 
	return result;
375 
}
376 
 
377 
#ifndef NO_OPT
378 
#define BUCKY
379 
#endif
380 
 
381 
#ifdef BUCKY
382 
static int
383 
all_bucky(State *a, State *b)
384 
{	Transition *s, *t;
385 
	int found, result = 0;
386 
 
387 
	for (s = a->trans; s; s = s->nxt)
388 
	{	if (s->redundant) continue;
389 
		found = 0;
390 
		for (t = b->trans; t; t = t->nxt)
391 
		{	if (t->redundant) continue;
392 
 
393 
			if (isequal(s->cond, t->cond))
394 
			{	if (strcmp(s->name->name, b->name->name) == 0
395 
				&&  strcmp(t->name->name, a->name->name) == 0)
396 
				{	found = 1;	/* they point to each other */
397 
					t->marked = 1;
398 
					break;
399 
				}
400 
				if (strcmp(s->name->name, t->name->name) == 0
401 
				&&  strcmp(s->name->name, "accept_all") == 0)
402 
				{	found = 1;
403 
					t->marked = 1;
404 
					break;
405 
				/* same exit from which there is no return */
406 
				}
407 
			}
408 
		}
409 
		if (!found)
410 
			goto done;
411 
	}
412 
	for (s = b->trans; s; s = s->nxt)
413 
	{	if (s->redundant || s->marked) continue;
414 
		found = 0;
415 
		for (t = a->trans; t; t = t->nxt)
416 
		{	if (t->redundant) continue;
417 
 
418 
			if (isequal(s->cond, t->cond))
419 
			{	if (strcmp(s->name->name, a->name->name) == 0
420 
				&&  strcmp(t->name->name, b->name->name) == 0)
421 
				{	found = 1;
422 
					t->marked = 1;
423 
					break;
424 
				}
425 
				if (strcmp(s->name->name, t->name->name) == 0
426 
				&&  strcmp(s->name->name, "accept_all") == 0)
427 
				{	found = 1;
428 
					t->marked = 1;
429 
					break;
430 
				}
431 
			}
432 
		}
433 
		if (!found)
434 
			goto done;
435 
	}
436 
	result = 1;
437 
done:
438 
	for (s = b->trans; s; s = s->nxt)
439 
		s->marked = 0;
440 
	return result;
441 
}
442 
 
443 
static int
444 
buckyballs(void)
445 
{	State *a, *b, *c, *d;
446 
	int m, cnt=0;
447 
 
448 
	do {
449 
		m = 0; cnt++;
450 
		for (a = never; a; a = a->nxt)
451 
		{	if (!a->reachable) continue;
452 
 
453 
			if (a->redundant) continue;
454 
 
455 
			for (b = a->nxt; b; b = b->nxt)
456 
			{	if (!b->reachable) continue;
457 
 
458 
				if (b->redundant) continue;
459 
 
460 
				if (all_bucky(a, b))
461 
				{	m++;
462 
					if (tl_verbose)
463 
					{	printf("%s bucky match %s\n",
464 
						a->name->name, b->name->name);
465 
					}
466 
 
467 
					if (a->accepting && !b->accepting)
468 
					{	if (strcmp(b->name->name, "T0_init") == 0)
469 
						{	c = a; d = b;
470 
							b->accepting = 1;
471 
						} else
472 
						{	c = b; d = a;
473 
						}
474 
					} else
475 
					{	c = a; d = b;
476 
					}
477 
 
478 
					retarget(c->name->name, d->name->name);
479 
					if (!strncmp(c->name->name, "accept", 6)
480 
					&&  Max_Red == 0)
481 
					{	char buf[64];
482 
						sprintf(buf, "T0%s", &(c->name->name[6]));
483 
						retarget(buf, d->name->name);
484 
					}
485 
					break;
486 
				}
487 
		}	}
488 
	} while (m && cnt < 10);
489 
	return cnt-1;
490 
}
491 
#endif
492 
 
493 
static int
494 
mergestates(int v)
495 
{	State *a, *b;
496 
	int m, cnt=0;
497 
 
498 
	if (tl_verbose)
499 
		return 0;
500 
 
501 
	do {
502 
		m = 0; cnt++;
503 
		for (a = never; a; a = a->nxt)
504 
		{	if (v && !a->reachable) continue;
505 
 
506 
			if (a->redundant) continue; /* 3.3.10 */
507 
 
508 
			for (b = a->nxt; b; b = b->nxt)
509 
			{	if (v && !b->reachable) continue;
510 
 
511 
				if (b->redundant) continue; /* 3.3.10 */
512 
 
513 
				if (all_trans_match(a, b))
514 
				{	m++;
515 
					if (tl_verbose)
516 
					{	printf("%d: state %s equals state %s\n",
517 
						cnt, a->name->name, b->name->name);
518 
						showtrans(a);
519 
						printf("==\n");
520 
						showtrans(b);
521 
					}
522 
					retarget(a->name->name, b->name->name);
523 
					if (!strncmp(a->name->name, "accept", 6)
524 
					&&  Max_Red == 0)
525 
					{	char buf[64];
526 
						sprintf(buf, "T0%s", &(a->name->name[6]));
527 
						retarget(buf, b->name->name);
528 
					}
529 
					break;
530 
				}
531 
#if 0
532 
				else if (tl_verbose)
533 
				{	printf("\n%d: state %s differs from state %s [%d,%d]\n",
534 
						cnt, a->name->name, b->name->name,
535 
						a->accepting, b->accepting);
536 
					showtrans(a);
537 
					printf("==\n");
538 
					showtrans(b);
539 
					printf("\n");
540 
				}
541 
#endif
542 
		}	}
543 
	} while (m && cnt < 10);
544 
	return cnt-1;
545 
}
546 
 
547 
static int tcnt;
548 
 
549 
static void
550 
rev_trans(Transition *t) /* print transitions  in reverse order... */
551 
{
552 
	if (!t) return;
553 
	rev_trans(t->nxt);
554 
 
555 
	if (t->redundant && !tl_verbose) return;
556 
	fprintf(tl_out, "\t:: (");
557 
	if (dump_cond(t->cond, t->cond, 1))
558 
		fprintf(tl_out, "1");
559 
	fprintf(tl_out, ") -> goto %s\n", t->name->name);
560 
	tcnt++;
561 
}
562 
 
563 
static void
564 
printstate(State *b)
565 
{
566 
	if (!b || (!tl_verbose && !b->reachable)) return;
567 
 
568 
	b->reachable = 0;	/* print only once */
569 
	fprintf(tl_out, "%s:\n", b->name->name);
570 
 
571 
	if (tl_verbose)
572 
	{	fprintf(tl_out, "	/* ");
573 
		dump(b->colors->Other);
574 
		fprintf(tl_out, " */\n");
575 
	}
576 
 
577 
	if (strncmp(b->name->name, "accept", 6) == 0
578 
	&&  Max_Red == 0)
579 
		fprintf(tl_out, "T0%s:\n", &(b->name->name[6]));
580 
 
581 
	fprintf(tl_out, "\tif\n");
582 
	tcnt = 0;
583 
	rev_trans(b->trans);
584 
	if (!tcnt) fprintf(tl_out, "\t:: false\n");
585 
	fprintf(tl_out, "\tfi;\n");
586 
	Total++;
587 
}
588 
 
589 
void
590 
addtrans(Graph *col, char *from, Node *op, char *to)
591 
{	State *b;
592 
	Transition *t;
593 
 
594 
	t = (Transition *) tl_emalloc(sizeof(Transition));
595 
	t->name = tl_lookup(to);
596 
	t->cond = Prune(dupnode(op));
597 
 
598 
	if (tl_verbose)
599 
	{	printf("\n%s <<\t", from); dump(op);
600 
		printf("\n\t"); dump(t->cond);
601 
		printf(">> %s\n", t->name->name);
602 
	}
603 
	if (t->cond) t->cond = rewrite(t->cond);
604 
 
605 
	for (b = never; b; b = b->nxt)
606 
		if (!strcmp(b->name->name, from))
607 
		{	t->nxt = b->trans;
608 
			b->trans = t;
609 
			return;
610 
		}
611 
	b = (State *) tl_emalloc(sizeof(State));
612 
	b->name   = tl_lookup(from);
613 
	b->colors = col;
614 
	b->trans  = t;
615 
	if (!strncmp(from, "accept", 6))
616 
		b->accepting = 1;
617 
	b->nxt = never;
618 
	never  = b;
619 
}
620 
 
621 
static void
622 
clr_reach(void)
623 
{	State *p;
624 
	for (p = never; p; p = p->nxt)
625 
		p->reachable = 0;
626 
	hitsall = 0;
627 
}
628 
 
629 
void
630 
fsm_print(void)
631 
{	State *b; int cnt1, cnt2=0;
632 
	extern void put_uform(void);
633 
 
634 
	if (tl_clutter) clutter();
635 
 
636 
	b = findstate("T0_init");
637 
	if (b && (Max_Red == 0))
638 
		b->accepting = 1;
639 
 
640 
	mergestates(0);
641 
	b = findstate("T0_init");
642 
 
643 
	fprintf(tl_out, "never %s {    /* ", claim_name?claim_name:"");
644 
		put_uform();
645 
	fprintf(tl_out, " */\n");
646 
 
647 
	do {
648 
		clr_reach();
649 
		Dfs(b);
650 
		cnt1 = mergetrans();
651 
		cnt2 = mergestates(1);
652 
		if (tl_verbose)
653 
			printf("/* >>%d,%d<< */\n", cnt1, cnt2);
654 
	} while (cnt2 > 0);
655 
 
656 
#ifdef BUCKY
657 
	buckyballs();
658 
	clr_reach();
659 
	Dfs(b);
660 
#endif
661 
	if (b && b->accepting)
662 
		fprintf(tl_out, "accept_init:\n");
663 
 
664 
	if (!b && !never)
665 
	{	fprintf(tl_out, "	0 /* false */;\n");
666 
	} else
667 
	{	printstate(b);	/* init state must be first */
668 
		for (b = never; b; b = b->nxt)
669 
			printstate(b);
670 
	}
671 
	if (hitsall)
672 
	fprintf(tl_out, "accept_all:\n	skip\n");
673 
	fprintf(tl_out, "}\n");
674 
}