move everything out of trunk

[lttv.git] / trunk / verif / Spin / Src5.1.6 / tl.h

diff --git a/trunk/verif/Spin/Src5.1.6/tl.h b/trunk/verif/Spin/Src5.1.6/tl.h
deleted file mode 100755 (executable)
index 1e6c094..0000000
--- a/trunk/verif/Spin/Src5.1.6/tl.h
+++ /dev/null
@@ -1,128 +0,0 @@
-/***** tl_spin: tl.h *****/
-
-/* Copyright (c) 1995-2003 by Lucent Technologies, Bell Laboratories.     */
-/* All Rights Reserved.  This software is for educational purposes only.  */
-/* No guarantee whatsoever is expressed or implied by the distribution of */
-/* this code.  Permission is given to distribute this code provided that  */
-/* this introductory message is not removed and no monies are exchanged.  */
-/* Software written by Gerard J. Holzmann.  For tool documentation see:   */
-/*             http://spinroot.com/                                       */
-/* Send all bug-reports and/or questions to: bugs@spinroot.com            */
-
-/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
-/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.   */
-
-#include <stdio.h>
-#include <string.h>
-
-typedef struct Symbol {
-       char            *name;
-       struct Symbol   *next;  /* linked list, symbol table */
-} Symbol;
-
-typedef struct Node {
-       short           ntyp;   /* node type */
-       struct Symbol   *sym;
-       struct Node     *lft;   /* tree */
-       struct Node     *rgt;   /* tree */
-       struct Node     *nxt;   /* if linked list */
-} Node;
-
-typedef struct Graph {
-       Symbol          *name;
-       Symbol          *incoming;
-       Symbol          *outgoing;
-       Symbol          *oldstring;
-       Symbol          *nxtstring;
-       Node            *New;
-       Node            *Old;
-       Node            *Other;
-       Node            *Next;
-       unsigned char   isred[64], isgrn[64];
-       unsigned char   redcnt, grncnt;
-       unsigned char   reachable;
-       struct Graph    *nxt;
-} Graph;
-
-typedef struct Mapping {
-       char    *from;
-       Graph   *to;
-       struct Mapping  *nxt;
-} Mapping;
-
-enum {
-       ALWAYS=257,
-       AND,            /* 258 */
-       EQUIV,          /* 259 */
-       EVENTUALLY,     /* 260 */
-       FALSE,          /* 261 */
-       IMPLIES,        /* 262 */
-       NOT,            /* 263 */
-       OR,             /* 264 */
-       PREDICATE,      /* 265 */
-       TRUE,           /* 266 */
-       U_OPER,         /* 267 */
-       V_OPER          /* 268 */
-#ifdef NXT
-       , NEXT          /* 269 */
-#endif
-};
-
-Node   *Canonical(Node *);
-Node   *canonical(Node *);
-Node   *cached(Node *);
-Node   *dupnode(Node *);
-Node   *getnode(Node *);
-Node   *in_cache(Node *);
-Node   *push_negation(Node *);
-Node   *right_linked(Node *);
-Node   *tl_nn(int, Node *, Node *);
-
-Symbol *tl_lookup(char *);
-Symbol *getsym(Symbol *);
-Symbol *DoDump(Node *);
-
-extern char    *emalloc(size_t);       /* in main.c */
-
-int    anywhere(int, Node *, Node *);
-int    dump_cond(Node *, Node *, int);
-int    hash(char *);   /* in sym.c */
-int    isalnum_(int);  /* in spinlex.c */
-int    isequal(Node *, Node *);
-int    tl_Getchar(void);
-
-void   *tl_emalloc(int);
-void   a_stats(void);
-void   addtrans(Graph *, char *, Node *, char *);
-void   cache_stats(void);
-void   dump(Node *);
-void   exit(int);
-void   Fatal(char *, char *);
-void   fatal(char *, char *);
-void   fsm_print(void);
-void   releasenode(int, Node *);
-void   tfree(void *);
-void   tl_explain(int);
-void   tl_UnGetchar(void);
-void   tl_parse(void);
-void   tl_yyerror(char *);
-void   trans(Node *);
-
-#define ZN     (Node *)0
-#define ZS     (Symbol *)0
-#define Nhash  255     /* must match size in spin.h */
-#define True   tl_nn(TRUE,  ZN, ZN)
-#define False  tl_nn(FALSE, ZN, ZN)
-#define Not(a) push_negation(tl_nn(NOT, a, ZN))
-#define rewrite(n)     canonical(right_linked(n))
-
-typedef Node   *Nodeptr;
-#define YYSTYPE         Nodeptr
-
-#define Debug(x)       { if (tl_verbose) printf(x); }
-#define Debug2(x,y)    { if (tl_verbose) printf(x,y); }
-#define Dump(x)                { if (tl_verbose) dump(x); }
-#define Explain(x)     { if (tl_verbose) tl_explain(x); }
-
-#define Assert(x, y)   { if (!(x)) { tl_explain(y); \
-                         Fatal(": assertion failed\n",(char *)0); } }