1 /***** ltl2ba : ltl2ba.h *****/ 2 3 /* Written by Denis Oddoux, LIAFA, France */ 4 /* Copyright (c) 2001 Denis Oddoux */ 5 /* Modified by Paul Gastin, LSV, France */ 6 /* Copyright (c) 2007 Paul Gastin */ 7 /* */ 8 /* This program is free software; you can redistribute it and/or modify */ 9 /* it under the terms of the GNU General Public License as published by */ 10 /* the Free Software Foundation; either version 2 of the License, or */ 11 /* (at your option) any later version. */ 12 /* */ 13 /* This program is distributed in the hope that it will be useful, */ 14 /* but WITHOUT ANY WARRANTY; without even the implied warranty of */ 15 /* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */ 16 /* GNU General Public License for more details. */ 17 /* */ 18 /* You should have received a copy of the GNU General Public License */ 19 /* along with this program; if not, write to the Free Software */ 20 /* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/ 21 /* */ 22 /* Based on the translation algorithm by Gastin and Oddoux, */ 23 /* presented at the 13th International Conference on Computer Aided */ 24 /* Verification, CAV 2001, Paris, France. */ 25 /* Proceedings - LNCS 2102, pp. 53-65 */ 26 /* */ 27 /* Send bug-reports and/or questions to Paul Gastin */ 28 /* http://www.lsv.ens-cachan.fr/~gastin */ 29 /* */ 30 /* Some of the code in this file was taken from the Spin software */ 31 /* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A. */ 32 33 #include <stdio.h> 34 #include <string.h> 35 #include <stdlib.h> 36 #include <sys/time.h> 37 #include <sys/resource.h> 38 39 typedef struct Symbol { 40 char *name; 41 struct Symbol *next; /* linked list, symbol table */ 42 } Symbol; 43 44 typedef struct Node { 45 short ntyp; /* node type */ 46 struct Symbol *sym; 47 struct Node *lft; /* tree */ 48 struct Node *rgt; /* tree */ 49 struct Node *nxt; /* if linked list */ 50 } Node; 51 52 typedef struct Graph { 53 Symbol *name; 54 Symbol *incoming; 55 Symbol *outgoing; 56 Symbol *oldstring; 57 Symbol *nxtstring; 58 Node *New; 59 Node *Old; 60 Node *Other; 61 Node *Next; 62 unsigned char isred[64], isgrn[64]; 63 unsigned char redcnt, grncnt; 64 unsigned char reachable; 65 struct Graph *nxt; 66 } Graph; 67 68 typedef struct Mapping { 69 char *from; 70 Graph *to; 71 struct Mapping *nxt; 72 } Mapping; 73 74 typedef struct ATrans { 75 int *to; 76 int *pos; 77 int *neg; 78 struct ATrans *nxt; 79 } ATrans; 80 81 typedef struct AProd { 82 int astate; 83 struct ATrans *prod; 84 struct ATrans *trans; 85 struct AProd *nxt; 86 struct AProd *prv; 87 } AProd; 88 89 90 typedef struct GTrans { 91 int *pos; 92 int *neg; 93 struct GState *to; 94 int *final; 95 struct GTrans *nxt; 96 } GTrans; 97 98 typedef struct GState { 99 int id; 100 int incoming; 101 int *nodes_set; 102 struct GTrans *trans; 103 struct GState *nxt; 104 struct GState *prv; 105 } GState; 106 107 typedef struct BTrans { 108 struct BState *to; 109 int *pos; 110 int *neg; 111 struct BTrans *nxt; 112 } BTrans; 113 114 typedef struct BState { 115 struct GState *gstate; 116 int id; 117 int incoming; 118 int final; 119 struct BTrans *trans; 120 struct BState *nxt; 121 struct BState *prv; 122 } BState; 123 124 typedef struct GScc { 125 struct GState *gstate; 126 int rank; 127 int theta; 128 struct GScc *nxt; 129 } GScc; 130 131 typedef struct BScc { 132 struct BState *bstate; 133 int rank; 134 int theta; 135 struct BScc *nxt; 136 } BScc; 137 138 enum { 139 ALWAYS=257, 140 AND, /* 258 */ 141 EQUIV, /* 259 */ 142 EVENTUALLY, /* 260 */ 143 FALSE, /* 261 */ 144 IMPLIES, /* 262 */ 145 NOT, /* 263 */ 146 OR, /* 264 */ 147 PREDICATE, /* 265 */ 148 TRUE, /* 266 */ 149 U_OPER, /* 267 */ 150 V_OPER /* 268 */ 151 #ifdef NXT 152 , NEXT /* 269 */ 153 #endif 154 }; 155 156 Node *Canonical(Node *); 157 Node *canonical(Node *); 158 Node *cached(Node *); 159 Node *dupnode(Node *); 160 Node *getnode(Node *); 161 Node *in_cache(Node *); 162 Node *push_negation(Node *); 163 Node *right_linked(Node *); 164 Node *tl_nn(int, Node *, Node *); 165 166 Symbol *tl_lookup(char *); 167 Symbol *getsym(Symbol *); 168 Symbol *DoDump(Node *); 169 170 char *emalloc(int); 171 172 int anywhere(int, Node *, Node *); 173 int dump_cond(Node *, Node *, int); 174 int isequal(Node *, Node *); 175 int tl_Getchar(void); 176 177 void *tl_emalloc(int); 178 ATrans *emalloc_atrans(); 179 void free_atrans(ATrans *, int); 180 void free_all_atrans(); 181 GTrans *emalloc_gtrans(); 182 void free_gtrans(GTrans *, GTrans *, int); 183 BTrans *emalloc_btrans(); 184 void free_btrans(BTrans *, BTrans *, int); 185 void a_stats(void); 186 void addtrans(Graph *, char *, Node *, char *); 187 void cache_stats(void); 188 void dump(Node *); 189 void Fatal(const char *); 190 void fatal(const char *); 191 void fsm_print(void); 192 void releasenode(int, Node *); 193 void tfree(void *); 194 void tl_explain(int); 195 void tl_UnGetchar(void); 196 void tl_parse(void); 197 void tl_yyerror(char *); 198 void trans(Node *); 199 200 void mk_alternating(Node *); 201 void mk_generalized(); 202 void mk_buchi(); 203 204 ATrans *dup_trans(ATrans *); 205 ATrans *merge_trans(ATrans *, ATrans *); 206 void do_merge_trans(ATrans **, ATrans *, ATrans *); 207 208 int *new_set(int); 209 int *clear_set(int *, int); 210 int *make_set(int , int); 211 void copy_set(int *, int *, int); 212 int *dup_set(int *, int); 213 void merge_sets(int *, int *, int); 214 void do_merge_sets(int *, int *, int *, int); 215 int *intersect_sets(int *, int *, int); 216 void add_set(int *, int); 217 void rem_set(int *, int); 218 void spin_print_set(int *, int*); 219 void print_set(int *, int); 220 int empty_set(int *, int); 221 int empty_intersect_sets(int *, int *, int); 222 int same_sets(int *, int *, int); 223 int included_set(int *, int *, int); 224 int in_set(int *, int); 225 int *list_set(int *, int); 226 227 int timeval_subtract (struct timeval *, struct timeval *, struct timeval *); 228 229 void put_uform(void); 230 231 #define ZN (Node *)0 232 #define ZS (Symbol *)0 233 #define Nhash 255 234 #define True tl_nn(TRUE, ZN, ZN) 235 #define False tl_nn(FALSE, ZN, ZN) 236 #define Not(a) push_negation(tl_nn(NOT, a, ZN)) 237 #define rewrite(n) canonical(right_linked(n)) 238 239 typedef Node *Nodeptr; 240 #define YYSTYPE Nodeptr 241 242 #define Debug(x) { if (0) printf(x); } 243 #define Debug2(x,y) { if (tl_verbose) printf(x,y); } 244 #define Dump(x) { if (0) dump(x); } 245 #define Explain(x) { if (tl_verbose) tl_explain(x); } 246 247 #define Assert(x, y) { if (!(x)) { tl_explain(y); \ 248 Fatal(": assertion failed\n"); } } 249 #define min(x,y) ((x<y)?x:y) 250