sys/src/cmd/spin/tl.h

   1 /***** tl_spin: tl.h *****/
   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 <stdio.h>
  13 #include <string.h>
  14
  15 typedef struct Symbol {
  16         char            *name;
  17         struct Symbol   *next;  /* linked list, symbol table */
  18 } Symbol;
  19
  20 typedef struct Node {
  21         short           ntyp;   /* node type */
  22         struct Symbol   *sym;
  23         struct Node     *lft;   /* tree */
  24         struct Node     *rgt;   /* tree */
  25         struct Node     *nxt;   /* if linked list */
  26 } Node;
  27
  28 typedef struct Graph {
  29         Symbol          *name;
  30         Symbol          *incoming;
  31         Symbol          *outgoing;
  32         Symbol          *oldstring;
  33         Symbol          *nxtstring;
  34         Node            *New;
  35         Node            *Old;
  36         Node            *Other;
  37         Node            *Next;
  38         unsigned char   isred[64], isgrn[64];
  39         unsigned char   redcnt, grncnt;
  40         unsigned char   reachable;
  41         struct Graph    *nxt;
  42 } Graph;
  43
  44 typedef struct Mapping {
  45         char    *from;
  46         Graph   *to;
  47         struct Mapping  *nxt;
  48 } Mapping;
  49
  50 enum {
  51         ALWAYS=257,
  52         AND,            /* 258 */
  53         EQUIV,          /* 259 */
  54         EVENTUALLY,     /* 260 */
  55         FALSE,          /* 261 */
  56         IMPLIES,        /* 262 */
  57         NOT,            /* 263 */
  58         OR,             /* 264 */
  59         PREDICATE,      /* 265 */
  60         TRUE,           /* 266 */
  61         U_OPER,         /* 267 */
  62         V_OPER          /* 268 */
  63 #ifdef NXT
  64         , NEXT          /* 269 */
  65 #endif
  66         , CEXPR         /* 270 */
  67 };
  68
  69 Node    *Canonical(Node *);
  70 Node    *canonical(Node *);
  71 Node    *cached(Node *);
  72 Node    *dupnode(Node *);
  73 Node    *getnode(Node *);
  74 Node    *in_cache(Node *);
  75 Node    *push_negation(Node *);
  76 Node    *right_linked(Node *);
  77 Node    *tl_nn(int, Node *, Node *);
  78
  79 Symbol  *tl_lookup(char *);
  80 Symbol  *getsym(Symbol *);
  81 Symbol  *DoDump(Node *);
  82
  83 extern char     *emalloc(size_t);       /* in main.c */
  84
  85 extern unsigned int     hash(const char *);     /* in sym.c */
  86
  87 int     anywhere(int, Node *, Node *);
  88 int     dump_cond(Node *, Node *, int);
  89 int     isalnum_(int);  /* in spinlex.c */
  90 int     isequal(Node *, Node *);
  91 int     tl_Getchar(void);
  92
  93 void    *tl_emalloc(int);
  94 void    a_stats(void);
  95 void    addtrans(Graph *, char *, Node *, char *);
  96 void    cache_stats(void);
  97 void    dump(Node *);
  98 void    exit(int);
  99 void    Fatal(char *, char *);
 100 void    fatal(char *, char *);
 101 void    fsm_print(void);
 102 void    ini_buchi(void);
 103 void    ini_cache(void);
 104 void    ini_rewrt(void);
 105 void    ini_trans(void);
 106 void    releasenode(int, Node *);
 107 void    tfree(void *);
 108 void    tl_explain(int);
 109 void    tl_UnGetchar(void);
 110 void    tl_parse(void);
 111 void    tl_yyerror(char *);
 112 void    trans(Node *);
 113
 114 #define ZN      (Node *)0
 115 #define ZS      (Symbol *)0
 116 #define Nhash   255     /* must match size in spin.h */
 117 #define True    tl_nn(TRUE,  ZN, ZN)
 118 #define False   tl_nn(FALSE, ZN, ZN)
 119 #define Not(a)  push_negation(tl_nn(NOT, a, ZN))
 120 #define rewrite(n)      canonical(right_linked(n))
 121
 122 typedef Node    *Nodeptr;
 123 #define YYSTYPE  Nodeptr
 124
 125 #define Debug(x)        { if (tl_verbose) printf(x); }
 126 #define Debug2(x,y)     { if (tl_verbose) printf(x,y); }
 127 #define Dump(x)         { if (tl_verbose) dump(x); }
 128 #define Explain(x)      { if (tl_verbose) tl_explain(x); }
 129
 130 #define Assert(x, y)    { if (!(x)) { tl_explain(y); \
 131                           Fatal(": assertion failed\n",(char *)0); } }