sys/src/cmd/spin/tl_buchi.c

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