Subversion Repositories planix.SVN

Rev

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

Rev Author Line No. Line
2 - 1 
/***** spin: pangen7.c *****/
2 
 
3 
/* Copyright (c) 1989-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 
/* pangen7.c: Version 5.3.0 2010, synchronous product of never claims     */
12 
 
13 
#include <stdlib.h>
14 
#include "spin.h"
15 
#include "y.tab.h"
16 
#include <assert.h>
17 
#ifdef PC
18 
extern int unlink(const char *);
19 
#else
20 
#include <unistd.h>
21 
#endif
22 
 
23 
extern ProcList	*rdy;
24 
extern Element *Al_El;
25 
extern int nclaims, verbose, Strict;
26 
 
27 
typedef struct Succ_List Succ_List;
28 
typedef struct SQueue SQueue;
29 
typedef struct OneState OneState;
30 
typedef struct State_Stack State_Stack;
31 
typedef struct Guard Guard;
32 
 
33 
struct Succ_List {
34 
	SQueue	*s;
35 
	Succ_List *nxt;
36 
};
37 
 
38 
struct OneState {
39 
	int	*combo;	/* the combination of claim states */
40 
	Succ_List	*succ;	/* list of ptrs to immediate successor states */
41 
};
42 
 
43 
struct SQueue {
44 
	OneState	state;
45 
	SQueue	*nxt;
46 
};
47 
 
48 
struct State_Stack {
49 
	int *n;
50 
	State_Stack *nxt;
51 
};
52 
 
53 
struct Guard {
54 
	Lextok *t;
55 
	Guard *nxt;
56 
};
57 
 
58 
SQueue	*sq, *sd, *render;	/* states move from sq to sd to render to holding */
59 
SQueue	*holding, *lasthold;
60 
State_Stack *dsts;
61 
 
62 
int nst;		/* max nr of states in claims */
63 
int *Ist;		/* initial states */
64 
int *Nacc;		/* number of accept states in claim */
65 
int *Nst;		/* next states */
66 
int **reached;		/* n claims x states */
67 
int unfolding;		/* to make sure all accept states are reached */
68 
int is_accept;		/* remember if the current state is accepting in any claim */
69 
int not_printing;	/* set during explore_product */
70 
 
71 
Element ****matrix;	/* n x two-dimensional arrays state x state */
72 
Element **Selfs;	/* self-loop states at end of claims */
73 
 
74 
static void get_seq(int, Sequence *);
75 
static void set_el(int n, Element *e);
76 
static void gen_product(void);
77 
static void print_state_nm(char *, int *, char *);
78 
static SQueue *find_state(int *);
79 
static SQueue *retrieve_state(int *);
80 
 
81 
static int
82 
same_state(int *a, int *b)
83 
{	int i;
84 
 
85 
	for (i = 0; i < nclaims; i++)
86 
	{	if (a[i] != b[i])
87 
		{	return 0;
88 
	}	}
89 
	return 1;
90 
}
91 
 
92 
static int
93 
in_stack(SQueue *s, SQueue *in)
94 
{	SQueue *q;
95 
 
96 
	for (q = in; q; q = q->nxt)
97 
	{	if (same_state(q->state.combo, s->state.combo))
98 
		{	return 1;
99 
	}	}
100 
	return 0;
101 
}
102 
 
