1 /***** tl_spin: tl_rewrt.c *****/
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 */
12 /* Based on the translation algorithm by Gerth, Peled, Vardi, and Wolper, */
13 /* presented at the PSTV Conference, held in 1995, Warsaw, Poland 1995. */
17 extern int tl_verbose
;
19 static Node
*can
= ZN
;
26 if (n
->ntyp
== AND
|| n
->ntyp
== OR
)
27 while (n
->lft
&& n
->lft
->ntyp
== n
->ntyp
)
34 n
->lft
= right_linked(n
->lft
);
35 n
->rgt
= right_linked(n
->rgt
);
42 { Node
*m
; /* assumes input is right_linked */
45 if ((m
= in_cache(n
)) != ZN
)
48 n
->rgt
= canonical(n
->rgt
);
49 n
->lft
= canonical(n
->lft
);
55 push_negation(Node
*n
)
58 Assert(n
->ntyp
== NOT
, n
->ntyp
);
60 switch (n
->lft
->ntyp
) {
62 Debug("!true => false\n");
63 releasenode(0, n
->lft
);
68 Debug("!false => true\n");
69 releasenode(0, n
->lft
);
76 releasenode(0, n
->lft
);
82 Debug("!(p V q) => (!p U !q)\n");
86 Debug("!(p U q) => (!p V !q)\n");
94 n
->lft
= push_negation(n
->lft
);
98 Debug("!(p && q) => !p || !q\n");
102 Debug("!(p || q) => !p && !q\n");
105 same
: m
= n
->lft
->rgt
;
111 n
->lft
= push_negation(m
);
119 addcan(int tok
, Node
*n
)
120 { Node
*m
, *prev
= ZN
;
123 Symbol
*s
, *t
; int cmp
;
128 { addcan(tok
, n
->rgt
);
140 if (can
->ntyp
!= tok
) /* only one element in list so far */
145 /* there are at least 2 elements in list */
147 for (m
= can
; m
->ntyp
== tok
&& m
->rgt
; prev
= m
, m
= m
->rgt
)
148 { t
= DoDump(m
->lft
);
150 cmp
= strcmp(s
->name
, t
->name
);
153 if (cmp
== 0) /* duplicate */
157 { can
= tl_nn(tok
, N
, can
);
160 { ptr
= &(prev
->rgt
);
164 /* new entry goes at the end of the list */
168 cmp
= strcmp(s
->name
, t
->name
);
169 if (cmp
== 0) /* duplicate */
172 *ptr
= tl_nn(tok
, N
, *ptr
);
174 *ptr
= tl_nn(tok
, *ptr
, N
);
178 marknode(int tok
, Node
*m
)
181 { releasenode(0, m
->rgt
);
189 { Node
*m
, *p
, *k1
, *k2
, *prev
, *dflt
= ZN
;
195 if (tok
!= AND
&& tok
!= OR
)
201 Debug("\nA0: "); Dump(can
);
202 Debug("\nA1: "); Dump(n
); Debug("\n");
206 /* mark redundant nodes */
208 { for (m
= can
; m
; m
= (m
->ntyp
== AND
) ? m
->rgt
: ZN
)
209 { k1
= (m
->ntyp
== AND
) ? m
->lft
: m
;
210 if (k1
->ntyp
== TRUE
)
215 if (k1
->ntyp
== FALSE
)
216 { releasenode(1, can
);
220 for (m
= can
; m
; m
= (m
->ntyp
== AND
) ? m
->rgt
: ZN
)
221 for (p
= can
; p
; p
= (p
->ntyp
== AND
) ? p
->rgt
: ZN
)
226 k1
= (m
->ntyp
== AND
) ? m
->lft
: m
;
227 k2
= (p
->ntyp
== AND
) ? p
->lft
: p
;
233 if (anywhere(OR
, k1
, k2
))
239 { for (m
= can
; m
; m
= (m
->ntyp
== OR
) ? m
->rgt
: ZN
)
240 { k1
= (m
->ntyp
== OR
) ? m
->lft
: m
;
241 if (k1
->ntyp
== FALSE
)
246 if (k1
->ntyp
== TRUE
)
247 { releasenode(1, can
);
251 for (m
= can
; m
; m
= (m
->ntyp
== OR
) ? m
->rgt
: ZN
)
252 for (p
= can
; p
; p
= (p
->ntyp
== OR
) ? p
->rgt
: ZN
)
257 k1
= (m
->ntyp
== OR
) ? m
->lft
: m
;
258 k2
= (p
->ntyp
== OR
) ? p
->lft
: p
;
264 if (anywhere(AND
, k1
, k2
))
269 for (m
= can
, prev
= ZN
; m
; ) /* remove marked nodes */
274 { m
= can
= can
->rgt
;
276 { m
= prev
->rgt
= k2
;
277 /* if deleted the last node in a chain */
278 if (!prev
->rgt
&& prev
->lft
279 && (prev
->ntyp
== AND
|| prev
->ntyp
== OR
))
281 prev
->ntyp
= prev
->lft
->ntyp
;
282 prev
->sym
= prev
->lft
->sym
;
283 prev
->rgt
= prev
->lft
->rgt
;
284 prev
->lft
= prev
->lft
->lft
;
295 Debug("A2: "); Dump(can
); Debug("\n");
299 fatal("cannot happen, Canonical", (char *) 0);
This page took 0.064391 seconds and 4 git commands to generate.