sys/src/cmd/spin/tl_buchi.c

   1 /***** tl_spin: tl_buchi.c *****/
   2
   3 /* Copyright (c) 1995-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
  12 /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
  13 /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.   */
  14
  15 #include "tl.h"
  16
  17 extern int tl_verbose, tl_clutter, Total, Max_Red;
  18
  19 FILE    *tl_out;        /* if standalone: = stdout; */
  20
  21 typedef struct Transition {
  22         Symbol *name;
  23         Node *cond;
  24         int redundant, merged, marked;
  25         struct Transition *nxt;
  26 } Transition;
  27
  28 typedef struct State {
  29         Symbol  *name;
  30         Transition *trans;
  31         Graph   *colors;
  32         unsigned char redundant;
  33         unsigned char accepting;
  34         unsigned char reachable;
  35         struct State *nxt;
  36 } State;
  37
  38 static State *never = (State *) 0;
  39 static int hitsall;
  40
  41 static int
  42 sametrans(Transition *s, Transition *t)
  43 {
  44         if (strcmp(s->name->name, t->name->name) != 0)
  45                 return 0;
  46         return isequal(s->cond, t->cond);
  47 }
  48
  49 static Node *
  50 Prune(Node *p)
  51 {
  52         if (p)
  53         switch (p->ntyp) {
  54         case PREDICATE:
  55         case NOT:
  56         case FALSE:
  57         case TRUE:
  58 #ifdef NXT
  59         case NEXT:
  60 #endif
  61                 return p;
  62         case OR:
  63                 p->lft = Prune(p->lft);
  64                 if (!p->lft)
  65                 {       releasenode(1, p->rgt);
  66                         return ZN;
  67                 }
  68                 p->rgt = Prune(p->rgt);
  69                 if (!p->rgt)
  70                 {       releasenode(1, p->lft);
  71                         return ZN;
  72                 }
  73                 return p;
  74         case AND:
  75                 p->lft = Prune(p->lft);
  76                 if (!p->lft)
  77                         return Prune(p->rgt);
  78                 p->rgt = Prune(p->rgt);
  79                 if (!p->rgt)
  80                         return p->lft;
  81                 return p;
  82         }
  83         releasenode(1, p);
  84         return ZN;
  85 }
  86
  87 static State *
  88 findstate(char *nm)
  89 {       State *b;
  90         for (b = never; b; b = b->nxt)
  91                 if (!strcmp(b->name->name, nm))
  92                         return b;
  93         if (strcmp(nm, "accept_all"))
  94         {       if (strncmp(nm, "accept", 6))
  95                 {       int i; char altnm[64];
  96                         for (i = 0; i < 64; i++)
  97                                 if (nm[i] == '_')
  98                                         break;
  99                         if (i >= 64)
 100                                 Fatal("name too long %s", nm);
 101                         sprintf(altnm, "accept%s", &nm[i]);
 102                         return findstate(altnm);
 103                 }
 104         /*      Fatal("buchi: no state %s", nm); */
 105         }
 106         return (State *) 0;
 107 }
 108
 109 static void
 110 Dfs(State *b)
 111 {       Transition *t;
 112
 113         if (!b || b->reachable) return;
 114         b->reachable = 1;
 115
 116         if (b->redundant)
 117                 printf("/* redundant state %s */\n",
 118                         b->name->name);
 119         for (t = b->trans; t; t = t->nxt)
 120         {       if (!t->redundant)
 121                 {       Dfs(findstate(t->name->name));
 122                         if (!hitsall
 123                         &&  strcmp(t->name->name, "accept_all") == 0)
 124                                 hitsall = 1;
 125                 }
 126         }
 127 }
 128
 129 void
 130 retarget(char *from, char *to)
 131 {       State *b;
 132         Transition *t;
 133         Symbol *To = tl_lookup(to);
 134
 135         if (tl_verbose) printf("replace %s with %s\n", from, to);
 136
 137         for (b = never; b; b = b->nxt)
 138         {       if (!strcmp(b->name->name, from))
 139                         b->redundant = 1;
 140                 else
 141                 for (t = b->trans; t; t = t->nxt)
 142                 {       if (!strcmp(t->name->name, from))
 143                                 t->name = To;
 144         }       }
 145 }
 146
 147 #ifdef NXT
 148 static Node *
 149 nonxt(Node *n)
 150 {
 151         switch (n->ntyp) {
 152         case U_OPER:
 153         case V_OPER:
 154         case NEXT:
 155                 return ZN;
 156         case OR:
 157                 n->lft = nonxt(n->lft);
 158                 n->rgt = nonxt(n->rgt);
 159                 if (!n->lft || !n->rgt)
 160                         return True;
 161                 return n;
 162         case AND:
 163                 n->lft = nonxt(n->lft);
 164                 n->rgt = nonxt(n->rgt);
 165                 if (!n->lft)
 166                 {       if (!n->rgt)
 167                                 n = ZN;
 168                         else
 169                                 n = n->rgt;
 170                 } else if (!n->rgt)
 171                         n = n->lft;
 172                 return n;
 173         }
 174         return n;
 175 }
 176 #endif
 177
 178 static Node *
 179 combination(Node *s, Node *t)
 180 {       Node *nc;
 181 #ifdef NXT
 182         Node *a = nonxt(s);
 183         Node *b = nonxt(t);
 184
 185         if (tl_verbose)
 186         {       printf("\tnonxtA: "); dump(a);
 187                 printf("\n\tnonxtB: "); dump(b);
 188                 printf("\n");
 189         }
 190         /* if there's only a X(f), its equivalent to true */
 191         if (!a || !b)
 192                 nc = True;
 193         else
 194                 nc = tl_nn(OR, a, b);
 195 #else
 196         nc = tl_nn(OR, s, t);
 197 #endif
 198         if (tl_verbose)
 199         {       printf("\tcombo: "); dump(nc);
 200                 printf("\n");
 201         }
 202         return nc;
 203 }
 204
 205 Node *
 206 unclutter(Node *n, char *snm)
 207 {       Node *t, *s, *v, *u;
 208         Symbol *w;
 209
 210         /* check only simple cases like !q && q */
 211         for (t = n; t; t = t->rgt)
 212         {       if (t->rgt)
 213                 {       if (t->ntyp != AND || !t->lft)
 214                                 return n;
 215                         if (t->lft->ntyp != PREDICATE
 216 #ifdef NXT
 217                         &&  t->lft->ntyp != NEXT
 218 #endif
 219                         &&  t->lft->ntyp != NOT)
 220                                 return n;
 221                 } else
 222                 {       if (t->ntyp != PREDICATE
 223 #ifdef NXT
 224                         &&  t->ntyp != NEXT
 225 #endif
 226                         &&  t->ntyp != NOT)
 227                                 return n;
 228                 }
 229         }
 230
 231         for (t = n; t; t = t->rgt)
 232         {       if (t->rgt)
 233                         v = t->lft;
 234                 else
 235                         v = t;
 236                 if (v->ntyp == NOT
 237                 &&  v->lft->ntyp == PREDICATE)
 238                 {       w = v->lft->sym;
 239                         for (s = n; s; s = s->rgt)
 240                         {       if (s == t) continue;
 241                                 if (s->rgt)
 242                                         u = s->lft;
 243                                 else
 244                                         u = s;
 245                                 if (u->ntyp == PREDICATE
 246                                 &&  strcmp(u->sym->name, w->name) == 0)
 247                                 {       if (tl_verbose)
 248                                         {       printf("BINGO %s:\t", snm);
 249                                                 dump(n);
 250                                                 printf("\n");
 251                                         }
 252                                         return False;
 253                                 }
 254                         }
 255         }       }
 256         return n;
 257 }
 258
 259 static void
 260 clutter(void)
 261 {       State *p;
 262         Transition *s;
 263
 264         for (p = never; p; p = p->nxt)
 265         for (s = p->trans; s; s = s->nxt)
 266         {       s->cond = unclutter(s->cond, p->name->name);
 267                 if (s->cond
 268                 &&  s->cond->ntyp == FALSE)
 269                 {       if (s != p->trans
 270                         ||  s->nxt)
 271                                 s->redundant = 1;
 272                 }
 273         }
 274 }
 275
 276 static void
 277 showtrans(State *a)
 278 {       Transition *s;
 279
 280         for (s = a->trans; s; s = s->nxt)
 281         {       printf("%s ", s->name?s->name->name:"-");
 282                 dump(s->cond);
 283                 printf(" %d %d %d\n", s->redundant, s->merged, s->marked);
 284         }
 285 }
 286
 287 static int
 288 mergetrans(void)
 289 {       State *b;
 290         Transition *s, *t;
 291         Node *nc; int cnt = 0;
 292
 293         for (b = never; b; b = b->nxt)
 294         {       if (!b->reachable) continue;
 295
 296                 for (s = b->trans; s; s = s->nxt)
 297                 {       if (s->redundant) continue;
 298
 299                         for (t = s->nxt; t; t = t->nxt)
 300                         if (!t->redundant
 301                         &&  !strcmp(s->name->name, t->name->name))
 302                         {       if (tl_verbose)
 303                                 {       printf("===\nstate %s, trans to %s redundant\n",
 304                                         b->name->name, s->name->name);
 305                                         showtrans(b);
 306                                         printf(" conditions ");
 307                                         dump(s->cond); printf(" <-> ");
 308                                         dump(t->cond); printf("\n");
 309                                 }
 310
 311                                 if (!s->cond) /* same as T */
 312                                 {       releasenode(1, t->cond); /* T or t */
 313                                         nc = True;
 314                                 } else if (!t->cond)
 315                                 {       releasenode(1, s->cond);
 316                                         nc = True;
 317                                 } else
 318                                 {       nc = combination(s->cond, t->cond);
 319                                 }
 320                                 t->cond = rewrite(nc);
 321                                 t->merged = 1;
 322                                 s->redundant = 1;
 323                                 cnt++;
 324                                 break;
 325         }       }       }
 326         return cnt;
 327 }
 328
 329 static int
 330 all_trans_match(State *a, State *b)
 331 {       Transition *s, *t;
 332         int found, result = 0;
 333
 334         if (a->accepting != b->accepting)
 335                 goto done;
 336
 337         for (s = a->trans; s; s = s->nxt)
 338         {       if (s->redundant) continue;
 339                 found = 0;
 340                 for (t = b->trans; t; t = t->nxt)
 341                 {       if (t->redundant) continue;
 342                         if (sametrans(s, t))
 343                         {       found = 1;
 344                                 t->marked = 1;
 345                                 break;
 346                 }       }
 347                 if (!found)
 348                         goto done;
 349         }
 350         for (s = b->trans; s; s = s->nxt)
 351         {       if (s->redundant || s->marked) continue;
 352                 found = 0;
 353                 for (t = a->trans; t; t = t->nxt)
 354                 {       if (t->redundant) continue;
 355                         if (sametrans(s, t))
 356                         {       found = 1;
 357                                 break;
 358                 }       }
 359                 if (!found)
 360                         goto done;
 361         }
 362         result = 1;
 363 done:
 364         for (s = b->trans; s; s = s->nxt)
 365                 s->marked = 0;
 366         return result;
 367 }
 368
 369 #ifndef NO_OPT
 370 #define BUCKY
 371 #endif
 372
 373 #ifdef BUCKY
 374 static int
 375 all_bucky(State *a, State *b)
 376 {       Transition *s, *t;
 377         int found, result = 0;
 378
 379         for (s = a->trans; s; s = s->nxt)
 380         {       if (s->redundant) continue;
 381                 found = 0;
 382                 for (t = b->trans; t; t = t->nxt)
 383                 {       if (t->redundant) continue;
 384
 385                         if (isequal(s->cond, t->cond))
 386                         {       if (strcmp(s->name->name, b->name->name) == 0
 387                                 &&  strcmp(t->name->name, a->name->name) == 0)
 388                                 {       found = 1;      /* they point to each other */
 389                                         t->marked = 1;
 390                                         break;
 391                                 }
 392                                 if (strcmp(s->name->name, t->name->name) == 0
 393                                 &&  strcmp(s->name->name, "accept_all") == 0)
 394                                 {       found = 1;
 395                                         t->marked = 1;
 396                                         break;
 397                                 /* same exit from which there is no return */
 398                                 }
 399                         }
 400                 }
 401                 if (!found)
 402                         goto done;
 403         }
 404         for (s = b->trans; s; s = s->nxt)
 405         {       if (s->redundant || s->marked) continue;
 406                 found = 0;
 407                 for (t = a->trans; t; t = t->nxt)
 408                 {       if (t->redundant) continue;
 409
 410                         if (isequal(s->cond, t->cond))
 411                         {       if (strcmp(s->name->name, a->name->name) == 0
 412                                 &&  strcmp(t->name->name, b->name->name) == 0)
 413                                 {       found = 1;
 414                                         t->marked = 1;
 415                                         break;
 416                                 }
 417                                 if (strcmp(s->name->name, t->name->name) == 0
 418                                 &&  strcmp(s->name->name, "accept_all") == 0)
 419                                 {       found = 1;
 420                                         t->marked = 1;
 421                                         break;
 422                                 }
 423                         }
 424                 }
 425                 if (!found)
 426                         goto done;
 427         }
 428         result = 1;
 429 done:
 430         for (s = b->trans; s; s = s->nxt)
 431                 s->marked = 0;
 432         return result;
 433 }
 434
 435 static int
 436 buckyballs(void)
 437 {       State *a, *b, *c, *d;
 438         int m, cnt=0;
 439
 440         do {
 441                 m = 0; cnt++;
 442                 for (a = never; a; a = a->nxt)
 443                 {       if (!a->reachable) continue;
 444
 445                         if (a->redundant) continue;
 446
 447                         for (b = a->nxt; b; b = b->nxt)
 448                         {       if (!b->reachable) continue;
 449
 450                                 if (b->redundant) continue;
 451
 452                                 if (all_bucky(a, b))
 453                                 {       m++;
 454                                         if (tl_verbose)
 455                                         {       printf("%s bucky match %s\n",
 456                                                 a->name->name, b->name->name);
 457                                         }
 458
 459                                         if (a->accepting && !b->accepting)
 460                                         {       if (strcmp(b->name->name, "T0_init") == 0)
 461                                                 {       c = a; d = b;
 462                                                         b->accepting = 1;
 463                                                 } else
 464                                                 {       c = b; d = a;
 465                                                 }
 466                                         } else
 467                                         {       c = a; d = b;
 468                                         }
 469
 470                                         retarget(c->name->name, d->name->name);
 471                                         if (!strncmp(c->name->name, "accept", 6)
 472                                         &&  Max_Red == 0)
 473                                         {       char buf[64];
 474                                                 sprintf(buf, "T0%s", &(c->name->name[6]));
 475                                                 retarget(buf, d->name->name);
 476                                         }
 477                                         break;
 478                                 }
 479                 }       }
 480         } while (m && cnt < 10);
 481         return cnt-1;
 482 }
 483 #endif
 484
 485 static int
 486 mergestates(int v)
 487 {       State *a, *b;
 488         int m, cnt=0;
 489
 490         if (tl_verbose)
 491                 return 0;
 492
 493         do {
 494                 m = 0; cnt++;
 495                 for (a = never; a; a = a->nxt)
 496                 {       if (v && !a->reachable) continue;
 497
 498                         if (a->redundant) continue; /* 3.3.10 */
 499
 500                         for (b = a->nxt; b; b = b->nxt)
 501                         {       if (v && !b->reachable) continue;
 502
 503                                 if (b->redundant) continue; /* 3.3.10 */
 504
 505                                 if (all_trans_match(a, b))
 506                                 {       m++;
 507                                         if (tl_verbose)
 508                                         {       printf("%d: state %s equals state %s\n",
 509                                                 cnt, a->name->name, b->name->name);
 510                                                 showtrans(a);
 511                                                 printf("==\n");
 512                                                 showtrans(b);
 513                                         }
 514                                         retarget(a->name->name, b->name->name);
 515                                         if (!strncmp(a->name->name, "accept", 6)
 516                                         &&  Max_Red == 0)
 517                                         {       char buf[64];
 518                                                 sprintf(buf, "T0%s", &(a->name->name[6]));
 519                                                 retarget(buf, b->name->name);
 520                                         }
 521                                         break;
 522                                 }
 523 #if 0
 524                                 else if (tl_verbose)
 525                                 {       printf("\n%d: state %s differs from state %s [%d,%d]\n",
 526                                                 cnt, a->name->name, b->name->name,
 527                                                 a->accepting, b->accepting);
 528                                         showtrans(a);
 529                                         printf("==\n");
 530                                         showtrans(b);
 531                                         printf("\n");
 532                                 }
 533 #endif
 534                 }       }
 535         } while (m && cnt < 10);
 536         return cnt-1;
 537 }
 538
 539 static int tcnt;
 540
 541 static void
 542 rev_trans(Transition *t) /* print transitions  in reverse order... */
 543 {
 544         if (!t) return;
 545         rev_trans(t->nxt);
 546
 547         if (t->redundant && !tl_verbose) return;
 548         fprintf(tl_out, "\t:: (");
 549         if (dump_cond(t->cond, t->cond, 1))
 550                 fprintf(tl_out, "1");
 551         fprintf(tl_out, ") -> goto %s\n", t->name->name);
 552         tcnt++;
 553 }
 554
 555 static void
 556 printstate(State *b)
 557 {
 558         if (!b || (!tl_verbose && !b->reachable)) return;
 559
 560         b->reachable = 0;       /* print only once */
 561         fprintf(tl_out, "%s:\n", b->name->name);
 562
 563         if (tl_verbose)
 564         {       fprintf(tl_out, "       /* ");
 565                 dump(b->colors->Other);
 566                 fprintf(tl_out, " */\n");
 567         }
 568
 569         if (strncmp(b->name->name, "accept", 6) == 0
 570         &&  Max_Red == 0)
 571                 fprintf(tl_out, "T0%s:\n", &(b->name->name[6]));
 572
 573         fprintf(tl_out, "\tif\n");
 574         tcnt = 0;
 575         rev_trans(b->trans);
 576         if (!tcnt) fprintf(tl_out, "\t:: false\n");
 577         fprintf(tl_out, "\tfi;\n");
 578         Total++;
 579 }
 580
 581 void
 582 addtrans(Graph *col, char *from, Node *op, char *to)
 583 {       State *b;
 584         Transition *t;
 585
 586         t = (Transition *) tl_emalloc(sizeof(Transition));
 587         t->name = tl_lookup(to);
 588         t->cond = Prune(dupnode(op));
 589
 590         if (tl_verbose)
 591         {       printf("\n%s <<\t", from); dump(op);
 592                 printf("\n\t"); dump(t->cond);
 593                 printf(">> %s\n", t->name->name);
 594         }
 595         if (t->cond) t->cond = rewrite(t->cond);
 596
 597         for (b = never; b; b = b->nxt)
 598                 if (!strcmp(b->name->name, from))
 599                 {       t->nxt = b->trans;
 600                         b->trans = t;
 601                         return;
 602                 }
 603         b = (State *) tl_emalloc(sizeof(State));
 604         b->name   = tl_lookup(from);
 605         b->colors = col;
 606         b->trans  = t;
 607         if (!strncmp(from, "accept", 6))
 608                 b->accepting = 1;
 609         b->nxt = never;
 610         never  = b;
 611 }
 612
 613 static void
 614 clr_reach(void)
 615 {       State *p;
 616         for (p = never; p; p = p->nxt)
 617                 p->reachable = 0;
 618         hitsall = 0;
 619 }
 620
 621 void
 622 fsm_print(void)
 623 {       State *b; int cnt1, cnt2=0;
 624         extern void put_uform(void);
 625
 626         if (tl_clutter) clutter();
 627
 628         b = findstate("T0_init");
 629         if (Max_Red == 0)
 630                 b->accepting = 1;
 631
 632         mergestates(0);
 633         b = findstate("T0_init");
 634
 635         fprintf(tl_out, "never {    /* ");
 636                 put_uform();
 637         fprintf(tl_out, " */\n");
 638
 639         do {
 640                 clr_reach();
 641                 Dfs(b);
 642                 cnt1 = mergetrans();
 643                 cnt2 = mergestates(1);
 644                 if (tl_verbose)
 645                         printf("/* >>%d,%d<< */\n", cnt1, cnt2);
 646         } while (cnt2 > 0);
 647
 648 #ifdef BUCKY
 649         buckyballs();
 650         clr_reach();
 651         Dfs(b);
 652 #endif
 653         if (b && b->accepting)
 654                 fprintf(tl_out, "accept_init:\n");
 655
 656         if (!b && !never)
 657         {       fprintf(tl_out, "       0 /* false */;\n");
 658         } else
 659         {       printstate(b);  /* init state must be first */
 660                 for (b = never; b; b = b->nxt)
 661                         printstate(b);
 662         }
 663         if (hitsall)
 664         fprintf(tl_out, "accept_all:\n  skip\n");
 665         fprintf(tl_out, "}\n");
 666 }