103 
static void
104 
to_render(SQueue *s)
105 
{	SQueue *a, *q, *last; /* find in sd/sq and move to render, if not already there */
106 
	int n;
107 
 
108 
	for (n = 0; n < nclaims; n++)
109 
	{	reached[n][ s->state.combo[n] ] |= 2;
110 
	}
111 
 
112 
	for (q = render; q; q = q->nxt)
113 
	{	if (same_state(q->state.combo, s->state.combo))
114 
		{	return;
115 
	}	}
116 
	for (q = holding; q; q = q->nxt)
117 
	{	if (same_state(q->state.combo, s->state.combo))
118 
		{	return;
119 
	}	}
120 
 
121 
	a = sd;
122 
more:
123 
	for (q = a, last = 0; q; last = q, q = q->nxt)
124 
	{	if (same_state(q->state.combo, s->state.combo))
125 
		{	if (!last)
126 
			{	if (a == sd)
127 
				{	sd = q->nxt;
128 
				} else if (a == sq)
129 
				{	sq = q->nxt;
130 
				} else
131 
				{	holding = q->nxt;
132 
				}
133 
			} else
134 
			{	last->nxt = q->nxt;
135 
			}
136 
			q->nxt = render;
137 
			render = q;
138 
			return;
139 
	}	}
140 
	if (verbose)
141 
	{	print_state_nm("looking for: ", s->state.combo, "\n");
142 
	}
143 
	(void) find_state(s->state.combo);	/* creates it in sq */
144 
	if (a != sq)
145 
	{	a = sq;
146 
		goto more;
147 
	}
148 
	fatal("cannot happen, to_render", 0);
149 
}
150 
 
151 
static void
152 
wrap_text(char *pre, Lextok *t, char *post)
153 
{
154 
	printf(pre);
155 
	comment(stdout, t, 0);
156 
	printf(post);
157 
}
158 
 
159 
static State_Stack *
160 
push_dsts(int *n)
161 
{	State_Stack *s;
162 
	int i;
163 
 
164 
	for (s = dsts; s; s = s->nxt)
165 
	{	if (same_state(s->n, n))
166 
		{	if (verbose&64)
167 
			{	printf("\n");
168 
				for (s = dsts; s; s = s->nxt)
169 
				{	print_state_nm("\t", s->n, "\n");
170 
				}
171 
				print_state_nm("\t", n, "\n");
172 
			}
173 
			return s;
174 
	}	}
175 
 
176 
	s = (State_Stack *) emalloc(sizeof(State_Stack));
177 
	s->n = (int *) emalloc(nclaims * sizeof(int));
178 
	for (i = 0; i < nclaims; i++)
179 
		s->n[i] = n[i];
180 
	s->nxt = dsts;
181 
	dsts = s;
182 
	return 0;
183 
}
184 
 
185 
static void
186 
pop_dsts(void)
187 
{
188 
	assert(dsts);
189 
	dsts = dsts->nxt;
190 
}
191 
 
192 
static void
193 
complete_transition(Succ_List *sl, Guard *g)
194 
{	Guard *w;
195 
	int cnt = 0;
196 
 
197 
	printf("	:: ");
198 
	for (w = g; w; w = w->nxt)
199 
	{	if (w->t->ntyp == CONST
200 
		&&  w->t->val == 1)
201 
		{	continue;
202 
		} else if (w->t->ntyp == 'c'
203 
		&&  w->t->lft->ntyp == CONST
204 
		&&  w->t->lft->val == 1)
205 
		{	continue; /* 'true' */
206 
		}
207 
 
208 
		if (cnt > 0)
209 
		{	printf(" && ");
210 
		}
211 
		wrap_text("", w->t, "");
212 
		cnt++;
213 
	}
214 
	if (cnt == 0)
215 
	{	printf("true");
216 
	}
217 
	print_state_nm(" -> goto ", sl->s->state.combo, "");
218 
 
219 
	if (is_accept > 0)
220 
	{	printf("_U%d\n", (unfolding+1)%nclaims);
221 
	} else
222 
	{	printf("_U%d\n", unfolding);
223 
	}
224 
}
225 
 
