?? tl.h
字號:
/***** 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); } }
?? 快捷鍵說明
復制代碼
Ctrl + C
搜索代碼
Ctrl + F
全屏模式
F11
切換主題
Ctrl + Shift + D
顯示快捷鍵
?
增大字號
Ctrl + =
減小字號
Ctrl + -