1 /***** tl_spin: tl_rewrt.c *****/ 2 3 /* Copyright (c) 1995-2003 by Lucent Technologies, Bell Laboratories. */ 4 /* All Rights Reserved. This software is for educational purposes only. */ 5 /* No guarantee whatsoever is expressed or implied by the distribution of */ 6 /* this code. Permission is given to distribute this code provided that */ 7 /* this introductory message is not removed and no monies are exchanged. */ 8 /* Software written by Gerard J. Holzmann. For tool documentation see: */ 9 /* http://spinroot.com/ */ 10 /* Send all bug-reports and/or questions to: bugs@spinroot.com */ 11 12 /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */ 13 /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */ 14 15 #include "tl.h" 16 17 extern int tl_verbose; 18 19 static Node *can = ZN; 20 21 Node * 22 right_linked(Node *n) 23 { 24 if (!n) return n; 25 26 if (n->ntyp == AND || n->ntyp == OR) 27 while (n->lft && n->lft->ntyp == n->ntyp) 28 { Node *tmp = n->lft; 29 n->lft = tmp->rgt; 30 tmp->rgt = n; 31 n = tmp; 32 } 33 34 n->lft = right_linked(n->lft); 35 n->rgt = right_linked(n->rgt); 36 37 return n; 38 } 39 40 Node * 41 canonical(Node *n) 42 { Node *m; /* assumes input is right_linked */ 43 44 if (!n) return n; 45 if ((m = in_cache(n)) != ZN) 46 return m; 47 48 n->rgt = canonical(n->rgt); 49 n->lft = canonical(n->lft); 50 51 return cached(n); 52 } 53 54 Node * 55 push_negation(Node *n) 56 { Node *m; 57 58 Assert(n->ntyp == NOT, n->ntyp); 59 60 switch (n->lft->ntyp) { 61 case TRUE: 62 Debug("!true => false\n"); 63 releasenode(0, n->lft); 64 n->lft = ZN; 65 n->ntyp = FALSE; 66 break; 67 case FALSE: 68 Debug("!false => true\n"); 69 releasenode(0, n->lft); 70 n->lft = ZN; 71 n->ntyp = TRUE; 72 break; 73 case NOT: 74 Debug("!!p => p\n"); 75 m = n->lft->lft; 76 releasenode(0, n->lft); 77 n->lft = ZN; 78 releasenode(0, n); 79 n = m; 80 break; 81 case V_OPER: 82 Debug("!(p V q) => (!p U !q)\n"); 83 n->ntyp = U_OPER; 84 goto same; 85 case U_OPER: 86 Debug("!(p U q) => (!p V !q)\n"); 87 n->ntyp = V_OPER; 88 goto same; 89 #ifdef NXT 90 case NEXT: 91 Debug("!X -> X!\n"); 92 n->ntyp = NEXT; 93 n->lft->ntyp = NOT; 94 n->lft = push_negation(n->lft); 95 break; 96 #endif 97 case AND: 98 Debug("!(p && q) => !p || !q\n"); 99 n->ntyp = OR; 100 goto same; 101 case OR: 102 Debug("!(p || q) => !p && !q\n"); 103 n->ntyp = AND; 104 105 same: m = n->lft->rgt; 106 n->lft->rgt = ZN; 107 108 n->rgt = Not(m); 109 n->lft->ntyp = NOT; 110 m = n->lft; 111 n->lft = push_negation(m); 112 break; 113 } 114 115 return rewrite(n); 116 } 117 118 static void 119 addcan(int tok, Node *n) 120 { Node *m, *prev = ZN; 121 Node **ptr; 122 Node *N; 123 Symbol *s, *t; int cmp; 124 125 if (!n) return; 126 127 if (n->ntyp == tok) 128 { addcan(tok, n->rgt); 129 addcan(tok, n->lft); 130 return; 131 } 132 133 N = dupnode(n); 134 if (!can) 135 { can = N; 136 return; 137 } 138 139 s = DoDump(N); 140 if (can->ntyp != tok) /* only one element in list so far */ 141 { ptr = &can; 142 goto insert; 143 } 144 145 /* there are at least 2 elements in list */ 146 prev = ZN; 147 for (m = can; m->ntyp == tok && m->rgt; prev = m, m = m->rgt) 148 { t = DoDump(m->lft); 149 cmp = strcmp(s->name, t->name); 150 if (cmp == 0) /* duplicate */ 151 return; 152 if (cmp < 0) 153 { if (!prev) 154 { can = tl_nn(tok, N, can); 155 return; 156 } else 157 { ptr = &(prev->rgt); 158 goto insert; 159 } } } 160 161 /* new entry goes at the end of the list */ 162 ptr = &(prev->rgt); 163 insert: 164 t = DoDump(*ptr); 165 cmp = strcmp(s->name, t->name); 166 if (cmp == 0) /* duplicate */ 167 return; 168 if (cmp < 0) 169 *ptr = tl_nn(tok, N, *ptr); 170 else 171 *ptr = tl_nn(tok, *ptr, N); 172 } 173 174 static void 175 marknode(int tok, Node *m) 176 { 177 if (m->ntyp != tok) 178 { releasenode(0, m->rgt); 179 m->rgt = ZN; 180 } 181 m->ntyp = -1; 182 } 183 184 Node * 185 Canonical(Node *n) 186 { Node *m, *p, *k1, *k2, *prev, *dflt = ZN; 187 int tok; 188 189 if (!n) return n; 190 191 tok = n->ntyp; 192 if (tok != AND && tok != OR) 193 return n; 194 195 can = ZN; 196 addcan(tok, n); 197 #if 0 198 Debug("\nA0: "); Dump(can); 199 Debug("\nA1: "); Dump(n); Debug("\n"); 200 #endif 201 releasenode(1, n); 202 203 /* mark redundant nodes */ 204 if (tok == AND) 205 { for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN) 206 { k1 = (m->ntyp == AND) ? m->lft : m; 207 if (k1->ntyp == TRUE) 208 { marknode(AND, m); 209 dflt = True; 210 continue; 211 } 212 if (k1->ntyp == FALSE) 213 { releasenode(1, can); 214 can = False; 215 goto out; 216 } } 217 for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN) 218 for (p = can; p; p = (p->ntyp == AND) ? p->rgt : ZN) 219 { if (p == m 220 || p->ntyp == -1 221 || m->ntyp == -1) 222 continue; 223 k1 = (m->ntyp == AND) ? m->lft : m; 224 k2 = (p->ntyp == AND) ? p->lft : p; 225 226 if (isequal(k1, k2)) 227 { marknode(AND, p); 228 continue; 229 } 230 if (anywhere(OR, k1, k2)) 231 { marknode(AND, p); 232 continue; 233 } 234 } } 235 if (tok == OR) 236 { for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN) 237 { k1 = (m->ntyp == OR) ? m->lft : m; 238 if (k1->ntyp == FALSE) 239 { marknode(OR, m); 240 dflt = False; 241 continue; 242 } 243 if (k1->ntyp == TRUE) 244 { releasenode(1, can); 245 can = True; 246 goto out; 247 } } 248 for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN) 249 for (p = can; p; p = (p->ntyp == OR) ? p->rgt : ZN) 250 { if (p == m 251 || p->ntyp == -1 252 || m->ntyp == -1) 253 continue; 254 k1 = (m->ntyp == OR) ? m->lft : m; 255 k2 = (p->ntyp == OR) ? p->lft : p; 256 257 if (isequal(k1, k2)) 258 { marknode(OR, p); 259 continue; 260 } 261 if (anywhere(AND, k1, k2)) 262 { marknode(OR, p); 263 continue; 264 } 265 } } 266 for (m = can, prev = ZN; m; ) /* remove marked nodes */ 267 { if (m->ntyp == -1) 268 { k2 = m->rgt; 269 releasenode(0, m); 270 if (!prev) 271 { m = can = can->rgt; 272 } else 273 { m = prev->rgt = k2; 274 /* if deleted the last node in a chain */ 275 if (!prev->rgt && prev->lft 276 && (prev->ntyp == AND || prev->ntyp == OR)) 277 { k1 = prev->lft; 278 prev->ntyp = prev->lft->ntyp; 279 prev->sym = prev->lft->sym; 280 prev->rgt = prev->lft->rgt; 281 prev->lft = prev->lft->lft; 282 releasenode(0, k1); 283 } 284 } 285 continue; 286 } 287 prev = m; 288 m = m->rgt; 289 } 290 out: 291 #if 0 292 Debug("A2: "); Dump(can); Debug("\n"); 293 #endif 294 if (!can) 295 { if (!dflt) 296 fatal("cannot happen, Canonical", (char *) 0); 297 return dflt; 298 } 299 300 return can; 301 } 302