226 
static void
227 
state_body(OneState *s, Guard *guard)
228 
{	Succ_List *sl;
229 
	State_Stack *y;
230 
	Guard *g;
231 
	int i, once;
232 
 
233 
	for (sl = s->succ; sl; sl = sl->nxt)
234 
	{	once = 0;
235 
 
236 
		for (i = 0; i < nclaims; i++)
237 
		{	Element *e;
238 
			e = matrix[i][s->combo[i]][sl->s->state.combo[i]];
239 
 
240 
			/* if one of the claims has a DO or IF move
241 
			   then pull its target state forward, once
242 
			 */
243 
 
244 
			if (!e
245 
			|| e->n->ntyp == NON_ATOMIC
246 
			||  e->n->ntyp == DO
247 
			||  e->n->ntyp == IF)
248 
			{	s = &(sl->s->state);
249 
				y = push_dsts(s->combo);
250 
				if (!y)
251 
				{	if (once++ == 0)
252 
					{	assert(s->succ);
253 
						state_body(s, guard);
254 
					}
255 
					pop_dsts();
256 
				} else if (!y->nxt)	/* self-loop transition */
257 
				{	if (!not_printing) printf(" /* self-loop */\n");
258 
				} else
259 
				{	/* non_fatal("loop in state body", 0); ** maybe ok */
260 
				}
261 
				continue;
262 
			} else
263 
			{	g = (Guard *) emalloc(sizeof(Guard));
264 
				g->t = e->n;
265 
				g->nxt = guard;
266 
				guard = g;
267 
		}	}
268 
 
269 
		if (guard && !once)
270 
		{	if (!not_printing) complete_transition(sl, guard);
271 
			to_render(sl->s);
272 
	}	}
273 
}
274 
 
275 
static struct X {
276 
	char *s;	int n;
277 
} spl[] = {
278 
	{"end",		3 },
279 
	{"accept",	6 },
280 
	{0,		0 },
281 
};
282 
 
283 
static int slcnt;
284 
extern Label *labtab;
285 
 
286 
static ProcList *
287 
locate_claim(int n)
288 
{	ProcList *p;
289 
	int i;
290 
 
291 
	for (p = rdy, i = 0; p; p = p->nxt, i++) /* find claim name */
292 
	{	if (i == n)
293 
		{	break;
294 
	}	}
295 
	assert(p && p->b == N_CLAIM);
296 
 
297 
	return p;
298 
}
299 
 
300 
static void
301 
elim_lab(Element *e)
302 
{	Label *l, *lst;
303 
 
304 
	for (l = labtab, lst = NULL; l; lst = l, l = l->nxt)
305 
	{	if (l->e == e)
306 
		{	if (lst)
307 
			{	lst->nxt = l->nxt;
308 
			} else
309 
			{	labtab = l->nxt;
310 
			}
311 
			break;
312 
	}	}
313 
}
314 
 
315 
static int
316 
claim_has_accept(ProcList *p)
317 
{	Label *l;
318 
 
319 
	for (l = labtab; l; l = l->nxt)
320 
	{	if (strcmp(l->c->name, p->n->name) == 0
321 
		&&  strncmp(l->s->name, "accept", 6) == 0)
322 
		{	return 1;
323 
	}	}
324 
	return 0;
325 
}
326 
 
327 
static void
328 
prune_accept(void)
329 
{	int n;
330 
 
331 
	for (n = 0; n < nclaims; n++)
332 
	{	if ((reached[n][Selfs[n]->seqno] & 2) == 0)
333 
		{	if (verbose)
334 
			{	printf("claim %d: selfloop not reachable\n", n);
335 
			}
336 
			elim_lab(Selfs[n]);
337 
			Nacc[n] = claim_has_accept(locate_claim(n));
338 
	}	}
339 
}
340 
 
341 
static void
342 
mk_accepting(int n, Element *e)
343 
{	ProcList *p;
344 
	Label *l;
345 
	int i;
346 
 
347 
	assert(!Selfs[n]);
348 
	Selfs[n] = e;
349 
 
350 
	l = (Label *) emalloc(sizeof(Label));
351 
	l->s = (Symbol *) emalloc(sizeof(Symbol));
352 
	l->s->name = "accept00";
353 
	l->c = (Symbol *) emalloc(sizeof(Symbol));
354 
	l->uiid = 0;	/* this is not in an inline */
355 
 
356 
	for (p = rdy, i = 0; p; p = p->nxt, i++) /* find claim name */
357 
	{	if (i == n)
358 
		{	l->c->name = p->n->name;
359 
			break;
360 
	}	}
361 
	assert(p && p->b == N_CLAIM);
362 
	Nacc[n] = 1;
363 
 
364 
	l->e = e;
365 
	l->nxt = labtab;
366 
	labtab = l;
367 
}
368 
 
