ref: 5d202d345616907d511b46e395226958fe66a2c3
dir: /sys/src/cmd/spin/tl.h/
/***** tl_spin: tl.h *****/ /* * This file is part of the public release of Spin. It is subject to the * terms in the LICENSE file that is included in this source directory. * Tool documentation is available at http://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 , CEXPR /* 270 */ }; 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 */ extern unsigned int hash(const char *); /* in sym.c */ int anywhere(int, Node *, Node *); int dump_cond(Node *, Node *, int); 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 ini_buchi(void); void ini_cache(void); void ini_rewrt(void); void ini_trans(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); } }