sys/src/cmd/spin/pangen7.c

   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 *rdy;
  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
  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
  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
 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
 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 *
 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
 182 pop_dsts(void)
 183 {
 184         assert(dsts != NULL);
 185         dsts = dsts->nxt;
 186 }
 187
 188 static void
 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
 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 {
 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 *
 283 locate_claim(int n)
 284 {       ProcList *p;
 285         int i;
 286
 287         for (p = rdy, 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
 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
 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
 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
 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 = rdy, 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
 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 = rdy, 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
 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
 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
 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
 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
 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
 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 = rdy, 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 = rdy, 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
 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
 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
 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 *
 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 *
 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
 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
 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
 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
 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
 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
 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 }