369 
static void
370 
check_special(int *nrs)
371 
{	ProcList *p;
372 
	Label *l;
373 
	int i, j, nmatches;
374 
	int any_accepts = 0;
375 
 
376 
	for (i = 0; i < nclaims; i++)
377 
	{	any_accepts += Nacc[i];
378 
	}
379 
 
380 
	is_accept = 0;
381 
	for (j = 0; spl[j].n; j++) /* 2 special label prefixes */
382 
	{	nmatches = 0;
383 
		for (p = rdy, i = 0; p; p = p->nxt, i++) /* check each claim */
384 
		{	if (p->b != N_CLAIM)
385 
			{	continue;
386 
			}
387 
			/* claim i in state nrs[i], type p->tn, name p->n->name
388 
			 * either the state has an accept label, or the claim has none,
389 
			 * so that all its states should be considered accepting
390 
			 * --- but only if other claims do have accept states!
391 
			 */
392 
			if (Strict == 0 && j == 1 && Nacc[i] == 0 && any_accepts > 0)
393 
			{	if ((verbose&32) && i == unfolding)
394 
				{	printf("	/* claim %d pseudo-accept */\n", i);
395 
				}
396 
				goto is_accepting;
397 
			}
398 
			for (l = labtab; l; l = l->nxt)	/* check its labels */
399 
			{	if (strcmp(l->c->name, p->n->name) == 0  /* right claim */
400 
				&&  l->e->seqno == nrs[i]		 /* right state */
401 
				&&  strncmp(l->s->name, spl[j].s, spl[j].n) == 0)
402 
				{	if (j == 1)	/* accept state */
403 
					{	char buf[32];
404 
is_accepting:					if (strchr(p->n->name, ':'))
405 
						{	sprintf(buf, "N%d", i);
406 
						} else
407 
						{	strcpy(buf, p->n->name);
408 
						}
409 
						if (unfolding == 0 && i == 0)
410 
						{	if (!not_printing)
411 
							printf("%s_%s_%d:\n",	/* true accept */
412 
								spl[j].s, buf, slcnt++);
413 
						} else if (verbose&32)
414 
						{	if (!not_printing)
415 
							printf("%s_%s%d:\n",
416 
								buf, spl[j].s, slcnt++);
417 
						}
418 
						if (i == unfolding)
419 
						{	is_accept++; /* move to next unfolding */
420 
						}
421 
					} else
422 
					{	nmatches++;
423 
					}
424 
					break;
425 
		}	}	}
426 
		if (j == 0 && nmatches == nclaims)	/* end-state */
427 
		{	if (!not_printing)
428 
			{	printf("%s%d:\n", spl[j].s, slcnt++);
429 
	}	}	}
430 
}
431 
 
432 
static int
433 
render_state(SQueue *q)
434 
{
435 
	if (!q || !q->state.succ)
436 
	{	if (verbose&64)
437 
		{	printf("	no exit\n");
438 
		}
439 
		return 0;
440 
	}
441 
 
442 
	check_special(q->state.combo); /* accept or end-state labels */
443 
 
444 
	dsts = (State_Stack *) 0;
445 
	push_dsts(q->state.combo);	/* to detect loops */
446 
 
447 
	if (!not_printing)
448 
	{	print_state_nm("", q->state.combo, "");	/* the name */
449 
		printf("_U%d:\n\tdo\n", unfolding);
450 
	}
451 
 
452 
	state_body(&(q->state), (Guard *) 0);
453 
 
454 
	if (!not_printing)
455 
	{	printf("\tod;\n");
456 
	}
457 
	pop_dsts();
458 
	return 1;
459 
}
460 
 
