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