1 /***** ltl2ba : rewrt.c *****/
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 "ltl2ba.h"
34
35 extern int tl_verbose;
36
37 static Node *can = ZN;
38
39 Node *
right_linked(Node * n)40 right_linked(Node *n)
41 {
42 if (!n) return n;
43
44 if (n->ntyp == AND || n->ntyp == OR)
45 while (n->lft && n->lft->ntyp == n->ntyp)
46 { Node *tmp = n->lft;
47 n->lft = tmp->rgt;
48 tmp->rgt = n;
49 n = tmp;
50 }
51
52 n->lft = right_linked(n->lft);
53 n->rgt = right_linked(n->rgt);
54
55 return n;
56 }
57
58 Node *
canonical(Node * n)59 canonical(Node *n)
60 { Node *m; /* assumes input is right_linked */
61
62 if (!n) return n;
63 if ((m = in_cache(n)))
64 return m;
65
66 n->rgt = canonical(n->rgt);
67 n->lft = canonical(n->lft);
68
69 return cached(n);
70 }
71
72 Node *
push_negation(Node * n)73 push_negation(Node *n)
74 { Node *m;
75
76 Assert(n->ntyp == NOT, n->ntyp);
77
78 switch (n->lft->ntyp) {
79 case TRUE:
80 releasenode(0, n->lft);
81 n->lft = ZN;
82 n->ntyp = FALSE;
83 break;
84 case FALSE:
85 releasenode(0, n->lft);
86 n->lft = ZN;
87 n->ntyp = TRUE;
88 break;
89 case NOT:
90 m = n->lft->lft;
91 releasenode(0, n->lft);
92 n->lft = ZN;
93 releasenode(0, n);
94 n = m;
95 break;
96 case V_OPER:
97 n->ntyp = U_OPER;
98 goto same;
99 case U_OPER:
100 n->ntyp = V_OPER;
101 goto same;
102 #ifdef NXT
103 case NEXT:
104 n->ntyp = NEXT;
105 n->lft->ntyp = NOT;
106 n->lft = push_negation(n->lft);
107 break;
108 #endif
109 case AND:
110 n->ntyp = OR;
111 goto same;
112 case OR:
113 n->ntyp = AND;
114
115 same: m = n->lft->rgt;
116 n->lft->rgt = ZN;
117
118 n->rgt = Not(m);
119 n->lft->ntyp = NOT;
120 m = n->lft;
121 n->lft = push_negation(m);
122 break;
123 }
124
125 return rewrite(n);
126 }
127
128 static void
addcan(int tok,Node * n)129 addcan(int tok, Node *n)
130 { Node *m, *prev = ZN;
131 Node **ptr;
132 Node *N;
133 Symbol *s, *t; int cmp;
134
135 if (!n) return;
136
137 if (n->ntyp == tok)
138 { addcan(tok, n->rgt);
139 addcan(tok, n->lft);
140 return;
141 }
142 #if 0
143 if ((tok == AND && n->ntyp == TRUE)
144 || (tok == OR && n->ntyp == FALSE))
145 return;
146 #endif
147 N = dupnode(n);
148 if (!can)
149 { can = N;
150 return;
151 }
152
153 s = DoDump(N);
154 if (can->ntyp != tok) /* only one element in list so far */
155 { ptr = &can;
156 goto insert;
157 }
158
159 /* there are at least 2 elements in list */
160 prev = ZN;
161 for (m = can; m->ntyp == tok && m->rgt; prev = m, m = m->rgt)
162 { t = DoDump(m->lft);
163 cmp = strcmp(s->name, t->name);
164 if (cmp == 0) /* duplicate */
165 return;
166 if (cmp < 0)
167 { if (!prev)
168 { can = tl_nn(tok, N, can);
169 return;
170 } else
171 { ptr = &(prev->rgt);
172 goto insert;
173 } } }
174
175 /* new entry goes at the end of the list */
176 ptr = &(prev->rgt);
177 insert:
178 t = DoDump(*ptr);
179 cmp = strcmp(s->name, t->name);
180 if (cmp == 0) /* duplicate */
181 return;
182 if (cmp < 0)
183 *ptr = tl_nn(tok, N, *ptr);
184 else
185 *ptr = tl_nn(tok, *ptr, N);
186 }
187
188 static void
marknode(int tok,Node * m)189 marknode(int tok, Node *m)
190 {
191 if (m->ntyp != tok)
192 { releasenode(0, m->rgt);
193 m->rgt = ZN;
194 }
195 m->ntyp = -1;
196 }
197
198 Node *
Canonical(Node * n)199 Canonical(Node *n)
200 { Node *m, *p, *k1, *k2, *prev, *dflt = ZN;
201 int tok;
202
203 if (!n) return n;
204
205 tok = n->ntyp;
206 if (tok != AND && tok != OR)
207 return n;
208
209 can = ZN;
210 addcan(tok, n);
211 #if 1
212 Debug("\nA0: "); Dump(can);
213 Debug("\nA1: "); Dump(n); Debug("\n");
214 #endif
215 releasenode(1, n);
216
217 /* mark redundant nodes */
218 if (tok == AND)
219 { for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN)
220 { k1 = (m->ntyp == AND) ? m->lft : m;
221 if (k1->ntyp == TRUE)
222 { marknode(AND, m);
223 dflt = True;
224 continue;
225 }
226 if (k1->ntyp == FALSE)
227 { releasenode(1, can);
228 can = False;
229 goto out;
230 } }
231 for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN)
232 for (p = can; p; p = (p->ntyp == AND) ? p->rgt : ZN)
233 { if (p == m
234 || p->ntyp == -1
235 || m->ntyp == -1)
236 continue;
237 k1 = (m->ntyp == AND) ? m->lft : m;
238 k2 = (p->ntyp == AND) ? p->lft : p;
239
240 if (isequal(k1, k2))
241 { marknode(AND, p);
242 continue;
243 }
244 if (anywhere(OR, k1, k2))
245 { marknode(AND, p);
246 continue;
247 }
248 if (k2->ntyp == U_OPER
249 && anywhere(AND, k2->rgt, can))
250 { marknode(AND, p);
251 continue;
252 } /* q && (p U q) = q */
253 } }
254 if (tok == OR)
255 { for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN)
256 { k1 = (m->ntyp == OR) ? m->lft : m;
257 if (k1->ntyp == FALSE)
258 { marknode(OR, m);
259 dflt = False;
260 continue;
261 }
262 if (k1->ntyp == TRUE)
263 { releasenode(1, can);
264 can = True;
265 goto out;
266 } }
267 for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN)
268 for (p = can; p; p = (p->ntyp == OR) ? p->rgt : ZN)
269 { if (p == m
270 || p->ntyp == -1
271 || m->ntyp == -1)
272 continue;
273 k1 = (m->ntyp == OR) ? m->lft : m;
274 k2 = (p->ntyp == OR) ? p->lft : p;
275
276 if (isequal(k1, k2))
277 { marknode(OR, p);
278 continue;
279 }
280 if (anywhere(AND, k1, k2))
281 { marknode(OR, p);
282 continue;
283 }
284 if (k2->ntyp == V_OPER
285 && k2->lft->ntyp == FALSE
286 && anywhere(AND, k2->rgt, can))
287 { marknode(OR, p);
288 continue;
289 } /* p || (F V p) = p */
290 } }
291 for (m = can, prev = ZN; m; ) /* remove marked nodes */
292 { if (m->ntyp == -1)
293 { k2 = m->rgt;
294 releasenode(0, m);
295 if (!prev)
296 { m = can = can->rgt;
297 } else
298 { m = prev->rgt = k2;
299 /* if deleted the last node in a chain */
300 if (!prev->rgt && prev->lft
301 && (prev->ntyp == AND || prev->ntyp == OR))
302 { k1 = prev->lft;
303 prev->ntyp = prev->lft->ntyp;
304 prev->sym = prev->lft->sym;
305 prev->rgt = prev->lft->rgt;
306 prev->lft = prev->lft->lft;
307 releasenode(0, k1);
308 }
309 }
310 continue;
311 }
312 prev = m;
313 m = m->rgt;
314 }
315 out:
316 #if 1
317 Debug("A2: "); Dump(can); Debug("\n");
318 #endif
319 if (!can)
320 { if (!dflt)
321 fatal("cannot happen, Canonical");
322 return dflt;
323 }
324
325 return can;
326 }
327