123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128 |
- /***** 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 *);
- 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); } }
|