trunk/verif/Spin/Src5.1.6/tl.h

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