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
same_state(int * a,int * b)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
in_stack(SQueue * s,SQueue * in)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
to_render(SQueue * s)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
wrap_text(char * pre,Lextok * t,char * post)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 *
push_dsts(int * n)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
pop_dsts(void)186 pop_dsts(void)
187 {
188 assert(dsts);
189 dsts = dsts->nxt;
190 }
191
192 static void
complete_transition(Succ_List * sl,Guard * g)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
state_body(OneState * s,Guard * guard)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 *
locate_claim(int n)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
elim_lab(Element * e)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
claim_has_accept(ProcList * p)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
prune_accept(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
mk_accepting(int n,Element * e)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
check_special(int * nrs)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
render_state(SQueue * q)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
explore_product(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
print_product(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
prune_dead(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
print_raw(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
sync_product(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
nxt_trans(int n,int cs,int frst)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
print_state_nm(char * p,int * s,char * a)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
create_transition(OneState * s,SQueue * it)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 *
find_state(int * cs)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 *
retrieve_state(int * s)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
all_successors(int n,OneState * cur)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
gen_product(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
t_record(int n,Element * e,Element * g)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
get_sub(int n,Element * e)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
set_el(int n,Element * e)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
get_seq(int n,Sequence * s)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 }
926