/***** tl_spin: tl.h *****/

/* Copyright (c) 1995-2000 by Lucent Technologies - Bell Laboratories     */
/* All Rights Reserved.  This software is for educational purposes only.  */
/* Permission is given to distribute this code provided that this intro-  */
/* ductory message is not removed and no monies are exchanged.            */
/* No guarantee is expressed or implied by the distribution of this code. */
/* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A.               */
/* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
/* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995.   */
/* Send bug-reports and/or questions to: [email protected]    */

#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 *);

char    *emalloc(int);  /* 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); } }