461 
static void
462 
explore_product(void)
463 
{	SQueue *q;
464 
 
465 
	/* all states are in the sd queue */
466 
 
467 
	q = retrieve_state(Ist);	/* retrieve from the sd q */
468 
	q->nxt = render;		/* put in render q */
469 
	render = q;
470 
	do {
471 
		q = render;
472 
		render = render->nxt;
473 
		q->nxt = 0;		/* remove from render q */
474 
 
475 
		if (verbose&64)
476 
		{	print_state_nm("explore: ", q->state.combo, "\n");
477 
		}
478 
 
479 
		not_printing = 1;
480 
		render_state(q);	/* may add new states */
481 
		not_printing = 0;
482 
 
483 
		if (lasthold)
484 
		{	lasthold->nxt = q;
485 
			lasthold = q;
486 
		} else
487 
		{	holding = lasthold = q;
488 
		}
489 
	} while (render);
490 
	assert(!dsts);
491 
 
492 
}
493 
 
494 
static void
495 
print_product(void)
496 
{	SQueue *q;
497 
	int cnt;
498 
 
499 
	if (unfolding == 0)
500 
	{	printf("never Product {\n");	/* name expected by iSpin */
501 
		q = find_state(Ist);	/* should find it in the holding q */
502 
		assert(q);
503 
		q->nxt = holding;	/* put it at the front */
504 
		holding = q;
505 
	}
506 
	render = holding;
507 
	holding = lasthold = 0;
508 
 
509 
	printf("/* ============= U%d ============= */\n", unfolding);
510 
	cnt = 0;
511 
	do {
512 
		q = render;
513 
		render = render->nxt;
514 
		q->nxt = 0;
515 
		if (verbose&64)
516 
		{	print_state_nm("print: ", q->state.combo, "\n");
517 
		}
518 
		cnt += render_state(q);
519 
 
520 
		if (lasthold)
521 
		{	lasthold->nxt = q;
522 
			lasthold = q;
523 
		} else
524 
		{	holding = lasthold = q;
525 
		}
526 
	} while (render);
527 
	assert(!dsts);
528 
 
529 
	if (cnt == 0)
530 
	{	printf("	0;\n");
531 
	}
532 
 
533 
	if (unfolding == nclaims-1)
534 
	{	printf("}\n");
535 
	}
536 
}
537 
 
538 
static void
539 
prune_dead(void)
540 
{	Succ_List *sl, *last;
541 
	SQueue *q;
542 
	int cnt;
543 
 
544 
	do {	cnt = 0;
545 
		for (q = sd; q; q = q->nxt)
546 
		{	/* if successor is deadend, remove it
547 
			 * unless it's a move to the end-state of the claim
548 
			 */
549 
			last = (Succ_List *) 0;
550 
			for (sl = q->state.succ; sl; last = sl, sl = sl->nxt)
551 
			{	if (!sl->s->state.succ)	/* no successor */
552 
				{	if (!last)
553 
					{	q->state.succ = sl->nxt;
554 
					} else
555 
					{	last->nxt = sl->nxt;
556 
					}
557 
					cnt++;
558 
		}	}	}
559 
	} while (cnt > 0);
560 
}
561 
 
562 
static void
563 
print_raw(void)
564 
{	int i, j, n;
565 
 
566 
	printf("#if 0\n");
567 
	for (n = 0; n < nclaims; n++)
568 
	{	printf("C%d:\n", n);
569 
		for (i = 0; i < nst; i++)
570 
		{	if (reached[n][i])
571 
			for (j = 0; j < nst; j++)
572 
			{	if (matrix[n][i][j])
573 
				{	if (reached[n][i] & 2) printf("+");
574 
					if (i == Ist[n]) printf("*");
575 
					printf("\t%d", i);
576 
					wrap_text(" -[", matrix[n][i][j]->n, "]->\t");
577 
					printf("%d\n", j);
578 
	}	}	}	}
579 
	printf("#endif\n\n");
580 
	fflush(stdout);
581 
}
582 
 
