123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894895896897898899900901902903904905906907908909910911912913914915916917918919920921922923924925 |
- /***** spin: pangen7.c *****/
- /* Copyright (c) 1989-2003 by Lucent Technologies, Bell Laboratories. */
- /* All Rights Reserved. This software is for educational purposes only. */
- /* No guarantee whatsoever is expressed or implied by the distribution of */
- /* this code. Permission is given to distribute this code provided that */
- /* this introductory message is not removed and no monies are exchanged. */
- /* Software written by Gerard J. Holzmann. For tool documentation see: */
- /* http://spinroot.com/ */
- /* Send all bug-reports and/or questions to: bugs@spinroot.com */
- /* pangen7.c: Version 5.3.0 2010, synchronous product of never claims */
- #include <stdlib.h>
- #include "spin.h"
- #include "y.tab.h"
- #include <assert.h>
- #ifdef PC
- extern int unlink(const char *);
- #else
- #include <unistd.h>
- #endif
- extern ProcList *rdy;
- extern Element *Al_El;
- extern int nclaims, verbose, Strict;
- typedef struct Succ_List Succ_List;
- typedef struct SQueue SQueue;
- typedef struct OneState OneState;
- typedef struct State_Stack State_Stack;
- typedef struct Guard Guard;
- struct Succ_List {
- SQueue *s;
- Succ_List *nxt;
- };
- struct OneState {
- int *combo; /* the combination of claim states */
- Succ_List *succ; /* list of ptrs to immediate successor states */
- };
- struct SQueue {
- OneState state;
- SQueue *nxt;
- };
- struct State_Stack {
- int *n;
- State_Stack *nxt;
- };
- struct Guard {
- Lextok *t;
- Guard *nxt;
- };
- SQueue *sq, *sd, *render; /* states move from sq to sd to render to holding */
- SQueue *holding, *lasthold;
- State_Stack *dsts;
- int nst; /* max nr of states in claims */
- int *Ist; /* initial states */
- int *Nacc; /* number of accept states in claim */
- int *Nst; /* next states */
- int **reached; /* n claims x states */
- int unfolding; /* to make sure all accept states are reached */
- int is_accept; /* remember if the current state is accepting in any claim */
- int not_printing; /* set during explore_product */
- Element ****matrix; /* n x two-dimensional arrays state x state */
- Element **Selfs; /* self-loop states at end of claims */
- static void get_seq(int, Sequence *);
- static void set_el(int n, Element *e);
- static void gen_product(void);
- static void print_state_nm(char *, int *, char *);
- static SQueue *find_state(int *);
- static SQueue *retrieve_state(int *);
- static int
- same_state(int *a, int *b)
- { int i;
- for (i = 0; i < nclaims; i++)
- { if (a[i] != b[i])
- { return 0;
- } }
- return 1;
- }
- static int
- in_stack(SQueue *s, SQueue *in)
- { SQueue *q;
- for (q = in; q; q = q->nxt)
- { if (same_state(q->state.combo, s->state.combo))
- { return 1;
- } }
- return 0;
- }
- static void
- to_render(SQueue *s)
- { SQueue *a, *q, *last; /* find in sd/sq and move to render, if not already there */
- int n;
- for (n = 0; n < nclaims; n++)
- { reached[n][ s->state.combo[n] ] |= 2;
- }
- for (q = render; q; q = q->nxt)
- { if (same_state(q->state.combo, s->state.combo))
- { return;
- } }
- for (q = holding; q; q = q->nxt)
- { if (same_state(q->state.combo, s->state.combo))
- { return;
- } }
- a = sd;
- more:
- for (q = a, last = 0; q; last = q, q = q->nxt)
- { if (same_state(q->state.combo, s->state.combo))
- { if (!last)
- { if (a == sd)
- { sd = q->nxt;
- } else if (a == sq)
- { sq = q->nxt;
- } else
- { holding = q->nxt;
- }
- } else
- { last->nxt = q->nxt;
- }
- q->nxt = render;
- render = q;
- return;
- } }
- if (verbose)
- { print_state_nm("looking for: ", s->state.combo, "\n");
- }
- (void) find_state(s->state.combo); /* creates it in sq */
- if (a != sq)
- { a = sq;
- goto more;
- }
- fatal("cannot happen, to_render", 0);
- }
- static void
- wrap_text(char *pre, Lextok *t, char *post)
- {
- printf(pre);
- comment(stdout, t, 0);
- printf(post);
- }
- static State_Stack *
- push_dsts(int *n)
- { State_Stack *s;
- int i;
- for (s = dsts; s; s = s->nxt)
- { if (same_state(s->n, n))
- { if (verbose&64)
- { printf("\n");
- for (s = dsts; s; s = s->nxt)
- { print_state_nm("\t", s->n, "\n");
- }
- print_state_nm("\t", n, "\n");
- }
- return s;
- } }
- s = (State_Stack *) emalloc(sizeof(State_Stack));
- s->n = (int *) emalloc(nclaims * sizeof(int));
- for (i = 0; i < nclaims; i++)
- s->n[i] = n[i];
- s->nxt = dsts;
- dsts = s;
- return 0;
- }
- static void
- pop_dsts(void)
- {
- assert(dsts);
- dsts = dsts->nxt;
- }
- static void
- complete_transition(Succ_List *sl, Guard *g)
- { Guard *w;
- int cnt = 0;
- printf(" :: ");
- for (w = g; w; w = w->nxt)
- { if (w->t->ntyp == CONST
- && w->t->val == 1)
- { continue;
- } else if (w->t->ntyp == 'c'
- && w->t->lft->ntyp == CONST
- && w->t->lft->val == 1)
- { continue; /* 'true' */
- }
- if (cnt > 0)
- { printf(" && ");
- }
- wrap_text("", w->t, "");
- cnt++;
- }
- if (cnt == 0)
- { printf("true");
- }
- print_state_nm(" -> goto ", sl->s->state.combo, "");
- if (is_accept > 0)
- { printf("_U%d\n", (unfolding+1)%nclaims);
- } else
- { printf("_U%d\n", unfolding);
- }
- }
- static void
- state_body(OneState *s, Guard *guard)
- { Succ_List *sl;
- State_Stack *y;
- Guard *g;
- int i, once;
- for (sl = s->succ; sl; sl = sl->nxt)
- { once = 0;
- for (i = 0; i < nclaims; i++)
- { Element *e;
- e = matrix[i][s->combo[i]][sl->s->state.combo[i]];
- /* if one of the claims has a DO or IF move
- then pull its target state forward, once
- */
- if (!e
- || e->n->ntyp == NON_ATOMIC
- || e->n->ntyp == DO
- || e->n->ntyp == IF)
- { s = &(sl->s->state);
- y = push_dsts(s->combo);
- if (!y)
- { if (once++ == 0)
- { assert(s->succ);
- state_body(s, guard);
- }
- pop_dsts();
- } else if (!y->nxt) /* self-loop transition */
- { if (!not_printing) printf(" /* self-loop */\n");
- } else
- { /* non_fatal("loop in state body", 0); ** maybe ok */
- }
- continue;
- } else
- { g = (Guard *) emalloc(sizeof(Guard));
- g->t = e->n;
- g->nxt = guard;
- guard = g;
- } }
- if (guard && !once)
- { if (!not_printing) complete_transition(sl, guard);
- to_render(sl->s);
- } }
- }
- static struct X {
- char *s; int n;
- } spl[] = {
- {"end", 3 },
- {"accept", 6 },
- {0, 0 },
- };
- static int slcnt;
- extern Label *labtab;
- static ProcList *
- locate_claim(int n)
- { ProcList *p;
- int i;
- for (p = rdy, i = 0; p; p = p->nxt, i++) /* find claim name */
- { if (i == n)
- { break;
- } }
- assert(p && p->b == N_CLAIM);
- return p;
- }
- static void
- elim_lab(Element *e)
- { Label *l, *lst;
- for (l = labtab, lst = NULL; l; lst = l, l = l->nxt)
- { if (l->e == e)
- { if (lst)
- { lst->nxt = l->nxt;
- } else
- { labtab = l->nxt;
- }
- break;
- } }
- }
- static int
- claim_has_accept(ProcList *p)
- { Label *l;
- for (l = labtab; l; l = l->nxt)
- { if (strcmp(l->c->name, p->n->name) == 0
- && strncmp(l->s->name, "accept", 6) == 0)
- { return 1;
- } }
- return 0;
- }
- static void
- prune_accept(void)
- { int n;
- for (n = 0; n < nclaims; n++)
- { if ((reached[n][Selfs[n]->seqno] & 2) == 0)
- { if (verbose)
- { printf("claim %d: selfloop not reachable\n", n);
- }
- elim_lab(Selfs[n]);
- Nacc[n] = claim_has_accept(locate_claim(n));
- } }
- }
- static void
- mk_accepting(int n, Element *e)
- { ProcList *p;
- Label *l;
- int i;
- assert(!Selfs[n]);
- Selfs[n] = e;
- l = (Label *) emalloc(sizeof(Label));
- l->s = (Symbol *) emalloc(sizeof(Symbol));
- l->s->name = "accept00";
- l->c = (Symbol *) emalloc(sizeof(Symbol));
- l->uiid = 0; /* this is not in an inline */
- for (p = rdy, i = 0; p; p = p->nxt, i++) /* find claim name */
- { if (i == n)
- { l->c->name = p->n->name;
- break;
- } }
- assert(p && p->b == N_CLAIM);
- Nacc[n] = 1;
- l->e = e;
- l->nxt = labtab;
- labtab = l;
- }
- static void
- check_special(int *nrs)
- { ProcList *p;
- Label *l;
- int i, j, nmatches;
- int any_accepts = 0;
- for (i = 0; i < nclaims; i++)
- { any_accepts += Nacc[i];
- }
- is_accept = 0;
- for (j = 0; spl[j].n; j++) /* 2 special label prefixes */
- { nmatches = 0;
- for (p = rdy, i = 0; p; p = p->nxt, i++) /* check each claim */
- { if (p->b != N_CLAIM)
- { continue;
- }
- /* claim i in state nrs[i], type p->tn, name p->n->name
- * either the state has an accept label, or the claim has none,
- * so that all its states should be considered accepting
- * --- but only if other claims do have accept states!
- */
- if (Strict == 0 && j == 1 && Nacc[i] == 0 && any_accepts > 0)
- { if ((verbose&32) && i == unfolding)
- { printf(" /* claim %d pseudo-accept */\n", i);
- }
- goto is_accepting;
- }
- for (l = labtab; l; l = l->nxt) /* check its labels */
- { if (strcmp(l->c->name, p->n->name) == 0 /* right claim */
- && l->e->seqno == nrs[i] /* right state */
- && strncmp(l->s->name, spl[j].s, spl[j].n) == 0)
- { if (j == 1) /* accept state */
- { char buf[32];
- is_accepting: if (strchr(p->n->name, ':'))
- { sprintf(buf, "N%d", i);
- } else
- { strcpy(buf, p->n->name);
- }
- if (unfolding == 0 && i == 0)
- { if (!not_printing)
- printf("%s_%s_%d:\n", /* true accept */
- spl[j].s, buf, slcnt++);
- } else if (verbose&32)
- { if (!not_printing)
- printf("%s_%s%d:\n",
- buf, spl[j].s, slcnt++);
- }
- if (i == unfolding)
- { is_accept++; /* move to next unfolding */
- }
- } else
- { nmatches++;
- }
- break;
- } } }
- if (j == 0 && nmatches == nclaims) /* end-state */
- { if (!not_printing)
- { printf("%s%d:\n", spl[j].s, slcnt++);
- } } }
- }
- static int
- render_state(SQueue *q)
- {
- if (!q || !q->state.succ)
- { if (verbose&64)
- { printf(" no exit\n");
- }
- return 0;
- }
- check_special(q->state.combo); /* accept or end-state labels */
- dsts = (State_Stack *) 0;
- push_dsts(q->state.combo); /* to detect loops */
- if (!not_printing)
- { print_state_nm("", q->state.combo, ""); /* the name */
- printf("_U%d:\n\tdo\n", unfolding);
- }
- state_body(&(q->state), (Guard *) 0);
- if (!not_printing)
- { printf("\tod;\n");
- }
- pop_dsts();
- return 1;
- }
- static void
- explore_product(void)
- { SQueue *q;
- /* all states are in the sd queue */
- q = retrieve_state(Ist); /* retrieve from the sd q */
- q->nxt = render; /* put in render q */
- render = q;
- do {
- q = render;
- render = render->nxt;
- q->nxt = 0; /* remove from render q */
- if (verbose&64)
- { print_state_nm("explore: ", q->state.combo, "\n");
- }
- not_printing = 1;
- render_state(q); /* may add new states */
- not_printing = 0;
- if (lasthold)
- { lasthold->nxt = q;
- lasthold = q;
- } else
- { holding = lasthold = q;
- }
- } while (render);
- assert(!dsts);
-
- }
- static void
- print_product(void)
- { SQueue *q;
- int cnt;
- if (unfolding == 0)
- { printf("never Product {\n"); /* name expected by iSpin */
- q = find_state(Ist); /* should find it in the holding q */
- assert(q);
- q->nxt = holding; /* put it at the front */
- holding = q;
- }
- render = holding;
- holding = lasthold = 0;
- printf("/* ============= U%d ============= */\n", unfolding);
- cnt = 0;
- do {
- q = render;
- render = render->nxt;
- q->nxt = 0;
- if (verbose&64)
- { print_state_nm("print: ", q->state.combo, "\n");
- }
- cnt += render_state(q);
- if (lasthold)
- { lasthold->nxt = q;
- lasthold = q;
- } else
- { holding = lasthold = q;
- }
- } while (render);
- assert(!dsts);
- if (cnt == 0)
- { printf(" 0;\n");
- }
- if (unfolding == nclaims-1)
- { printf("}\n");
- }
- }
- static void
- prune_dead(void)
- { Succ_List *sl, *last;
- SQueue *q;
- int cnt;
- do { cnt = 0;
- for (q = sd; q; q = q->nxt)
- { /* if successor is deadend, remove it
- * unless it's a move to the end-state of the claim
- */
- last = (Succ_List *) 0;
- for (sl = q->state.succ; sl; last = sl, sl = sl->nxt)
- { if (!sl->s->state.succ) /* no successor */
- { if (!last)
- { q->state.succ = sl->nxt;
- } else
- { last->nxt = sl->nxt;
- }
- cnt++;
- } } }
- } while (cnt > 0);
- }
- static void
- print_raw(void)
- { int i, j, n;
- printf("#if 0\n");
- for (n = 0; n < nclaims; n++)
- { printf("C%d:\n", n);
- for (i = 0; i < nst; i++)
- { if (reached[n][i])
- for (j = 0; j < nst; j++)
- { if (matrix[n][i][j])
- { if (reached[n][i] & 2) printf("+");
- if (i == Ist[n]) printf("*");
- printf("\t%d", i);
- wrap_text(" -[", matrix[n][i][j]->n, "]->\t");
- printf("%d\n", j);
- } } } }
- printf("#endif\n\n");
- fflush(stdout);
- }
- void
- sync_product(void)
- { ProcList *p;
- Element *e;
- int n, i;
- if (nclaims <= 1) return;
- (void) unlink("pan.pre");
- Ist = (int *) emalloc(sizeof(int) * nclaims);
- Nacc = (int *) emalloc(sizeof(int) * nclaims);
- Nst = (int *) emalloc(sizeof(int) * nclaims);
- reached = (int **) emalloc(sizeof(int *) * nclaims);
- Selfs = (Element **) emalloc(sizeof(Element *) * nclaims);
- matrix = (Element ****) emalloc(sizeof(Element ***) * nclaims); /* claims */
- for (p = rdy, i = 0; p; p = p->nxt, i++)
- { if (p->b == N_CLAIM)
- { nst = max(p->s->maxel, nst);
- Nacc[i] = claim_has_accept(p);
- } }
- for (n = 0; n < nclaims; n++)
- { reached[n] = (int *) emalloc(sizeof(int) * nst);
- matrix[n] = (Element ***) emalloc(sizeof(Element **) * nst); /* rows */
- for (i = 0; i < nst; i++) /* cols */
- { matrix[n][i] = (Element **) emalloc(sizeof(Element *) * nst);
- } }
- for (e = Al_El; e; e = e->Nxt)
- { e->status &= ~DONE;
- }
- for (p = rdy, n=0; p; p = p->nxt, n++)
- { if (p->b == N_CLAIM)
- { /* fill in matrix[n] */
- e = p->s->frst;
- Ist[n] = huntele(e, e->status, -1)->seqno;
- reached[n][Ist[n]] = 1|2;
- get_seq(n, p->s);
- } }
- if (verbose) /* show only the input automata */
- { print_raw();
- }
- gen_product(); /* create product automaton */
- }
- static int
- nxt_trans(int n, int cs, int frst)
- { int j;
- for (j = frst; j < nst; j++)
- { if (reached[n][cs]
- && matrix[n][cs][j])
- { return j;
- } }
- return -1;
- }
- static void
- print_state_nm(char *p, int *s, char *a)
- { int i;
- printf("%sP", p);
- for (i = 0; i < nclaims; i++)
- { printf("_%d", s[i]);
- }
- printf("%s", a);
- }
- static void
- create_transition(OneState *s, SQueue *it)
- { int n, from, upto;
- int *F = s->combo;
- int *T = it->state.combo;
- Succ_List *sl;
- Lextok *t;
- if (verbose&64)
- { print_state_nm("", F, " ");
- print_state_nm("-> ", T, "\t");
- }
- /* check if any of the claims is blocked */
- /* which makes the state a dead-end */
- for (n = 0; n < nclaims; n++)
- { from = F[n];
- upto = T[n];
- t = matrix[n][from][upto]->n;
- if (verbose&64)
- { wrap_text("", t, " ");
- }
- if (t->ntyp == 'c'
- && t->lft->ntyp == CONST)
- { if (t->lft->val == 0) /* i.e., false */
- { goto done;
- } } }
- sl = (Succ_List *) emalloc(sizeof(Succ_List));
- sl->s = it;
- sl->nxt = s->succ;
- s->succ = sl;
- done:
- if (verbose&64)
- { printf("\n");
- }
- }
- static SQueue *
- find_state(int *cs)
- { SQueue *nq, *a = sq;
- int i;
- again: /* check in nq, sq, and then in the render q */
- for (nq = a; nq; nq = nq->nxt)
- { if (same_state(nq->state.combo, cs))
- { return nq; /* found */
- } }
- if (a == sq && sd)
- { a = sd;
- goto again; /* check the other stack too */
- } else if (a == sd && render)
- { a = render;
- goto again;
- }
- nq = (SQueue *) emalloc(sizeof(SQueue));
- nq->state.combo = (int *) emalloc(nclaims * sizeof(int));
- for (i = 0; i < nclaims; i++)
- { nq->state.combo[i] = cs[i];
- }
- nq->nxt = sq; /* add to sq stack */
- sq = nq;
- return nq;
- }
- static SQueue *
- retrieve_state(int *s)
- { SQueue *nq, *last = NULL;
- for (nq = sd; nq; last = nq, nq = nq->nxt)
- { if (same_state(nq->state.combo, s))
- { if (last)
- { last->nxt = nq->nxt;
- } else
- { sd = nq;
- }
- return nq; /* found */
- } }
- fatal("cannot happen: retrieve_state", 0);
- return (SQueue *) 0;
- }
- static void
- all_successors(int n, OneState *cur)
- { int i, j = 0;
- if (n >= nclaims)
- { create_transition(cur, find_state(Nst));
- } else
- { i = cur->combo[n];
- for (;;)
- { j = nxt_trans(n, i, j);
- if (j < 0) break;
- Nst[n] = j;
- all_successors(n+1, cur);
- j++;
- } }
- }
- static void
- gen_product(void)
- { OneState *cur_st;
- SQueue *q;
- find_state(Ist); /* create initial state */
- while (sq)
- { if (in_stack(sq, sd))
- { sq = sq->nxt;
- continue;
- }
- cur_st = &(sq->state);
- q = sq;
- sq = sq->nxt; /* delete from sq stack */
- q->nxt = sd; /* and move to done stack */
- sd = q;
- all_successors(0, cur_st);
- }
- /* all states are in the sd queue now */
- prune_dead();
- explore_product(); /* check if added accept-self-loops are reachable */
- prune_accept();
- if (verbose)
- { print_raw();
- }
- /* PM: merge states with identical successor lists */
- /* all outgoing transitions from accept-states
- from claim n in copy n connect to states in copy (n+1)%nclaims
- only accept states from claim 0 in copy 0 are true accept states
- in the product
- PM: what about claims that have no accept states (e.g., restrictions)
- */
- for (unfolding = 0; unfolding < nclaims; unfolding++)
- { print_product();
- }
- }
- static void
- t_record(int n, Element *e, Element *g)
- { int from = e->seqno, upto = g?g->seqno:0;
- assert(from >= 0 && from < nst);
- assert(upto >= 0 && upto < nst);
- matrix[n][from][upto] = e;
- reached[n][upto] |= 1;
- }
- static void
- get_sub(int n, Element *e)
- {
- if (e->n->ntyp == D_STEP
- || e->n->ntyp == ATOMIC)
- { fatal("atomic or d_step in never claim product", 0);
- }
- /* NON_ATOMIC */
- e->n->sl->this->last->nxt = e->nxt;
- get_seq(n, e->n->sl->this);
- t_record(n, e, e->n->sl->this->frst);
- }
- static void
- set_el(int n, Element *e)
- { Element *g;
- if (e->n->ntyp == '@') /* change to self-loop */
- { e->n->ntyp = CONST;
- e->n->val = 1; /* true */
- e->nxt = e;
- g = e;
- mk_accepting(n, e);
- } else
- if (e->n->ntyp == GOTO)
- { g = get_lab(e->n, 1);
- g = huntele(g, e->status, -1);
- } else if (e->nxt)
- { g = huntele(e->nxt, e->status, -1);
- } else
- { g = NULL;
- }
- t_record(n, e, g);
- }
- static void
- get_seq(int n, Sequence *s)
- { SeqList *h;
- Element *e;
- e = huntele(s->frst, s->frst->status, -1);
- for ( ; e; e = e->nxt)
- { if (e->status & DONE)
- { goto checklast;
- }
- e->status |= DONE;
- if (e->n->ntyp == UNLESS)
- { fatal("unless stmnt in never claim product", 0);
- }
- if (e->sub) /* IF or DO */
- { Lextok *x = NULL;
- Lextok *y = NULL;
- Lextok *haselse = NULL;
- for (h = e->sub; h; h = h->nxt)
- { Lextok *t = h->this->frst->n;
- if (t->ntyp == ELSE)
- { if (verbose&64) printf("else at line %d\n", t->ln);
- haselse = t;
- continue;
- }
- if (t->ntyp != 'c')
- { fatal("product, 'else' combined with non-condition", 0);
- }
- if (t->lft->ntyp == CONST /* true */
- && t->lft->val == 1
- && y == NULL)
- { y = nn(ZN, CONST, ZN, ZN);
- y->val = 0;
- } else
- { if (!x)
- x = t;
- else
- x = nn(ZN, OR, x, t);
- if (verbose&64)
- { wrap_text(" [", x, "]\n");
- } } }
- if (haselse)
- { if (!y)
- { y = nn(ZN, '!', x, ZN);
- }
- if (verbose&64)
- { wrap_text(" [else: ", y, "]\n");
- }
- haselse->ntyp = 'c'; /* replace else */
- haselse->lft = y;
- }
- for (h = e->sub; h; h = h->nxt)
- { t_record(n, e, h->this->frst);
- get_seq(n, h->this);
- }
- } else
- { if (e->n->ntyp == ATOMIC
- || e->n->ntyp == D_STEP
- || e->n->ntyp == NON_ATOMIC)
- { get_sub(n, e);
- } else
- { set_el(n, e);
- }
- }
- checklast: if (e == s->last)
- break;
- }
- }
|