source: vis_dev/vis-2.3/src/ctlp/ctlpUtil.c@ 87

Last change on this file since 87 was 14, checked in by cecile, 15 years ago

vis2.3
File size: 146.6 KB
Line 
1/**CFile***********************************************************************
2
3 FileName [ctlpUtil.c]
4
5 PackageName [ctlp]
6
7 Synopsis [Routines for manipulating CTL formulas.]
8
9 Description [This file contains routines for accessing the fields of the CTL
10 formula data structure, for printing CTL formulas, for reading CTL formulas
11 from a file, and for converting formulas to the existential form.]
12
13 Remarks [There are two types of conversion routines. One set, for
14 mc and amc, converts a formula to existential normal form, i.e. the
15 AX, AU and AG operators are converted. The other set, used in imc,
16 converts to simple existential form, a form consisting only of
17 E-operators and the boolean operators AND and NOT.
18
19 Simple existential form is incompatible with the mc debug routines,
20 because these depend on the specific form of the converted formula
21 to decide what the original formula was.
22
23 In the long run, the existential form should probably go, and the
24 debug routines should be adapted. The only drawback of simple
25 existential form is that the XOR gets expanded into three nontrivial
26 operations, so maybe XOR (or IFF) should be retained. (RB.)]
27
28
29 Author [Gary York, Ramin Hojati, Tom Shiple, Adnan Aziz, Yuji Kukimoto,
30 Jae-Young Jang, In-Ho Moon]
31
32 Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California.
33 All rights reserved.
34
35 Permission is hereby granted, without written agreement and without license
36 or royalty fees, to use, copy, modify, and distribute this software and its
37 documentation for any purpose, provided that the above copyright notice and
38 the following two paragraphs appear in all copies of this software.
39
40 IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
41 DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
42 OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
43 CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
44
45 THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
46 INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
47 FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN
48 "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
49 MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
50
51******************************************************************************/
52
53#include "ctlpInt.h"
54#include "errno.h"
55
56static char rcsid[] UNUSED = "$Id: ctlpUtil.c,v 1.71 2009/04/11 18:25:53 fabio Exp $";
57
58
59/*---------------------------------------------------------------------------*/
60/* Variable declarations */
61/*---------------------------------------------------------------------------*/
62
63/**Variable********************************************************************
64
65 Synopsis [Array of CTL formulas (Ctlp_Formula_t) read from a file.]
66
67 SeeAlso [Ctlp_FormulaArrayFree]
68
69******************************************************************************/
70static array_t *globalFormulaArray;
71static int changeBracket = 1;
72
73/* see ctlpInt.h for documentation */
74int CtlpGlobalError;
75Ctlp_Formula_t *CtlpGlobalFormula;
76st_table *CtlpMacroTable;
77
78/*---------------------------------------------------------------------------*/
79/* Macro declarations */
80/*---------------------------------------------------------------------------*/
81
82
83/**AutomaticStart*************************************************************/
84
85/*---------------------------------------------------------------------------*/
86/* Static function prototypes */
87/*---------------------------------------------------------------------------*/
88
89static Ctlp_Formula_t * FormulaCreateWithType(Ctlp_FormulaType type);
90static int FormulaCompare(const char *key1, const char *key2);
91static int FormulaHash(char *key, int modulus);
92static Ctlp_Formula_t * FormulaHashIntoUniqueTable(Ctlp_Formula_t *formula, st_table *uniqueTable);
93static Ctlp_Formula_t * FormulaConvertToExistentialDAG(Ctlp_Formula_t *formula);
94static void FormulaConvertToForward(Ctlp_Formula_t *formula, int compareValue);
95static void FormulaInsertForwardCompareNodes(Ctlp_Formula_t *formula, Ctlp_Formula_t *parent, int compareValue);
96static int FormulaGetCompareValue(Ctlp_Formula_t *formula);
97static int FormulaIsConvertible(Ctlp_Formula_t *formula);
98static Ctlp_Formula_t * ReplaceSimpleFormula(Ctlp_Formula_t *formula);
99
100/**AutomaticEnd***************************************************************/
101
102
103/*---------------------------------------------------------------------------*/
104/* Definition of exported functions */
105/*---------------------------------------------------------------------------*/
106
107/**Function********************************************************************
108
109 Synopsis [Parses a file containing a set of CTL formulas.]
110
111 Description [Parses a file containing a set of semicolon-ending CTL
112 formulas, and returns an array of Ctlp_Formula_t representing those
113 formulas. If an error is detected while parsing the file, the routine frees
114 any allocated memory and returns NULL.]
115
116 SideEffects [Manipulates the global variables globalFormulaArray,
117 CtlpGlobalError and CtlpGlobalFormula.]
118
119 SeeAlso [Ctlp_FormulaArrayFree Ctlp_FormulaPrint]
120
121******************************************************************************/
122array_t *
123Ctlp_FileParseFormulaArray(
124 FILE * fp)
125{
126 st_generator *stGen;
127 char *name;
128 Ctlp_Formula_t *formula;
129 char *flagValue;
130 /*
131 * Initialize the global variables.
132 */
133 globalFormulaArray = array_alloc(Ctlp_Formula_t *, 0);
134 CtlpGlobalError = 0;
135 CtlpGlobalFormula = NIL(Ctlp_Formula_t);
136 CtlpMacroTable = st_init_table(strcmp,st_strhash);
137 CtlpFileSetup(fp);
138 /*
139 * Check if changing "[] -> <>" is disabled.
140 */
141 flagValue = Cmd_FlagReadByName("ctl_change_bracket");
142 if (flagValue != NIL(char)) {
143 if (strcmp(flagValue, "yes") == 0)
144 changeBracket = 1;
145 else if (strcmp(flagValue, "no") == 0)
146 changeBracket = 0;
147 else {
148 fprintf(vis_stderr,
149 "** ctl error : invalid value %s for ctl_change_bracket[yes/no]. ***\n",
150 flagValue);
151 }
152 }
153
154 (void)CtlpYyparse();
155 st_foreach_item(CtlpMacroTable,stGen,&name,&formula){
156 FREE(name);
157 CtlpFormulaFree(formula);
158 }
159 st_free_table(CtlpMacroTable);
160
161 /*
162 * Clean up if there was an error, otherwise return the array.
163 */
164 if (CtlpGlobalError){
165 Ctlp_FormulaArrayFree(globalFormulaArray);
166 return NIL(array_t);
167 }
168 else {
169 return globalFormulaArray;
170 }
171}
172
173/**Function********************************************************************
174
175 Synopsis [Returns formula as a character string.]
176
177 Description [Returns formula as a character string. All subformulas are
178 delimited by parenthesis. The syntax used is the same as used by the CTL
179 parser. Does nothing if passed a NULL formula.]
180
181 SideEffects []
182
183******************************************************************************/
184char *
185Ctlp_FormulaConvertToString(
186 Ctlp_Formula_t * formula)
187{
188 char *s1 = NIL(char);
189 char *s2 = NIL(char);
190 char *tmpString = NIL(char);
191 char *result;
192
193
194 if (formula == NIL(Ctlp_Formula_t)) {
195 return NIL(char);
196 }
197
198 /* The formula is a leaf. */
199 if (formula->type == Ctlp_ID_c){
200 return util_strcat3((char *)(formula->left), "=",(char *)(formula->right));
201 }
202
203 /* If the formula is a non-leaf, the function is called recursively */
204 s1 = Ctlp_FormulaConvertToString(formula->left);
205 s2 = Ctlp_FormulaConvertToString(formula->right);
206
207 switch(formula->type) {
208 /*
209 * The cases are listed in rough order of their expected frequency.
210 */
211 case Ctlp_OR_c:
212 tmpString = util_strcat3(s1, " + ",s2);
213 result = util_strcat3("(", tmpString, ")");
214 break;
215 case Ctlp_AND_c:
216 tmpString = util_strcat3(s1, " * ", s2);
217 result = util_strcat3("(", tmpString, ")");
218 break;
219 case Ctlp_THEN_c:
220 tmpString = util_strcat3(s1, " -> ", s2);
221 result = util_strcat3("(", tmpString, ")");
222 break;
223 case Ctlp_XOR_c:
224 tmpString = util_strcat3(s1, " ^ ", s2);
225 result = util_strcat3("(", tmpString, ")");
226 break;
227 case Ctlp_EQ_c:
228 tmpString = util_strcat3(s1, " <-> ", s2);
229 result = util_strcat3("(", tmpString, ")");
230 break;
231 case Ctlp_NOT_c:
232 tmpString = util_strcat3("(", s1, ")");
233 result = util_strcat3("!", tmpString, "");
234 break;
235 case Ctlp_EX_c:
236 result = util_strcat3("EX(", s1, ")");
237 FREE(s1);
238 break;
239 case Ctlp_EG_c:
240 result = util_strcat3("EG(", s1, ")");
241 break;
242 case Ctlp_EF_c:
243 result = util_strcat3("EF(", s1, ")");
244 break;
245 case Ctlp_EU_c:
246 tmpString = util_strcat3("E(", s1, " U ");
247 result = util_strcat3(tmpString, s2, ")");
248 break;
249 case Ctlp_AX_c:
250 result = util_strcat3("AX(", s1, ")");
251 break;
252 case Ctlp_AG_c:
253 result = util_strcat3("AG(", s1, ")");
254 break;
255 case Ctlp_AF_c:
256 result = util_strcat3("AF(", s1, ")");
257 break;
258 case Ctlp_AU_c:
259 tmpString = util_strcat3("A(", s1, " U ");
260 result = util_strcat3(tmpString, s2, ")");
261 break;
262 case Ctlp_TRUE_c:
263 result = util_strsav("TRUE");
264 break;
265 case Ctlp_FALSE_c:
266 result = util_strsav("FALSE");
267 break;
268 case Ctlp_Init_c:
269 result = util_strsav("Init");
270 break;
271 case Ctlp_Cmp_c:
272 if (formula->compareValue == 0)
273 tmpString = util_strcat3("[", s1, "] = ");
274 else
275 tmpString = util_strcat3("[", s1, "] != ");
276 result = util_strcat3(tmpString, s2, "");
277 break;
278 case Ctlp_FwdU_c:
279 tmpString = util_strcat3("FwdU(", s1, ",");
280 result = util_strcat3(tmpString, s2, ")");
281 break;
282 case Ctlp_FwdG_c:
283 tmpString = util_strcat3("FwdG(", s1, ",");
284 result = util_strcat3(tmpString, s2, ")");
285 break;
286 case Ctlp_EY_c:
287 result = util_strcat3("EY(", s1, ")");
288 break;
289 default:
290 fail("Unexpected type");
291 }
292
293 if (s1 != NIL(char)) {
294 FREE(s1);
295 }
296
297 if (s2 != NIL(char)) {
298 FREE(s2);
299 }
300
301 if (tmpString != NIL(char)) {
302 FREE(tmpString);
303 }
304
305 return result;
306}
307
308
309/**Function********************************************************************
310
311 Synopsis [Prints a formula to a file.]
312
313 Description [Prints a formula to a file. All subformulas are delimited by
314 parenthesis. The syntax used is the same as used by the CTL parser. Does
315 nothing if passed a NULL formula.]
316
317 SideEffects []
318
319******************************************************************************/
320void
321Ctlp_FormulaPrint(
322 FILE * fp,
323 Ctlp_Formula_t * formula)
324{
325 char *tmpString;
326 if (formula == NIL(Ctlp_Formula_t)) {
327 return;
328 }
329 tmpString = Ctlp_FormulaConvertToString(formula);
330 (void) fprintf(fp, "%s", tmpString);
331 FREE(tmpString);
332}
333
334
335/**Function********************************************************************
336
337 Synopsis [Gets the type of a formula.]
338
339 Description [Gets the type of a formula. See ctlp.h for all the types. It is
340 an error to call this function on a NULL formula.]
341
342 SideEffects []
343
344 SeeAlso []
345
346******************************************************************************/
347Ctlp_FormulaType
348Ctlp_FormulaReadType(
349 Ctlp_Formula_t * formula)
350{
351 assert( formula != NIL(Ctlp_Formula_t) );
352 return (formula->type);
353}
354
355#if 0
356boolean
357Ctlp_FormulaReadEvenNegations(
358 Ctlp_Formula_t * formula)
359{
360 assert(formula != NIL(Ctlp_Formula_t));
361 return (formula->even_negations);
362}
363#endif
364
365
366/**Function********************************************************************
367
368 Synopsis [Gets the compare value of a formula.]
369
370 Description [Gets the compare value of a formula. It is an error to call
371 this function on a NULL formula.]
372
373 SideEffects []
374
375 SeeAlso []
376
377******************************************************************************/
378int
379Ctlp_FormulaReadCompareValue(
380 Ctlp_Formula_t * formula)
381{
382 int value;
383
384 assert( formula != NIL(Ctlp_Formula_t));
385 value = formula->compareValue;
386 return (value);
387}
388
389
390/**Function********************************************************************
391
392 Synopsis [Reads the variable name of a leaf formula.]
393
394 Description [Reads the variable name of a leaf formula.
395 It is an error to call this function on a non-leaf formula.]
396
397 SideEffects []
398
399******************************************************************************/
400char *
401Ctlp_FormulaReadVariableName(
402 Ctlp_Formula_t * formula)
403{
404 if (formula->type != Ctlp_ID_c){
405 fail("Ctlp_FormulaReadVariableName() was called on a non-leaf formula.");
406 }
407 return ((char *)(formula->left));
408}
409
410
411/**Function********************************************************************
412
413 Synopsis [Reads the value name of a leaf formula.]
414
415 Description [Reads the value name of a leaf formula.
416 It is an error to call this function on a non-leaf formula.]
417
418 SideEffects []
419
420******************************************************************************/
421char *
422Ctlp_FormulaReadValueName(
423 Ctlp_Formula_t * formula)
424{
425 if (formula->type != Ctlp_ID_c){
426 fail("Ctlp_FormulaReadValueName() was called on a non-leaf formula.");
427 }
428 return ((char *)(formula->right));
429}
430
431/**Function********************************************************************
432
433 Synopsis [Gets the left child of a formula.]
434
435 Description [Gets the left child of a formula. User must not free this
436 formula. If a formula is a leaf formula, NIL(Ctlp_Formula_t) is returned.]
437
438 SideEffects []
439
440 SeeAlso [Ctlp_FormulaReadRightChild]
441
442******************************************************************************/
443Ctlp_Formula_t *
444Ctlp_FormulaReadLeftChild(
445 Ctlp_Formula_t * formula)
446{
447 if (formula->type != Ctlp_ID_c){
448 return (formula->left);
449 }
450 return NIL(Ctlp_Formula_t);
451}
452
453
454/**Function********************************************************************
455
456 Synopsis [Gets the right child of a formula.]
457
458 Description [Gets the right child of a formula. User must not free this
459 formula. If a formula is a leaf formula, NIL(Ctlp_Formula_t) is returned.]
460
461 SideEffects []
462
463 SeeAlso [Ctlp_FormulaReadLeftChild]
464
465******************************************************************************/
466Ctlp_Formula_t *
467Ctlp_FormulaReadRightChild(
468 Ctlp_Formula_t * formula)
469{
470 if (formula->type != Ctlp_ID_c){
471 return (formula->right);
472 }
473 return NIL(Ctlp_Formula_t);
474}
475
476
477/**Function********************************************************************
478
479 Synopsis [Gets a copy of the set of states for which this formula is
480 true.]
481
482 Description [Gets a copy of the MDD representing the set of states for which
483 this formula is true. It is the user's responsibility to free this MDD. If
484 the set of states has not yet been computed, then a NULL mdd_t is
485 returned. It is an error to call this function on a NULL formula.]
486
487 SideEffects []
488
489 SeeAlso [Ctlp_FormulaSetStates]
490
491******************************************************************************/
492mdd_t *
493Ctlp_FormulaObtainStates(
494 Ctlp_Formula_t * formula)
495{
496 assert(formula != NIL(Ctlp_Formula_t));
497 if (formula->states == NIL(mdd_t) ||
498 formula->latest == Ctlp_Incomparable_c) {
499 return NIL(mdd_t);
500 }
501 else {
502 return mdd_dup(formula->states);
503 }
504}
505
506
507/**Function********************************************************************
508
509 Synopsis [Stores the set of states with the formula.]
510
511 Description [Stores the MDD with the formula (a copy is not made,
512 and hence, the caller should not later free this MDD). This MDD is
513 intended to represent the set of states for which the formula is
514 true. It is an error to call this function on a NULL formula.]
515
516 SideEffects []
517
518 SeeAlso [Ctlp_FormulaObtainStates]
519
520******************************************************************************/
521void
522Ctlp_FormulaSetStates(
523 Ctlp_Formula_t * formula,
524 mdd_t * states)
525{
526 assert(formula != NIL(Ctlp_Formula_t));
527 /* RB: added the next two lines. Given the Description, this was a
528 bug */
529 if(formula->states != NIL(mdd_t))
530 mdd_free(formula->states);
531 formula->states = states;
532 formula->latest = Ctlp_Exact_c;
533}
534
535
536/**Function********************************************************************
537
538 Synopsis [Gets (a copy of) the latest approximation of the satisfying set]
539
540 Description [Gets the satisfying set or an approximation of it. The most
541 recently computed approximation is returned. If the
542 exact set is available, it will return that, because it is never superseded.
543 If neither exact nor approximate satisfying set is available, or
544 approx is Ctlp_Incomparable_c, it fails.]
545
546 SideEffects []
547
548 SeeAlso [Ctlp_FormulaSetApproxStates]
549
550******************************************************************************/
551mdd_t *
552Ctlp_FormulaObtainLatestApprox(
553 Ctlp_Formula_t *formula)
554{
555 if (formula->latest == Ctlp_Exact_c)
556 return mdd_dup(formula->states);
557
558 if (formula->latest == Ctlp_Overapprox_c)
559 return mdd_dup(formula->overapprox);
560
561 if (formula->latest == Ctlp_Underapprox_c)
562 return mdd_dup(formula->underapprox);
563
564 if (formula->latest == Ctlp_Incomparable_c)
565 return mdd_dup(formula->states);
566
567 assert(0); /* we should never get here */
568 return NIL(mdd_t);
569}
570
571
572/**Function********************************************************************
573
574 Synopsis [Gets (a copy of) an approximation of the satisfying set]
575
576 Description [Gets the required approximation of the satisfying set. If the
577 exact set is available, it will return that. If neither is available, or
578 approx is Ctlp_Incomparable_c, it will return NULL.]
579
580 SideEffects []
581
582 SeeAlso [Ctlp_FormulaSetApproxStates]
583
584******************************************************************************/
585mdd_t *
586Ctlp_FormulaObtainApproxStates(
587 Ctlp_Formula_t *formula,
588 Ctlp_Approx_t approx)
589{
590 if(approx == Ctlp_Incomparable_c)
591 return NIL(mdd_t);
592
593 if (formula->states != NIL(mdd_t))
594 return mdd_dup(formula->states);
595
596 if(approx == Ctlp_Exact_c)
597 return NIL(mdd_t);
598
599 if(approx == Ctlp_Overapprox_c){
600 if(formula->overapprox == NIL(mdd_t))
601 return NIL(mdd_t);
602 else
603 return mdd_dup(formula->overapprox);
604 }
605
606 if(approx == Ctlp_Underapprox_c){
607 if(formula->underapprox == NIL(mdd_t))
608 return NIL(mdd_t);
609 else
610 return mdd_dup(formula->underapprox);
611 }
612
613 assert(0); /* we should never get here */
614 return NIL(mdd_t);
615}
616
617
618/**Function********************************************************************
619
620 Synopsis [Stores (an approximation of) the set of states with the
621 formula.]
622
623 Description [Sets the set of states or an under or overapproximation
624 thereof, depending on the approx flag. If there is already an under
625 or overapproximation, it is overwritten. If the exact set is given,
626 the approx fields are cleared. Setting an incomparable
627 approximation results in no action being taken. An approximation
628 does not replace the exact set. A copy of the mdd is not made, so
629 the caller should not free it.]
630
631 SideEffects []
632
633 SeeAlso [Ctlp_FormulaObtainApproxStates Ctlp_FormulaObtainLatestApprox]
634
635******************************************************************************/
636void
637Ctlp_FormulaSetApproxStates(
638 Ctlp_Formula_t * formula,
639 mdd_t * states,
640 Ctlp_Approx_t approx)
641{
642 if (formula->latest == Ctlp_Exact_c) {
643 mdd_free(states);
644 return;
645 }
646
647 formula->latest = approx;
648
649 if (approx == Ctlp_Exact_c) {
650 if (formula->states != NIL(mdd_t))
651 mdd_free(formula->states);
652 formula->states = states;
653
654 if (formula->underapprox != NIL(mdd_t)) {
655 mdd_free(formula->underapprox);
656 formula->underapprox = NIL(mdd_t);
657 }
658
659 if (formula->overapprox != NIL(mdd_t)) {
660 mdd_free(formula->overapprox);
661 formula->overapprox = NIL(mdd_t);
662 }
663
664 return;
665 }
666
667 if (approx == Ctlp_Underapprox_c) {
668 /* you could perform a union instead, but typical use will
669 have monotonically increasing underapproximations */
670 if(formula->underapprox != NIL(mdd_t))
671 mdd_free(formula->underapprox);
672 formula->underapprox = states;
673 }
674
675 if (approx == Ctlp_Overapprox_c) {
676 /* you could perform an intersection instead */
677 if (formula->overapprox != NIL(mdd_t))
678 mdd_free(formula->overapprox);
679 formula->overapprox = states;
680 }
681
682 /* This case is possible; for instance when both children of an implication
683 * with (All, S) condition are underapproximated. We may lose some states
684 * from the left if they are not in S. These cause an overapproximation.
685 * We may also lose some states from the right. These cause an
686 * underapproximation. When the two effects are combined, we get something
687 * incomparable, yet sufficient to produce the exact result, because it is
688 * accurate over S. */
689 if (approx == Ctlp_Incomparable_c) {
690 if (formula->states != NIL(mdd_t))
691 mdd_free(formula->states);
692 formula->states = states;
693 }
694
695 return;
696}
697
698
699/**Function********************************************************************
700
701 Synopsis [Sets the debug information of a formula.]
702
703 Description [Sets the debug information of a CTL formula. The data is
704 uninterpreted. FreeFn is a pointer to a function that takes a formula as
705 input and returns void. FreeFn should free all the memory associated with
706 the debug data; it is called when this formula is freed.]
707
708 SideEffects []
709
710 SeeAlso [Ctlp_FormulaReadDebugData]
711
712******************************************************************************/
713void
714Ctlp_FormulaSetDbgInfo(
715 Ctlp_Formula_t * formula,
716 void *data,
717 Ctlp_DbgInfoFreeFn freeFn)
718{
719 if (formula->dbgInfo.data != NIL(void)){
720 assert(formula->dbgInfo.freeFn != NULL);
721
722 (*formula->dbgInfo.freeFn)(formula);
723 }
724
725 formula->dbgInfo.data = data;
726 formula->dbgInfo.freeFn = freeFn;
727}
728
729
730/**Function********************************************************************
731
732 Synopsis [Returns the debug data associated with a formula.]
733
734 Description [Returns the debug data associated with a formula. These data
735 are uninterpreted by the ctlp package.]
736
737 SideEffects []
738
739 SeeAlso [Ctlp_FormulaSetDbgInfo]
740
741******************************************************************************/
742void *
743Ctlp_FormulaReadDebugData(
744 Ctlp_Formula_t * formula)
745{
746 return formula->dbgInfo.data;
747}
748
749
750/**Function********************************************************************
751
752 Synopsis [Returns TRUE if formula was converted, else FALSE.]
753 from AX/AG/AU/AF]
754
755 Description [Returns TRUE if formula was converted from a formula of type
756 AG, AX, AU, AF, or EF via a call to
757 Ctlp_FormulaConvertToExistentialFormTree or
758 Ctlp_FormulaConvertToExistentialFormDAG. Otherwise, returns FALSE.]
759
760 SideEffects []
761
762******************************************************************************/
763boolean
764Ctlp_FormulaTestIsConverted(
765 Ctlp_Formula_t * formula)
766{
767 return formula->dbgInfo.convertedFlag;
768}
769
770
771/**Function********************************************************************
772
773 Synopsis [Returns TRUE if formula contains no path quantifiers.]
774
775 Description [Test if a CTL formula has any path quantifiers in it;
776 if so return false, else true. For a CTL formula, being quantifier-free
777 and being propositional are equivalent.]
778
779 SideEffects []
780
781******************************************************************************/
782boolean
783Ctlp_FormulaTestIsQuantifierFree(
784 Ctlp_Formula_t *formula)
785{
786 boolean lCheck;
787 boolean rCheck;
788 Ctlp_Formula_t *leftChild;
789 Ctlp_Formula_t *rightChild;
790 Ctlp_FormulaType type;
791
792 if ( formula == NIL( Ctlp_Formula_t ) ) {
793 return TRUE;
794 }
795
796 type = Ctlp_FormulaReadType( formula );
797
798 if ( ( type == Ctlp_ID_c ) ||
799 ( type == Ctlp_TRUE_c ) ||
800 ( type == Ctlp_FALSE_c ) ) {
801 return TRUE;
802 }
803
804 if ( ( type != Ctlp_OR_c ) &&
805 ( type != Ctlp_AND_c ) &&
806 ( type != Ctlp_NOT_c ) &&
807 ( type != Ctlp_THEN_c ) &&
808 ( type != Ctlp_XOR_c ) &&
809 ( type != Ctlp_EQ_c ) ) {
810 return FALSE;
811 }
812
813 leftChild = Ctlp_FormulaReadLeftChild( formula );
814 lCheck = Ctlp_FormulaTestIsQuantifierFree( leftChild );
815
816 if (lCheck == FALSE)
817 return FALSE;
818
819 rightChild = Ctlp_FormulaReadRightChild( formula );
820 rCheck = Ctlp_FormulaTestIsQuantifierFree( rightChild );
821
822 return rCheck;
823}
824
825
826/**Function********************************************************************
827
828 Synopsis [Annotates the each node in parse tree with its negation
829 parity.]
830
831 Description [This function must be called at the top level with
832 parity = Ctlp_Even_c. It will then annotate each node with its parity.
833 A node in a formula with sharing may have both parities and a descendant
834 of a XOR or EQ node will have both. Only backward CTL formulae are
835 considered.]
836
837 SideEffects [changes the negation_parity fields of all nodes in the formula]
838
839******************************************************************************/
840void
841Ctlp_FormulaNegations(
842 Ctlp_Formula_t * formula,
843 Ctlp_Parity_t parity)
844{
845
846 Ctlp_FormulaType formulaType;
847 Ctlp_Formula_t *leftChild;
848 Ctlp_Formula_t *rightChild;
849 Ctlp_Parity_t newparity;
850
851 assert(formula != NIL(Ctlp_Formula_t));
852 if (formula->negation_parity == parity)
853 return; /* already done */
854 if (formula->negation_parity != Ctlp_NoParity_c)
855 parity = Ctlp_EvenOdd_c; /* reconverging paths with different parity */
856 formula->negation_parity = parity;
857
858 formulaType = Ctlp_FormulaReadType(formula);
859 leftChild = Ctlp_FormulaReadLeftChild(formula);
860 rightChild = Ctlp_FormulaReadRightChild(formula);
861
862 switch (formulaType) {
863 case Ctlp_AX_c:
864 case Ctlp_AG_c:
865 case Ctlp_AF_c:
866 case Ctlp_EX_c:
867 case Ctlp_EG_c:
868 case Ctlp_EF_c:
869 Ctlp_FormulaNegations(leftChild,parity);
870 break;
871 case Ctlp_AU_c:
872 case Ctlp_EU_c:
873 case Ctlp_OR_c:
874 case Ctlp_AND_c:
875 Ctlp_FormulaNegations(leftChild,parity);
876 Ctlp_FormulaNegations(rightChild,parity);
877 break;
878 case Ctlp_NOT_c:
879 if (parity == Ctlp_Even_c)
880 newparity = Ctlp_Odd_c;
881 else if (parity == Ctlp_Odd_c)
882 newparity = Ctlp_Even_c;
883 else newparity = Ctlp_EvenOdd_c;
884 Ctlp_FormulaNegations(leftChild,newparity);
885 break;
886 case Ctlp_THEN_c:
887 if (parity == Ctlp_Even_c)
888 newparity = Ctlp_Odd_c;
889 else if (parity == Ctlp_Odd_c)
890 newparity = Ctlp_Even_c;
891 else newparity = Ctlp_EvenOdd_c;
892 Ctlp_FormulaNegations(leftChild,newparity);
893 Ctlp_FormulaNegations(rightChild,parity);
894 break;
895 case Ctlp_XOR_c:
896 case Ctlp_EQ_c:
897 Ctlp_FormulaNegations(leftChild,Ctlp_EvenOdd_c);
898 Ctlp_FormulaNegations(rightChild,Ctlp_EvenOdd_c);
899 break;
900 default:
901 break;
902 }
903}
904
905
906/**Function********************************************************************
907
908 Synopsis [Checks whether an ACTL formula is W-ACTL.]
909
910 Description [Test if the binary operators in an ACTL formula have at
911 least one propositional formula as one of the operands. If not return
912 Ctlp_NONWACTL_c, else return either Ctlp_WACTLsimple_c for propositional
913 formulae or Ctlp_WACTLstate_c for formulae containing temporal operators.
914 A W-ACTL formula must contain no exitential operators and no forward
915 operators. XOR and EQ are allowed only in propositional subformulae.]
916
917 SideEffects [none]
918
919******************************************************************************/
920Ctlp_FormulaACTLSubClass
921Ctlp_CheckIfWACTL(
922 Ctlp_Formula_t *formula)
923{
924 Ctlp_FormulaType formulaType;
925 Ctlp_Formula_t *rightFormula, *leftFormula;
926 Ctlp_FormulaACTLSubClass resultLeft, resultRight;
927
928 assert(formula != NIL(Ctlp_Formula_t));
929 if(formula == NIL(Ctlp_Formula_t))
930 return Ctlp_WACTLsimple_c;
931
932 formulaType = Ctlp_FormulaReadType(formula);
933 leftFormula = Ctlp_FormulaReadLeftChild(formula);
934 rightFormula = Ctlp_FormulaReadRightChild(formula);
935
936 /* Depending on the formula type, create result or recur. */
937 switch (formulaType) {
938 case Ctlp_AX_c:
939 case Ctlp_AG_c:
940 case Ctlp_AF_c:
941 resultLeft = Ctlp_CheckIfWACTL(leftFormula);
942 if (resultLeft == Ctlp_NONWACTL_c)
943 return Ctlp_NONWACTL_c;
944 else
945 return Ctlp_WACTLstate_c;
946 break;
947 case Ctlp_AU_c:
948 resultLeft = Ctlp_CheckIfWACTL(leftFormula);
949 if (resultLeft == Ctlp_NONWACTL_c)
950 return Ctlp_NONWACTL_c;
951 resultRight = Ctlp_CheckIfWACTL(rightFormula);
952 if (resultRight == Ctlp_NONWACTL_c)
953 return Ctlp_NONWACTL_c;
954 if (resultLeft == Ctlp_WACTLsimple_c || resultRight == Ctlp_WACTLsimple_c)
955 return Ctlp_WACTLstate_c;
956 else
957 return Ctlp_NONWACTL_c;
958 break;
959 case Ctlp_OR_c:
960 case Ctlp_AND_c:
961 case Ctlp_THEN_c:
962 resultLeft = Ctlp_CheckIfWACTL(leftFormula);
963 if (resultLeft == Ctlp_NONWACTL_c) {
964 return Ctlp_NONWACTL_c;
965 } else {
966 resultRight = Ctlp_CheckIfWACTL(rightFormula);
967 if (resultRight == Ctlp_WACTLsimple_c) {
968 return resultLeft;
969 } else if (resultLeft == Ctlp_WACTLsimple_c) {
970 return resultRight;
971 } else {
972 return Ctlp_NONWACTL_c;
973 }
974 }
975 break;
976 case Ctlp_NOT_c:
977 resultLeft = Ctlp_CheckIfWACTL(leftFormula);
978 return resultLeft;
979 break;
980 case Ctlp_XOR_c:
981 case Ctlp_EQ_c:
982 resultLeft = Ctlp_CheckIfWACTL(leftFormula);
983 if (resultLeft != Ctlp_WACTLsimple_c) {
984 return Ctlp_NONWACTL_c;
985 } else {
986 resultRight = Ctlp_CheckIfWACTL(rightFormula);
987 if (resultRight == Ctlp_WACTLsimple_c)
988 return Ctlp_WACTLsimple_c;
989 else
990 return Ctlp_NONWACTL_c;
991 }
992 break;
993 case Ctlp_ID_c:
994 case Ctlp_TRUE_c:
995 case Ctlp_FALSE_c:
996 return Ctlp_WACTLsimple_c;
997 break;
998 default:
999 fprintf(vis_stderr, "#Ctlp Result : The formula should be in Universal operators!\n");
1000 return Ctlp_NONWACTL_c;
1001 break;
1002 }
1003} /* End of Ctlp_CheckTypeOfExistentialFormula */
1004
1005
1006/**Function********************************************************************
1007
1008 Synopsis [Returns original formula corresponding to converted formula.]
1009
1010 SideEffects []
1011
1012******************************************************************************/
1013Ctlp_Formula_t *
1014Ctlp_FormulaReadOriginalFormula(
1015 Ctlp_Formula_t * formula)
1016{
1017 return formula->dbgInfo.originalFormula;
1018}
1019
1020
1021/**Function********************************************************************
1022
1023 Synopsis [Frees a formula if no other formula refers to it as a
1024 sub-formula.]
1025
1026 Description [The function decrements the refCount of the formula. As a
1027 consequence, if the refCount becomes 0, the formula is freed.]
1028
1029 SideEffects []
1030
1031 SeeAlso [CtlpFormulaFree, CtlpDecrementRefCount]
1032
1033******************************************************************************/
1034void
1035Ctlp_FormulaFree(
1036 Ctlp_Formula_t *formula)
1037{
1038 CtlpFormulaDecrementRefCount(formula);
1039}
1040
1041/**Function********************************************************************
1042
1043 Synopsis [Recursively frees states, underapprox and overapprox fields of
1044 Ctlp_Formula_t, and the debug data]
1045
1046 Description []
1047
1048 SideEffects []
1049
1050 SeeAlso [Ctlp_FormulaFree]
1051
1052******************************************************************************/
1053void
1054Ctlp_FlushStates(
1055 Ctlp_Formula_t * formula)
1056{
1057 if (formula != NIL(Ctlp_Formula_t)) {
1058
1059 if (formula->type != Ctlp_ID_c){
1060 if (formula->left != NIL(Ctlp_Formula_t)) {
1061 Ctlp_FlushStates(formula->left);
1062 }
1063 if (formula->right != NIL(Ctlp_Formula_t)) {
1064 Ctlp_FlushStates(formula->right);
1065 }
1066 }
1067
1068 if (formula->states != NIL(mdd_t)){
1069 mdd_free(formula->states);
1070 formula->states = NIL(mdd_t);
1071 }
1072 if (formula->underapprox != NIL(mdd_t)){
1073 mdd_free(formula->underapprox);
1074 formula->underapprox = NIL(mdd_t);
1075 }
1076 if (formula->overapprox != NIL(mdd_t)){
1077 mdd_free(formula->overapprox);
1078 formula->overapprox = NIL(mdd_t);
1079 }
1080
1081 if (formula->dbgInfo.data != NIL(void)){
1082 (*formula->dbgInfo.freeFn)(formula);
1083 formula->dbgInfo.data = NIL(void);
1084 }
1085
1086 }
1087
1088}
1089
1090/**Function********************************************************************
1091
1092
1093 Synopsis [Duplicates a CTL formula.]
1094
1095 Description [Recursively duplicate a formula. Does nothing if the formula
1096 is NIL. Does not copy mdd for states, underapprox, overapprox, dbgInfo, and
1097 in general all the information that is used to annotate the formula.]
1098
1099 SideEffects []
1100
1101 SeeAlso []
1102
1103******************************************************************************/
1104Ctlp_Formula_t *
1105Ctlp_FormulaDup(
1106 Ctlp_Formula_t * formula)
1107{
1108 Ctlp_Formula_t *result = NIL(Ctlp_Formula_t);
1109
1110 if ( formula == NIL(Ctlp_Formula_t)) {
1111 return NIL(Ctlp_Formula_t);
1112 }
1113
1114 result = ALLOC(Ctlp_Formula_t, 1);
1115
1116 result->type = formula->type;
1117 result->states = NIL(mdd_t);
1118 result->underapprox = NIL(mdd_t);
1119 result->overapprox = NIL(mdd_t);
1120 result->latest = Ctlp_Incomparable_c;
1121 result->Bottomstates = NIL(array_t);
1122 result->Topstates = NIL(array_t);
1123 result->negation_parity = Ctlp_NoParity_c;
1124 result->leaves = formula->leaves == NIL(array_t) ?
1125 NIL(array_t) : array_dup(formula->leaves);
1126 result->matchfound_top = NIL(array_t);
1127 result->matchelement_top = NIL(array_t);
1128 result->matchfound_bot = NIL(array_t);
1129 result->matchelement_bot = NIL(array_t);
1130 result->refCount = 1;
1131 result->dbgInfo.data = NIL(void);
1132 result->dbgInfo.freeFn = (Ctlp_DbgInfoFreeFn) NULL;
1133 result->dbgInfo.convertedFlag = FALSE;
1134 result->dbgInfo.originalFormula = NIL(Ctlp_Formula_t);
1135 result->top = 0;
1136 result->compareValue = 0;
1137
1138 if ( formula->type != Ctlp_ID_c ) {
1139 result->left = Ctlp_FormulaDup( formula->left );
1140 result->right = Ctlp_FormulaDup( formula->right );
1141 }
1142 else {
1143 result->left = (Ctlp_Formula_t *) util_strsav((char *)formula->left );
1144 result->right = (Ctlp_Formula_t *) util_strsav((char *)formula->right );
1145 }
1146 result->share = 1;
1147 result->BotOnionRings = NIL(array_t);
1148 result->TopOnionRings = NIL(array_t);
1149 return result;
1150}
1151
1152/**Function********************************************************************
1153
1154
1155 Synopsis [Complements a CTL formula.]
1156
1157 Description []
1158
1159 SideEffects []
1160
1161 SeeAlso []
1162
1163******************************************************************************/
1164Ctlp_Formula_t *
1165Ctlp_FormulaConverttoComplement(
1166 Ctlp_Formula_t * formula)
1167{
1168 Ctlp_Formula_t *result;
1169
1170 if (formula == NIL(Ctlp_Formula_t)) {
1171 return NIL(Ctlp_Formula_t);
1172 }
1173 result = Ctlp_FormulaCreate(Ctlp_NOT_c,formula,NIL(Ctlp_Formula_t));
1174 CtlpFormulaIncrementRefCount(formula);
1175#if 0
1176 result = FormulaCreateWithType(Ctlp_NOT_c);
1177 result->left = FormulaCreateWithType(formula->type);
1178 result->left->left = formula->left;
1179 result->left->right = formula->right;
1180 switch (formula->type) {
1181 case Ctlp_ID_c:
1182 case Ctlp_TRUE_c:
1183 case Ctlp_FALSE_c:
1184 case Ctlp_Init_c:
1185 break;
1186 default:
1187 CtlpFormulaIncrementRefCount(formula->left);
1188 CtlpFormulaIncrementRefCount(formula->right);
1189 break;
1190 }
1191#endif
1192 return result;
1193} /* Ctlp_FormulaConverttoComplement */
1194
1195
1196/**Function********************************************************************
1197
1198
1199 Synopsis [Converts AFp to A (TRUE) U p.]
1200
1201 Description []
1202
1203 SideEffects [Should be called only for AF formula]
1204
1205 SeeAlso []
1206
1207******************************************************************************/
1208Ctlp_Formula_t *
1209Ctlp_FormulaConvertAFtoAU(
1210 Ctlp_Formula_t * formula)
1211{
1212 Ctlp_Formula_t *result;
1213 /* AFf --> (A true U f) */
1214 assert(formula->type == Ctlp_AF_c);
1215 result = FormulaCreateWithType(Ctlp_AU_c);
1216 result->left = FormulaCreateWithType(Ctlp_TRUE_c);
1217 result->right = formula->left;
1218 CtlpFormulaIncrementRefCount(formula->left);
1219 return result;
1220}
1221
1222
1223/**Function********************************************************************
1224
1225
1226 Synopsis [Converts EFp to p + EX(EFp).]
1227
1228 Description []
1229
1230 SideEffects [Should be called only for EF formula]
1231
1232 SeeAlso []
1233
1234******************************************************************************/
1235Ctlp_Formula_t *
1236Ctlp_FormulaConvertEFtoOR(
1237 Ctlp_Formula_t * formula)
1238{
1239 Ctlp_Formula_t *result;
1240 /* EFf --> f + EX(EF(f)) */
1241 assert(formula->type == Ctlp_EF_c);
1242 result = FormulaCreateWithType(Ctlp_OR_c);
1243 result->left = formula->left;
1244 result->right = FormulaCreateWithType(Ctlp_EX_c);
1245 result->right->left = formula;
1246 CtlpFormulaIncrementRefCount(formula->left);
1247 CtlpFormulaIncrementRefCount(formula);
1248 return result;
1249}
1250
1251
1252/**Function********************************************************************
1253
1254
1255 Synopsis [Converts EpUq to q + p*EX(EpUq).]
1256
1257 Description []
1258
1259 SideEffects [Should be called only for EU formula]
1260
1261 SeeAlso []
1262
1263******************************************************************************/
1264Ctlp_Formula_t *
1265Ctlp_FormulaConvertEUtoOR(
1266 Ctlp_Formula_t * formula)
1267{
1268 Ctlp_Formula_t *result;
1269 assert(formula->type == Ctlp_EU_c);
1270 /* E(f1)U(f2) --> f2 + f1*EX( E(f1)U(f2) ) */
1271 result = FormulaCreateWithType(Ctlp_OR_c);
1272 result->left = formula->right;
1273 result->right = FormulaCreateWithType(Ctlp_AND_c);
1274 result->right->left = formula->left;
1275 result->right->right = FormulaCreateWithType(Ctlp_EX_c);
1276 result->right->right->left = formula;
1277 CtlpFormulaIncrementRefCount(formula->left);
1278 CtlpFormulaIncrementRefCount(formula->right);
1279 CtlpFormulaIncrementRefCount(formula);
1280 return result;
1281}
1282
1283
1284/**Function********************************************************************
1285
1286
1287 Synopsis [Convert p^q to !p*q + p*!q.]
1288
1289 Description []
1290
1291 SideEffects [Should be called only for XOR formula]
1292
1293 SeeAlso []
1294
1295******************************************************************************/
1296Ctlp_Formula_t *
1297Ctlp_FormulaConvertXORtoOR(
1298 Ctlp_Formula_t * formula)
1299{
1300 Ctlp_Formula_t *result;
1301 assert(formula->type == Ctlp_XOR_c);
1302 result = FormulaCreateWithType(Ctlp_OR_c);
1303 result->left = FormulaCreateWithType(Ctlp_AND_c);
1304 result->right = FormulaCreateWithType(Ctlp_AND_c);
1305 result->left->left = Ctlp_FormulaConverttoComplement(formula->left);
1306 result->left->right = formula->right;
1307 result->right->left = formula->left;
1308 result->right->right = Ctlp_FormulaConverttoComplement(formula->right);
1309 CtlpFormulaIncrementRefCount(formula->left);
1310 CtlpFormulaIncrementRefCount(formula->right);
1311 return result;
1312}
1313
1314
1315/**Function********************************************************************
1316
1317
1318 Synopsis [Converts p<->q to p*q + !p*!q.]
1319
1320 Description []
1321
1322 SideEffects [Should be called only for EQ formula]
1323
1324 SeeAlso []
1325
1326******************************************************************************/
1327Ctlp_Formula_t *
1328Ctlp_FormulaConvertEQtoOR(
1329 Ctlp_Formula_t * formula)
1330{
1331 Ctlp_Formula_t *result;
1332 assert(formula->type == Ctlp_EQ_c);
1333 result = FormulaCreateWithType(Ctlp_OR_c);
1334 result->left = FormulaCreateWithType(Ctlp_AND_c);
1335 result->right = FormulaCreateWithType(Ctlp_AND_c);
1336 result->left->left = formula->left;
1337 result->left->right = formula->right;
1338 result->right->left = Ctlp_FormulaConverttoComplement(formula->left);
1339 result->right->right = Ctlp_FormulaConverttoComplement(formula->right);
1340 CtlpFormulaIncrementRefCount(formula->left);
1341 CtlpFormulaIncrementRefCount(formula->right);
1342 return result;
1343}
1344
1345
1346/**Function********************************************************************
1347
1348 Synopsis [Returns formula with a negation pushed down]
1349
1350 Description [Returns formula with a negation pushed down. It is assumed that
1351 the formula being passsed to it is not a proposition]
1352
1353 SideEffects []
1354
1355******************************************************************************/
1356Ctlp_Formula_t *
1357Ctlp_FormulaPushNegation(
1358 Ctlp_Formula_t * formula)
1359{
1360 Ctlp_Formula_t *result;
1361 if (formula == NIL(Ctlp_Formula_t)) {
1362 return NIL(Ctlp_Formula_t);
1363 }
1364
1365 switch(formula->type) {
1366 /*
1367 * The cases are listed in rough order of their expected frequency.
1368 */
1369 case Ctlp_OR_c: /*!(f1 v f2) = !f1 * !f2*/
1370 result = FormulaCreateWithType(Ctlp_AND_c);
1371 result->left = Ctlp_FormulaConverttoComplement(formula->left);
1372 result->right = Ctlp_FormulaConverttoComplement(formula->right);
1373 break;
1374 case Ctlp_AND_c: /*!(f1 * f2) = !f1 v !f2*/
1375 result = FormulaCreateWithType(Ctlp_OR_c);
1376 result->left = Ctlp_FormulaConverttoComplement(formula->left);
1377 result->right = Ctlp_FormulaConverttoComplement(formula->right);
1378 break;
1379 case Ctlp_THEN_c: /*!(f1 -> f2) = !(!f1 v f2) = f1 * !f2 */
1380 result = FormulaCreateWithType(Ctlp_AND_c);
1381 result->left = formula->left;
1382 CtlpFormulaIncrementRefCount(formula->left);
1383 result->right = Ctlp_FormulaConverttoComplement(formula->right);
1384 break;
1385 case Ctlp_XOR_c: /*!(f1 ^ f2) = f1 <-> f2*/
1386 result = FormulaCreateWithType(Ctlp_EQ_c);
1387 result->left = formula->left;
1388 result->right = formula->right;
1389 CtlpFormulaIncrementRefCount(formula->left);
1390 CtlpFormulaIncrementRefCount(formula->right);
1391 break;
1392 case Ctlp_EQ_c: /*!(f1 <-> f2) = f1 ^ f2*/
1393 result = FormulaCreateWithType(Ctlp_XOR_c);
1394 result->left = formula->left;
1395 result->right = formula->right;
1396 CtlpFormulaIncrementRefCount(formula->left);
1397 CtlpFormulaIncrementRefCount(formula->right);
1398 break;
1399 case Ctlp_NOT_c:/* !(!f1) = f1*/
1400 result = formula->left;
1401 CtlpFormulaIncrementRefCount(formula->left);
1402 break;
1403 case Ctlp_EX_c:/* !(EX(f1)) = AX(!f1)*/
1404 result = FormulaCreateWithType(Ctlp_AX_c);
1405 result->left = Ctlp_FormulaConverttoComplement(formula->left);
1406 break;
1407 case Ctlp_EG_c: /*!(EG(f1)) = AF(!f1)*/
1408 result = FormulaCreateWithType(Ctlp_AF_c);
1409 result->left = Ctlp_FormulaConverttoComplement(formula->left);
1410 break;
1411 case Ctlp_EF_c: /*!(EF(f1)) = AG(!f1)*/
1412 result = FormulaCreateWithType(Ctlp_AG_c);
1413 result->left = Ctlp_FormulaConverttoComplement(formula->left);
1414 break;
1415 case Ctlp_EU_c: /* !(EpUq) = A(!q)U(!(p+q) + AG(!q))*/
1416 result = FormulaCreateWithType(Ctlp_AU_c);
1417 result->left = Ctlp_FormulaConverttoComplement(formula->right);
1418 result->right = FormulaCreateWithType(Ctlp_OR_c);
1419 result->right->left = FormulaCreateWithType(Ctlp_NOT_c);
1420 result->right->left->left = FormulaCreateWithType(Ctlp_OR_c);
1421 result->right->left->left->left = formula->left;
1422 result->right->left->left->right = formula->right;
1423 result->right->right = FormulaCreateWithType(Ctlp_AG_c);
1424 result->right->right->left = Ctlp_FormulaConverttoComplement(formula->right);
1425 CtlpFormulaIncrementRefCount(formula->left);
1426 CtlpFormulaIncrementRefCount(formula->right);
1427 break;
1428 case Ctlp_AX_c:/* !AX(f1) = EX(!f1)*/
1429 result = FormulaCreateWithType(Ctlp_EX_c);
1430 result->left = Ctlp_FormulaConverttoComplement(formula->left);
1431 break;
1432 case Ctlp_AG_c:/* !AG(f1) = EF(!f1) */
1433 result = FormulaCreateWithType(Ctlp_EF_c);
1434 result->left = Ctlp_FormulaConverttoComplement(formula->left);
1435 break;
1436 case Ctlp_AF_c: /* !AF(f1) = EG(!f1)*/
1437 result = FormulaCreateWithType(Ctlp_EG_c);
1438 result->left = Ctlp_FormulaConverttoComplement(formula->left);
1439 break;
1440 case Ctlp_AU_c: /* !(ApUq) = (E(!q)U(!(p+q)))+(EG!q)*/
1441 result = FormulaCreateWithType(Ctlp_OR_c);
1442 result->left = FormulaCreateWithType(Ctlp_EU_c);
1443 result->left->left = Ctlp_FormulaConverttoComplement(formula->right);
1444 result->left->right = FormulaCreateWithType(Ctlp_NOT_c);
1445 result->left->right->left= FormulaCreateWithType(Ctlp_OR_c);
1446 result->left->right->left->left = formula->left;
1447 result->left->right->left->right = formula->right;
1448 result->right = FormulaCreateWithType(Ctlp_EG_c);
1449 result->right->left = Ctlp_FormulaConverttoComplement(formula->right);
1450 CtlpFormulaIncrementRefCount(formula->left);
1451 CtlpFormulaIncrementRefCount(formula->right);
1452 break;
1453 case Ctlp_TRUE_c:/* !TRUE = FALSE*/
1454 result = FormulaCreateWithType(Ctlp_FALSE_c);
1455 break;
1456 case Ctlp_FALSE_c:/*!FALSE = TRUE*/
1457 result = FormulaCreateWithType(Ctlp_TRUE_c);
1458 break;
1459 case Ctlp_Init_c: /* ???*/
1460 case Ctlp_Cmp_c: /* ???*/
1461 /* if (formula->compareValue == 0)
1462 tmpString = util_strcat3("[", s1, "] = ");
1463 else
1464 tmpString = util_strcat3("[", s1, "] != ");
1465 result = util_strcat3(tmpString, s2, "");
1466 break;*/
1467 case Ctlp_FwdU_c: /* ???*/
1468 case Ctlp_FwdG_c: /* ??? */
1469 case Ctlp_EY_c: /* ??? */
1470 result = formula;
1471 break;
1472 default:
1473 fail("Unexpected type");
1474 }
1475
1476 return result;
1477}
1478/*****************************************************************************/
1479
1480/**Function********************************************************************
1481
1482 Synopsis [Frees an array of CTL formulas.]
1483
1484 Description [Calls CtlpFormulaDecrementRefCount on each formula in
1485 formulaArray, and then frees the array itself. It is okay to call this
1486 function with an empty array, but it is an error to call it with a NULL
1487 array.]
1488
1489 SideEffects []
1490
1491 SeeAlso [Ctlp_FormulaFree]
1492
1493******************************************************************************/
1494void
1495Ctlp_FormulaArrayFree(
1496 array_t * formulaArray /* of Ctlp_Formula_t */)
1497{
1498 int i;
1499 int numFormulas = array_n(formulaArray);
1500
1501 assert(formulaArray != NIL(array_t));
1502 for (i = 0; i < numFormulas; i++) {
1503 Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
1504
1505 CtlpFormulaDecrementRefCount(formula);
1506 }
1507
1508 array_free(formulaArray);
1509}
1510
1511
1512/**Function********************************************************************
1513
1514 Synopsis [Converts a CTL formula to existential form.]
1515
1516 Description [Converts a CTL formula to existential form. That is, all
1517 universal path quantifiers are replaced with the appropriate combination of
1518 existential quantifiers and Boolean negation. Also converts "finally"
1519 operators to "until" operators.<p>
1520
1521 <p>Returns a new formula that shares absolutely nothing with the original
1522 formula (not even the strings). Also, the new formula does not have any MDDs
1523 associated with it. The "originalFormula" field of each new subformula is
1524 set to point to the formula passed as an argument. In addition, if (and only
1525 if) the original formula is of type AG, AX, AU, AF, or EF, the "converted
1526 flag" is set. Returns NULL if called with a NULL formula.
1527
1528 <p>Note: the debugger takes advantage of the exact way that the conversion is
1529 done. Hence, you cannot play around much with the syntax of the converted
1530 formula.
1531
1532 <p>A list of conversion rules shouls be included here (RB).
1533
1534 <br> AG phi turns into !EU(true,! phi'), where the top ! has converted set
1535 and points to the AG, and phi' points to phi.
1536
1537 <br> AU?
1538
1539 <br> AX?
1540
1541 <br> Any others?
1542 ]
1543
1544 SideEffects []
1545
1546
1547 SeeAlso [Ctlp_FormulaArrayConvertToExistentialForm,
1548 Ctlp_ConvertToSimpleExistentialForm]
1549
1550******************************************************************************/
1551Ctlp_Formula_t *
1552Ctlp_FormulaConvertToExistentialForm(
1553 Ctlp_Formula_t * formula)
1554{
1555 Ctlp_Formula_t *new_;
1556 char *variableNameCopy, *valueNameCopy;
1557
1558 if (formula == NIL(Ctlp_Formula_t)) {
1559 return NIL(Ctlp_Formula_t);
1560 }
1561
1562 /*
1563 * Recursively convert each subformula.
1564 */
1565
1566 switch(formula->type) {
1567 case Ctlp_EF_c:
1568 /* EFf --> (E true U f) */
1569 new_ = FormulaCreateWithType(Ctlp_EU_c);
1570 new_->left = FormulaCreateWithType(Ctlp_TRUE_c);
1571 new_->right = Ctlp_FormulaConvertToExistentialForm(formula->left);
1572 new_->dbgInfo.convertedFlag = TRUE;
1573 break;
1574
1575 case Ctlp_AX_c:
1576 /* AXf --> !(EX(!f)) */
1577 new_ = FormulaCreateWithType(Ctlp_NOT_c);
1578 new_->left = FormulaCreateWithType(Ctlp_EX_c);
1579 new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
1580 new_->left->left->left = Ctlp_FormulaConvertToExistentialForm(formula->left);
1581 new_->dbgInfo.convertedFlag = TRUE;
1582 break;
1583
1584 case Ctlp_AG_c:
1585 /* AGf --> ![(E true U !f)] */
1586 new_ = FormulaCreateWithType(Ctlp_NOT_c);
1587 new_->left = FormulaCreateWithType(Ctlp_EU_c);
1588 new_->left->left = FormulaCreateWithType(Ctlp_TRUE_c);
1589 new_->left->right = FormulaCreateWithType(Ctlp_NOT_c);
1590 new_->left->right->left = Ctlp_FormulaConvertToExistentialForm(formula->left);
1591 new_->dbgInfo.convertedFlag = TRUE;
1592 break;
1593
1594 case Ctlp_AF_c:
1595 /* AFf --> ![EG(!f)] */
1596 new_ = FormulaCreateWithType(Ctlp_NOT_c);
1597 new_->left = FormulaCreateWithType(Ctlp_EG_c);
1598 new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
1599 new_->left->left->left = Ctlp_FormulaConvertToExistentialForm(formula->left);
1600 new_->dbgInfo.convertedFlag = TRUE;
1601 break;
1602
1603 case Ctlp_AU_c:
1604 /* A[fUg] --> !((E[!g U (!f*!g)]) + (EG!g)) */
1605
1606 new_ = FormulaCreateWithType(Ctlp_NOT_c); /* top */
1607 new_->left = FormulaCreateWithType(Ctlp_OR_c); /* ((E[!g U (!f*!g)]) + (EG!g)) */
1608
1609 new_->left->right = FormulaCreateWithType(Ctlp_EG_c); /* EG !g */
1610 new_->left->right->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
1611 new_->left->right->left->left = Ctlp_FormulaConvertToExistentialForm(formula->right); /* g */
1612
1613 new_->left->left = FormulaCreateWithType(Ctlp_EU_c); /* E[!g U (!f*!g)] */
1614 new_->left->left->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
1615 new_->left->left->left->left = Ctlp_FormulaConvertToExistentialForm(formula->right); /* g */
1616 new_->left->left->right = FormulaCreateWithType(Ctlp_AND_c); /* !f*!g */
1617 new_->left->left->right->left = FormulaCreateWithType(Ctlp_NOT_c); /* !f */
1618 new_->left->left->right->left->left = Ctlp_FormulaConvertToExistentialForm(formula->left); /* f */
1619 new_->left->left->right->right = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
1620 new_->left->left->right->right->left = Ctlp_FormulaConvertToExistentialForm(formula->right); /* g */
1621 new_->dbgInfo.convertedFlag = TRUE;
1622 break;
1623
1624 case Ctlp_ID_c:
1625 /* Make a copy of the name, and create a new formula. */
1626 variableNameCopy = util_strsav((char *)(formula->left));
1627 valueNameCopy = util_strsav((char *)(formula->right));
1628 new_ = Ctlp_FormulaCreate(Ctlp_ID_c, variableNameCopy, valueNameCopy);
1629 break;
1630
1631 case Ctlp_THEN_c:
1632 case Ctlp_EX_c:
1633 case Ctlp_EG_c:
1634 case Ctlp_EU_c:
1635 case Ctlp_OR_c:
1636 case Ctlp_AND_c:
1637 case Ctlp_NOT_c:
1638 case Ctlp_XOR_c:
1639 case Ctlp_EQ_c:
1640 case Ctlp_TRUE_c:
1641 case Ctlp_FALSE_c:
1642 /* These are already in the correct form. Just convert subformulas. */
1643 new_ = FormulaCreateWithType(formula->type);
1644 new_->left = Ctlp_FormulaConvertToExistentialForm(formula->left);
1645 new_->right = Ctlp_FormulaConvertToExistentialForm(formula->right);
1646 break;
1647
1648 default:
1649 fail("Unexpected type");
1650 }
1651
1652 new_->dbgInfo.originalFormula = formula;
1653 return new_;
1654}
1655
1656/**Function********************************************************************
1657
1658 Synopsis [Converts a CTL formula to simple existential form.]
1659
1660 Description [Converts a CTL formula to simple existential form.
1661 That is, all universal path quantifiers are replaced with the
1662 appropriate combination of existential quantifiers and Boolean
1663 negation. Only `NOT' and `AND' Boolean operators are allowed. Also
1664 converts "finally" operators to "until" operators.
1665
1666 The converted bit is set in the converted formula only when temporal
1667 operators are converted, not when boolean operators are converted.
1668
1669 A new formula is created that needs to be freed seperately.]
1670
1671 SideEffects []
1672
1673 Remarks [Ctl formulas in simple existential form are incompatible
1674 with the mc debug routines. The reason is that the debug routines
1675 count on a very specific form of the converted formula to conclude
1676 what the original formula was.]
1677
1678 SeeAlso [Ctlp_FormulaArrayConvertToExistentialForm]
1679
1680******************************************************************************/
1681Ctlp_Formula_t *
1682Ctlp_FormulaConvertToSimpleExistentialForm(
1683 Ctlp_Formula_t * formula)
1684{
1685 Ctlp_Formula_t *new_;
1686 char *variableNameCopy, *valueNameCopy;
1687
1688 if (formula == NIL(Ctlp_Formula_t)) {
1689 return NIL(Ctlp_Formula_t);
1690 }
1691
1692 /*
1693 * Recursively convert each subformula.
1694 */
1695
1696 switch(formula->type) {
1697 case Ctlp_EF_c:
1698 /* EFf --> (E true U f) */
1699 new_ = FormulaCreateWithType(Ctlp_EU_c);
1700 new_->left = FormulaCreateWithType(Ctlp_TRUE_c);
1701 new_->right = Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1702 new_->dbgInfo.convertedFlag = TRUE;
1703 break;
1704
1705 case Ctlp_AX_c:
1706 /* AXf --> !(EX(!f)) */
1707 new_ = FormulaCreateWithType(Ctlp_NOT_c);
1708 new_->left = FormulaCreateWithType(Ctlp_EX_c);
1709 new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
1710 new_->left->left->left =
1711 Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1712 new_->dbgInfo.convertedFlag = TRUE;
1713 break;
1714
1715 case Ctlp_AG_c:
1716 /* AGf --> ![(E true U !f)] */
1717 new_ = FormulaCreateWithType(Ctlp_NOT_c);
1718 new_->left = FormulaCreateWithType(Ctlp_EU_c);
1719 new_->left->left = FormulaCreateWithType(Ctlp_TRUE_c);
1720 new_->left->right = FormulaCreateWithType(Ctlp_NOT_c);
1721 new_->left->right->left =
1722 Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1723 new_->dbgInfo.convertedFlag = TRUE;
1724 break;
1725
1726 case Ctlp_AF_c:
1727 /* AFf --> ![EG(!f)] */
1728 new_ = FormulaCreateWithType(Ctlp_NOT_c);
1729 new_->left = FormulaCreateWithType(Ctlp_EG_c);
1730 new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
1731 new_->left->left->left = Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1732 new_->dbgInfo.convertedFlag = TRUE;
1733 break;
1734
1735 case Ctlp_AU_c:
1736 /* A[fUg] --> !(E[!g U (!f*!g)]) * !(EG!g)) */
1737
1738 new_ = FormulaCreateWithType(Ctlp_AND_c); /* top */
1739 new_->left = FormulaCreateWithType(Ctlp_NOT_c);
1740 new_->right = FormulaCreateWithType(Ctlp_NOT_c);
1741 new_->left->left = FormulaCreateWithType(Ctlp_EG_c); /* EG !g */
1742 new_->left->left->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
1743 new_->left->left->left->left =
1744 Ctlp_FormulaConvertToSimpleExistentialForm(formula->right); /* g */
1745
1746 new_->right->left = FormulaCreateWithType(Ctlp_EU_c); /* E[!g U (!f*!g)] */
1747 new_->right->left->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
1748 new_->right->left->left->left =
1749 Ctlp_FormulaConvertToSimpleExistentialForm(formula->right); /* g */
1750 new_->right->left->right = FormulaCreateWithType(Ctlp_AND_c); /* !f*!g */
1751 new_->right->left->right->left = FormulaCreateWithType(Ctlp_NOT_c); /* !f */
1752 new_->right->left->right->left->left =
1753 Ctlp_FormulaConvertToSimpleExistentialForm(formula->left); /* f */
1754 new_->right->left->right->right = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
1755 new_->right->left->right->right->left =
1756 Ctlp_FormulaConvertToSimpleExistentialForm(formula->right); /* g */
1757 new_->dbgInfo.convertedFlag = TRUE;
1758 break;
1759
1760 case Ctlp_ID_c:
1761 /* Make a copy of the name, and create a new formula. */
1762 variableNameCopy = util_strsav((char *)(formula->left));
1763 valueNameCopy = util_strsav((char *)(formula->right));
1764 new_ = Ctlp_FormulaCreate(Ctlp_ID_c, variableNameCopy, valueNameCopy);
1765 break;
1766
1767 /* RB: I think THEN (and also OR, and maybe some others) should also have converted set. */
1768 case Ctlp_THEN_c:
1769 /* p->q --> !(p * !q) */
1770 new_ = FormulaCreateWithType(Ctlp_NOT_c);
1771 new_->left = FormulaCreateWithType(Ctlp_AND_c);
1772 new_->left->left =
1773 Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1774 new_->left->right = FormulaCreateWithType(Ctlp_NOT_c);
1775 new_->left->right->left =
1776 Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
1777 break;
1778
1779 case Ctlp_EX_c:
1780 case Ctlp_EG_c:
1781 case Ctlp_EU_c:
1782 case Ctlp_AND_c:
1783 case Ctlp_NOT_c:
1784 case Ctlp_TRUE_c:
1785 case Ctlp_FALSE_c:
1786 /* These are already in the correct form. Just convert subformulas. */
1787 new_ = FormulaCreateWithType(formula->type);
1788 new_->left = Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1789 new_->right = Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
1790 break;
1791
1792 case Ctlp_OR_c:
1793 /* p + q --> !(!p * !q) */
1794 new_ = FormulaCreateWithType(Ctlp_NOT_c);
1795 new_->left = FormulaCreateWithType(Ctlp_AND_c);
1796 new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
1797 new_->left->right = FormulaCreateWithType(Ctlp_NOT_c);
1798 new_->left->left->left =
1799 Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1800 new_->left->right->left =
1801 Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
1802 break;
1803 case Ctlp_XOR_c:
1804 /* p ^ q --> !(p * q) * !(!p * !q) */
1805 new_ = FormulaCreateWithType(Ctlp_AND_c);
1806 new_->left = FormulaCreateWithType(Ctlp_NOT_c);
1807 new_->left->left = FormulaCreateWithType(Ctlp_AND_c);
1808 new_->left->left->left =
1809 Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1810 new_->left->left->right =
1811 Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
1812 new_->right = FormulaCreateWithType(Ctlp_NOT_c);
1813 new_->right->left = FormulaCreateWithType(Ctlp_AND_c);
1814 new_->right->left->left = FormulaCreateWithType(Ctlp_NOT_c);
1815 new_->right->left->left->left =
1816 Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1817 new_->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
1818 new_->right->left->right->left =
1819 Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
1820 break;
1821
1822 case Ctlp_EQ_c:
1823 /* p <-> q --> !(p * !q) * !(!p * q) */
1824 new_ = FormulaCreateWithType(Ctlp_AND_c);
1825 new_->left = FormulaCreateWithType(Ctlp_NOT_c);
1826 new_->left->left = FormulaCreateWithType(Ctlp_AND_c);
1827 new_->left->left->left =
1828 Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1829 new_->left->left->right = FormulaCreateWithType(Ctlp_NOT_c);
1830 new_->left->left->right->left =
1831 Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
1832 new_->right = FormulaCreateWithType(Ctlp_NOT_c);
1833 new_->right->left = FormulaCreateWithType(Ctlp_AND_c);
1834 new_->right->left->left = FormulaCreateWithType(Ctlp_NOT_c);
1835 new_->right->left->left->left =
1836 Ctlp_FormulaConvertToSimpleExistentialForm(formula->left);
1837 new_->right->left->right =
1838 Ctlp_FormulaConvertToSimpleExistentialForm(formula->right);
1839 break;
1840
1841 default:
1842 fail("Unexpected type");
1843 }
1844
1845 new_->dbgInfo.originalFormula = formula;
1846 return new_;
1847}
1848
1849/**Function********************************************************************
1850
1851 Synopsis [Converts an array of CTL formulas to existential form.]
1852
1853 Description [Calls Ctlp_FormulaConvertToExistentialForm on each formula. It
1854 is okay to call this function with an empty array (in which case an empty
1855 array is returned), but it is an error to call it with a NULL array.
1856
1857 All formulas in the array are copied, and hence Ctlp_FormulaArrayFree() needs
1858 to be called on the result at the end.]
1859
1860 SideEffects []
1861
1862 SeeAlso [Ctlp_FormulaConvertToExistentialForm]
1863
1864******************************************************************************/
1865array_t *
1866Ctlp_FormulaArrayConvertToExistentialFormTree(
1867 array_t * formulaArray /* of Ctlp_Formula_t */)
1868{
1869 int i;
1870 int numFormulas = array_n(formulaArray);
1871 array_t *convertedArray = array_alloc(Ctlp_Formula_t *, numFormulas);
1872
1873 assert(formulaArray != NIL(array_t));
1874
1875 for (i = 0; i < numFormulas; i++) {
1876 Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
1877 Ctlp_Formula_t *convertedFormula = Ctlp_FormulaConvertToExistentialForm(formula);
1878
1879 array_insert(Ctlp_Formula_t *, convertedArray, i, convertedFormula);
1880 }
1881
1882 return convertedArray;
1883}
1884
1885/**Function********************************************************************
1886
1887 Synopsis [Converts an array of CTL formulas to simple existential form.]
1888
1889 Description [Calls Ctlp_FormulaConvertToSimpleExistentialForm on
1890 each formula. It is okay to call this function with an empty array
1891 (in which case an empty array is returned), but it is an error to
1892 call it with a NULL array.]
1893
1894 SideEffects []
1895
1896 SeeAlso [Ctlp_FormulaConvertToExistentialForm]
1897
1898******************************************************************************/
1899array_t *
1900Ctlp_FormulaArrayConvertToSimpleExistentialFormTree(
1901 array_t * formulaArray /* of Ctlp_Formula_t */)
1902{
1903 int i;
1904 int numFormulas;
1905 array_t *convertedArray;
1906
1907 assert( formulaArray != NIL(array_t));
1908
1909 numFormulas = array_n(formulaArray);
1910 convertedArray = array_alloc(Ctlp_Formula_t *, numFormulas);
1911
1912 for (i = 0; i < numFormulas; i++) {
1913 Ctlp_Formula_t *formula;
1914 Ctlp_Formula_t *convertedFormula;
1915
1916 formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
1917 convertedFormula = Ctlp_FormulaConvertToSimpleExistentialForm(formula);
1918
1919 array_insert(Ctlp_Formula_t *, convertedArray, i, convertedFormula);
1920 }
1921
1922 return convertedArray;
1923}
1924
1925/**Function********************************************************************
1926
1927 Synopsis [Converts an array of CTL formulae to a multi-rooted DAG.]
1928
1929 Description [The function hashes each subformula of a formula
1930 (including the formula itself) into a uniqueTable. It returns an
1931 array containing the roots of the multi-rooted DAG thus created by
1932 the sharing of the subformulae. It is okay to call this function
1933 with an empty array (in which case an empty array is returned), but
1934 it is an error to call it with a NULL array.]
1935
1936 SideEffects [A formula in formulaArray might be freed if it had been
1937 encountered as a subformula of some other formula. Other formulae in
1938 formulaArray might be present in the returned array. Therefore, the
1939 formulae in formulaArray should not be freed. Only formulaArray
1940 itself should be freed.
1941
1942
1943
1944 RB: What does that mean?
1945
1946 I understand this as follows. Copies of the formulae are not made,
1947 but rather pointers to the argument subformulae are kept. Hence, not only
1948 should the formulae in the result not be freed, but also you cannot free the
1949 argument before you are done with the result. Furthermore, by invocation of
1950 this function, the argument gets altered. It is still valid, but pointers
1951 may have changed. Is this correct?
1952
1953
1954 RB rewrite: A formula in formulaArray is freed if it is encountered as a
1955 subformula of some other formula. Other formulae in formulaArray might be
1956 present in the returned array. Therefore, the formulae in formulaArray should
1957 not be freed. Only formulaArray itself should be freed.]
1958
1959 SeeAlso []
1960
1961******************************************************************************/
1962array_t *
1963Ctlp_FormulaArrayConvertToDAG(
1964 array_t *formulaArray)
1965{
1966 int i;
1967 Ctlp_Formula_t *formula, *uniqueFormula;
1968 st_table *uniqueTable = st_init_table(FormulaCompare, FormulaHash);
1969 int numFormulae = array_n(formulaArray);
1970 array_t *rootsOfFormulaDAG = array_alloc(Ctlp_Formula_t *, numFormulae);
1971
1972 assert(formulaArray != NIL(array_t));
1973
1974 for(i=0; i < numFormulae; i++) {
1975 formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
1976 uniqueFormula = FormulaHashIntoUniqueTable(formula, uniqueTable);
1977 if(uniqueFormula != formula) {
1978 CtlpFormulaDecrementRefCount(formula);
1979 CtlpFormulaIncrementRefCount(uniqueFormula);
1980 array_insert(Ctlp_Formula_t *, rootsOfFormulaDAG, i, uniqueFormula);
1981 }
1982 else
1983 array_insert(Ctlp_Formula_t *, rootsOfFormulaDAG, i, formula);
1984 }
1985 st_free_table(uniqueTable);
1986 return rootsOfFormulaDAG;
1987}
1988
1989/**Function********************************************************************
1990
1991 Synopsis [Converts a DAG of CTL formulae to a DAG of existential CTL
1992 formulae.]
1993
1994 Description [The function converts a DAG of CTL formulae to a DAG of
1995 existential CTL formulae. The function recursively converts each
1996 subformula of each of the formulae in the DAG and remembers the
1997 converted formula in the field states. It is okay to call this
1998 function with an empty array (in which case an empty array is
1999 returned), but it is an error to call it with a NULL array.
2000
2001 The states fileds in the formula need to be NULL.]
2002
2003 SideEffects []
2004
2005 SeeAlso [FormulaConvertToExistentialDAG]
2006
2007******************************************************************************/
2008array_t *
2009Ctlp_FormulaDAGConvertToExistentialFormDAG(
2010 array_t *formulaDAG)
2011{
2012 int i;
2013 Ctlp_Formula_t *formula;
2014 int numFormulae = array_n(formulaDAG);
2015 array_t *existentialFormulaDAG = array_alloc(Ctlp_Formula_t *, numFormulae);
2016
2017 assert( formulaDAG != NIL(array_t));
2018
2019 for(i=0; i<numFormulae; i++) {
2020 formula = array_fetch(Ctlp_Formula_t *, formulaDAG, i);
2021 array_insert(Ctlp_Formula_t *, existentialFormulaDAG, i,
2022 FormulaConvertToExistentialDAG(formula));
2023 }
2024 for(i=0; i<numFormulae; i++) {
2025 formula = array_fetch(Ctlp_Formula_t *, formulaDAG, i);
2026 CtlpFormulaSetStatesToNULL(formula);
2027 }
2028 return existentialFormulaDAG;
2029}
2030
2031
2032/**Function********************************************************************
2033
2034 Synopsis [Creates a CTL formula with the specified fields.]
2035
2036 Description [Allocates a Ctlp_Formula_t, and sets the 2 fields given as
2037 arguments. If the type is Ctlp_ID_c, then the left and right fields
2038 should contain a pointer to a variable name and a pointer to a value
2039 respectively. Otherwise, the two fields point to subformulas. refCount is
2040 set to 1. The states field is set to NULL, the converted flag is set to
2041 FALSE, and the originalFormula field is set to NULL.]
2042
2043 Comment []
2044
2045 SideEffects []
2046
2047 SeeAlso [CtlpFormulaDecrementRefCount]
2048
2049******************************************************************************/
2050Ctlp_Formula_t *
2051Ctlp_FormulaCreate(
2052 Ctlp_FormulaType type,
2053 void * left,
2054 void * right)
2055{
2056 Ctlp_Formula_t *formula = ALLOC(Ctlp_Formula_t, 1);
2057
2058 formula->type = type;
2059 formula->left = (Ctlp_Formula_t *)left;
2060 formula->right = (Ctlp_Formula_t *)right;
2061 formula->refCount = 1;
2062 formula->states = NIL(mdd_t);
2063 formula->underapprox = NIL(mdd_t);
2064 formula->overapprox = NIL(mdd_t);
2065 formula->Topstates = NIL(array_t);
2066 formula->Bottomstates = NIL(array_t);
2067 formula->leaves = NIL(array_t);
2068 formula->matchfound_top = NIL(array_t);
2069 formula->matchelement_top = NIL(array_t);
2070 formula->matchfound_bot = NIL(array_t);
2071 formula->matchelement_bot = NIL(array_t);
2072 formula->negation_parity = Ctlp_NoParity_c;
2073 formula->share = 1;
2074 formula->dbgInfo.data = NIL(void);
2075 formula->dbgInfo.freeFn = (Ctlp_DbgInfoFreeFn) NULL;
2076 formula->dbgInfo.convertedFlag = FALSE;
2077 formula->dbgInfo.originalFormula = NIL(Ctlp_Formula_t);
2078 formula->top = 0;
2079 formula->compareValue = 0;
2080 formula->latest = Ctlp_Incomparable_c;
2081 formula->BotOnionRings = NIL(array_t);
2082 formula->TopOnionRings = NIL(array_t);
2083
2084 return formula;
2085}
2086
2087
2088/**Function********************************************************************
2089
2090 Synopsis [Creates a CTL formula with disjunction of atomic propositions]
2091
2092 Description [This function returns Ctlp_Formula_t for name = {v1,v2,...}.
2093 In case of failure, a NULL pointer is returned.]
2094
2095 SideEffects []
2096
2097 SeeAlso []
2098
2099******************************************************************************/
2100Ctlp_Formula_t *
2101Ctlp_FormulaCreateOr(
2102 char *name,
2103 char *valueStr)
2104{
2105 Ctlp_Formula_t *formula, *tempFormula;
2106 char *preStr;
2107
2108 preStr = strtok(valueStr,",");
2109 formula = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(name),
2110 util_strsav(preStr));
2111 if (formula == NIL(Ctlp_Formula_t)) {
2112 return NIL(Ctlp_Formula_t);
2113 }
2114 while ((preStr = strtok(NIL(char),",")) != NIL(char)) {
2115 tempFormula = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(name),
2116 util_strsav(preStr));
2117 if (tempFormula == NIL(Ctlp_Formula_t)) {
2118 Ctlp_FormulaFree(formula);
2119 return NIL(Ctlp_Formula_t);
2120 }
2121 formula = Ctlp_FormulaCreate(Ctlp_OR_c,formula,tempFormula);
2122 }
2123 return formula;
2124}
2125
2126
2127/**Function********************************************************************
2128
2129 Synopsis [Creates a CTL formula with conjunction of atomic propositions]
2130
2131 Description [This function returns Ctlp_Formula_t for nameVector = value,
2132 nameVector is a form of var[i:j] or var<j:j> and value is any integer n or
2133 binary string starting with 'b', for instance, b0011. If n is not
2134 fitted in var[i:j] or size of binary string is not matched with
2135 var[i:j], NULL pointer is returned]
2136
2137 SideEffects []
2138
2139 SeeAlso []
2140
2141******************************************************************************/
2142Ctlp_Formula_t *
2143Ctlp_FormulaCreateVectorAnd(
2144 char *nameVector,
2145 char *value)
2146{
2147 Ctlp_Formula_t *formula, *tempFormula;
2148 int startValue, endValue, inc, i,j, interval,startInd;
2149 char *binValueStr, *varName, *name;
2150 char *bitValue;
2151
2152 varName = CtlpGetVectorInfoFromStr(nameVector,&startValue,&endValue,&interval,&inc);
2153 binValueStr = ALLOC(char,interval+1);
2154 if (!CtlpStringChangeValueStrToBinString(value,binValueStr,interval) ){
2155 FREE(varName);
2156 FREE(binValueStr);
2157 return NIL(Ctlp_Formula_t);
2158 }
2159
2160 name = ALLOC(char,MAX_LENGTH_OF_VAR_NAME);
2161 (void) sprintf(name,"%s[%d]",varName,startValue);
2162 (void) CtlpChangeBracket(name);
2163
2164 bitValue = ALLOC(char,2);
2165 bitValue[0] = binValueStr[0];
2166 bitValue[1] = '\0';
2167
2168 formula = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(name),
2169 util_strsav(bitValue));
2170 j = 0;
2171 startInd = startValue;
2172 for(i=startValue;i!=endValue;i=i+inc){
2173 startInd += inc;
2174 j++;
2175 (void) sprintf(name,"%s[%d]",varName,startInd);
2176 (void) CtlpChangeBracket(name);
2177 bitValue[0] = binValueStr[j];
2178 tempFormula = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(name),
2179 util_strsav(bitValue));
2180 formula = Ctlp_FormulaCreate(Ctlp_AND_c,formula,tempFormula);
2181 }
2182 FREE(varName);
2183 FREE(name);
2184 FREE(binValueStr);
2185 FREE(bitValue);
2186 return formula;
2187}
2188
2189
2190/**Function********************************************************************
2191
2192 Synopsis [Creates a CTL formula with OR of Vector AND]
2193
2194 Description [This function returns Ctlp_Formula_t for nameVector = valueStr,
2195 nameVector is a form of var[i:j] or var<j:j>, valueStr is "k,l,...,q",
2196 and k,l,...,q is either integer or binary string. Binary string starting
2197 with 'b', for instance, b0011. If n is not fitted in var[i:j] or size of
2198 binary string is not matched with var[i:j], NULL pointer is returned]
2199
2200 SideEffects []
2201
2202 SeeAlso []
2203
2204******************************************************************************/
2205Ctlp_Formula_t *
2206Ctlp_FormulaCreateVectorOr(
2207 char *nameVector,
2208 char *valueStr)
2209{
2210 Ctlp_Formula_t *formula,*tempFormula;
2211 char *preStr;
2212
2213 preStr = strtok(valueStr,",");
2214 formula = Ctlp_FormulaCreateVectorAnd(nameVector,preStr);
2215 if ( formula == NIL(Ctlp_Formula_t)){
2216 return NIL(Ctlp_Formula_t);
2217 }
2218 while( (preStr = strtok(NIL(char),",")) != NIL(char) ){
2219 tempFormula = Ctlp_FormulaCreateVectorAnd(nameVector,preStr);
2220 if ( tempFormula == NIL(Ctlp_Formula_t)){
2221 Ctlp_FormulaFree(formula);
2222 return NIL(Ctlp_Formula_t);
2223 }
2224 formula = Ctlp_FormulaCreate(Ctlp_OR_c,formula,tempFormula);
2225 }
2226 return formula;
2227}
2228
2229
2230/**Function********************************************************************
2231
2232 Synopsis [Creates a CTL formula for equivalent property]
2233
2234 Description [This function assumes that each child is defined in binary
2235 domain. Enumerate type is not supported]
2236
2237 SideEffects []
2238
2239 SeeAlso []
2240
2241******************************************************************************/
2242Ctlp_Formula_t *
2243Ctlp_FormulaCreateEquiv(
2244 char *left,
2245 char *right)
2246{
2247 Ctlp_Formula_t *formula,*formula1,*formula2;
2248
2249 char *one;
2250 char *zero;
2251
2252 one = "1";
2253 zero = "0";
2254
2255 formula1 = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(left),
2256 util_strsav(one));
2257 formula2 = Ctlp_FormulaCreate(Ctlp_ID_c, util_strsav(right),
2258 util_strsav(zero));
2259 formula = Ctlp_FormulaCreate(Ctlp_XOR_c,formula1,formula2);
2260 return formula;
2261}
2262
2263/**Function********************************************************************
2264
2265 Synopsis [Creates a CTL formula for equivalent of vector]
2266
2267 Description [This function returns a formula, which is the AND of a bitwise
2268 equivalence]
2269
2270 SideEffects []
2271
2272 SeeAlso []
2273
2274******************************************************************************/
2275Ctlp_Formula_t *
2276Ctlp_FormulaCreateVectorEquiv(
2277 char *left,
2278 char *right)
2279{
2280 Ctlp_Formula_t *formula,*tempFormula;
2281 char *leftName,*rightName;
2282 char *leftVar, *rightVar;
2283 int leftStart,leftEnd,rightStart,rightEnd,leftInterval,rightInterval;
2284 int leftInc,rightInc,leftInd,rightInd,i;
2285
2286 leftName = CtlpGetVectorInfoFromStr(left,&leftStart,&leftEnd,&leftInterval,&leftInc);
2287 rightName = CtlpGetVectorInfoFromStr(right,&rightStart,&rightEnd,&rightInterval,&rightInc);
2288 if (leftInterval != rightInterval){
2289 return NIL(Ctlp_Formula_t);
2290 }
2291 leftVar = ALLOC(char,MAX_LENGTH_OF_VAR_NAME);
2292 (void) sprintf(leftVar,"%s[%d]",leftName,leftStart);
2293 (void) CtlpChangeBracket(leftVar);
2294 rightVar = ALLOC(char,MAX_LENGTH_OF_VAR_NAME);
2295 (void) sprintf(rightVar,"%s[%d]",rightName,rightStart);
2296 (void) CtlpChangeBracket(rightVar);
2297
2298 formula = Ctlp_FormulaCreateEquiv(leftVar,rightVar);
2299 leftInd = leftStart;
2300 rightInd = rightStart;
2301 for(i=leftStart;i!=leftEnd;i+=leftInc){
2302 leftInd += leftInc;
2303 rightInd += rightInc;
2304 (void) sprintf(leftVar,"%s[%d]",leftName,leftInd);
2305 (void) CtlpChangeBracket(leftVar);
2306 (void) sprintf(rightVar,"%s[%d]",rightName,rightInd);
2307 (void) CtlpChangeBracket(rightVar);
2308 tempFormula = Ctlp_FormulaCreateEquiv(leftVar,rightVar);
2309 formula = Ctlp_FormulaCreate(Ctlp_AND_c,formula,tempFormula);
2310 }
2311 FREE(leftName);
2312 FREE(rightName);
2313 FREE(leftVar);
2314 FREE(rightVar);
2315 return formula;
2316}
2317
2318
2319/**Function********************************************************************
2320
2321 Synopsis [Creates a CTL formula for multiple AX]
2322
2323 Description [This function returns a formula, which is the multiple
2324 times of AX. The given string includes the number of depth]
2325
2326 SideEffects []
2327
2328 SeeAlso []
2329
2330******************************************************************************/
2331Ctlp_Formula_t *
2332Ctlp_FormulaCreateAXMult(
2333 char *string,
2334 Ctlp_Formula_t *formula)
2335{
2336 int i,num;
2337 char *str, *ptr;
2338 Ctlp_Formula_t *result;
2339 str = strchr(string,':');
2340 if ( str == NULL) return(NIL(Ctlp_Formula_t));
2341 str++;
2342
2343 num = strtol(str,&ptr,0);
2344
2345 if (num<=0){
2346 return (NIL(Ctlp_Formula_t));
2347 }
2348 result = Ctlp_FormulaCreate(Ctlp_AX_c,formula,NIL(Ctlp_Formula_t));
2349 for(i=1;i<num;i++){
2350 result = Ctlp_FormulaCreate(Ctlp_AX_c,result,NIL(Ctlp_Formula_t));
2351 }
2352 return result;
2353}
2354
2355
2356/**Function********************************************************************
2357
2358 Synopsis [Creates a CTL formula for multiple EX]
2359
2360 Description [This function returns a formula, which is the multiple
2361 times of EX. The given string includes the number of depth]
2362
2363 SideEffects []
2364
2365 SeeAlso []
2366
2367******************************************************************************/
2368Ctlp_Formula_t *
2369Ctlp_FormulaCreateEXMult(
2370 char *string,
2371 Ctlp_Formula_t *formula)
2372{
2373 int i, num;
2374 char *str, *ptr;
2375 Ctlp_Formula_t *result;
2376 str = strchr(string,':');
2377 if ( str == NULL) return(NIL(Ctlp_Formula_t));
2378 str++;
2379
2380 num = strtol(str,&ptr,0);
2381
2382 if (num<=0){
2383 return (NIL(Ctlp_Formula_t));
2384 }
2385 result = Ctlp_FormulaCreate(Ctlp_EX_c,formula,NIL(Ctlp_Formula_t));
2386 for(i=1;i<num;i++){
2387 result = Ctlp_FormulaCreate(Ctlp_EX_c,result,NIL(Ctlp_Formula_t));
2388 }
2389 return result;
2390}
2391
2392/**Function********************************************************************
2393
2394 Synopsis [Converts an array of CTL formulae to forward form.]
2395
2396 Description [Converts an array of CTL formulae to forward. Creates a
2397 maximally shared representation if noshare is false, a representation without
2398 any sharing otherwise. ]
2399
2400 SideEffects []
2401
2402 SeeAlso []
2403
2404******************************************************************************/
2405array_t *
2406Ctlp_FormulaArrayConvertToForward(array_t *formulaArray, int singleInitial,
2407 boolean doNotShareFlag)
2408{
2409 int i;
2410 Ctlp_Formula_t *formula, *existentialFormula, *forwardFormula;
2411 int numFormulae = array_n(formulaArray);
2412 array_t *forwardFormulaArray = array_alloc(Ctlp_Formula_t *, numFormulae);
2413 array_t *forwardDagArray;
2414 int compareValue;
2415
2416 for(i=0; i < numFormulae; i++) {
2417 formula = array_fetch(Ctlp_Formula_t *, formulaArray, i);
2418 existentialFormula = Ctlp_FormulaConvertToExistentialForm(formula);
2419 assert(existentialFormula != NIL(Ctlp_Formula_t));
2420 formula = NIL(Ctlp_Formula_t);
2421 /*
2422 ** compareValue = 0 : check with FALSE
2423 ** compareValue = 1 : check with not-FALSE
2424 */
2425 if (singleInitial)
2426 compareValue = FormulaGetCompareValue(existentialFormula);
2427 else
2428 compareValue = 0;
2429 forwardFormula = FormulaCreateWithType(Ctlp_AND_c);
2430 forwardFormula->left = FormulaCreateWithType(Ctlp_Init_c);
2431 if (compareValue == 0) {
2432 forwardFormula->right = FormulaCreateWithType(Ctlp_NOT_c);
2433 forwardFormula->right->left = existentialFormula;
2434 } else
2435 forwardFormula->right = existentialFormula;
2436 forwardFormula->right->states = (mdd_t *)forwardFormula;
2437 /* if formula was converted before, keep that reference */
2438 if(existentialFormula->dbgInfo.originalFormula != NIL(Ctlp_Formula_t))
2439 forwardFormula->dbgInfo.originalFormula =
2440 existentialFormula->dbgInfo.originalFormula;
2441 else
2442 forwardFormula->dbgInfo.originalFormula = existentialFormula;
2443
2444 forwardFormula->top = 1;
2445 forwardFormula->compareValue = compareValue;
2446 FormulaConvertToForward(forwardFormula->right, compareValue);
2447 CtlpFormulaSetStatesToNULL(forwardFormula);
2448 FormulaInsertForwardCompareNodes(forwardFormula, NULL, compareValue);
2449 array_insert(Ctlp_Formula_t *, forwardFormulaArray, i, forwardFormula);
2450 }
2451
2452 if (doNotShareFlag)
2453 return(forwardFormulaArray);
2454
2455 forwardDagArray = Ctlp_FormulaArrayConvertToDAG(forwardFormulaArray);
2456 array_free(forwardFormulaArray);
2457 return forwardDagArray;
2458}
2459
2460
2461/**Function********************************************************************
2462
2463 Synopsis [Returns a string for each formula type.]
2464
2465 Description [Returns a string for each formula type.]
2466
2467 SideEffects []
2468
2469 SeeAlso []
2470
2471******************************************************************************/
2472char *
2473Ctlp_FormulaGetTypeString(Ctlp_Formula_t *formula)
2474{
2475 char *result;
2476
2477 switch(formula->type) {
2478 /*
2479 * The cases are listed in rough order of their expected frequency.
2480 */
2481 case Ctlp_ID_c:
2482 result = util_strsav("ID");
2483 break;
2484 case Ctlp_OR_c:
2485 result = util_strsav("OR");
2486 break;
2487 case Ctlp_AND_c:
2488 result = util_strsav("AND");
2489 break;
2490 case Ctlp_THEN_c:
2491 result = util_strsav("THEN");
2492 break;
2493 case Ctlp_XOR_c:
2494 result = util_strsav("XOR");
2495 break;
2496 case Ctlp_EQ_c:
2497 result = util_strsav("EQ");
2498 break;
2499 case Ctlp_NOT_c:
2500 result = util_strsav("NOT");
2501 break;
2502 case Ctlp_EX_c:
2503 result = util_strsav("EX");
2504 break;
2505 case Ctlp_EG_c:
2506 result = util_strsav("EG");
2507 break;
2508 case Ctlp_EF_c:
2509 result = util_strsav("EF");
2510 break;
2511 case Ctlp_EU_c:
2512 result = util_strsav("EU");
2513 break;
2514 case Ctlp_AX_c:
2515 result = util_strsav("AX");
2516 break;
2517 case Ctlp_AG_c:
2518 result = util_strsav("AG");
2519 break;
2520 case Ctlp_AF_c:
2521 result = util_strsav("AF");
2522 break;
2523 case Ctlp_AU_c:
2524 result = util_strsav("AU");
2525 break;
2526 case Ctlp_TRUE_c:
2527 result = util_strsav("TRUE");
2528 break;
2529 case Ctlp_FALSE_c:
2530 result = util_strsav("FALSE");
2531 break;
2532 case Ctlp_Init_c:
2533 result = util_strsav("Init");
2534 break;
2535 case Ctlp_Cmp_c:
2536 result = util_strsav("Cmp");
2537 break;
2538 case Ctlp_FwdU_c:
2539 result = util_strsav("FwdU");
2540 break;
2541 case Ctlp_FwdG_c:
2542 result = util_strsav("FwdG");
2543 break;
2544 case Ctlp_EY_c:
2545 result = util_strsav("EY");
2546 break;
2547 case Ctlp_EH_c:
2548 result = util_strsav("EH");
2549 break;
2550 default:
2551 fail("Unexpected type");
2552 }
2553 return(result);
2554}
2555
2556
2557/**Function********************************************************************
2558
2559 Synopsis [Tests if a formula is quantifier-free, ACTL, ECTL or
2560 mixed.]
2561
2562 Description [Tests if a formula is Quantifier free, ACTL, ECTL or mixed. We
2563 assume that the formula is in existential normal form, and hence only
2564 contains existential temporal operators.
2565
2566 <p>The formula is ECTL if every temporal operator appears under an even
2567 number of negations, and it is ACTL if every temporal operator appears under
2568 an odd number of negations. It is quantifier-free if it is both ECTL and
2569 ACTL (i.e., no temporal operators occur), and it is mixed if it is neither
2570 ECTL nor ACTL.]
2571
2572 SideEffects []
2573
2574 SeeAlso []
2575
2576******************************************************************************/
2577Ctlp_FormulaClass
2578Ctlp_CheckClassOfExistentialFormula(
2579 Ctlp_Formula_t *formula)
2580{
2581 Ctlp_FormulaType formulaType;
2582 Ctlp_Formula_t *rightFormula, *leftFormula;
2583 Ctlp_FormulaClass resultLeft, resultRight, tempResult, currentClass;
2584
2585 assert(formula != NIL(Ctlp_Formula_t));
2586 if(formula == NIL(Ctlp_Formula_t))
2587 return Ctlp_QuantifierFree_c;
2588
2589 formulaType = Ctlp_FormulaReadType(formula);
2590 leftFormula = Ctlp_FormulaReadLeftChild(formula);
2591 rightFormula = Ctlp_FormulaReadRightChild(formula);
2592
2593 /* Depending on the formula type, create result or recur */
2594 switch (formulaType) {
2595 case Ctlp_EX_c:
2596 case Ctlp_EG_c:
2597 case Ctlp_EF_c:
2598 case Ctlp_EU_c:
2599 case Ctlp_FwdU_c:
2600 case Ctlp_FwdG_c:
2601 case Ctlp_EY_c:
2602 case Ctlp_EH_c:
2603 resultLeft = Ctlp_CheckClassOfExistentialFormula(leftFormula);
2604 if (formulaType == Ctlp_EU_c || formulaType == Ctlp_FwdU_c ||
2605 formulaType == Ctlp_FwdG_c )
2606 resultRight = Ctlp_CheckClassOfExistentialFormula(rightFormula);
2607 else
2608 resultRight = Ctlp_QuantifierFree_c;
2609
2610 tempResult = CtlpResolveClass(resultLeft, resultRight);
2611 currentClass = Ctlp_ECTL_c;
2612 return CtlpResolveClass(currentClass, tempResult);
2613 case Ctlp_AX_c:
2614 case Ctlp_AG_c:
2615 case Ctlp_AF_c:
2616 case Ctlp_AU_c:
2617 /* The formula is supposed to be only existential */
2618 fprintf(vis_stdout,
2619 "** Ctlp Error: unexpected (universal) operator type\n");
2620 assert(0);
2621 return Ctlp_Mixed_c;
2622 case Ctlp_OR_c:
2623 case Ctlp_AND_c:
2624 resultLeft = Ctlp_CheckClassOfExistentialFormula(leftFormula);
2625 resultRight = Ctlp_CheckClassOfExistentialFormula(rightFormula);
2626 return CtlpResolveClass(resultLeft, resultRight);
2627 case Ctlp_NOT_c:
2628 tempResult = Ctlp_CheckClassOfExistentialFormula(leftFormula);
2629 return CtlpNegateFormulaClass(tempResult);
2630 case Ctlp_THEN_c:
2631 resultLeft = Ctlp_CheckClassOfExistentialFormula(leftFormula);
2632 resultRight = Ctlp_CheckClassOfExistentialFormula(rightFormula);
2633 tempResult = CtlpNegateFormulaClass(resultLeft);
2634 return CtlpResolveClass(tempResult, resultRight);
2635 case Ctlp_XOR_c:
2636 case Ctlp_EQ_c:
2637 resultLeft = Ctlp_CheckClassOfExistentialFormula(leftFormula);
2638 resultRight = Ctlp_CheckClassOfExistentialFormula(rightFormula);
2639 tempResult = CtlpResolveClass(resultLeft, resultRight);
2640 if( tempResult == Ctlp_QuantifierFree_c)
2641 return Ctlp_QuantifierFree_c;
2642 else
2643 return Ctlp_Mixed_c;
2644 case Ctlp_ID_c:
2645 case Ctlp_TRUE_c:
2646 case Ctlp_FALSE_c:
2647 case Ctlp_Init_c:
2648 return Ctlp_QuantifierFree_c;
2649 case Ctlp_Cmp_c:
2650 return Ctlp_Mixed_c;
2651 default:
2652 fprintf(vis_stderr, "**Ctlp Error: Unexpected operator detected.\n");
2653 assert(0);
2654 return Ctlp_Mixed_c;
2655 }
2656} /* End of Ctlp_CheckTypeOfExistentialFormula */
2657
2658/**Function********************************************************************
2659
2660 Synopsis [Tests if an array of simple existential formulae has only
2661 ACTL, only ECTL or mixture of formula.]
2662
2663 Description [Returns Ctlp_ECTL_c if the array contains only
2664 ECTL formulae, Ctlp_ACTL_c if it contains only ACTL formulae,
2665 Ctlp_QuantifierFree_c if there are no quantifiers in any formulae,
2666 and Ctlp_Mixed otherwise.]
2667
2668 SideEffects []
2669
2670 SeeAlso [Ctlp_CheckClassOfExistentialFormula]
2671
2672******************************************************************************/
2673Ctlp_FormulaClass
2674Ctlp_CheckClassOfExistentialFormulaArray(
2675 array_t *formulaArray)
2676{
2677 Ctlp_FormulaClass result;
2678 Ctlp_Formula_t *formula;
2679 int formulanr;
2680
2681 result = Ctlp_QuantifierFree_c;
2682 arrayForEachItem(Ctlp_Formula_t *, formulaArray, formulanr, formula){
2683 Ctlp_FormulaClass formulaType;
2684 formulaType = Ctlp_CheckClassOfExistentialFormula(formula);
2685 result = CtlpResolveClass(result, formulaType);
2686 if(result == Ctlp_Mixed_c)
2687 return result;
2688 }
2689 return result;
2690} /* End of Ctlp_CheckTypeOfExistentialFormulaArray */
2691
2692
2693/**Function********************************************************************
2694
2695 Synopsis [Compare two formulas for equality]
2696
2697 Description [Checks if two formulas are syntactically the same. Equivalent
2698 constructions such as TRUE and TRUE+FALSE are not recognized, but copies are
2699 handled correctly, and strings are compared using strcmp.]
2700
2701 SideEffects []
2702
2703 SeeAlso [FormulaCompare]
2704
2705******************************************************************************/
2706boolean
2707Ctlp_FormulaIdentical(
2708 Ctlp_Formula_t *formula1,
2709 Ctlp_Formula_t *formula2)
2710{
2711 return(FormulaCompare((char *)formula1, (char *)formula2) == 0);
2712}
2713
2714
2715/**Function********************************************************************
2716
2717 Synopsis [Replaces non-monotonic operators in a formula.]
2718
2719 Description [This function takes a parse tree for a CTL formula and
2720 transforms it into another tree that has only monotonic operators.
2721 The non-monotonic operators are <code>XOR</code> and <code>EQ</code>.
2722 They are replaced by eqivalent trees. Specificallt, <code>XOR(a,b)</code>
2723 is replaced by <code>OR(AND(a,NOT(b)),AND(NOT(a),b))</code> and
2724 <code>f <-> g</code> is replaced by <code>AND(f->g,g->f)</code>.<p>
2725
2726 It is important that the original formula be a tree. The idea is that this
2727 function should be called right after reading the formulae from file. Since
2728 the information attached to the parse tree by the model checking procedures
2729 is not preserved, it is also important that no such information exists.
2730 These conditions are checked by an assertion.<p>
2731
2732 This function does not deal with the forward CTL operators. Reduction to
2733 monotonic operators should be performed before conversion to forward CTL.]
2734
2735 SideEffects [The argument is modified. The new formulae will apprear
2736 when they are printed out.]
2737
2738 SeeAlso [Ctlp_FormulaArrayMakeMonotonic]
2739
2740******************************************************************************/
2741void
2742Ctlp_FormulaMakeMonotonic(
2743 Ctlp_Formula_t *formula)
2744{
2745 Ctlp_Formula_t *left, *right;
2746 Ctlp_FormulaType type;
2747
2748 if (formula == NIL(Ctlp_Formula_t)) {
2749 return;
2750 }
2751
2752 /* Make sure (recursively) that this (sub)-formula is still in its pristine
2753 * state. Specifically, that the parse graph is a tree.
2754 */
2755 assert(formula->refCount == 1 &&
2756 formula->states == NIL(mdd_t) &&
2757 formula->underapprox == NIL(mdd_t) &&
2758 formula->overapprox == NIL(mdd_t) &&
2759 formula->latest == Ctlp_Incomparable_c &&
2760 formula->dbgInfo.data == NIL(void) &&
2761 formula->dbgInfo.freeFn == (Ctlp_DbgInfoFreeFn) NULL &&
2762 formula->dbgInfo.convertedFlag == FALSE &&
2763 formula->dbgInfo.originalFormula == NIL(Ctlp_Formula_t) &&
2764 formula->top == 0 &&
2765 formula->compareValue == 0
2766 );
2767
2768 type = Ctlp_FormulaReadType(formula);
2769
2770 /* Leaves remain unchanged. */
2771 if (type == Ctlp_ID_c || type == Ctlp_TRUE_c || type == Ctlp_FALSE_c) {
2772 return;
2773 }
2774
2775 /* First recursively fix the children. */
2776 left = Ctlp_FormulaReadLeftChild(formula);
2777 Ctlp_FormulaMakeMonotonic(left);
2778 right = Ctlp_FormulaReadRightChild(formula);
2779 Ctlp_FormulaMakeMonotonic(right);
2780
2781 /* Fix this node if it is not monotonic. */
2782 switch (type) {
2783 case Ctlp_EX_c:
2784 case Ctlp_EG_c:
2785 case Ctlp_EF_c:
2786 case Ctlp_EU_c:
2787 case Ctlp_AX_c:
2788 case Ctlp_AG_c:
2789 case Ctlp_AF_c:
2790 case Ctlp_AU_c:
2791 case Ctlp_OR_c:
2792 case Ctlp_AND_c:
2793 case Ctlp_NOT_c:
2794 case Ctlp_THEN_c:
2795 case Ctlp_EY_c:
2796 case Ctlp_EH_c:
2797 /* Nothing to be done */
2798 break;
2799 case Ctlp_EQ_c: {
2800 Ctlp_Formula_t *dupLeft, *dupRight;
2801 Ctlp_Formula_t *thenLeft, *thenRight;
2802 dupLeft = Ctlp_FormulaDup(left);
2803 dupRight = Ctlp_FormulaDup(right);
2804 thenLeft = Ctlp_FormulaCreate(Ctlp_THEN_c, left, right);
2805 thenRight = Ctlp_FormulaCreate(Ctlp_THEN_c, dupRight, dupLeft);
2806 /* Fix the node in place. */
2807 formula->type = Ctlp_AND_c;
2808 formula->left = thenLeft;
2809 formula->right = thenRight;
2810 break;
2811 }
2812 case Ctlp_XOR_c: {
2813 Ctlp_Formula_t *dupLeft, *dupRight;
2814 Ctlp_Formula_t *negLeft, *negRight;
2815 Ctlp_Formula_t *andLeft, *andRight;
2816 dupLeft = Ctlp_FormulaDup(left);
2817 dupRight = Ctlp_FormulaDup(right);
2818 negLeft = Ctlp_FormulaCreate(Ctlp_NOT_c, dupLeft, NIL(Ctlp_Formula_t));
2819 negRight = Ctlp_FormulaCreate(Ctlp_NOT_c, dupRight, NIL(Ctlp_Formula_t));
2820 andLeft = Ctlp_FormulaCreate(Ctlp_AND_c, left, negRight);
2821 andRight = Ctlp_FormulaCreate(Ctlp_AND_c, negLeft, right);
2822 /* Fix the node in place. */
2823 formula->type = Ctlp_OR_c;
2824 formula->left = andLeft;
2825 formula->right = andRight;
2826 break;
2827 }
2828 default:
2829 /* Forward CTL operators (that are not supported) and leaves (that are
2830 * dealt with above) would fall here.
2831 */
2832 fail("unexpected CTL formula type\n");
2833 }
2834
2835 return;
2836
2837} /* Ctlp_FormulaMakeMonotonic */
2838
2839
2840/**Function********************************************************************
2841
2842 Synopsis [Replaces non-monotonic operators in an array of formulae.]
2843
2844 Description [Apply Ctlp_FormulaMakeMonotonic to each formula in the array.]
2845
2846 SideEffects [The formulae in the array are modified.]
2847
2848 SeeAlso [Ctlp_FormulaMakeMonotonic]
2849
2850******************************************************************************/
2851void
2852Ctlp_FormulaArrayMakeMonotonic(
2853 array_t *formulaArray /* of Ctlp_Formula_t */)
2854{
2855 int i;
2856 Ctlp_Formula_t *formula;
2857
2858 if (formulaArray == NIL(array_t)) return;
2859 arrayForEachItem(Ctlp_Formula_t *, formulaArray, i, formula) {
2860 Ctlp_FormulaMakeMonotonic(formula);
2861 }
2862
2863} /* Ctlp_FormulaArrayMakeMonotonic */
2864
2865
2866/*---------------------------------------------------------------------------*/
2867/* Definition of internal functions */
2868/*---------------------------------------------------------------------------*/
2869
2870
2871/**Function********************************************************************
2872
2873 Synopsis [Increments the reference count of a formula.]
2874
2875 Description [The function increments the reference count of a formula. If
2876 the formula is NULL, the function does nothing.]
2877
2878 SideEffects []
2879
2880 SeeAlso []
2881
2882******************************************************************************/
2883void
2884CtlpFormulaIncrementRefCount(
2885 Ctlp_Formula_t *formula)
2886{
2887 if(formula!=NIL(Ctlp_Formula_t)) {
2888 ++(formula->refCount);
2889 }
2890}
2891
2892/**Function********************************************************************
2893
2894 Synopsis [Decrements the reference count of a formula.]
2895
2896 Description [The function decrements the reference count of formula and if
2897 the reference count reaches 0, the formula is freed. If the formula is NULL,
2898 the function does nothing. It is an error to decrement the reference count
2899 below 0.]
2900
2901 SideEffects []
2902
2903 SeeAlso []
2904
2905******************************************************************************/
2906void
2907CtlpFormulaDecrementRefCount(
2908 Ctlp_Formula_t *formula)
2909{
2910 if(formula!=NIL(Ctlp_Formula_t)) {
2911 assert(formula->refCount>0);
2912 if(--(formula->refCount) == 0)
2913 CtlpFormulaFree(formula);
2914 }
2915}
2916/**Function********************************************************************
2917
2918 Synopsis [Adds formula to the end of globalFormulaArray.]
2919
2920 SideEffects [Manipulates the global variable globalFormulaArray.]
2921
2922 SeeAlso [CtlpYyparse]
2923
2924******************************************************************************/
2925void
2926CtlpFormulaAddToGlobalArray(
2927 Ctlp_Formula_t * formula)
2928{
2929 array_insert_last(Ctlp_Formula_t *, globalFormulaArray, formula);
2930}
2931
2932/**Function********************************************************************
2933
2934 Synopsis [Frees a CTL formula.]
2935
2936 Description [The function frees all memory associated with the formula,
2937 including all MDDs and all character strings (however, does not free
2938 dbgInfo.originalFormula). It also decrements the reference counts of its two
2939 chidren. The function does nothing if formula is NULL.]
2940
2941 SideEffects []
2942
2943 SeeAlso [Ctlp_FormulaArrayFree]
2944
2945******************************************************************************/
2946void
2947CtlpFormulaFree(
2948 Ctlp_Formula_t * formula)
2949{
2950 if (formula != NIL(Ctlp_Formula_t)) {
2951
2952 /*
2953 * Free any fields that are not NULL.
2954 */
2955
2956 if (formula->type == Ctlp_ID_c) {
2957 FREE(formula->left);
2958 FREE(formula->right);
2959 }
2960 else {
2961 if (formula->left != NIL(Ctlp_Formula_t)) {
2962 CtlpFormulaDecrementRefCount(formula->left);
2963 }
2964 if (formula->right != NIL(Ctlp_Formula_t)) {
2965 CtlpFormulaDecrementRefCount(formula->right);
2966 }
2967 }
2968 if (formula->states != NIL(mdd_t))
2969 mdd_free(formula->states);
2970 if (formula->underapprox != NIL(mdd_t))
2971 mdd_free(formula->underapprox);
2972 if (formula->overapprox != NIL(mdd_t))
2973 mdd_free(formula->overapprox);
2974 if (formula->Bottomstates != NIL(array_t))
2975 mdd_array_free(formula->Bottomstates);
2976 if (formula->Topstates != NIL(array_t))
2977 mdd_array_free(formula->Topstates);
2978 if (formula->matchfound_top != NIL(array_t))
2979 array_free(formula->matchfound_top);
2980 if (formula->matchelement_top != NIL(array_t))
2981 array_free(formula->matchelement_top);
2982 if (formula->matchfound_bot != NIL(array_t))
2983 array_free(formula->matchfound_bot);
2984 if (formula->matchelement_bot != NIL(array_t))
2985 array_free(formula->matchelement_bot);
2986 if (formula->leaves != NIL(array_t))
2987 array_free(formula->leaves);
2988 if (formula->dbgInfo.data != NIL(void)) {
2989 (*formula->dbgInfo.freeFn)(formula);
2990 }
2991 FREE(formula);
2992 }
2993}
2994
2995
2996/**Function********************************************************************
2997
2998 Synopsis [Create a binary string of given value with size of interval ]
2999
3000 Description [The value is a binary string starting with 'b',
3001 a hexadecimal string starting with 'x', or an
3002 integer string. If Value is not fitted in the interval, 0 is return.
3003 Otherwise 1 is returned. Result string is saved at given pointer.]
3004
3005 SideEffects []
3006
3007 SeeAlso []
3008
3009******************************************************************************/
3010int
3011CtlpStringChangeValueStrToBinString(
3012 char *value,
3013 char *binValueStr,
3014 int interval)
3015{
3016 int i;
3017 long int num, mask;
3018 double maxNum;
3019 char *ptr;
3020
3021 mask = 1;
3022 maxNum = pow(2.0,(double)interval);
3023 errno = 0;
3024
3025 if(value[0] == 'b'){
3026 if ((int)strlen(value)-1 == interval){
3027 for(i=1;i<=interval;i++){
3028 if (value[i] == '0' || value[i] == '1'){
3029 binValueStr[i-1] = value[i];
3030 }else{
3031 return 0;
3032 }
3033 }
3034 binValueStr[interval] = '\0';
3035 }else{
3036 return 0;
3037 }
3038 }else if (value[0] == 'x'){
3039 for(i=1; i < (int)strlen(value); i++){
3040 if (!isxdigit((int)value[i])){
3041 return 0;
3042 }
3043 }
3044 num = strtol(++value,&ptr,16);
3045 if (errno) return 0;
3046 if ( num >= maxNum) return 0;
3047 for(i=0;i<interval;i++){
3048 if(num & (mask<<i)) binValueStr[interval-i-1] = '1';
3049 else binValueStr[interval-i-1] = '0';
3050 }
3051 binValueStr[interval] = '\0';
3052 }else{
3053 for(i=0;i<(int)strlen(value);i++){
3054 if (!isdigit((int)value[i])){
3055 return 0;
3056 }
3057 }
3058 num = strtol(value,&ptr,0);
3059 if (errno) return 0;
3060 if ( num >= maxNum) return 0;
3061 mask = 1;
3062 for(i=0;i<interval;i++){
3063 if(num & (mask<<i)) binValueStr[interval-i-1] = '1';
3064 else binValueStr[interval-i-1] = '0';
3065 }
3066 binValueStr[interval] = '\0';
3067 }
3068
3069 return(1);
3070}
3071
3072
3073/**Function********************************************************************
3074
3075 Synopsis [Change [] to <>]
3076
3077 Description []
3078
3079 SideEffects [The input string contains ...[num] and this function changes it
3080 to ...<num>.]
3081
3082 SeeAlso []
3083
3084******************************************************************************/
3085void
3086CtlpChangeBracket(
3087 char *inStr)
3088{
3089 int i, j;
3090 char *str;
3091
3092 j = 0;
3093 for (i=0;i<(int)strlen(inStr)+1;i++){
3094 if (inStr[i] != ' '){
3095 inStr[i-j] = inStr[i];
3096 }else{
3097 j++;
3098 }
3099 }
3100
3101 if (changeBracket == 0)
3102 return;
3103
3104 str = strchr(inStr,'[');
3105 if (str == NULL) return;
3106
3107 *str = '<';
3108 str = strchr(inStr,']');
3109 *str = '>';
3110}
3111
3112
3113/**Function********************************************************************
3114
3115 Synopsis [Parse a given vector string.]
3116
3117 Description [Parse given vector string of the form of var<i:j> and
3118 string var is returned. Other information such as i, j, interval between
3119 i and j, and increment or decrement from i to j are saved.]
3120
3121 SideEffects []
3122
3123 SeeAlso []
3124
3125******************************************************************************/
3126char *
3127CtlpGetVectorInfoFromStr(
3128 char *str,
3129 int *start,
3130 int *end,
3131 int *interval,
3132 int *inc)
3133{
3134 char *str1, *str2, *str3;
3135 char *startStr, *endStr;
3136 char *name, *ptr;
3137
3138 str1 = strchr(str,'[');
3139 str2 = strchr(str,':');
3140 str3 = strchr(str,']');
3141 startStr = ALLOC(char, str2-str1);
3142 endStr = ALLOC(char, str3-str2);
3143 name = ALLOC(char, str1-str+1);
3144
3145 (void) strncpy(name, str, str1-str);
3146 (void) strncpy(startStr, str1+1, str2-str1-1);
3147 (void) strncpy(endStr, str2+1, str3-str2-1);
3148
3149 startStr[str2-str1-1] = '\0';
3150 endStr[str3-str2-1] = '\0';
3151 name[str1-str] = '\0';
3152 *start = strtol(startStr,&ptr,0);
3153 *end = strtol(endStr,&ptr,0);
3154 if(*start > *end){
3155 *inc = -1;
3156 *interval = *start - *end + 1;
3157 } else {
3158 *inc = 1;
3159 *interval = *end - *start + 1;
3160 }
3161 FREE(startStr);
3162 FREE(endStr);
3163 return name;
3164}
3165
3166/**Function********************************************************************
3167
3168 Synopsis [Insert macro formula into symbol table.]
3169
3170 Description [If the name is already in table return 0, otherwise insert the
3171 formula into the table and return 1]
3172
3173 SideEffects []
3174
3175 SeeAlso []
3176
3177******************************************************************************/
3178int
3179CtlpFormulaAddToTable(
3180 char *name,
3181 Ctlp_Formula_t *formula,
3182 st_table *macroTable)
3183{
3184 if(macroTable == NIL(st_table)){
3185 macroTable = st_init_table(strcmp, st_strhash);
3186 }
3187 if(st_is_member(macroTable, name)){
3188 return 0;
3189 }
3190 st_insert(macroTable, name, (char *)formula);
3191 return 1;
3192}
3193
3194
3195/**Function********************************************************************
3196
3197 Synopsis [Get macro formula from symbol table]
3198
3199 Description [If macro string is not found in table, NULL pointer is returned]
3200
3201 SideEffects []
3202
3203 SeeAlso []
3204
3205******************************************************************************/
3206Ctlp_Formula_t *
3207CtlpFormulaFindInTable(
3208 char *name,
3209 st_table *macroTable)
3210{
3211 Ctlp_Formula_t *formula;
3212 if (st_lookup(macroTable, name, &formula)){
3213 return (Ctlp_FormulaDup(formula));
3214 }else{
3215 return NIL(Ctlp_Formula_t);
3216 }
3217}
3218
3219/**Function********************************************************************
3220
3221 Synopsis [Returns the greatest lower bound of two classes]
3222
3223 Description [Returns the class of a formula that is the combination of a
3224 formula of class1 and class2. Does this by computing the glb, where mixed <
3225 ECTL < quantifierFree, and mixed < ACTL < quantifierfree.]
3226
3227 SideEffects []
3228
3229 SeeAlso [Ctlp_CheckClassOfExistentialFormula]
3230
3231******************************************************************************/
3232Ctlp_FormulaClass
3233CtlpResolveClass(
3234 Ctlp_FormulaClass class1,
3235 Ctlp_FormulaClass class2)
3236{
3237 if ((class1 == Ctlp_Mixed_c) || (class2 == Ctlp_Mixed_c))
3238 return Ctlp_Mixed_c;
3239 if (class1 == Ctlp_QuantifierFree_c)
3240 return class2;
3241 if (class2 == Ctlp_QuantifierFree_c)
3242 return class1;
3243 if (class1 == class2)
3244 return class1;
3245
3246 return Ctlp_Mixed_c;
3247
3248}
3249
3250
3251/**Function********************************************************************
3252
3253 Synopsis [Returns the class of a formula that is the negation of a formula
3254 of class "class".]
3255
3256 Description [The negation of a mixed (quantifier free, ECTL, ACTL) formula is
3257 mixed (quantifier free, ACTL, ECTL).]
3258
3259 SideEffects []
3260
3261 SeeAlso [Ctlp_CheckClassOfExistentialFormula]
3262
3263******************************************************************************/
3264Ctlp_FormulaClass
3265CtlpNegateFormulaClass(
3266 Ctlp_FormulaClass class_
3267)
3268{
3269 switch(class_){
3270 case Ctlp_Mixed_c:
3271 return Ctlp_Mixed_c;
3272 case Ctlp_QuantifierFree_c:
3273 return Ctlp_QuantifierFree_c;
3274 case Ctlp_ECTL_c:
3275 return Ctlp_ACTL_c;
3276 case Ctlp_ACTL_c:
3277 return Ctlp_ECTL_c;
3278 default:
3279 fprintf(vis_stderr, "**Ctlp Error: Unknown formula class\n");
3280 assert(0);
3281 return Ctlp_Mixed_c;
3282 }
3283}
3284
3285
3286/**Function********************************************************************
3287
3288 Synopsis [Replaces the smallest important sub-fomula in a w-ACTL
3289 formula by bottom.]
3290
3291 Description [Creates a witness formula for a given w-ACTL formula by
3292 replacing the smallest inpurtant subformula with bottom. This function is
3293 used in the approach to vacuity detection of Beer et al. (CAV97). Formulae
3294 in w-ACTL are guaranteed to have a unique smallest important subformula,
3295 which is defined as follow. If the formula is simple, its operands are not
3296 important. (An exception is made for implications. See
3297 ReplaceSimpleFormula.) Otherwise, the non-simple operand is the important
3298 operand. For (A p U q) or (E p U q), where p and q are both simple, p is the
3299 important operand. For unary formulae, the only child is the important
3300 operand. This function works also for ACTL formulae that are not in w-ACTL,
3301 and for which smallest important subformulae are not unique.
3302 The function picks up a smallest important subformula.]
3303
3304 SideEffects [none]
3305
3306 SeeAlso [ReplaceSimpleFormula]
3307
3308******************************************************************************/
3309Ctlp_Formula_t *
3310Ctlp_FormulaCreateWitnessFormula(
3311 Ctlp_Formula_t *formula)
3312{
3313 Ctlp_FormulaType formulaType;
3314 Ctlp_Formula_t *rightFormula, *leftFormula;
3315 Ctlp_Formula_t *newLeftFormula, *newRightFormula;
3316
3317 assert(formula != NIL(Ctlp_Formula_t));
3318
3319 if(formula == NIL(Ctlp_Formula_t))
3320 return NIL(Ctlp_Formula_t);
3321
3322 formulaType = Ctlp_FormulaReadType(formula);
3323 leftFormula = Ctlp_FormulaReadLeftChild(formula);
3324 rightFormula = Ctlp_FormulaReadRightChild(formula);
3325
3326 if (Ctlp_FormulaTestIsQuantifierFree(formula)) {
3327 return ReplaceSimpleFormula(formula);
3328 }
3329
3330 switch (formulaType) {
3331 case Ctlp_AX_c:
3332 case Ctlp_EX_c:
3333 case Ctlp_AG_c:
3334 case Ctlp_EG_c:
3335 case Ctlp_AF_c:
3336 case Ctlp_EF_c:
3337 case Ctlp_NOT_c:
3338 newLeftFormula = Ctlp_FormulaCreateWitnessFormula(leftFormula);
3339 newRightFormula = NIL(Ctlp_Formula_t);
3340 break;
3341 case Ctlp_AU_c:
3342 case Ctlp_EU_c:
3343 /* If both or neither operands are simple, we choose the left one
3344 as important. Deal with special case of converted AG p (E true U p). */
3345 if ((formulaType == Ctlp_EU_c &&
3346 Ctlp_FormulaReadType(leftFormula) == Ctlp_TRUE_c) ||
3347 (Ctlp_FormulaTestIsQuantifierFree(leftFormula) &&
3348 !Ctlp_FormulaTestIsQuantifierFree(rightFormula))) {
3349 newLeftFormula = Ctlp_FormulaDup(leftFormula);
3350 newRightFormula = Ctlp_FormulaCreateWitnessFormula(rightFormula);
3351 } else {
3352 newLeftFormula = Ctlp_FormulaCreateWitnessFormula(leftFormula);
3353 newRightFormula = Ctlp_FormulaDup(rightFormula);
3354 }
3355 break;
3356 case Ctlp_OR_c:
3357 case Ctlp_AND_c:
3358 case Ctlp_THEN_c:
3359 /* Here we know one is not simple */
3360 if (Ctlp_FormulaTestIsQuantifierFree(leftFormula)) {
3361 newLeftFormula = Ctlp_FormulaDup(leftFormula);
3362 newRightFormula = Ctlp_FormulaCreateWitnessFormula(rightFormula);
3363 } else {
3364 newLeftFormula = Ctlp_FormulaCreateWitnessFormula(leftFormula);
3365 newRightFormula = Ctlp_FormulaDup(rightFormula);
3366 }
3367 break;
3368 case Ctlp_XOR_c:
3369 case Ctlp_EQ_c:
3370 newLeftFormula = Ctlp_FormulaDup(leftFormula);
3371 newRightFormula = Ctlp_FormulaDup(rightFormula);
3372 break;
3373 default:
3374 newLeftFormula = NIL(Ctlp_Formula_t);
3375 newRightFormula = NIL(Ctlp_Formula_t);
3376 fprintf(vis_stderr, "**Ctlp Error: Unexpected operator detected.\n");
3377 assert(0);
3378 break;
3379 }
3380 return Ctlp_FormulaCreate(formulaType,newLeftFormula,newRightFormula);
3381
3382} /* Ctlp_FormulaCreateWitnessFormula */
3383
3384
3385/*---------------------------------------------------------------------------*/
3386/* Definition of static functions */
3387/*---------------------------------------------------------------------------*/
3388
3389/**Function********************************************************************
3390
3391 Synopsis [Creates a CTL formula with just the type set.]
3392
3393 Description [Calls Ctlp_FormulaCreate with type, and all other fields NULL.]
3394
3395 SideEffects []
3396
3397 SeeAlso [Ctlp_FormulaCreate]
3398
3399******************************************************************************/
3400static Ctlp_Formula_t *
3401FormulaCreateWithType(
3402 Ctlp_FormulaType type)
3403{
3404 return (Ctlp_FormulaCreate(type, NIL(Ctlp_Formula_t), NIL(Ctlp_Formula_t)));
3405}
3406
3407
3408/**Function********************************************************************
3409
3410 Synopsis [The comparison function for the formula unique table.]
3411
3412 Description [The function takes as parameters two CTL formulae. It compares
3413 the formula type, the left child and the right child, and returns 0 if they
3414 match. Otherwise, it returns -1.]
3415
3416 SideEffects []
3417
3418 SeeAlso [FormulaHash]
3419
3420******************************************************************************/
3421static int
3422FormulaCompare(
3423 const char *key1,
3424 const char *key2)
3425{
3426 Ctlp_Formula_t *formula1 = (Ctlp_Formula_t *) key1;
3427 Ctlp_Formula_t *formula2 = (Ctlp_Formula_t *) key2;
3428
3429 assert(key1 != NIL(char));
3430 assert(key2 != NIL(char));
3431
3432
3433 if(formula1->type != formula2->type) {
3434 return -1;
3435 }
3436 if(formula1->type == Ctlp_ID_c) {
3437 if(strcmp((char *) (formula1->left), (char *) (formula2->left)) ||
3438 strcmp((char *) (formula1->right), (char *) (formula2->right))) {
3439 return -1;
3440 } else
3441 return 0;
3442 } else {
3443 if(formula1->left != formula2->left)
3444 return -1;
3445 if(formula1->right != formula2->right)
3446 return -1;
3447 if (formula1->type == Ctlp_Cmp_c &&
3448 formula1->compareValue != formula2->compareValue) {
3449 return -1;
3450 }
3451 return 0;
3452 }
3453}
3454
3455/**Function********************************************************************
3456
3457 Synopsis [The hash function for the formula unique table.]
3458
3459 Description [The function takes as parameter a CTL formula. If the formula
3460 type is Ctlp_ID_c, st_strhash is used with a concatenation of left and
3461 right children as the key string. Otherwise, something very similar to
3462 st_ptrhash is done.]
3463
3464 SideEffects []
3465
3466 SeeAlso [FormulaCompare]
3467
3468******************************************************************************/
3469static int
3470FormulaHash(
3471 char *key,
3472 int modulus)
3473{
3474 char *hashString;
3475 int hashValue;
3476 Ctlp_Formula_t *formula = (Ctlp_Formula_t *) key;
3477
3478 if(formula->type==Ctlp_ID_c) {
3479 hashString = util_strcat3((char *) (formula->left), (char *)
3480 (formula->right), "");
3481 hashValue = st_strhash(hashString, modulus);
3482 FREE(hashString);
3483 return hashValue;
3484 }
3485 return (int) ((((unsigned long) formula->left >>2) +
3486 ((unsigned long) formula->right >>2)) % modulus);
3487}
3488
3489/**Function********************************************************************
3490
3491 Synopsis [Hashes the formula into the unique table.]
3492
3493 Description [The function takes a formula and hashes it and all its
3494 subformulae into a unique table. It returns the unique formula identical to
3495 the formula being hashed. The formula returned will have maximum sharing
3496 with the formulae that are already present in uniqueTable. It returns
3497 NIL(Ctlp_Formula_t) if the formula is NIL(Ctlp_Formula_t).]
3498
3499 SideEffects [If a copy of some subformula of formula is present in
3500 uniqueTable then the copy is substituted for it and the reference count of
3501 the subform
3502 ula is decremented.]
3503
3504 SeeAlso [FormulaCompare]
3505
3506******************************************************************************/
3507static Ctlp_Formula_t *
3508FormulaHashIntoUniqueTable(
3509 Ctlp_Formula_t *formula,
3510 st_table *uniqueTable)
3511{
3512 Ctlp_Formula_t *uniqueFormula, *uniqueLeft, *uniqueRight;
3513
3514 if(formula == NIL(Ctlp_Formula_t))
3515 return NIL(Ctlp_Formula_t);
3516 if(st_lookup(uniqueTable, formula, &uniqueFormula)) {
3517 return uniqueFormula;
3518 }
3519 else {
3520 if(formula->type == Ctlp_ID_c) {
3521 st_insert(uniqueTable, formula, formula);
3522 return formula;
3523 }
3524 else {
3525 uniqueLeft = FormulaHashIntoUniqueTable(formula->left, uniqueTable);
3526 if(uniqueLeft != NIL(Ctlp_Formula_t))
3527 if(uniqueLeft != formula->left) {
3528 CtlpFormulaDecrementRefCount(formula->left);
3529 formula->left = uniqueLeft;
3530 CtlpFormulaIncrementRefCount(formula->left);
3531 }
3532 uniqueRight = FormulaHashIntoUniqueTable(formula->right, uniqueTable);
3533 if(uniqueRight != NIL(Ctlp_Formula_t))
3534 if(uniqueRight != formula->right) {
3535 CtlpFormulaDecrementRefCount(formula->right);
3536 formula->right = uniqueRight;
3537 CtlpFormulaIncrementRefCount(formula->right);
3538 }
3539 if(st_lookup(uniqueTable, formula, &uniqueFormula)) {
3540 return uniqueFormula;
3541 }
3542 else {
3543 st_insert(uniqueTable, formula, formula);
3544 return formula;
3545 }
3546 }
3547 }
3548}
3549
3550/**Function********************************************************************
3551
3552 Synopsis [Converts the formula tree to a DAG.]
3553
3554 Description [The function recursively builds an existential DAG for the
3555 formula. If a particular sub-formula has been encountered before, the
3556 converted existential sub-formula is pointed to by the field states and it
3557 is returned without creating a new formula.]
3558
3559 SideEffects [We abuse states to store which converted formula an original
3560 formula points to.]
3561
3562 SeeAlso []
3563
3564******************************************************************************/
3565static Ctlp_Formula_t *
3566FormulaConvertToExistentialDAG(
3567 Ctlp_Formula_t *formula)
3568{
3569
3570 Ctlp_Formula_t *new_;
3571 char *variableNameCopy, *valueNameCopy;
3572
3573 if(formula==NIL(Ctlp_Formula_t))
3574 return NIL(Ctlp_Formula_t);
3575
3576 if(formula->states!=NIL(mdd_t)) {
3577 Ctlp_Formula_t *temp = (Ctlp_Formula_t *) (formula->states);
3578
3579 ++(temp->refCount);
3580 return temp;
3581 }
3582
3583 /*
3584 * Recursively convert each subformula.
3585 */
3586
3587 switch(formula->type) {
3588 case Ctlp_EF_c:
3589 /* EFf --> (E true U f) */
3590 new_ = FormulaCreateWithType(Ctlp_EU_c);
3591 new_->left = FormulaCreateWithType(Ctlp_TRUE_c);
3592 new_->right = FormulaConvertToExistentialDAG(formula->left);
3593 new_->dbgInfo.convertedFlag = TRUE;
3594 break;
3595
3596 case Ctlp_AX_c:
3597 /* AXf --> !(EX(!f)) */
3598 new_ = FormulaCreateWithType(Ctlp_NOT_c);
3599 new_->left = FormulaCreateWithType(Ctlp_EX_c);
3600 new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
3601 new_->left->left->left = FormulaConvertToExistentialDAG(formula->left);
3602 new_->dbgInfo.convertedFlag = TRUE;
3603 break;
3604
3605 case Ctlp_AG_c:
3606 /* AGf --> ![(E true U !f)] */
3607 new_ = FormulaCreateWithType(Ctlp_NOT_c);
3608 new_->left = FormulaCreateWithType(Ctlp_EU_c);
3609 new_->left->left = FormulaCreateWithType(Ctlp_TRUE_c);
3610 new_->left->right = FormulaCreateWithType(Ctlp_NOT_c);
3611 new_->left->right->left = FormulaConvertToExistentialDAG(formula->left);
3612 new_->dbgInfo.convertedFlag = TRUE;
3613 break;
3614
3615 case Ctlp_AF_c:
3616 /* AFf --> ![EG(!f)] */
3617 new_ = FormulaCreateWithType(Ctlp_NOT_c);
3618 new_->left = FormulaCreateWithType(Ctlp_EG_c);
3619 new_->left->left = FormulaCreateWithType(Ctlp_NOT_c);
3620 new_->left->left->left = FormulaConvertToExistentialDAG(formula->left);
3621 new_->dbgInfo.convertedFlag = TRUE;
3622 break;
3623
3624 case Ctlp_AU_c:
3625 /* A[fUg] --> !((E[!g U (!f*!g)]) + (EG!g)) */
3626
3627 new_ = FormulaCreateWithType(Ctlp_NOT_c); /* top */
3628 new_->left = FormulaCreateWithType(Ctlp_OR_c); /* ((E[!g U (!f*!g)]) + (EG!g)) */
3629
3630 new_->left->right = FormulaCreateWithType(Ctlp_EG_c); /* EG !g */
3631 new_->left->right->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
3632 new_->left->right->left->left = FormulaConvertToExistentialDAG(formula->right); /* g */
3633
3634 new_->left->left = FormulaCreateWithType(Ctlp_EU_c); /* E[!g U (!f*!g)] */
3635 new_->left->left->left = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
3636 new_->left->left->left->left = FormulaConvertToExistentialDAG(formula->right); /* g */
3637 new_->left->left->right = FormulaCreateWithType(Ctlp_AND_c); /* !f*!g */
3638 new_->left->left->right->left = FormulaCreateWithType(Ctlp_NOT_c); /* !f */
3639 new_->left->left->right->left->left = FormulaConvertToExistentialDAG(formula->left); /* f */
3640 new_->left->left->right->right = FormulaCreateWithType(Ctlp_NOT_c); /* !g */
3641 new_->left->left->right->right->left = FormulaConvertToExistentialDAG(formula->right); /* g */
3642 new_->dbgInfo.convertedFlag = TRUE;
3643 break;
3644
3645 case Ctlp_ID_c:
3646 /* Make a copy of the name, and create a new formula. */
3647 variableNameCopy = util_strsav((char *)(formula->left));
3648 valueNameCopy = util_strsav((char *)(formula->right));
3649 new_ = Ctlp_FormulaCreate(Ctlp_ID_c, variableNameCopy, valueNameCopy);
3650 break;
3651
3652 case Ctlp_THEN_c:
3653 case Ctlp_EX_c:
3654 case Ctlp_EG_c:
3655 case Ctlp_EU_c:
3656 case Ctlp_OR_c:
3657 case Ctlp_AND_c:
3658 case Ctlp_NOT_c:
3659 case Ctlp_XOR_c:
3660 case Ctlp_EQ_c:
3661 case Ctlp_TRUE_c:
3662 case Ctlp_FALSE_c:
3663 /* These are already in the correct form. Just convert subformulas. */
3664 new_ = FormulaCreateWithType(formula->type);
3665 new_->left = FormulaConvertToExistentialDAG(formula->left);
3666 new_->right = FormulaConvertToExistentialDAG(formula->right);
3667 break;
3668
3669 default:
3670 fail("Unexpected type");
3671 }
3672
3673 formula->states = (mdd_t *) new_; /*using states as pointer to the converted
3674 formula */
3675 new_->dbgInfo.originalFormula = formula;
3676 return new_;
3677}
3678
3679
3680/**Function********************************************************************
3681
3682 Synopsis [Converts an existential formula to forward form.]
3683
3684 Description [Converts an existential formula to forward form. To
3685 convert current formula, it always refer to its parent node and left
3686 child of parent node. Current formula is right child of parent node.
3687 Parent node should be always Ctlp_AND_c and left child of parent node
3688 is already converted. States is used to store a parent pointer
3689 throughout the procedure.]
3690
3691 SideEffects []
3692
3693 SeeAlso []
3694
3695******************************************************************************/
3696static void
3697FormulaConvertToForward(Ctlp_Formula_t *formula, int compareValue)
3698{
3699 Ctlp_Formula_t *parent, *save;
3700 Ctlp_Formula_t *p, *q, *r, *f, *g;
3701 int p_qf, q_qf;
3702 int same_order;
3703
3704 if (formula == NIL(Ctlp_Formula_t))
3705 return;
3706
3707 parent = (Ctlp_Formula_t *)formula->states;
3708 r = parent->left; /* already converted */
3709
3710 /*
3711 * Recursively convert each subformula.
3712 */
3713
3714 switch(formula->type) {
3715 case Ctlp_EX_c:
3716 /*
3717 ** p ^ EXf -> Img(p) ^ f , Img(p) = EY(p)
3718 **
3719 ** * *
3720 ** / \ / \
3721 ** p EX => EY f
3722 ** | |
3723 ** f p
3724 */
3725
3726 formula->type = Ctlp_EY_c;
3727 save = formula->left;
3728 formula->left = parent->left;
3729 parent->left = formula;
3730 parent->right = save;
3731
3732 parent->top = 1;
3733 parent->compareValue = compareValue;
3734 parent->right->states = (mdd_t *)parent;
3735
3736 FormulaConvertToForward(parent->right, compareValue);
3737 break;
3738
3739 case Ctlp_EF_c:
3740 /*
3741 ** EFf --> (E true U f)
3742 ** p ^ (E true U f) --> FwdU(p, true) ^ f
3743 **
3744 ** * *
3745 ** / \ / \
3746 ** p EF => FwdU f
3747 ** | / \
3748 ** f p true
3749 */
3750
3751 formula->type = Ctlp_FwdU_c;
3752 save = formula->left;
3753 formula->right = FormulaCreateWithType(Ctlp_TRUE_c);
3754 formula->left = parent->left;
3755 parent->left = formula;
3756 parent->right = save;
3757
3758 parent->top = 1;
3759 parent->compareValue = compareValue;
3760 parent->right->states = (mdd_t *)parent;
3761
3762
3763 FormulaConvertToForward(parent->right, compareValue);
3764 break;
3765
3766 case Ctlp_EU_c:
3767 /*
3768 ** p ^ (E q U f) --> FwdU(p, q) ^ f
3769 **
3770 ** * *
3771 ** / \ / \
3772 ** p EU => FwdU f
3773 ** /\ / \
3774 ** q f p q
3775 */
3776
3777 formula->type = Ctlp_FwdU_c;
3778 save = formula->right;
3779 formula->right = formula->left;
3780 formula->left = parent->left;
3781 parent->left = formula;
3782 parent->right = save;
3783
3784 parent->top = 1;
3785 parent->compareValue = compareValue;
3786 parent->right->states = (mdd_t *)parent;
3787
3788 FormulaConvertToForward(parent->right, compareValue);
3789 break;
3790
3791 case Ctlp_EG_c:
3792 /*
3793 ** p ^ EGq --> FwdG(p, q)
3794 **
3795 ** * FwdG
3796 ** / \ / \
3797 ** p EG => p q
3798 ** /
3799 ** q
3800 */
3801
3802 parent->type = Ctlp_FwdG_c;
3803 parent->right = formula->left;
3804
3805 formula->left = NIL(Ctlp_Formula_t);
3806 formula->states = NIL(mdd_t);
3807 Ctlp_FormulaFree(formula);
3808
3809 parent->top = 1;
3810 parent->compareValue = compareValue;
3811 break;
3812
3813 case Ctlp_NOT_c:
3814 if (formula->left->type == Ctlp_NOT_c) {
3815 /*
3816 ** * *
3817 ** / \ => / \
3818 ** r NOT r f
3819 ** /
3820 ** NOT
3821 ** /
3822 ** f
3823 */
3824
3825 parent->right = formula->left->left;
3826 formula->left->left = NIL(Ctlp_Formula_t);
3827 formula->left->states = NIL(mdd_t);
3828 Ctlp_FormulaFree(formula->left);
3829 formula->left = NIL(Ctlp_Formula_t);
3830 formula->states = NIL(mdd_t);
3831 Ctlp_FormulaFree(formula);
3832
3833 parent->top = 1;
3834 parent->compareValue = compareValue;
3835 parent->right->states = (mdd_t *)parent;
3836
3837 FormulaConvertToForward(parent->right, compareValue);
3838 } else if (formula->left->type == Ctlp_THEN_c) {
3839 /*
3840 ** *
3841 ** / \
3842 ** r NOT
3843 ** /
3844 ** THEN
3845 ** / \
3846 ** p q
3847 */
3848
3849 p = formula->left->left;
3850 q = formula->left->right;
3851 p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
3852 q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
3853
3854 if (p_qf && q_qf)
3855 break;
3856 else if (p_qf ||
3857 (p_qf == 0 && q_qf == 0 && !FormulaIsConvertible(q))) {
3858 /*
3859 ** !(p -> q) = p * !q
3860 **
3861 ** * => * => *
3862 ** / \ / \ / \
3863 ** r NOT r * * NOT
3864 ** / / \ / \ /
3865 ** THEN p NOT r p q
3866 ** / \ /
3867 ** p q q
3868 */
3869
3870 parent->left = formula->left;
3871 parent->left->type = Ctlp_AND_c;
3872 parent->left->left = r;
3873 parent->left->right = p;
3874 parent->right = formula;
3875 parent->right->left = q;
3876
3877 parent->top = 1;
3878 parent->compareValue = compareValue;
3879 parent->right->states = (mdd_t *)parent;
3880
3881 FormulaConvertToForward(parent->right, compareValue);
3882 } else {
3883 /*
3884 ** !(p -> q) = p * !q
3885 **
3886 ** * => * => *
3887 ** / \ / \ / \
3888 ** r NOT r * * p
3889 ** / / \ / \
3890 ** THEN p NOT r NOT
3891 ** / \ / /
3892 ** p q q q
3893 */
3894
3895 parent->left = formula->left;
3896 parent->left->type = Ctlp_AND_c;
3897 parent->left->left = r;
3898 parent->left->right = formula;
3899 parent->left->right->left = q;
3900 parent->left->right->right = NIL(Ctlp_Formula_t);
3901 parent->right = p;
3902
3903 parent->top = 1;
3904 parent->compareValue = compareValue;
3905 p->states = (mdd_t *)parent;
3906
3907 FormulaConvertToForward(p, compareValue);
3908 }
3909 } else if (formula->left->type == Ctlp_OR_c) {
3910 /*
3911 ** !(p + q) = !p * !q
3912 **
3913 ** * => * => *
3914 ** / \ / \ / \
3915 ** r NOT r * * NOT
3916 ** / / \ / \ /
3917 ** OR NOT NOT r NOT g=q(p)
3918 ** / \ / / /
3919 ** p q p q f=p(q)
3920 */
3921
3922 p = formula->left->left;
3923 q = formula->left->right;
3924 p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
3925 q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
3926
3927 if (p_qf && q_qf)
3928 break;
3929 else if (p_qf) {
3930 f = p;
3931 g = q;
3932 } else if (q_qf) {
3933 f = q;
3934 g = p;
3935 } else {
3936 if (!FormulaIsConvertible(q)) {
3937 f = p;
3938 g = q;
3939 } else {
3940 f = q;
3941 g = p;
3942 }
3943 }
3944
3945 parent->left = formula->left;
3946 parent->left->type = Ctlp_AND_c;
3947 parent->left->left = r;
3948 parent->left->right = formula;
3949 parent->left->right->left = f;
3950 parent->left->right->right = NIL(Ctlp_Formula_t);
3951 parent->right = FormulaCreateWithType(Ctlp_NOT_c);
3952 parent->right->left = g;
3953
3954 parent->top = 1;
3955 parent->compareValue = compareValue;
3956 parent->right->states = (mdd_t *)parent;
3957
3958 FormulaConvertToForward(parent->right, compareValue);
3959 } else if (formula->left->type == Ctlp_AND_c) {
3960 /*
3961 ** !(p * q) = !p + !q
3962 **
3963 ** * *(+) *(+)
3964 ** / \ / \ / \
3965 ** r NOT => r OR => * *
3966 ** / / \ / \ / \
3967 ** AND NOT NOT r NOT r NOT
3968 ** / \ / / / /
3969 ** p q p q p q
3970 */
3971
3972 p = formula->left->left;
3973 q = formula->left->right;
3974
3975 if (Ctlp_FormulaTestIsQuantifierFree(p) &&
3976 Ctlp_FormulaTestIsQuantifierFree(q)) {
3977 break;
3978 }
3979
3980 if (compareValue)
3981 parent->type = Ctlp_OR_c;
3982 parent->left = formula->left;
3983 parent->left->left = r;
3984 parent->left->right = formula;
3985 parent->left->right->left = p;
3986
3987 parent->right = FormulaCreateWithType(Ctlp_AND_c);
3988 parent->right->left = Ctlp_FormulaDup(r);
3989 parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
3990 parent->right->right->left = q;
3991
3992 parent->top = 0;
3993 parent->left->top = 1;
3994 parent->right->top = 1;
3995 parent->left->compareValue = compareValue;
3996 parent->right->compareValue = compareValue;
3997 parent->left->right->states = (mdd_t *)parent->left;
3998 parent->right->right->states = (mdd_t *)parent->right;
3999
4000 FormulaConvertToForward(parent->left->right, compareValue);
4001 FormulaConvertToForward(parent->right->right, compareValue);
4002 } else if (formula->left->type == Ctlp_XOR_c) {
4003 /*
4004 ** !(p ^ q) = p * q + !p * !q
4005 **
4006 ** * *(+) *(+)
4007 ** / \ / \ / \
4008 ** | | => * * => * *
4009 ** | | / \ / \ / \ / \
4010 ** r NOT r * r * * g * NOT
4011 ** / / \ / \ / \ / \ /
4012 ** XOR p q NOT NOT r f r NOT g=q(p)
4013 ** / \ / / /
4014 ** p q p q f=p(q)
4015 */
4016
4017 p = formula->left->left;
4018 q = formula->left->right;
4019 p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
4020 q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
4021
4022 same_order = 1;
4023 if (p_qf && q_qf)
4024 break;
4025 else if (p_qf) {
4026 f = p;
4027 g = q;
4028 } else if (q_qf) {
4029 f = q;
4030 g = p;
4031 } else {
4032 if (FormulaIsConvertible(p) && !FormulaIsConvertible(q)) {
4033 /*
4034 ** !(p ^ q) = q * p + !p * !q
4035 **
4036 ** * *(+) *(+)
4037 ** / \ / \ / \
4038 ** | | => * * => * *
4039 ** | | / \ / \ / \ / \
4040 ** r NOT r * r * * p * NOT
4041 ** / / \ / \ / \ / \ /
4042 ** XOR p q NOT NOT r q r NOT q
4043 ** / \ / / /
4044 ** p q p q p
4045 */
4046
4047 f = q;
4048 g = p;
4049 same_order = 0;
4050 } else if (!FormulaIsConvertible(p) && FormulaIsConvertible(q)) {
4051 /*
4052 ** !(p ^ q) = p * q + !q * !p
4053 **
4054 ** * *(+) *(+)
4055 ** / \ / \ / \
4056 ** | | => * * => * *
4057 ** | | / \ / \ / \ / \
4058 ** r NOT r * r * * q * NOT
4059 ** / / \ / \ / \ / \ /
4060 ** XOR p q NOT NOT r p r NOT p
4061 ** / \ / / /
4062 ** p q p q q
4063 */
4064
4065 f = p;
4066 g = q;
4067 same_order = 0;
4068 } else {
4069 f = p;
4070 g = q;
4071 }
4072 }
4073
4074 if (compareValue)
4075 parent->type = Ctlp_OR_c;
4076 parent->left = formula;
4077 parent->left->type = Ctlp_AND_c;
4078 parent->left->left->type = Ctlp_AND_c;
4079 parent->left->left->left = r;
4080 parent->left->left->right = f;
4081 parent->left->right = g;
4082
4083 parent->right = FormulaCreateWithType(Ctlp_AND_c);
4084 parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
4085 parent->right->left->left = Ctlp_FormulaDup(r);
4086 parent->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4087 if (same_order)
4088 parent->right->left->right->left = Ctlp_FormulaDup(f);
4089 else
4090 parent->right->left->right->left = Ctlp_FormulaDup(g);
4091 parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
4092 if (same_order)
4093 parent->right->right->left = Ctlp_FormulaDup(g);
4094 else
4095 parent->right->right->left = Ctlp_FormulaDup(f);
4096
4097 parent->top = 0;
4098 parent->left->top = 1;
4099 parent->right->top = 1;
4100 parent->left->compareValue = compareValue;
4101 parent->right->compareValue = compareValue;
4102 parent->left->right->states = (mdd_t *)parent->left;
4103 parent->right->right->states = (mdd_t *)parent->right;
4104
4105 FormulaConvertToForward(parent->left->right, compareValue);
4106 FormulaConvertToForward(parent->right->right, compareValue);
4107 } else if (formula->left->type == Ctlp_EQ_c) {
4108 /*
4109 ** !(EQ(p, q) = XOR(p, q)
4110 **
4111 ** * *(+) *(+)
4112 ** / \ / \ / \
4113 ** | | => * * => * *
4114 ** | | / \ / \ / \ / \
4115 ** r NOT r * r * * g * NOT
4116 ** / / \ / \ / \ / \ /
4117 ** EQ p NOT NOT q r NOT r f g=q(p)
4118 ** / \ / / /
4119 ** p q q p f=p(q)
4120 */
4121
4122 p = formula->left->left;
4123 q = formula->left->right;
4124 p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
4125 q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
4126
4127 if (p_qf && q_qf)
4128 break;
4129 else if (p_qf) {
4130 f = p;
4131 g = q;
4132 } else if (q_qf) {
4133 f = q;
4134 g = p;
4135 } else {
4136 if (FormulaIsConvertible(p) && FormulaIsConvertible(q)) {
4137 /*
4138 ** !(EQ(p, q) = XOR(p, q)
4139 **
4140 ** * *(+) *(+)
4141 ** / \ / \ / \
4142 ** | | => * * => * *
4143 ** | | / \ / \ / \ / \
4144 ** r NOT r * r * * p * q
4145 ** / / \ / \ / \ / \
4146 ** EQ p NOT NOT q r NOT r NOT
4147 ** / \ / / / /
4148 ** p q q p q p
4149 */
4150
4151 if (compareValue)
4152 parent->type = Ctlp_OR_c;
4153 parent->left = parent->right;
4154 parent->left->type = Ctlp_AND_c;
4155 parent->left->left->type = Ctlp_AND_c;
4156 parent->left->left->left = r;
4157 parent->left->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4158 parent->left->left->right->left = q;
4159 parent->left->right = p;
4160
4161 parent->right = FormulaCreateWithType(Ctlp_AND_c);
4162 parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
4163 parent->right->left->left = Ctlp_FormulaDup(r);
4164 parent->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4165 parent->right->left->right->left = Ctlp_FormulaDup(p);
4166 parent->right->right = Ctlp_FormulaDup(q);
4167
4168 parent->top = 0;
4169 parent->left->top = 1;
4170 parent->right->top = 1;
4171 parent->left->compareValue = compareValue;
4172 parent->right->compareValue = compareValue;
4173 parent->left->right->states = (mdd_t *)parent->left;
4174 parent->right->right->states = (mdd_t *)parent->right;
4175
4176 FormulaConvertToForward(parent->left->right, compareValue);
4177 FormulaConvertToForward(parent->right->right, compareValue);
4178 break;
4179 } else if (!FormulaIsConvertible(p) && !FormulaIsConvertible(q)) {
4180 /*
4181 ** !(EQ(p, q) = XOR(p, q)
4182 **
4183 ** * *(+) *(+)
4184 ** / \ / \ / \
4185 ** | | => * * => * *
4186 ** | | / \ / \ / \ / \
4187 ** r NOT r * r * * NOT * NOT
4188 ** / / \ / \ / \ / / \ /
4189 ** EQ p NOT NOT q r p q r q p
4190 ** / \ / /
4191 ** p q q p
4192 */
4193
4194 if (compareValue)
4195 parent->type = Ctlp_OR_c;
4196 parent->left = parent->right;
4197 parent->left->type = Ctlp_AND_c;
4198 parent->left->left->type = Ctlp_AND_c;
4199 parent->left->left->left = r;
4200 parent->left->left->right = p;
4201 parent->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4202 parent->left->right->left = q;
4203
4204 parent->right = FormulaCreateWithType(Ctlp_AND_c);
4205 parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
4206 parent->right->left->left = Ctlp_FormulaDup(r);
4207 parent->right->left->right = Ctlp_FormulaDup(q);
4208 parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
4209 parent->right->right->left = Ctlp_FormulaDup(p);
4210
4211 parent->top = 0;
4212 parent->left->top = 1;
4213 parent->right->top = 1;
4214 parent->left->compareValue = compareValue;
4215 parent->right->compareValue = compareValue;
4216 parent->left->right->states = (mdd_t *)parent->left;
4217 parent->right->right->states = (mdd_t *)parent->right;
4218
4219 FormulaConvertToForward(parent->left->right, compareValue);
4220 FormulaConvertToForward(parent->right->right, compareValue);
4221 break;
4222 } else {
4223 f = p;
4224 g = q;
4225 }
4226 }
4227
4228 if (compareValue)
4229 parent->type = Ctlp_OR_c;
4230 parent->left = parent->right;
4231 parent->left->type = Ctlp_AND_c;
4232 parent->left->left->type = Ctlp_AND_c;
4233 parent->left->left->left = r;
4234 parent->left->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4235 parent->left->left->right->left = f;
4236 parent->left->right = g;
4237
4238 parent->right = FormulaCreateWithType(Ctlp_AND_c);
4239 parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
4240 parent->right->left->left = Ctlp_FormulaDup(r);
4241 parent->right->left->right = Ctlp_FormulaDup(f);
4242 parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
4243 parent->right->right->left = Ctlp_FormulaDup(g);
4244
4245 parent->top = 0;
4246 parent->left->top = 1;
4247 parent->right->top = 1;
4248 parent->left->compareValue = compareValue;
4249 parent->right->compareValue = compareValue;
4250 parent->left->right->states = (mdd_t *)parent->left;
4251 parent->right->right->states = (mdd_t *)parent->right;
4252
4253 FormulaConvertToForward(parent->left->right, compareValue);
4254 FormulaConvertToForward(parent->right->right, compareValue);
4255 }
4256 break;
4257
4258 case Ctlp_THEN_c:
4259 /*
4260 ** (p -> q) = !p + q
4261 **
4262 ** * *(+)
4263 ** / \ / \
4264 ** r THEN => * *
4265 ** / \ / \ / \
4266 ** p q r NOT r q
4267 ** /
4268 ** p
4269 */
4270
4271 p = formula->left;
4272 q = formula->right;
4273
4274 if (Ctlp_FormulaTestIsQuantifierFree(p) &&
4275 Ctlp_FormulaTestIsQuantifierFree(q)) {
4276 break;
4277 }
4278
4279 if (compareValue)
4280 parent->type = Ctlp_OR_c;
4281 parent->left = formula;
4282 parent->left->type = Ctlp_AND_c;
4283 parent->left->left = r;
4284 parent->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4285 parent->left->right->left = p;
4286
4287 parent->right = FormulaCreateWithType(Ctlp_AND_c);
4288 parent->right->left = Ctlp_FormulaDup(r);
4289 parent->right->right = q;
4290
4291 parent->top = 0;
4292 parent->left->top = 1;
4293 parent->right->top = 1;
4294 parent->left->compareValue = compareValue;
4295 parent->right->compareValue = compareValue;
4296 parent->left->right->states = (mdd_t *)parent->left;
4297 parent->right->right->states = (mdd_t *)parent->right;
4298
4299 FormulaConvertToForward(parent->left->right, compareValue);
4300 FormulaConvertToForward(parent->right->right, compareValue);
4301 break;
4302
4303 case Ctlp_OR_c:
4304 /*
4305 ** * *(+)
4306 ** / \ / \
4307 ** r OR => * *
4308 ** / \ / \ / \
4309 ** p q r p r q
4310 */
4311
4312 p = formula->left;
4313 q = formula->right;
4314
4315 if (Ctlp_FormulaTestIsQuantifierFree(p) &&
4316 Ctlp_FormulaTestIsQuantifierFree(q)) {
4317 break;
4318 }
4319
4320 if (compareValue)
4321 parent->type = Ctlp_OR_c;
4322 parent->left = formula;
4323 parent->left->type = Ctlp_AND_c;
4324 parent->left->left = r;
4325 parent->left->right = p;
4326
4327 parent->right = FormulaCreateWithType(Ctlp_AND_c);
4328 parent->right->left = Ctlp_FormulaDup(r);
4329 parent->right->right = q;
4330
4331 parent->top = 0;
4332 parent->left->top = 1;
4333 parent->right->top = 1;
4334 parent->left->compareValue = compareValue;
4335 parent->right->compareValue = compareValue;
4336 parent->left->right->states = (mdd_t *)parent->left;
4337 parent->right->right->states = (mdd_t *)parent->right;
4338
4339 FormulaConvertToForward(parent->left->right, compareValue);
4340 FormulaConvertToForward(parent->right->right, compareValue);
4341 break;
4342
4343 case Ctlp_AND_c:
4344 /*
4345 ** * => *
4346 ** / \ / \
4347 ** r AND AND g=q(p)
4348 ** / \ / \
4349 ** p q r f=p(q)
4350 */
4351
4352 p = formula->left;
4353 q = formula->right;
4354 p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
4355 q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
4356
4357 if (p_qf && q_qf)
4358 break;
4359 else if (q_qf) {
4360 f = q;
4361 g = p;
4362 } else {
4363 f = p;
4364 g = q;
4365 }
4366
4367 parent->left = parent->right;
4368 parent->left->left = r;
4369 parent->left->right = f;
4370 parent->right = g;
4371
4372 parent->top = 1;
4373 parent->compareValue = compareValue;
4374 g->states = (mdd_t *)parent;
4375
4376 FormulaConvertToForward(g, compareValue);
4377 break;
4378
4379 case Ctlp_XOR_c:
4380 /*
4381 ** * *(+) *(+)
4382 ** / \ / \ / \
4383 ** | | => * * => * *
4384 ** | | / \ / \ / \ / \
4385 ** r XOR r * r * * NOT * g=q(p)
4386 ** / \ / \ / \ / \ / / \
4387 ** p q q NOT NOT p r f g r NOT
4388 ** / / /
4389 ** p q f=p(q)
4390 */
4391
4392 p = formula->left;
4393 q = formula->right;
4394 p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
4395 q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
4396
4397 if (p_qf && q_qf)
4398 break;
4399 else if (p_qf) {
4400 f = p;
4401 g = q;
4402 } else if (q_qf) {
4403 f = q;
4404 g = p;
4405 } else {
4406 if (FormulaIsConvertible(p) && FormulaIsConvertible(q)) {
4407 /*
4408 ** * *(+) *(+)
4409 ** / \ / \ / \
4410 ** | | => * * => * *
4411 ** | | / \ / \ / \ / \
4412 ** r XOR r * r * * q * p
4413 ** / \ / \ / \ / \ / \
4414 ** p q q NOT NOT p r NOT r NOT
4415 ** / / / /
4416 ** p q p q
4417 */
4418
4419 if (compareValue)
4420 parent->type = Ctlp_OR_c;
4421 parent->left = parent->right;
4422 parent->left->type = Ctlp_AND_c;
4423 parent->left->left->type = Ctlp_AND_c;
4424 parent->left->left->left = r;
4425 parent->left->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4426 parent->left->left->right->left = p;
4427 parent->left->right = q;
4428
4429 parent->right = FormulaCreateWithType(Ctlp_AND_c);
4430 parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
4431 parent->right->left->left = Ctlp_FormulaDup(r);
4432 parent->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4433 parent->right->left->right->left = Ctlp_FormulaDup(q);
4434 parent->right->right = Ctlp_FormulaDup(p);
4435
4436 parent->top = 0;
4437 parent->left->top = 1;
4438 parent->right->top = 1;
4439 parent->left->compareValue = compareValue;
4440 parent->right->compareValue = compareValue;
4441 parent->left->right->states = (mdd_t *)parent->left;
4442 parent->right->right->states = (mdd_t *)parent->right;
4443
4444 FormulaConvertToForward(parent->left->right, compareValue);
4445 FormulaConvertToForward(parent->right->right, compareValue);
4446 break;
4447 } else if (!FormulaIsConvertible(p) && !FormulaIsConvertible(q)) {
4448 /*
4449 ** * *(+) *(+)
4450 ** / \ / \ / \
4451 ** | | => * * => * *
4452 ** | | / \ / \ / \ / \
4453 ** r XOR r * r * * NOT * NOT
4454 ** / \ / \ / \ / \ / / \ /
4455 ** p q q NOT NOT p r p q r q p
4456 ** / /
4457 ** p q
4458 */
4459
4460 if (compareValue)
4461 parent->type = Ctlp_OR_c;
4462 parent->left = parent->right;
4463 parent->left->type = Ctlp_AND_c;
4464 parent->left->left->type = Ctlp_AND_c;
4465 parent->left->left->left = r;
4466 parent->left->left->right = p;
4467 parent->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4468 parent->left->right->left = q;
4469
4470 parent->right = FormulaCreateWithType(Ctlp_AND_c);
4471 parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
4472 parent->right->left->left = Ctlp_FormulaDup(r);
4473 parent->right->left->right = Ctlp_FormulaDup(q);
4474 parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
4475 parent->right->right->left = Ctlp_FormulaDup(p);
4476
4477 parent->top = 0;
4478 parent->left->top = 1;
4479 parent->right->top = 1;
4480 parent->left->compareValue = compareValue;
4481 parent->right->compareValue = compareValue;
4482 parent->left->right->states = (mdd_t *)parent->left;
4483 parent->right->right->states = (mdd_t *)parent->right;
4484
4485 FormulaConvertToForward(parent->left->right, compareValue);
4486 FormulaConvertToForward(parent->right->right, compareValue);
4487 break;
4488 } else {
4489 f = p;
4490 g = q;
4491 }
4492 }
4493
4494 if (compareValue)
4495 parent->type = Ctlp_OR_c;
4496 parent->left = parent->right;
4497 parent->left->type = Ctlp_AND_c;
4498 parent->left->left = FormulaCreateWithType(Ctlp_AND_c);
4499 parent->left->left->left = r;
4500 parent->left->left->right = f;
4501 parent->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4502 parent->left->right->left = g;
4503
4504 parent->right = FormulaCreateWithType(Ctlp_AND_c);
4505 parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
4506 parent->right->left->left = Ctlp_FormulaDup(r);
4507 parent->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4508 parent->right->left->right->left = Ctlp_FormulaDup(f);
4509 parent->right->right = Ctlp_FormulaDup(g);
4510
4511 parent->top = 0;
4512 parent->left->top = 1;
4513 parent->right->top = 1;
4514 parent->left->compareValue = compareValue;
4515 parent->right->compareValue = compareValue;
4516 parent->left->right->states = (mdd_t *)parent->left;
4517 parent->right->right->states = (mdd_t *)parent->right;
4518
4519 FormulaConvertToForward(parent->left->right, compareValue);
4520 FormulaConvertToForward(parent->right->right, compareValue);
4521 break;
4522
4523 case Ctlp_EQ_c:
4524 /*
4525 ** * *(+) *(+)
4526 ** / \ / \ / \
4527 ** | | => * * => * *
4528 ** | | / \ / \ / \ / \
4529 ** r EQ r * r * * g * NOT
4530 ** /\ / \ / \ / \ / \ /
4531 ** p q p q NOT NOT r f r NOT g=q(p)
4532 ** / / /
4533 ** p q f=p(q)
4534 */
4535
4536 p = formula->left;
4537 q = formula->right;
4538 p_qf = Ctlp_FormulaTestIsQuantifierFree(p);
4539 q_qf = Ctlp_FormulaTestIsQuantifierFree(q);
4540
4541 same_order = 1;
4542 if (p_qf && q_qf)
4543 break;
4544 else if (p_qf) {
4545 f = p;
4546 g = q;
4547 } else if (q_qf) {
4548 f = q;
4549 g = p;
4550 } else {
4551 if (FormulaIsConvertible(p) && !FormulaIsConvertible(q)) {
4552 /*
4553 ** * *(+) *(+)
4554 ** / \ / \ / \
4555 ** | | => * * => * *
4556 ** | | / \ / \ / \ / \
4557 ** r EQ r * r * * p * NOT
4558 ** /\ / \ / \ / \ / \ /
4559 ** p q p q NOT NOT r q r NOT q
4560 ** / / /
4561 ** p q p
4562 */
4563
4564 f = q;
4565 g = p;
4566 same_order = 0;
4567 } else if (!FormulaIsConvertible(p) && FormulaIsConvertible(q)) {
4568 /*
4569 ** * *(+) *(+)
4570 ** / \ / \ / \
4571 ** | | => * * => * *
4572 ** | | / \ / \ / \ / \
4573 ** r EQ r * r * * q * NOT
4574 ** /\ / \ / \ / \ / \ /
4575 ** p q p q NOT NOT r p r NOT p
4576 ** / / /
4577 ** p q q
4578 */
4579
4580 f = p;
4581 g = q;
4582 same_order = 0;
4583 } else {
4584 f = p;
4585 g = q;
4586 }
4587 }
4588
4589 if (compareValue)
4590 parent->type = Ctlp_OR_c;
4591 parent->left = parent->right;
4592 parent->left->type = Ctlp_AND_c;
4593 parent->left->left = FormulaCreateWithType(Ctlp_AND_c);
4594 parent->left->left->left = r;
4595 parent->left->left->right = f;
4596 parent->left->right = g;
4597
4598 parent->right = FormulaCreateWithType(Ctlp_AND_c);
4599 parent->right->left = FormulaCreateWithType(Ctlp_AND_c);
4600 parent->right->left->left = Ctlp_FormulaDup(r);
4601 parent->right->left->right = FormulaCreateWithType(Ctlp_NOT_c);
4602 if (same_order)
4603 parent->right->left->right->left = Ctlp_FormulaDup(f);
4604 else
4605 parent->right->left->right->left = Ctlp_FormulaDup(g);
4606 parent->right->right = FormulaCreateWithType(Ctlp_NOT_c);
4607 if (same_order)
4608 parent->right->right->left = Ctlp_FormulaDup(g);
4609 else
4610 parent->right->right->left = Ctlp_FormulaDup(f);
4611
4612 parent->top = 0;
4613 parent->left->top = 1;
4614 parent->right->top = 1;
4615 parent->left->compareValue = compareValue;
4616 parent->right->compareValue = compareValue;
4617 parent->left->right->states = (mdd_t *)parent->left;
4618 parent->right->right->states = (mdd_t *)parent->right;
4619
4620 FormulaConvertToForward(parent->left->right, compareValue);
4621 FormulaConvertToForward(parent->right->right, compareValue);
4622 break;
4623
4624 case Ctlp_AX_c:
4625 case Ctlp_AG_c:
4626 case Ctlp_AF_c:
4627 case Ctlp_AU_c:
4628 fprintf(vis_stderr,
4629 "** ctl error : invalid node type in converting to forward formula.\n"
4630 );
4631 assert(0);
4632 break;
4633
4634 case Ctlp_ID_c:
4635 case Ctlp_TRUE_c:
4636 case Ctlp_FALSE_c:
4637 break;
4638
4639 default:
4640 fail("Unexpected type");
4641 }
4642}
4643
4644
4645/**Function********************************************************************
4646
4647 Synopsis [Inserts compare nodes into forward formula.]
4648
4649 Description [Inserts compare nodes into forward formula.]
4650
4651 SideEffects []
4652
4653 SeeAlso []
4654
4655******************************************************************************/
4656static void
4657FormulaInsertForwardCompareNodes(Ctlp_Formula_t *formula,
4658 Ctlp_Formula_t *parent,
4659 int compareValue)
4660{
4661 Ctlp_Formula_t *new_;
4662
4663 if (formula->top) {
4664 if (!parent) {
4665 new_ = FormulaCreateWithType(Ctlp_Cmp_c);
4666 memcpy((void *)new_, (void *)formula, sizeof(Ctlp_Formula_t));
4667 formula->type = Ctlp_Cmp_c;
4668 formula->left = new_;
4669 formula->right = FormulaCreateWithType(Ctlp_FALSE_c);
4670 formula->compareValue = compareValue;
4671 } else {
4672 new_ = FormulaCreateWithType(Ctlp_Cmp_c);
4673 new_->left = formula;
4674 new_->right = FormulaCreateWithType(Ctlp_FALSE_c);
4675 new_->compareValue = compareValue;
4676 if (parent->left == formula)
4677 parent->left = new_;
4678 else
4679 parent->right = new_;
4680 }
4681 return;
4682 }
4683 FormulaInsertForwardCompareNodes(formula->left, formula, compareValue);
4684 FormulaInsertForwardCompareNodes(formula->right, formula, compareValue);
4685}
4686
4687
4688/**Function********************************************************************
4689
4690 Synopsis [Determines which conversion formula is better.]
4691
4692 Description [Determines which conversion formula is better between
4693 init ^ f != FALSE and init ^ !f == FALSE.]
4694
4695 SideEffects []
4696
4697 SeeAlso []
4698
4699******************************************************************************/
4700static int
4701FormulaGetCompareValue(Ctlp_Formula_t *formula)
4702{
4703 int compareValue;
4704
4705 if (FormulaIsConvertible(formula))
4706 compareValue = 1; /* check whether the result is not FALSE */
4707 else
4708 compareValue = 0; /* check whether the result is FALSE. */
4709
4710 return(compareValue);
4711}
4712
4713
4714/**Function********************************************************************
4715
4716 Synopsis [Checks whether a formula can be converted to forward further.]
4717
4718 Description [Checks whether a formula can be converted to forward further.
4719 It returns 1 if it is convertible, and returns 0 if it is not convertible,
4720 and returns 2 if it is partially convertible.]
4721
4722 SideEffects []
4723
4724 SeeAlso []
4725
4726******************************************************************************/
4727static int
4728FormulaIsConvertible(Ctlp_Formula_t *formula)
4729{
4730 int convertible;
4731 int value1, value2;
4732
4733 if (Ctlp_FormulaTestIsQuantifierFree(formula))
4734 convertible = 1;
4735 else if (formula->type == Ctlp_ID_c)
4736 convertible = 1;
4737 else if (formula->type == Ctlp_EX_c ||
4738 formula->type == Ctlp_EU_c ||
4739 formula->type == Ctlp_EF_c ||
4740 formula->type == Ctlp_EG_c) {
4741 convertible = 1;
4742 } else if (formula->type == Ctlp_NOT_c) {
4743 if (formula->left->type == Ctlp_NOT_c) {
4744 if (formula->left->left->type == Ctlp_EX_c ||
4745 formula->left->left->type == Ctlp_EU_c ||
4746 formula->left->left->type == Ctlp_EF_c ||
4747 formula->left->left->type == Ctlp_EG_c) {
4748 convertible = 1;
4749 } else {
4750 convertible = FormulaIsConvertible(formula->left->left);
4751 }
4752 } else {
4753 if (formula->left->type == Ctlp_EX_c ||
4754 formula->left->type == Ctlp_EU_c ||
4755 formula->left->type == Ctlp_EF_c ||
4756 formula->left->type == Ctlp_EG_c) {
4757 convertible = 0;
4758 } else {
4759 value1 = FormulaIsConvertible(formula->left);
4760 value2 = FormulaIsConvertible(formula->right);
4761 switch (formula->type) {
4762 case Ctlp_AND_c:
4763 case Ctlp_OR_c:
4764 convertible = (value1 & 0x1) * (value2 & 0x1);
4765 break;
4766 case Ctlp_THEN_c:
4767 convertible = value1 * (value2 & 0x1);
4768 break;
4769 default :
4770 convertible = 2;
4771 break;
4772 }
4773 }
4774 }
4775 } else {
4776 value1 = FormulaIsConvertible(formula->left);
4777 value2 = FormulaIsConvertible(formula->right);
4778 switch (formula->type) {
4779 case Ctlp_AND_c:
4780 case Ctlp_OR_c:
4781 convertible = value1 * value2;
4782 break;
4783 case Ctlp_THEN_c:
4784 convertible = (value1 & 0x1) * value2;
4785 break;
4786 default :
4787 convertible = 2;
4788 break;
4789 }
4790 }
4791
4792 return(convertible);
4793}
4794
4795
4796/**Function********************************************************************
4797
4798 Synopsis [Replaces a simple formula with bottom.]
4799
4800 Description [This function is used in generating the witness formula from a
4801 w-ACTL formula in Beer's approach to vacuity detection. Replaces a simple
4802 (propositional) subformula with bottom, which is FALSE for even negation
4803 parity and TRUE for odd negation parity. An exception is made when the top
4804 node of the subformula is an implication. In that case, the top node and the
4805 antecedent (left child) are retained in the replacement, while the
4806 consequent (right child) is replaced by bottom.]
4807
4808 SideEffects [none]
4809
4810 SeeAlso [Ctlp_FormulaCreateWitnessFormula]
4811
4812******************************************************************************/
4813static Ctlp_Formula_t *
4814ReplaceSimpleFormula(
4815 Ctlp_Formula_t * formula)
4816{
4817 Ctlp_Formula_t *newFormula;
4818
4819 assert(formula->negation_parity == Ctlp_Even_c ||
4820 formula->negation_parity == Ctlp_Odd_c);
4821
4822 if (Ctlp_FormulaReadType(formula) == Ctlp_THEN_c) {
4823 Ctlp_Formula_t *leftFormula, *rightFormula;
4824 Ctlp_Formula_t *newLeftFormula, *newRightFormula;
4825
4826 leftFormula = Ctlp_FormulaReadLeftChild(formula);
4827 rightFormula = Ctlp_FormulaReadRightChild(formula);
4828 newLeftFormula = Ctlp_FormulaDup(leftFormula);
4829 newRightFormula = ReplaceSimpleFormula(rightFormula);
4830 return Ctlp_FormulaCreate(Ctlp_THEN_c,newLeftFormula,newRightFormula);
4831 }
4832
4833 fprintf(vis_stderr, "Replacing formula ");
4834 Ctlp_FormulaPrint(vis_stderr, formula);
4835 if (formula->negation_parity == Ctlp_Even_c){
4836 fprintf(vis_stderr, " by FALSE\n");
4837 newFormula = FormulaCreateWithType(Ctlp_FALSE_c);
4838 } else{
4839 fprintf(vis_stderr, " by TRUE\n");
4840 newFormula = FormulaCreateWithType(Ctlp_TRUE_c);
4841 }
4842 newFormula->negation_parity = formula->negation_parity;
4843 return(newFormula);
4844}
Note: See TracBrowser for help on using the repository browser.