583 
void
584 
sync_product(void)
585 
{	ProcList *p;
586 
	Element *e;
587 
	int n, i;
588 
 
589 
	if (nclaims <= 1) return;
590 
 
591 
	(void) unlink("pan.pre");
592 
 
593 
	Ist  = (int *) emalloc(sizeof(int) * nclaims);
594 
	Nacc = (int *) emalloc(sizeof(int) * nclaims);
595 
	Nst  = (int *) emalloc(sizeof(int) * nclaims);
596 
	reached = (int **) emalloc(sizeof(int *) * nclaims);
597 
	Selfs   = (Element **) emalloc(sizeof(Element *) * nclaims);
598 
	matrix  = (Element ****) emalloc(sizeof(Element ***) * nclaims); /* claims */
599 
 
600 
	for (p = rdy, i = 0; p; p = p->nxt, i++)
601 
	{	if (p->b == N_CLAIM)
602 
		{	nst = max(p->s->maxel, nst);
603 
			Nacc[i] = claim_has_accept(p);
604 
	}	}
605 
 
606 
	for (n = 0; n < nclaims; n++)
607 
	{	reached[n] = (int *) emalloc(sizeof(int) * nst);
608 
		matrix[n] = (Element ***) emalloc(sizeof(Element **) * nst);	/* rows */
609 
		for (i = 0; i < nst; i++)					/* cols */
610 
		{	matrix[n][i] = (Element **) emalloc(sizeof(Element *) * nst);
611 
	}	}
612 
 
613 
	for (e = Al_El; e; e = e->Nxt)
614 
	{	e->status &= ~DONE;
615 
	}
616 
 
617 
	for (p = rdy, n=0; p; p = p->nxt, n++)
618 
	{	if (p->b == N_CLAIM)
619 
		{	/* fill in matrix[n] */
620 
			e = p->s->frst;
621 
			Ist[n] = huntele(e, e->status, -1)->seqno;
622 
 
623 
			reached[n][Ist[n]] = 1|2;
624 
			get_seq(n, p->s);
625 
	}	}
626 
 
627 
	if (verbose)	/* show only the input automata */
628 
	{	print_raw();
629 
	}
630 
 
631 
	gen_product();	/* create product automaton */
632 
}
633 
 
634 
static int
635 
nxt_trans(int n, int cs, int frst)
636 
{	int j;
637 
 
638 
	for (j = frst; j < nst; j++)
639 
	{	if (reached[n][cs]
640 
		&&  matrix[n][cs][j])
641 
		{	return j;
642 
	}	}
643 
	return -1;
644 
}
645 
 
646 
static void
647 
print_state_nm(char *p, int *s, char *a)
648 
{	int i;
649 
	printf("%sP", p);
650 
	for (i = 0; i < nclaims; i++)
651 
	{	printf("_%d", s[i]);
652 
	}
653 
	printf("%s", a);
654 
}
655 
 
656 
static void
657 
create_transition(OneState *s, SQueue *it)
658 
{	int n, from, upto;
659 
	int *F = s->combo;
660 
	int *T = it->state.combo;
661 
	Succ_List *sl;
662 
	Lextok *t;
663 
 
664 
	if (verbose&64)
665 
	{	print_state_nm("", F, " ");
666 
		print_state_nm("-> ", T, "\t");
667 
	}
668 
 
669 
	/* check if any of the claims is blocked */
670 
	/* which makes the state a dead-end */
671 
	for (n = 0; n < nclaims; n++)
672 
	{	from = F[n];
673 
		upto = T[n];
674 
		t = matrix[n][from][upto]->n;
675 
		if (verbose&64)
676 
		{	wrap_text("", t, " ");
677 
		}
678 
		if (t->ntyp == 'c'
679 
		&&  t->lft->ntyp == CONST)
680 
		{	if (t->lft->val == 0)	/* i.e., false */
681 
			{	goto done;
682 
	}	}	}
683 
 
684 
	sl = (Succ_List *) emalloc(sizeof(Succ_List));
685 
	sl->s = it;
686 
	sl->nxt = s->succ;
687 
	s->succ = sl;
688 
done:
689 
	if (verbose&64)
690 
	{	printf("\n");
691 
	}
692 
}
693 
 
694 
static SQueue *
695 
find_state(int *cs)
696 
{	SQueue *nq, *a = sq;
697 
	int i;
698 
 
699 
again:	/* check in nq, sq, and then in the render q */
700 
	for (nq = a; nq; nq = nq->nxt)
701 
	{	if (same_state(nq->state.combo, cs))
702 
		{	return nq;	/* found */
703 
	}	}
704 
	if (a == sq && sd)
705 
	{	a = sd;
706 
		goto again; /* check the other stack too */
707 
	} else if (a == sd && render)
708 
	{	a = render;
709 
		goto again;
710 
	}
711 
 
712 
	nq = (SQueue *) emalloc(sizeof(SQueue));
713 
	nq->state.combo = (int *) emalloc(nclaims * sizeof(int));
714 
	for (i = 0; i < nclaims; i++)
715 
	{	nq->state.combo[i] = cs[i];
716 
	}
717 
	nq->nxt = sq;	/* add to sq stack */
718 
	sq = nq;
719 
 
720 
	return nq;
721 
}
722 
 
723 
static SQueue *
724 
retrieve_state(int *s)
725 
{	SQueue *nq, *last = NULL;
726 
 
727 
	for (nq = sd; nq; last = nq, nq = nq->nxt)
728 
	{	if (same_state(nq->state.combo, s))
729 
		{	if (last)
730 
			{	last->nxt = nq->nxt;
731 
			} else
732 
			{	sd = nq;
733 
			}
734 
			return nq;	/* found */
735 
	}	}
736 
 
737 
	fatal("cannot happen: retrieve_state", 0);
738 
	return (SQueue *) 0;
739 
}
740 
 
741 
static void
742 
all_successors(int n, OneState *cur)
743 
{	int i, j = 0;
744 
 
745 
	if (n >= nclaims)
746 
	{	create_transition(cur, find_state(Nst));
747 
	} else
748 
	{	i = cur->combo[n];
749 
		for (;;)
750 
		{	j = nxt_trans(n, i, j);
751 
			if (j < 0) break;
752 
			Nst[n] = j;
753 
			all_successors(n+1, cur);
754 
			j++;
755 
	}	}
756 
}
757 
 
758 
static void
759 
gen_product(void)
760 
{	OneState *cur_st;
761 
	SQueue *q;
762 
 
763 
	find_state(Ist);	/* create initial state */
764 
 
765 
	while (sq)
766 
	{	if (in_stack(sq, sd))
767 
		{	sq = sq->nxt;
768 
			continue;
769 
		}
770 
		cur_st = &(sq->state);
771 
 
772 
		q = sq;
773 
		sq = sq->nxt;	/* delete from sq stack */
774 
		q->nxt = sd;	/* and move to done stack */
775 
		sd = q;
776 
 
777 
		all_successors(0, cur_st);
778 
	}
779 
	/* all states are in the sd queue now */
780 
	prune_dead();
781 
	explore_product();	/* check if added accept-self-loops are reachable */
782 
	prune_accept();
783 
 
784 
	if (verbose)
785 
	{	print_raw();
786 
	}
787 
 
788 
	/* PM: merge states with identical successor lists */
789 
 
790 
	/* all outgoing transitions from accept-states
791 
	   from claim n in copy n connect to states in copy (n+1)%nclaims
792 
	   only accept states from claim 0 in copy 0 are true accept states
793 
	   in the product
794 
 
795 
	   PM: what about claims that have no accept states (e.g., restrictions)
796 
	*/
797 
 
798 
	for (unfolding = 0; unfolding < nclaims; unfolding++)
799 
	{	print_product();
800 
	}
801 
}
802 
 
803 
static void
804 
t_record(int n, Element *e, Element *g)
805 
{	int from = e->seqno, upto = g?g->seqno:0;
806 
 
807 
	assert(from >= 0 && from < nst);
808 
	assert(upto >= 0 && upto < nst);
809 
 
810 
	matrix[n][from][upto] = e;
811 
	reached[n][upto] |= 1;
812 
}
813 
 
814 
static void
815 
get_sub(int n, Element *e)
816 
{
817 
	if (e->n->ntyp == D_STEP
818 
	||  e->n->ntyp == ATOMIC)
819 
	{	fatal("atomic or d_step in never claim product", 0);
820 
	}
821 
	/* NON_ATOMIC */
822 
	e->n->sl->this->last->nxt = e->nxt;
823 
	get_seq(n, e->n->sl->this);
824 
 
825 
	t_record(n, e, e->n->sl->this->frst);
826 
 
827 
}
828 
 
829 
static void
830 
set_el(int n, Element *e)
831 
{	Element *g;
832 
 
833 
	if (e->n->ntyp == '@')	/* change to self-loop */
834 
	{	e->n->ntyp = CONST;
835 
		e->n->val = 1;	/* true */
836 
		e->nxt = e;
837 
		g = e;
838 
		mk_accepting(n, e);
839 
	} else
840 
 
841 
	if (e->n->ntyp == GOTO)
842 
	{	g = get_lab(e->n, 1);
843 
		g = huntele(g, e->status, -1);
844 
	} else if (e->nxt)
845 
	{	g = huntele(e->nxt, e->status, -1);
846 
	} else
847 
	{	g = NULL;
848 
	}
849 
 
850 
	t_record(n, e, g);
851 
}
852 
 
853 
static void
854 
get_seq(int n, Sequence *s)
855 
{	SeqList *h;
856 
	Element *e;
857 
 
858 
	e = huntele(s->frst, s->frst->status, -1);
859 
	for ( ; e; e = e->nxt)
860 
	{	if (e->status & DONE)
861 
		{	goto checklast;
862 
		}
863 
		e->status |= DONE;
864 
 
865 
		if (e->n->ntyp == UNLESS)
866 
		{	fatal("unless stmnt in never claim product", 0);
867 
		}
868 
 
869 
		if (e->sub)	/* IF or DO */
870 
		{	Lextok *x = NULL;
871 
			Lextok *y = NULL;
872 
			Lextok *haselse = NULL;
873 
 
874 
			for (h = e->sub; h; h = h->nxt)
875 
			{	Lextok *t = h->this->frst->n;
876 
				if (t->ntyp == ELSE)
877 
				{	if (verbose&64) printf("else at line %d\n", t->ln);
878 
					haselse = t;
879 
					continue;
880 
				}
881 
				if (t->ntyp != 'c')
882 
				{	fatal("product, 'else' combined with non-condition", 0);
883 
				}
884 
 
885 
				if (t->lft->ntyp == CONST	/* true */
886 
				&&  t->lft->val == 1
887 
				&&  y == NULL)
888 
				{	y = nn(ZN, CONST, ZN, ZN);
889 
					y->val = 0;
890 
				} else
891 
				{	if (!x)
892 
						x = t;
893 
					else
894 
						x = nn(ZN, OR, x, t);
895 
					if (verbose&64)
896 
					{	wrap_text(" [", x, "]\n");
897 
			}	}	}
898 
			if (haselse)
899 
			{	if (!y)
900 
				{	y = nn(ZN, '!', x, ZN);
901 
				}
902 
				if (verbose&64)
903 
				{	wrap_text(" [else: ", y, "]\n");
904 
				}
905 
				haselse->ntyp = 'c';	/* replace else */
906 
				haselse->lft = y;
907 
			}
908 
 
909 
			for (h = e->sub; h; h = h->nxt)
910 
			{	t_record(n, e, h->this->frst);
911 
				get_seq(n, h->this);
912 
			}
913 
		} else
914 
		{	if (e->n->ntyp == ATOMIC
915 
			||  e->n->ntyp == D_STEP
916 
			||  e->n->ntyp == NON_ATOMIC)
917 
			{	get_sub(n, e);
918 
			} else
919 
			{	set_el(n, e);
920 
			}
921 
		}
922 
checklast:	if (e == s->last)
923 
			break;
924 
	}
925 
}