source: vis_dev/vis-2.3/src/ctlsp/ctlspUtil.c @ 36

Last change on this file since 36 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 159.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [ctlspUtil.c]
4
5  PackageName [ctlsp]
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  Author      [Mohammad Awedh, Chao Wang]
14
15  Copyright   [This file was created at the University of Colorado at Boulder.
16  The University of Colorado at Boulder makes no warranty about the suitability
17  of this software for any purpose.  It is presented on an AS IS basis.]
18
19******************************************************************************/
20
21#include "ctlspInt.h"
22#include "errno.h"
23#include "ntk.h"
24
25static char rcsid[] UNUSED = "$Id: ctlspUtil.c,v 1.64 2009/04/11 18:25:55 fabio Exp $";
26
27/*---------------------------------------------------------------------------*/
28/* Variable declarations                                                     */
29/*---------------------------------------------------------------------------*/
30
31/**Variable********************************************************************
32
33  Synopsis    [Array of CTL* formulas (Ctlsp_Formula_t) read from a file.]
34
35  SeeAlso     [Ctlsp_FormulaArrayFree]
36
37******************************************************************************/
38static array_t *globalFormulaArray;
39static int      changeBracket = 1;
40
41/* see ctlspInt.h for documentation */
42int CtlspGlobalError;
43Ctlsp_Formula_t *CtlspGlobalFormula;
44st_table *CtlspMacroTable;
45
46/*---------------------------------------------------------------------------*/
47/* Macro declarations                                                        */
48/*---------------------------------------------------------------------------*/
49
50
51/**AutomaticStart*************************************************************/
52
53/*---------------------------------------------------------------------------*/
54/* Static function prototypes                                                */
55/*---------------------------------------------------------------------------*/
56
57static Ctlsp_Formula_t * FormulaCreateWithType(Ctlsp_FormulaType type);
58static int FormulaCompare(const char *key1, const char *key2);
59static int FormulaHash(char *key, int modulus);
60static Ctlsp_Formula_t * FormulaHashIntoUniqueTable(Ctlsp_Formula_t *formula, st_table *uniqueTable);
61static Ctlsp_Formula_t * createSNFnode(Ctlsp_Formula_t *formula, array_t *formulaArray, int *index);
62
63/**AutomaticEnd***************************************************************/
64
65
66/*---------------------------------------------------------------------------*/
67/* Definition of exported functions                                          */
68/*---------------------------------------------------------------------------*/
69
70/**Function********************************************************************
71
72  Synopsis    [Parses a file containing a set of CTL* formulas.]
73
74  Description [Parses a file containing a set of semicolon-ending CTL*
75  formulas, and returns an array of Ctlsp_Formula_t representing those
76  formulas.  If an error is detected while parsing the file, the routine frees
77  any allocated memory and returns NULL.]
78
79  SideEffects [Manipulates the global variables globalFormulaArray,
80  CtlspGlobalError and CtlspGlobalFormula.]
81
82  SeeAlso     [Ctlsp_FormulaArrayFree Ctlsp_FormulaPrint]
83
84******************************************************************************/
85array_t *
86Ctlsp_FileParseFormulaArray(
87  FILE * fp)
88{
89  st_generator *stGen;
90  char *name;
91  Ctlsp_Formula_t *formula;
92  char *flagValue;
93  /*
94   * Initialize the global variables.
95   */
96  globalFormulaArray = array_alloc(Ctlsp_Formula_t *, 0);
97  CtlspGlobalError = 0;
98  CtlspGlobalFormula = NIL(Ctlsp_Formula_t);
99  CtlspMacroTable = st_init_table(strcmp,st_strhash);
100  CtlspFileSetup(fp);
101  /*
102   * Check if changing "[] -> <>" is disabled.
103   */
104  flagValue = Cmd_FlagReadByName("ctl_change_bracket");
105  if (flagValue != NIL(char)) {
106    if (strcmp(flagValue, "yes") == 0)
107      changeBracket = 1;
108    else if (strcmp(flagValue, "no") == 0)
109      changeBracket = 0;
110    else {
111      fprintf(vis_stderr,
112        "** ctl error : invalid value %s for ctl_change_bracket[yes/no]. ***\n",
113        flagValue);
114    }
115  }
116
117  (void)CtlspYyparse();
118  st_foreach_item(CtlspMacroTable,stGen,&name, &formula){
119     FREE(name);
120     CtlspFormulaFree(formula);
121  }
122  st_free_table(CtlspMacroTable);
123
124  /*
125   * Clean up if there was an error, otherwise return the array.
126   */
127  if (CtlspGlobalError){
128    Ctlsp_FormulaArrayFree(globalFormulaArray);
129    return NIL(array_t);
130  }
131  else {
132    return globalFormulaArray;
133  }
134}
135
136
137/**Function********************************************************************
138
139  Synopsis    [Parses a file containing a set of CTL formulas.]
140
141  Description [Parses a file containing a set of semicolon-terminated CTL
142  formulae, and returns an array of Ctlp_Formula_t representing those
143  formulae.  If an error is detected while parsing the file, the routine frees
144  any allocated memory and returns NULL.]
145
146  SideEffects [Manipulates the global variables globalFormulaArray,
147  CtlspGlobalError and CtlspGlobalFormula.]
148
149  SeeAlso     [Ctlsp_FileParseFormulaArray]
150
151******************************************************************************/
152array_t *
153Ctlsp_FileParseCTLFormulaArray(
154  FILE *fp)
155{
156  array_t *ctlsArray = Ctlsp_FileParseFormulaArray(fp);
157  array_t *ctlArray;
158
159  if (ctlsArray == NIL(array_t)) return NIL(array_t);
160  ctlArray = Ctlsp_FormulaArrayConvertToCTL(ctlsArray);
161  Ctlsp_FormulaArrayFree(ctlsArray);
162  return ctlArray;
163 
164} /* Ctlsp_FileParseCTLFormulaArray */
165
166/**Function********************************************************************
167
168  Synopsis    [Returns a character string represents the CTL* formula]
169
170  Description [Returns formula as a character string. All subformulas are
171  delimited by parenthesis. Does nothing if passed a NULL formula.]
172
173  SideEffects []
174
175******************************************************************************/
176char *
177Ctlsp_FormulaConvertToString(
178  Ctlsp_Formula_t * formula)
179{
180  char *s1        = NIL(char);
181  char *s2        = NIL(char);
182  char *tmpString = NIL(char);
183  char *result;
184
185
186  if (formula == NIL(Ctlsp_Formula_t)) {
187    return NIL(char);
188  }
189
190  /* leaf node */
191  if (formula->type == Ctlsp_ID_c){
192  result = util_strcat3((char *)(formula->left), "=",(char *)(formula->right));
193  /*
194  tmpString = util_strcat3("[", util_inttostr(formula->CTLclass),"]");
195  return util_strcat3(result, " ",tmpString);
196  */
197  return result;
198  }
199
200  /* If the formula is a non-leaf, the function is called recursively */
201  s1 = Ctlsp_FormulaConvertToString(formula->left);
202  s2 = Ctlsp_FormulaConvertToString(formula->right);
203
204  switch(formula->type) {
205    /*
206     * The cases are listed in rough order of their expected frequency.
207     */
208    case Ctlsp_OR_c:
209      tmpString = util_strcat3(s1, " + ",s2);
210      result    = util_strcat3("(", tmpString, ")");
211      break;
212    case Ctlsp_AND_c:
213      tmpString = util_strcat3(s1, " * ", s2);
214      result    = util_strcat3("(", tmpString, ")");
215      break;
216    case Ctlsp_THEN_c:
217      tmpString = util_strcat3(s1, " -> ", s2);
218      result    = util_strcat3("(", tmpString, ")");
219      break;
220    case Ctlsp_XOR_c:
221      tmpString = util_strcat3(s1, " ^ ", s2);
222      result    = util_strcat3("(", tmpString, ")");
223      break;
224    case Ctlsp_EQ_c:
225      tmpString = util_strcat3(s1, " <-> ", s2);
226      result    = util_strcat3("(", tmpString, ")");
227      break;
228    case Ctlsp_NOT_c:
229      tmpString = util_strcat3("(", s1, ")");
230      result    = util_strcat3("!", tmpString, "");
231      break;
232    case Ctlsp_E_c:
233      result = util_strcat3("E(", s1, ")");
234      FREE(s1);
235      break;
236    case Ctlsp_G_c:
237      result = util_strcat3("G(", s1, ")");
238      break;
239    case Ctlsp_F_c:
240      result = util_strcat3("F(", s1, ")");
241      break;
242    case Ctlsp_U_c:
243      tmpString = util_strcat3("(", s1, " U ");
244      result    = util_strcat3(tmpString, s2, ")");
245      break;
246    case Ctlsp_R_c:
247      tmpString = util_strcat3("(", s1, " R ");
248      result    = util_strcat3(tmpString, s2, ")");
249      break;
250    case Ctlsp_W_c:
251      tmpString = util_strcat3("(", s1, " W ");
252      result    = util_strcat3(tmpString, s2, ")");
253      break;
254    case Ctlsp_X_c:
255      result = util_strcat3("X(", s1, ")");
256      break;
257    case Ctlsp_A_c:
258      result = util_strcat3("A(", s1, ")");
259      break;;
260    case Ctlsp_TRUE_c:
261      result = util_strsav("TRUE");
262      break;
263    case Ctlsp_FALSE_c:
264      result = util_strsav("FALSE");
265      break;
266    case Ctlsp_Init_c:
267      result = util_strsav("Init");
268      break;
269    case Ctlsp_Cmp_c:
270      if (formula->compareValue == 0)
271        tmpString = util_strcat3("[", s1, "] = ");
272      else
273        tmpString = util_strcat3("[", s1, "] != ");
274      result    = util_strcat3(tmpString, s2, "");
275      break;
276    case Ctlsp_Fwd_c:
277      tmpString = util_strcat3("FwdG(", s1, ",");
278      result    = util_strcat3(tmpString, s2, ")");
279      break;
280      /*   case Ctlsp_EY_c:
281      result = util_strcat3("EY(", s1, ")");
282      break;*/
283    default:
284      fail("Unexpected type");
285
286  }
287  if (s1 != NIL(char)) {
288    FREE(s1);
289  }
290  if (s2 != NIL(char)) {
291    FREE(s2);
292  }
293  if (tmpString != NIL(char)) {
294    FREE(tmpString);
295  }
296
297  return result;
298}
299
300
301/**Function********************************************************************
302
303  Synopsis    [Prints a formula to a file.]
304
305  Description [Prints a formula to a file. All subformulas are delimited by
306  parenthesis. The syntax used is the same as used by the CTL* parser.  Does
307  nothing if passed a NULL formula.]
308
309  SideEffects []
310
311******************************************************************************/
312void
313Ctlsp_FormulaPrint(
314  FILE * fp,
315  Ctlsp_Formula_t * formula)
316{
317  char *tmpString;
318  if (formula == NIL(Ctlsp_Formula_t)) {
319    return;
320  }
321  tmpString = Ctlsp_FormulaConvertToString(formula);
322  (void) fprintf(fp, "%s", tmpString);
323  FREE(tmpString);
324}
325
326
327/**Function********************************************************************
328
329  Synopsis    [Gets the type of a formula.]
330
331  Description [Gets the type of a formula. See ctlsp.h for all the types. It is
332  an error to call this function on a NULL formula.]
333
334  SideEffects []
335
336  SeeAlso     [ctlsp.h]
337
338******************************************************************************/
339Ctlsp_FormulaType
340Ctlsp_FormulaReadType(
341  Ctlsp_Formula_t * formula)
342{
343  return (formula->type);
344}
345
346
347/**Function********************************************************************
348
349  Synopsis    [Gets the compare value of a formula.]
350
351  Description [Gets the compare value of a formula. See ctlsp.h for all the
352  types. It is an error to call this function on a NULL formula.]
353
354  SideEffects []
355
356  SeeAlso     [ctlsp.h]
357
358******************************************************************************/
359int
360Ctlsp_FormulaReadCompareValue(
361  Ctlsp_Formula_t * formula)
362{
363  int value;
364  value = formula->compareValue;
365  return (value);
366}
367
368
369/**Function********************************************************************
370
371  Synopsis    [Reads the variable name of a leaf formula.]
372
373  Description [Reads the variable name of a leaf formula.
374  It is an error to call this function on a non-leaf formula.]
375
376  SideEffects []
377
378******************************************************************************/
379char *
380Ctlsp_FormulaReadVariableName(
381  Ctlsp_Formula_t * formula)
382{
383  if (formula->type != Ctlsp_ID_c){
384    fail("Ctlsp_FormulaReadVariableName() was called on a non-leaf formula.");
385  }
386  return ((char *)(formula->left));
387}
388
389
390/**Function********************************************************************
391
392  Synopsis    [Reads the value name of a leaf formula.]
393
394  Description [Reads the value 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 *
401Ctlsp_FormulaReadValueName(
402  Ctlsp_Formula_t * formula)
403{
404  if (formula->type != Ctlsp_ID_c){
405    fail("Ctlsp_FormulaReadValueName() was called on a non-leaf formula.");
406  }
407  return ((char *)(formula->right));
408}
409
410/**Function********************************************************************
411
412  Synopsis    [Gets the left child of a formula.]
413
414  Description [Gets the left child of a formula.  User must not free this
415  formula. If a formula is a leaf formula, NIL(Ctlsp_Formula_t) is returned.]
416
417  SideEffects []
418
419  SeeAlso     [Ctlsp_FormulaReadRightChild]
420
421******************************************************************************/
422Ctlsp_Formula_t *
423Ctlsp_FormulaReadLeftChild(
424  Ctlsp_Formula_t * formula)
425{
426  if (formula->type != Ctlsp_ID_c){
427    return (formula->left);
428  }
429  return NIL(Ctlsp_Formula_t);
430}
431
432
433/**Function********************************************************************
434
435  Synopsis    [Gets the right child of a formula.]
436
437  Description [Gets the right child of a formula.  User must not free this
438  formula. If a formula is a leaf formula, NIL(Ctlsp_Formula_t) is returned.]
439
440  SideEffects []
441
442  SeeAlso     [Ctlsp_FormulaReadLeftChild]
443
444******************************************************************************/
445Ctlsp_Formula_t *
446Ctlsp_FormulaReadRightChild(
447  Ctlsp_Formula_t * formula)
448{
449  if (formula->type != Ctlsp_ID_c){
450    return (formula->right);
451  }
452  return NIL(Ctlsp_Formula_t);
453}
454
455
456/**Function********************************************************************
457
458  Synopsis [Gets a copy of the set of states for which this formula is
459  true.]
460
461  Description [Gets a copy of the MDD representing the set of states for which
462  this formula is true.  It is the user's responsibility to free this MDD. If
463  the set of states has not yet been computed, then a NULL mdd_t is
464  returned. It is an error to call this function on a NULL formula.]
465
466  SideEffects []
467
468  SeeAlso     [Ctlsp_FormulaSetStates]
469
470******************************************************************************/
471mdd_t *
472Ctlsp_FormulaObtainStates(
473  Ctlsp_Formula_t * formula)
474{
475  if (formula->states == NIL(mdd_t)) {
476    return NIL(mdd_t);
477  }
478  else {
479    return mdd_dup(formula->states);
480  }
481}
482/**Function********************************************************************
483
484  Synopsis [Gets (a copy of) an approximation of the satisfying set]
485
486  Description [Gets the required approximation of the satisfying set.  If the
487  exact set is available, it will return that.  If neither is available, or
488  approx is Ctlsp_Incomparable_c, it will return NULL.]
489
490  SideEffects []
491
492  SeeAlso     [Ctlsp_FormulaSetStates]
493
494******************************************************************************/
495mdd_t *
496Ctlsp_FormulaObtainApproxStates(
497  Ctlsp_Formula_t *formula,
498  Ctlsp_Approx_t approx)
499{
500  if(approx == Ctlsp_Incomparable_c)
501    return NIL(mdd_t);
502
503  if (formula->states != NIL(mdd_t))
504    return mdd_dup(formula->states);
505
506  if(approx == Ctlsp_Exact_c)
507    return NIL(mdd_t);
508
509  if(approx == Ctlsp_Overapprox_c){
510    if(formula->overapprox == NIL(mdd_t))
511      return NIL(mdd_t);
512    else
513      return mdd_dup(formula->overapprox);
514  }
515
516  if(approx == Ctlsp_Underapprox_c){
517    if(formula->underapprox == NIL(mdd_t))
518      return NIL(mdd_t);
519    else
520      return mdd_dup(formula->underapprox);
521  }
522
523  assert(0);  /* we should never get here */
524  return NIL(mdd_t);
525}
526
527
528/**Function********************************************************************
529
530  Synopsis    [Stores the set of states with the formula.]
531
532  Description [Stores the MDD with the formula (a copy is not made,
533  and hence, the caller should not later free this MDD). This MDD is
534  intended to represent the set of states for which the formula is
535  true. It is an error to call this function on a NULL formula.]
536
537  SideEffects []
538
539  SeeAlso     [Ctlsp_FormulaObtainStates]
540
541******************************************************************************/
542void
543Ctlsp_FormulaSetStates(
544  Ctlsp_Formula_t * formula,
545  mdd_t * states)
546{
547  /* RB: added the next two lines.  Given the Description, this was a
548     bug */
549    if(formula->states != NIL(mdd_t))
550      mdd_free(formula->states);
551    formula->states = states;
552}
553
554
555/**Function********************************************************************
556
557  Synopsis [Stores (an approximation of) the set of states with the
558  formula.]
559
560  Description [Sets the set of states or an under or overapproximation thereof,
561  depending on the approx flag.  If there is already an under or
562  overapproximation, it is overwritten.  If the exact set is given, the approx
563  fields are cleared.  Setting an incomparable approximation results in no
564  action being taken.  A copy of the bdd is not made, so the caller should not
565  free it.  ]
566
567  SideEffects []
568
569  SeeAlso     [Ctlsp_FormulaObtainStates]
570
571******************************************************************************/
572void
573Ctlsp_FormulaSetApproxStates(
574  Ctlsp_Formula_t * formula,
575  mdd_t * states,
576  Ctlsp_Approx_t approx)
577{
578  if(approx == Ctlsp_Incomparable_c){
579    mdd_free(states);
580    return;
581  }
582
583  if(approx == Ctlsp_Exact_c){
584    if(formula->states != NIL(mdd_t))
585      mdd_free(formula->states);
586    formula->states = states;
587
588    if(formula->underapprox != NIL(mdd_t)){
589      mdd_free(formula->underapprox);
590      formula->underapprox = NIL(mdd_t);
591    }
592
593    if(formula->overapprox != NIL(mdd_t)){
594      mdd_free(formula->overapprox);
595      formula->overapprox = NIL(mdd_t);
596    }
597  }
598
599  if( approx == Ctlsp_Underapprox_c){
600    /* you could perform a union instead, but typical use will
601       have monotonically increasing underapproximations */
602    if(formula->underapprox != NIL(mdd_t))
603      mdd_free(formula->underapprox);
604    formula->underapprox = states;
605  }
606
607  if( approx == Ctlsp_Overapprox_c){
608    /* you could perform an intersaection instead */
609    if(formula->overapprox != NIL(mdd_t))
610      mdd_free(formula->overapprox);
611    formula->overapprox = states;
612  }
613
614  return;
615}
616
617
618
619/**Function********************************************************************
620
621  Synopsis    [Sets the debug information of a formula.]
622
623  Description [Sets the debug information of a CTL formula.  The data is
624  uninterpreted.  FreeFn is a pointer to a function that takes a formula as
625  input and returns void.  FreeFn should free all the memory associated with
626  the debug data; it is called when this formula is freed.]
627
628  SideEffects []
629
630  SeeAlso     [Ctlsp_FormulaReadDebugData]
631
632******************************************************************************/
633void
634Ctlsp_FormulaSetDbgInfo(
635  Ctlsp_Formula_t * formula,
636  void *data,
637  Ctlsp_DbgInfoFreeFn freeFn)
638{
639  formula->dbgInfo.data   = data;
640  formula->dbgInfo.freeFn = freeFn;
641}
642
643
644/**Function********************************************************************
645
646  Synopsis    [Returns the debug data associated with a formula.]
647
648  Description [Returns the debug data associated with a formula.  This data is
649  uninterpreted by the ctlsp package.]
650
651  SideEffects []
652
653  SeeAlso     [Ctlsp_FormulaSetDbgInfo]
654
655******************************************************************************/
656void *
657Ctlsp_FormulaReadDebugData(
658  Ctlsp_Formula_t * formula)
659{
660  return formula->dbgInfo.data;
661}
662
663
664/**Function********************************************************************
665
666  Synopsis    [Returns TRUE if formula was converted, else FALSE.]
667  from AX/AG/AU/AF]
668
669  Description [Returns TRUE if formula was converted from a formula of type
670  AG, AX, AU, AF, or EF via a call to
671  Ctlsp_FormulaConvertToExistentialFormTree or
672  Ctlsp_FormulaConvertToExistentialFormDAG. Otherwise, returns FALSE.]
673
674  SideEffects []
675
676******************************************************************************/
677boolean
678Ctlsp_FormulaTestIsConverted(
679  Ctlsp_Formula_t * formula)
680{
681  return formula->dbgInfo.convertedFlag;
682}
683
684
685/**Function********************************************************************
686
687  Synopsis    [Returns TRUE if formula contains no path quantifiers.]
688
689  Description [Test if a CTL* formula has any path quantifiers in it;
690  if so return false, else true.  For a CTL* formula, being quantifier-free
691  and being propositional are not equivalent.]
692
693  SideEffects []
694
695******************************************************************************/
696boolean
697Ctlsp_FormulaTestIsQuantifierFree(
698  Ctlsp_Formula_t *formula)
699{
700  boolean lCheck;
701  boolean rCheck;
702  Ctlsp_Formula_t *leftChild;
703  Ctlsp_Formula_t *rightChild;
704  Ctlsp_FormulaType type;
705
706  if ( formula == NIL( Ctlsp_Formula_t ) ) {
707    return TRUE;
708  }
709
710  type = Ctlsp_FormulaReadType( formula );
711
712  if ( ( type == Ctlsp_ID_c ) ||
713       ( type == Ctlsp_TRUE_c ) ||
714       ( type == Ctlsp_FALSE_c ) ) {
715    return TRUE;
716  }
717
718  if ( ( type == Ctlsp_E_c ) || ( type == Ctlsp_A_c ) ) {
719    return FALSE;
720  }
721
722  leftChild = Ctlsp_FormulaReadLeftChild( formula );
723  lCheck = Ctlsp_FormulaTestIsQuantifierFree( leftChild );
724
725  if (lCheck == FALSE)
726    return FALSE;
727
728  rightChild = Ctlsp_FormulaReadRightChild( formula );
729  rCheck = Ctlsp_FormulaTestIsQuantifierFree( rightChild );
730
731  return rCheck;
732}
733
734
735/**Function********************************************************************
736
737  Synopsis    [Returns original formula corresponding to converted formula.]
738
739  SideEffects []
740
741******************************************************************************/
742Ctlsp_Formula_t *
743Ctlsp_FormulaReadOriginalFormula(
744  Ctlsp_Formula_t * formula)
745{
746  return formula->dbgInfo.originalFormula;
747}
748
749
750/**Function********************************************************************
751
752  Synopsis    [Returns the Alpha-Beta Index. used for LTL->AUT]
753
754  SideEffects []
755
756******************************************************************************/
757int
758Ctlsp_FormulaReadABIndex(
759  Ctlsp_Formula_t * formula)
760{
761  return formula->ab_idx;
762}
763
764/**Function********************************************************************
765
766  Synopsis    [Set the Alpha-Beta Index. used for LTL->AUT]
767
768  SideEffects []
769
770******************************************************************************/
771void
772Ctlsp_FormulaSetABIndex(
773  Ctlsp_Formula_t * formula,
774  int ab_idx)
775{
776  formula->ab_idx = ab_idx;
777}
778
779
780/**Function********************************************************************
781
782  Synopsis    [Returns the Label Index. used for LTL->AUT]
783
784  SideEffects []
785
786******************************************************************************/
787int
788Ctlsp_FormulaReadLabelIndex(
789  Ctlsp_Formula_t * formula)
790{
791  return formula->label_idx;
792}
793
794/**Function********************************************************************
795
796  Synopsis    [Set the Label Index. used for LTL->AUT]
797
798  SideEffects []
799
800******************************************************************************/
801void
802Ctlsp_FormulaSetLabelIndex(
803  Ctlsp_Formula_t * formula,
804  int label_idx)
805{
806  formula->label_idx = label_idx;
807}
808
809
810/**Function********************************************************************
811
812  Synopsis    [Returns the RHS. used for LTL->AUT]
813
814  SideEffects []
815
816******************************************************************************/
817char
818Ctlsp_FormulaReadRhs(
819  Ctlsp_Formula_t * formula)
820{
821  return formula->rhs;
822}
823
824/**Function********************************************************************
825
826  Synopsis    [Set the RHS. used for LTL->AUT]
827
828  SideEffects []
829
830******************************************************************************/
831void
832Ctlsp_FormulaSetRhs(
833  Ctlsp_Formula_t * formula)
834{
835  formula->rhs = 1;
836}
837
838/**Function********************************************************************
839
840  Synopsis    [Reset the RHS. used for LTL->AUT]
841
842  SideEffects []
843
844******************************************************************************/
845void
846Ctlsp_FormulaResetRhs(
847  Ctlsp_Formula_t * formula)
848{
849  formula->rhs = 0;
850}
851
852/**Function********************************************************************
853
854  Synopsis    [Returns the marked. used for LTL->AUT]
855
856  SideEffects []
857
858******************************************************************************/
859char
860Ctlsp_FormulaReadMarked(
861  Ctlsp_Formula_t * formula)
862{
863  return formula->marked;
864}
865
866/**Function********************************************************************
867
868  Synopsis    [Set the Alpha-Beta Index. used for LTL->AUT]
869
870  SideEffects []
871
872******************************************************************************/
873void
874Ctlsp_FormulaSetMarked(
875  Ctlsp_Formula_t * formula)
876{
877  formula->marked = 1;
878}
879
880/**Function********************************************************************
881
882  Synopsis    [Reset the Alpha-Beta Index. used for LTL->AUT]
883
884  SideEffects []
885
886******************************************************************************/
887void
888Ctlsp_FormulaResetMarked(
889  Ctlsp_Formula_t * formula)
890{
891  formula->marked = 0;
892}
893
894/**Function********************************************************************
895
896  Synopsis    [Frees a formula if no other formula refers to it as a
897  sub-formula.]
898
899  Description [The function decrements the refCount of the formula. As a
900  consequence, if the refCount becomes 0, the formula is freed.]
901
902  SideEffects []
903
904  SeeAlso     [CtlspFormulaFree, CtlspDecrementRefCount]
905
906******************************************************************************/
907void
908Ctlsp_FormulaFree(
909  Ctlsp_Formula_t *formula)
910{
911  CtlspFormulaDecrementRefCount(formula);
912}
913
914/**Function********************************************************************
915
916  Synopsis [Recursively frees states, underapprox and overapprox fields of
917  Ctlsp_Formula_t, and the debug data]
918
919  Description []
920
921  SideEffects []
922
923  SeeAlso     [Ctlsp_FormulaFree]
924
925******************************************************************************/
926void
927Ctlsp_FlushStates(
928  Ctlsp_Formula_t * formula)
929{
930  if (formula != NIL(Ctlsp_Formula_t)) {
931
932    if (formula->type != Ctlsp_ID_c){
933      if (formula->left  != NIL(Ctlsp_Formula_t)) {
934        Ctlsp_FlushStates(formula->left);
935      }
936      if (formula->right != NIL(Ctlsp_Formula_t)) {
937        Ctlsp_FlushStates(formula->right);
938      }
939    }
940
941    if (formula->states != NIL(mdd_t)){
942      mdd_free(formula->states);
943      formula->states = NIL(mdd_t);
944    }
945    if (formula->underapprox != NIL(mdd_t)){
946      mdd_free(formula->underapprox);
947      formula->underapprox = NIL(mdd_t);
948    }
949    if (formula->overapprox != NIL(mdd_t)){
950      mdd_free(formula->overapprox);
951      formula->overapprox = NIL(mdd_t);
952    }
953
954    if (formula->dbgInfo.data != NIL(void)){
955      (*formula->dbgInfo.freeFn)(formula);
956      formula->dbgInfo.data = NIL(void);
957    }
958
959  }
960
961}
962
963/**Function********************************************************************
964
965
966  Synopsis    [Duplicates a CTL* formula.]
967
968  Description [Recursively duplicate a formula. Does nothing if the formula
969  is NIL. Does not copy mdd for states, underapprox, overapprox, dbgInfo.]
970
971  SideEffects []
972
973  SeeAlso     []
974
975******************************************************************************/
976Ctlsp_Formula_t *
977Ctlsp_FormulaDup(
978  Ctlsp_Formula_t * formula)
979{
980  Ctlsp_Formula_t *result = NIL(Ctlsp_Formula_t);
981
982  if ( formula == NIL(Ctlsp_Formula_t)) {
983        return NIL(Ctlsp_Formula_t);
984  }
985
986  result = ALLOC(Ctlsp_Formula_t, 1);
987
988  result->type                    = formula->type;
989  result->class_                  = formula->class_;
990  result->CTLclass                = formula->CTLclass;
991  result->states                  = NIL(mdd_t);
992  result->underapprox             = NIL(mdd_t);
993  result->overapprox              = NIL(mdd_t);
994  result->refCount                = 1;
995  result->dbgInfo.data            = NIL(void);
996  result->dbgInfo.freeFn          = (Ctlsp_DbgInfoFreeFn) NULL;
997  result->dbgInfo.convertedFlag   = FALSE;
998  result->dbgInfo.originalFormula = NIL(Ctlsp_Formula_t);
999
1000  if ( formula->type != Ctlsp_ID_c )  {
1001    result->left  = Ctlsp_FormulaDup(formula->left);
1002    result->right = Ctlsp_FormulaDup(formula->right);
1003  }
1004  else {
1005    result->left  = (Ctlsp_Formula_t *) util_strsav((char *)formula->left );
1006    result->right = (Ctlsp_Formula_t *) util_strsav((char *)formula->right );
1007  }
1008
1009  return result;
1010}
1011
1012/**Function********************************************************************
1013
1014  Synopsis    [Frees an array of CTL* formulas.]
1015
1016  Description [Calls CtlspFormulaDecrementRefCount on each formula in
1017  formulaArray, and then frees the array itself. It is okay to call this
1018  function with an empty array, but it is an error to call it with a NULL
1019  array.]
1020
1021  SideEffects []
1022
1023  SeeAlso     [Ctlsp_FormulaFree]
1024
1025******************************************************************************/
1026void
1027Ctlsp_FormulaArrayFree(
1028  array_t * formulaArray /* of Ctlsp_Formula_t  */)
1029{
1030  int i;
1031  int numFormulas = array_n(formulaArray);
1032
1033  for (i = 0; i < numFormulas; i++) {
1034    Ctlsp_Formula_t *formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i);
1035
1036    CtlspFormulaDecrementRefCount(formula);
1037  }
1038
1039  array_free(formulaArray);
1040}
1041/**Function********************************************************************
1042
1043  Synopsis    [Converts an array of CTL formulae to a multi-rooted DAG.]
1044
1045  Description [The function hashes each subformula of a formula
1046  (including the formula itself) into a uniqueTable.  It returns an
1047  array containing the roots of the multi-rooted DAG thus created by
1048  the sharing of the subformulae.  It is okay to call this function
1049  with an empty array (in which case an empty array is returned), but
1050  it is an error to call it with a NULL array.]
1051
1052  SideEffects [A formula in formulaArray might be freed if it had been
1053  encountered as a subformula of some other formula. Other formulae in
1054  formulaArray might be present in the returned array. Therefore, the
1055  formulae in formulaArray should not be freed. Only formulaArray
1056  itself should be freed.
1057
1058
1059
1060  RB:  What does that mean?
1061
1062  I understand this as follows.  Copies of the formulae are not made,
1063  but rather pointers to the argument subformulae are kept.  Hence, not only
1064  should the formulae in the result not be freed, but also you cannot free the
1065  argument before you are done with the result.  Furthermore, by invocation of
1066  this function, the argument gets altered.  It is still valid, but pointers
1067  may have changed.  Is this correct?
1068
1069
1070  RB rewrite: A formula in formulaArray is freed if it is encountered as a
1071  subformula of some other formula. Other formulae in formulaArray might be
1072  present in the returned array. Therefore, the formulae in formulaArray should
1073  not be freed. Only formulaArray itself should be freed.]
1074
1075  SeeAlso     []
1076
1077******************************************************************************/
1078array_t *
1079Ctlsp_FormulaArrayConvertToDAG(
1080  array_t *formulaArray)
1081{
1082  int i;
1083  Ctlsp_Formula_t *formula, *uniqueFormula;
1084  st_table *uniqueTable = st_init_table(FormulaCompare, FormulaHash);
1085  int numFormulae = array_n(formulaArray);
1086  array_t *rootsOfFormulaDAG = array_alloc(Ctlsp_Formula_t *, numFormulae);
1087
1088  for(i=0; i < numFormulae; i++) {
1089    formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i);
1090    uniqueFormula = FormulaHashIntoUniqueTable(formula, uniqueTable);
1091    if(uniqueFormula != formula) {
1092      CtlspFormulaDecrementRefCount(formula);
1093      CtlspFormulaIncrementRefCount(uniqueFormula);
1094      array_insert(Ctlsp_Formula_t *, rootsOfFormulaDAG, i, uniqueFormula);
1095    }
1096    else
1097      array_insert(Ctlsp_Formula_t *, rootsOfFormulaDAG, i, formula);
1098  }
1099  st_free_table(uniqueTable);
1100  return rootsOfFormulaDAG;
1101}
1102
1103/**Function********************************************************************
1104
1105  Synopsis    [Creates a CTL formula with the specified fields.]
1106
1107  Description [Allocates a Ctlsp_Formula_t, and sets the 2 fields given as
1108  arguments.  If the type is Ctlsp_ID_c, then the left and right fields
1109  should contain a pointer to a variable name and a pointer to a value
1110  respectively. Otherwise, the two fields point to subformulas. refCount is
1111  set to 1. The states field is set to NULL, the converted flag is set to
1112  FALSE, and the originalFormula field is set to NULL.]
1113
1114  Comment     []
1115
1116  SideEffects []
1117
1118  SeeAlso     [CtlspFormulaDecrementRefCount]
1119
1120******************************************************************************/
1121Ctlsp_Formula_t *
1122Ctlsp_FormulaCreate(
1123  Ctlsp_FormulaType  type,
1124  void * left_,
1125  void * right_)
1126{
1127  Ctlsp_Formula_t *formula = ALLOC(Ctlsp_Formula_t, 1);
1128  Ctlsp_Formula_t *left    = (Ctlsp_Formula_t *) left_;
1129  Ctlsp_Formula_t *right   = (Ctlsp_Formula_t *) right_;
1130
1131  formula->type                    = type;
1132  formula->left                    = left;
1133  formula->right                   = right;
1134  formula->states                  = NIL(mdd_t);
1135  formula->underapprox             = NIL(mdd_t);
1136  formula->overapprox              = NIL(mdd_t);
1137  formula->refCount                = 1;
1138  formula->dbgInfo.data            = NIL(void);
1139  formula->dbgInfo.freeFn          = (Ctlsp_DbgInfoFreeFn) NULL;
1140  formula->dbgInfo.convertedFlag   = FALSE;
1141  formula->dbgInfo.originalFormula = NIL(Ctlsp_Formula_t);
1142  formula->top                     = 0;
1143  formula->compareValue            = 0;
1144  formula->class_                  = Ctlsp_propformula_c;
1145  formula->CTLclass                = Ctlsp_CTL_c;
1146  formula->rhs                     = 0;
1147
1148  if (left == NIL(Ctlsp_Formula_t)){
1149    return formula;
1150  }
1151
1152  switch(formula->type) {
1153    case Ctlsp_OR_c:
1154    case Ctlsp_AND_c:
1155    case Ctlsp_THEN_c:
1156    case Ctlsp_XOR_c:
1157    case Ctlsp_EQ_c:
1158      Ctlsp_FormulaSetClass(formula, table1(Ctlsp_FormulaReadClass(left),Ctlsp_FormulaReadClass(right)));
1159      if ((Ctlsp_FormulaReadClassOfCTL(left)  ==  Ctlsp_CTL_c) &&
1160          (Ctlsp_FormulaReadClassOfCTL(right) == Ctlsp_CTL_c)){
1161        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_CTL_c);
1162      } else {
1163        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_NotCTL_c);
1164      }
1165      break;
1166    case Ctlsp_NOT_c:
1167      Ctlsp_FormulaSetClass(formula, Ctlsp_FormulaReadClass(left));
1168      Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_FormulaReadClassOfCTL(left));
1169      break;
1170    case Ctlsp_E_c:
1171    case Ctlsp_A_c:
1172      Ctlsp_FormulaSetClass(formula, Ctlsp_stateformula_c);
1173      if (Ctlsp_FormulaReadClassOfCTL(left) ==  Ctlsp_PathCTL_c) {
1174        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_CTL_c);
1175      } else {
1176        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_NotCTL_c);
1177      }
1178      break;
1179    case Ctlsp_G_c:
1180    case Ctlsp_F_c:
1181      Ctlsp_FormulaSetClass(formula, table2(Ctlsp_FormulaReadClass(left)));
1182      if (Ctlsp_FormulaReadClassOfCTL(left) ==  Ctlsp_CTL_c){
1183        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_PathCTL_c);
1184      } else {
1185        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_NotCTL_c);
1186      }
1187      break;
1188    case Ctlsp_U_c:
1189    case Ctlsp_R_c:
1190    case Ctlsp_W_c:
1191      Ctlsp_FormulaSetClass(formula, table3(Ctlsp_FormulaReadClass(left),Ctlsp_FormulaReadClass(right)));
1192      if ((Ctlsp_FormulaReadClassOfCTL(left) ==  Ctlsp_CTL_c) &&
1193          (Ctlsp_FormulaReadClassOfCTL(right) == Ctlsp_CTL_c)) {
1194        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_PathCTL_c);
1195      } else {
1196        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_NotCTL_c);
1197      }
1198      break;
1199    case Ctlsp_X_c:
1200      Ctlsp_FormulaSetClass(formula, table2(Ctlsp_FormulaReadClass(left)));
1201      if (Ctlsp_FormulaReadClassOfCTL(left) ==  Ctlsp_CTL_c){
1202
1203        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_PathCTL_c);
1204      }  else {
1205        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_NotCTL_c);
1206      }
1207      break;
1208    default:
1209      break;
1210  }
1211  return formula;
1212}
1213
1214/**Function********************************************************************
1215
1216  Synopsis    [Creates a CTL* formula with disjunction of atomic propositions]
1217
1218  Description [This function returns Ctlsp_Formula_t for name = {v1,v2,...}.
1219  In case of failure, a NULL pointer is returned.]
1220
1221  SideEffects []
1222
1223  SeeAlso     []
1224
1225******************************************************************************/
1226Ctlsp_Formula_t *
1227Ctlsp_FormulaCreateOr(
1228  char *name,
1229  char *valueStr)
1230{
1231  Ctlsp_Formula_t *formula, *tempFormula;
1232  char *preStr;
1233
1234  preStr = strtok(valueStr,",");
1235  formula = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(name),
1236                               util_strsav(preStr));
1237  if (formula == NIL(Ctlsp_Formula_t)) {
1238     return NIL(Ctlsp_Formula_t);
1239  }
1240  while ((preStr = strtok(NIL(char),",")) != NIL(char)) {
1241    tempFormula = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(name),
1242                                     util_strsav(preStr));
1243    if (tempFormula == NIL(Ctlsp_Formula_t)) {
1244      Ctlsp_FormulaFree(formula);
1245      return NIL(Ctlsp_Formula_t);
1246    }
1247    formula = Ctlsp_FormulaCreate(Ctlsp_OR_c,formula,tempFormula);
1248  }
1249  return formula;
1250}
1251
1252
1253/**Function********************************************************************
1254
1255  Synopsis    [Creates a CTL* formula with conjunction of atomic propositions]
1256
1257  Description [This function returns Ctlsp_Formula_t for nameVector =
1258  value, nameVector is a form of var[i:j] or var<j:j> and value is any
1259  integer n or binary string starting with 'b' or 'x', for instance,
1260  b0011 or x100. If n does not fit in var[i:j] or the size of the binary
1261  string is not matched with var[i:j], NULL pointer is returned]
1262
1263  SideEffects []
1264
1265  SeeAlso     []
1266
1267******************************************************************************/
1268Ctlsp_Formula_t *
1269Ctlsp_FormulaCreateVectorAnd(
1270  char *nameVector,
1271  char *value)
1272{
1273  Ctlsp_Formula_t *formula, *tempFormula;
1274  int startValue, endValue, inc, i,j, interval,startInd;
1275  char *binValueStr, *varName, *name;
1276  char *bitValue;
1277
1278  varName = CtlspGetVectorInfoFromStr(nameVector,&startValue,&endValue,&interval,&inc);
1279  binValueStr = ALLOC(char,interval+1);
1280  if (!CtlspStringChangeValueStrToBinString(value,binValueStr,interval) ){
1281     FREE(varName);
1282     FREE(binValueStr);
1283     return NIL(Ctlsp_Formula_t);
1284  }
1285
1286  name = ALLOC(char,MAX_LENGTH_OF_VAR_NAME);
1287  (void) sprintf(name,"%s[%d]",varName,startValue);
1288  (void) CtlspChangeBracket(name);
1289
1290  bitValue = ALLOC(char,2);
1291  bitValue[0] = binValueStr[0];
1292  bitValue[1] = '\0';
1293
1294  formula = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(name),
1295                               util_strsav(bitValue));
1296  j = 0;
1297  startInd = startValue;
1298  for(i=startValue;i!=endValue;i=i+inc){
1299     startInd += inc;
1300     j++;
1301     (void) sprintf(name,"%s[%d]",varName,startInd);
1302     (void) CtlspChangeBracket(name);
1303     bitValue[0] = binValueStr[j];
1304     tempFormula = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(name),
1305                                      util_strsav(bitValue));
1306     formula = Ctlsp_FormulaCreate(Ctlsp_AND_c,formula,tempFormula);
1307  }
1308  FREE(varName);
1309  FREE(name);
1310  FREE(binValueStr);
1311  FREE(bitValue);
1312  return formula;
1313}
1314
1315
1316/**Function********************************************************************
1317
1318  Synopsis    [Creates a CTL formula with OR of Vector AND]
1319
1320  Description [This function returns Ctlsp_Formula_t for nameVector = valueStr,
1321  nameVector is a form of var[i:j] or var<j:j>, valueStr is "k,l,...,q",
1322  and k,l,...,q is either integer or binary string.  Binary string starting
1323  with 'b', for instance, b0011. If n is not fitted in var[i:j] or size of
1324  binary string is not matched with var[i:j], NULL pointer is returned]
1325
1326  SideEffects []
1327
1328  SeeAlso     []
1329
1330******************************************************************************/
1331Ctlsp_Formula_t *
1332Ctlsp_FormulaCreateVectorOr(
1333  char *nameVector,
1334  char *valueStr)
1335{
1336  Ctlsp_Formula_t *formula,*tempFormula;
1337  char *preStr;
1338
1339  preStr = strtok(valueStr,",");
1340  formula = Ctlsp_FormulaCreateVectorAnd(nameVector,preStr);
1341  if ( formula == NIL(Ctlsp_Formula_t)){
1342     Ctlsp_FormulaFree(formula);
1343     return NIL(Ctlsp_Formula_t);
1344  }
1345  while( (preStr = strtok(NIL(char),",")) != NIL(char) ){
1346     tempFormula = Ctlsp_FormulaCreateVectorAnd(nameVector,preStr);
1347     if ( tempFormula == NIL(Ctlsp_Formula_t)){
1348        Ctlsp_FormulaFree(formula);
1349        return NIL(Ctlsp_Formula_t);
1350     }
1351     formula = Ctlsp_FormulaCreate(Ctlsp_OR_c,formula,tempFormula);
1352  }
1353  return formula;
1354}
1355
1356
1357/**Function********************************************************************
1358
1359  Synopsis    [Creates a CTL formula for equivalent property]
1360
1361  Description [This function assumes that each child is defined in binary
1362  domain. Enumerate type is not supported]
1363
1364  SideEffects []
1365
1366  SeeAlso     []
1367
1368******************************************************************************/
1369Ctlsp_Formula_t *
1370Ctlsp_FormulaCreateEquiv(
1371  char *left,
1372  char *right)
1373{
1374  Ctlsp_Formula_t *formula,*formula1,*formula2;
1375
1376  char *one;
1377  char *zero;
1378
1379  one = "1";
1380  zero = "0";
1381
1382  formula1 = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(left),
1383                                 util_strsav(one));
1384  formula2 = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(right),
1385                                 util_strsav(zero));
1386  formula = Ctlsp_FormulaCreate(Ctlsp_XOR_c,formula1,formula2);
1387  return formula;
1388}
1389
1390/**Function********************************************************************
1391
1392  Synopsis    [Creates a CTL formula for equivalent of vector]
1393
1394  Description [This function returns a formula, which is the AND of a bitwise
1395  equivalence]
1396
1397  SideEffects []
1398
1399  SeeAlso     []
1400
1401******************************************************************************/
1402Ctlsp_Formula_t *
1403Ctlsp_FormulaCreateVectorEquiv(
1404  char *left,
1405  char *right)
1406{
1407  Ctlsp_Formula_t *formula,*tempFormula;
1408  char *leftName,*rightName;
1409  char *leftVar, *rightVar;
1410  int  leftStart,leftEnd,rightStart,rightEnd,leftInterval,rightInterval;
1411  int  leftInc,rightInc,leftInd,rightInd,i;
1412
1413  leftName  = CtlspGetVectorInfoFromStr(left,&leftStart,&leftEnd,&leftInterval,&leftInc);
1414  rightName = CtlspGetVectorInfoFromStr(right,&rightStart,&rightEnd,&rightInterval,&rightInc);
1415  if (leftInterval != rightInterval){
1416     return NIL(Ctlsp_Formula_t);
1417  }
1418  leftVar = ALLOC(char,MAX_LENGTH_OF_VAR_NAME);
1419  (void) sprintf(leftVar,"%s[%d]",leftName,leftStart);
1420  (void) CtlspChangeBracket(leftVar);
1421  rightVar = ALLOC(char,MAX_LENGTH_OF_VAR_NAME);
1422  (void) sprintf(rightVar,"%s[%d]",rightName,rightStart);
1423  (void) CtlspChangeBracket(rightVar);
1424
1425  formula = Ctlsp_FormulaCreateEquiv(leftVar,rightVar);
1426  leftInd  = leftStart;
1427  rightInd = rightStart;
1428  for(i=leftStart;i!=leftEnd;i+=leftInc){
1429     leftInd  += leftInc;
1430     rightInd += rightInc;
1431     (void) sprintf(leftVar,"%s[%d]",leftName,leftInd);
1432     (void) CtlspChangeBracket(leftVar);
1433     (void) sprintf(rightVar,"%s[%d]",rightName,rightInd);
1434     (void) CtlspChangeBracket(rightVar);
1435     tempFormula = Ctlsp_FormulaCreateEquiv(leftVar,rightVar);
1436     formula = Ctlsp_FormulaCreate(Ctlsp_AND_c,formula,tempFormula);
1437  }
1438  FREE(leftName);
1439  FREE(rightName);
1440  FREE(leftVar);
1441  FREE(rightVar);
1442  return formula;
1443}
1444
1445
1446/**Function********************************************************************
1447
1448  Synopsis    [Creates a CTL formula for multiple X]
1449
1450  Description [This function returns a formula, which is the multiple
1451  times of AX. The given string includes the number of depth]
1452
1453  SideEffects []
1454
1455  SeeAlso     []
1456
1457******************************************************************************/
1458Ctlsp_Formula_t *
1459Ctlsp_FormulaCreateXMult(
1460  char *string,
1461  Ctlsp_Formula_t *formula)
1462{
1463  int i,num;
1464  char *str, *ptr;
1465  Ctlsp_Formula_t *result = NIL(Ctlsp_Formula_t);
1466  str = strchr(string,':');
1467  if ( str == NULL) return(NIL(Ctlsp_Formula_t));
1468  str++;
1469
1470  num = strtol(str,&ptr,0);
1471
1472  for(i=0;i<num;i++){
1473    result = Ctlsp_FormulaCreate(Ctlsp_X_c, formula, NIL(Ctlsp_Formula_t));
1474    Ctlsp_FormulaSetClass(result, table2(Ctlsp_FormulaReadClass(formula)));
1475    if (Ctlsp_FormulaReadClassOfCTL(formula) ==  Ctlsp_CTL_c){
1476      Ctlsp_FormulaSetClassOfCTL(result, Ctlsp_PathCTL_c);
1477     }
1478    else{
1479      Ctlsp_FormulaSetClassOfCTL(result, Ctlsp_NotCTL_c);
1480     }
1481    formula = result;
1482    }
1483  return result;
1484}
1485
1486/**Function********************************************************************
1487
1488  Synopsis    [Creates a CTL* formula for multiple EX]
1489
1490  Description [This function returns a formula, which is the multiple
1491  times of EX. The given string includes the number of depth]
1492
1493  SideEffects []
1494
1495  SeeAlso     []
1496
1497******************************************************************************/
1498Ctlsp_Formula_t *
1499Ctlsp_FormulaCreateEXMult(
1500  char *string,
1501  Ctlsp_Formula_t *formula)
1502{
1503  int i,num;
1504  char *str, *ptr;
1505  Ctlsp_Formula_t *result = NIL(Ctlsp_Formula_t);
1506
1507  str = strchr(string,':');
1508  if ( str == NULL) return(NIL(Ctlsp_Formula_t));
1509  str++;
1510
1511  num = strtol(str,&ptr,0);
1512
1513  for(i=0;i<num;i++){
1514    result = Ctlsp_FormulaCreate(Ctlsp_X_c, formula, NIL(Ctlsp_Formula_t));
1515    Ctlsp_FormulaSetClass(result, table2(Ctlsp_FormulaReadClass(formula)));
1516    result = Ctlsp_FormulaCreate(Ctlsp_E_c, result, NIL(Ctlsp_Formula_t));
1517    Ctlsp_FormulaSetClass(result, Ctlsp_stateformula_c);
1518    if (Ctlsp_FormulaReadClassOfCTL(formula) ==  Ctlsp_CTL_c)
1519    {
1520      Ctlsp_FormulaSetClassOfCTL(result, Ctlsp_CTL_c);
1521    }
1522    else
1523    {
1524      Ctlsp_FormulaSetClassOfCTL(result, Ctlsp_NotCTL_c);
1525    }
1526    formula = result;
1527  }
1528
1529  return result;
1530}
1531
1532/**Function********************************************************************
1533
1534  Synopsis    [Creates a CTL* formula for multiple AX]
1535
1536  Description [This function returns a formula, which is the multiple
1537  times of AX. The given string includes the number of depth]
1538
1539  SideEffects []
1540
1541  SeeAlso     []
1542
1543******************************************************************************/
1544Ctlsp_Formula_t *
1545Ctlsp_FormulaCreateAXMult(
1546  char *string,
1547  Ctlsp_Formula_t *formula)
1548{
1549  int i,num;
1550  char *str, *ptr;
1551  Ctlsp_Formula_t *result = NIL(Ctlsp_Formula_t);
1552
1553  str = strchr(string,':');
1554  if ( str == NULL) return(NIL(Ctlsp_Formula_t));
1555  str++;
1556
1557  num = strtol(str,&ptr,0);
1558
1559  for(i=0;i<num;i++){
1560    result = Ctlsp_FormulaCreate(Ctlsp_X_c, formula, NIL(Ctlsp_Formula_t));
1561    Ctlsp_FormulaSetClass(result, table2(Ctlsp_FormulaReadClass(formula)));
1562    result = Ctlsp_FormulaCreate(Ctlsp_A_c, result, NIL(Ctlsp_Formula_t));
1563    Ctlsp_FormulaSetClass(result, Ctlsp_stateformula_c);
1564    if (Ctlsp_FormulaReadClassOfCTL(formula) ==  Ctlsp_CTL_c)
1565    {
1566      Ctlsp_FormulaSetClassOfCTL(result, Ctlsp_CTL_c);
1567    }
1568    else
1569    {
1570      Ctlsp_FormulaSetClassOfCTL(result, Ctlsp_NotCTL_c);
1571    }
1572    formula = result;
1573  }
1574
1575  return result;
1576}
1577
1578
1579/**Function********************************************************************
1580
1581  Synopsis    [Returns a string for each formula type.]
1582
1583  Description [Returns a string for each formula type.]
1584
1585  SideEffects []
1586
1587  SeeAlso     []
1588
1589******************************************************************************/
1590char *
1591Ctlsp_FormulaGetTypeString(Ctlsp_Formula_t *formula)
1592{
1593  char *result;
1594
1595  switch(formula->type) {
1596    /*
1597     * The cases are listed in rough order of their expected frequency.
1598     */
1599    case Ctlsp_ID_c:
1600      result = util_strsav("ID");
1601      break;
1602    case Ctlsp_OR_c:
1603      result = util_strsav("OR");
1604      break;
1605    case Ctlsp_AND_c:
1606      result = util_strsav("AND");
1607      break;
1608    case Ctlsp_THEN_c:
1609      result = util_strsav("THEN");
1610      break;
1611    case Ctlsp_XOR_c:
1612      result = util_strsav("XOR");
1613      break;
1614    case Ctlsp_EQ_c:
1615      result = util_strsav("EQ");
1616      break;
1617    case Ctlsp_NOT_c:
1618      result = util_strsav("NOT");
1619      break;
1620    case Ctlsp_E_c:
1621      result = util_strsav("E");
1622      break;
1623    case Ctlsp_G_c:
1624      result = util_strsav("G");
1625      break;
1626    case Ctlsp_F_c:
1627      result = util_strsav("F");
1628      break;
1629    case Ctlsp_U_c:
1630      result = util_strsav("U");
1631      break;
1632    case Ctlsp_R_c:
1633      result = util_strsav("R");
1634      break;
1635    case Ctlsp_W_c:
1636      result = util_strsav("W");
1637      break;
1638    case Ctlsp_X_c:
1639      result = util_strsav("X");
1640      break;
1641    case Ctlsp_A_c:
1642      result = util_strsav("A");
1643      break;
1644    case Ctlsp_TRUE_c:
1645      result = util_strsav("TRUE");
1646      break;
1647    case Ctlsp_FALSE_c:
1648      result = util_strsav("FALSE");
1649      break;
1650    case Ctlsp_Init_c:
1651      result = util_strsav("Init");
1652      break;
1653    case Ctlsp_Cmp_c:
1654      result = util_strsav("Cmp");
1655      break;
1656    case Ctlsp_Fwd_c:
1657      result = util_strsav("Fwd");
1658      break;
1659      /*    case Ctlsp_EY_c:
1660      result = util_strsav("EY");
1661      break;*/
1662      /*  case Ctlsp_EH_c:
1663      result = util_strsav("EH");
1664      break;
1665      break;*/
1666    default:
1667      fail("Unexpected type");
1668  }
1669  return(result);
1670}
1671
1672
1673/**Function********************************************************************
1674
1675  Synopsis           [Tests if a formula is a ACTL, ECTL or mixed formula.]
1676
1677  Description        [Tests if a formula is a ACTL, ECTL or mixed formula. '0'
1678  for ECTL, '1' for ACTL and '2' for a mixed formula. If a formula doesn't have
1679  any path quantifier, '3' is returned.]
1680
1681  SideEffects        []
1682
1683  SeeAlso            []
1684
1685******************************************************************************/
1686Ctlsp_FormulaClass
1687Ctlsp_CheckClassOfExistentialFormula(
1688  Ctlsp_Formula_t *formula)
1689{
1690  Ctlsp_FormulaClass result;
1691
1692  result = CtlspCheckClassOfExistentialFormulaRecur(formula, FALSE);
1693
1694  return result;
1695} /* End of Ctlsp_CheckTypeOfExistentialFormula */
1696
1697/**Function********************************************************************
1698
1699  Synopsis [Tests if an array of simple existential formulae has only
1700  ACTL, only ECTL or mixture of formula.]
1701
1702  Description        [Returns Ctlsp_ECTL_c if the array contains only
1703  ECTL formulae, Ctlsp_ACTL_c if it contains only ACTL formulae,
1704  Ctlsp_QuantifierFree_c if there are no quantifiers in any formulae,
1705  and Ctlsp_Mixed otherwise.]
1706
1707  SideEffects        []
1708
1709  SeeAlso            [Ctlsp_CheckClassOfExistentialFormula]
1710
1711******************************************************************************/
1712Ctlsp_FormulaClass
1713Ctlsp_CheckClassOfExistentialFormulaArray(
1714  array_t *formulaArray)
1715{
1716  Ctlsp_FormulaClass result;
1717  Ctlsp_Formula_t *formula;
1718  int formulanr;
1719
1720  result = Ctlsp_QuantifierFree_c;
1721  arrayForEachItem(Ctlsp_Formula_t *, formulaArray, formulanr, formula){
1722    Ctlsp_FormulaClass  formulaType;
1723    formulaType = Ctlsp_CheckClassOfExistentialFormula(formula);
1724    result = CtlspResolveClass(result, formulaType);
1725    if(result == Ctlsp_Mixed_c)
1726      return result;
1727  }
1728  return result;
1729} /* End of Ctlsp_CheckTypeOfExistentialFormulaArray */
1730
1731/**Function********************************************************************
1732
1733  Synopsis    [Get the class of a formula]
1734
1735  Description [Get the current class of a CTL* sub-formula]
1736
1737  SideEffects []
1738
1739  SeeAlso     []
1740
1741******************************************************************************/
1742Ctlsp_ClassOfFormula
1743Ctlsp_FormulaReadClass(Ctlsp_Formula_t *formula)
1744{
1745  return formula->class_;
1746}
1747
1748/**Function********************************************************************
1749
1750  Synopsis    [Set the class of a formula]
1751
1752  Description []
1753
1754  SideEffects []
1755
1756  SeeAlso     []
1757
1758******************************************************************************/
1759void
1760Ctlsp_FormulaSetClass(Ctlsp_Formula_t *formula, Ctlsp_ClassOfFormula newClass)
1761{
1762  if (formula == NIL(Ctlsp_Formula_t)){
1763    return;
1764  }
1765  formula->class_ = newClass;
1766}
1767
1768
1769/**Function********************************************************************
1770
1771  Synopsis    [Get the type of a CTL formula]
1772
1773  Description []
1774
1775  SideEffects []
1776
1777  SeeAlso     []
1778
1779******************************************************************************/
1780
1781Ctlsp_ClassOfCTLFormula
1782Ctlsp_FormulaReadClassOfCTL(Ctlsp_Formula_t *formula)
1783{
1784  return formula->CTLclass;
1785}
1786
1787/**Function********************************************************************
1788
1789  Synopsis    [Set the class of CTL]
1790
1791  Description []
1792
1793  SideEffects []
1794
1795  SeeAlso     []
1796
1797******************************************************************************/
1798void
1799Ctlsp_FormulaSetClassOfCTL(
1800  Ctlsp_Formula_t *formula,
1801  Ctlsp_ClassOfCTLFormula newCTLclass)
1802{
1803  if (formula == NIL(Ctlsp_Formula_t)){
1804    return;
1805  }
1806  formula->CTLclass = newCTLclass;
1807}
1808
1809/**Function********************************************************************
1810
1811  Synopsis    [Returns an array of LTL formulae.]
1812
1813  Description [Returns an array of LTL formulae given the array of CTL*
1814               formulae.
1815               If any of the CTL* formula is not LTL formula, retuns NIL.
1816               The return LTL formulae share absolutely nothing with the
1817               original CTL* formulae (not even a string).]
1818
1819  SideEffects []
1820
1821  SeeAlso     []
1822
1823******************************************************************************/
1824array_t *
1825Ctlsp_FormulaArrayConvertToLTL(
1826   array_t *formulaArray)
1827{
1828  array_t *ltlFormulaArray;
1829  int i;
1830
1831  ltlFormulaArray = array_alloc(Ctlsp_Formula_t *, 0);
1832
1833  /* Check if all CTL* formulas are LTL formulas */
1834  for (i = 0; i < array_n(formulaArray); i++) {
1835    Ctlsp_Formula_t *formula, *ltlFormula;
1836
1837    formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i);
1838
1839    if (!Ctlsp_isLtlFormula(formula)){
1840     Ctlsp_FormulaArrayFree(ltlFormulaArray);
1841     return NIL(array_t);
1842    }
1843    ltlFormula = Ctlsp_FormulaDup(formula);
1844    array_insert_last(Ctlsp_Formula_t *, ltlFormulaArray, ltlFormula);
1845
1846   } /* For Loop */
1847  return ltlFormulaArray;
1848} /*  Ctlsp_FormulaArrayConvertToLTL() */
1849
1850/**Function********************************************************************
1851
1852  Synopsis [Returns an array of CTL formulas from the parsed array of
1853  CTL* formulas]
1854
1855  Description [This function takes an array of CTL* formulae and returns
1856               an array of CTL formulae if applicable.  Function
1857               returns NIL if any CTL * formula can't be converted to
1858               CTL formula.  The returned CTL formulae share absolutely
1859               nothing with the original CTL* formulae (not even a
1860               string).]
1861
1862  SideEffects []
1863
1864  SeeAlso     [Ctlsp_FormulaConvertToCTL]
1865
1866******************************************************************************/
1867array_t *
1868Ctlsp_FormulaArrayConvertToCTL(
1869  array_t *formulaArray)
1870{
1871  array_t *CtlFormulaArray;
1872  int i;
1873
1874  CtlFormulaArray = array_alloc(Ctlp_Formula_t *, 0);
1875
1876  /* Convert each formula in the array to CTL */
1877  for (i = 0; i < array_n(formulaArray); i++) {
1878    Ctlsp_Formula_t *formula;
1879    Ctlp_Formula_t *newFormula;
1880
1881    formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i);
1882    newFormula = Ctlsp_FormulaConvertToCTL(formula);
1883
1884    if (newFormula !=  NIL(Ctlp_Formula_t)){
1885       array_insert_last(Ctlp_Formula_t *, CtlFormulaArray, newFormula);
1886    }
1887    else{
1888       (void) fprintf(vis_stderr, "** ctl* error : Can't Convert CTL* No. %d to CTL formula\n\n", i);
1889       Ctlp_FormulaArrayFree(CtlFormulaArray);
1890       return NIL(array_t);
1891    }
1892   } /* For Loop */
1893  return CtlFormulaArray;
1894} /*  Ctlsp_FormulaArrayConvertToCTL() */
1895
1896/**Function********************************************************************
1897
1898  Synopsis    [Convert an CTL* formula to CTL formula]
1899
1900  Description [This function takes a formula in CTL* and returns a CTL formula
1901  if applicable.  CTL* consists of two formula classes: state formulas and
1902  path formulas. CTL formula is a state formula.  CTL* formula can be
1903  converted to CTL formula if the CTL* formula is state formula.
1904  Note: This function must be called for each formula in a given array.]
1905
1906  SideEffects []
1907
1908  SeeAlso     [Ctlsp_FormulaArrayConvertToCTL]
1909
1910******************************************************************************/
1911Ctlp_Formula_t *
1912Ctlsp_FormulaConvertToCTL(
1913  Ctlsp_Formula_t *formula)
1914{
1915  if (Ctlsp_FormulaReadClassOfCTL(formula) ==  Ctlsp_CTL_c) {/* CTL* can be converted to CTL */
1916    return CtlspFormulaConvertToCTL(formula);
1917  }
1918  else{
1919    return NIL(Ctlp_Formula_t);
1920  }
1921} /*  Ctlsp_FormulaConvertToCTL() */
1922
1923/**Function********************************************************************
1924  Synopsis    [Convert a propositional CTL* formula to CTL formula]
1925
1926  Description [A wrapper to CtlspFormulaConvertToCTL]
1927
1928  SideEffects []
1929
1930  SeeAlso     [Ctlsp_FormulaArrayConvertToCTL]
1931
1932******************************************************************************/
1933Ctlp_Formula_t *
1934Ctlsp_PropositionalFormulaToCTL(
1935  Ctlsp_Formula_t *formula)
1936{
1937    return CtlspFormulaConvertToCTL(formula);
1938}
1939
1940
1941/**Function********************************************************************
1942
1943  Synopsis    [Return true if CTL* formula is a propositional formula.]
1944
1945  Description []
1946
1947  SideEffects []
1948
1949  SeeAlso     [Ctlsp_FormulaReadClass()]
1950
1951******************************************************************************/
1952int
1953Ctlsp_isPropositionalFormula(
1954  Ctlsp_Formula_t *formula)
1955{
1956  return (Ctlsp_FormulaReadClass(formula) == Ctlsp_propformula_c);
1957} /* Ctlsp_isPropositionalFormula() */
1958
1959/**Function********************************************************************
1960
1961  Synopsis    [Return true if CTL* formula is an CTL formula.]
1962
1963  Description []
1964
1965  SideEffects []
1966
1967  SeeAlso     [Ctlsp_FormulaReadClassOfCTL()]
1968
1969******************************************************************************/
1970int
1971Ctlsp_isCtlFormula(
1972  Ctlsp_Formula_t *formula)
1973{
1974  return (Ctlsp_FormulaReadClassOfCTL(formula) ==  Ctlsp_CTL_c);
1975} /* Ctlsp_isCtlFormula() */
1976
1977/**Function********************************************************************
1978
1979  Synopsis    [Return true if CTL* formula is an LTL formula.]
1980
1981  Description [a formula is LTL formul if its one of the following:
1982               - Its class is Ctlsp_LTLformula_c
1983               - it is in the form A(Ctlsp_LTLformula_c).
1984               - Its class is Ctlsp_propformula_c.
1985               - it is in the form A(Ctlsp_propformula_c)
1986              ]
1987  SideEffects []
1988
1989  SeeAlso     [Ctlsp_FormulaReadClass()]
1990
1991******************************************************************************/
1992int
1993Ctlsp_isLtlFormula(
1994  Ctlsp_Formula_t *formula)
1995{
1996  if (Ctlsp_FormulaReadClass(formula) == Ctlsp_LTLformula_c){
1997    return 1;
1998  }
1999  if (Ctlsp_FormulaReadClass(formula) == Ctlsp_propformula_c){
2000    return 1;
2001  }
2002  if (formula->type ==  Ctlsp_A_c) {
2003    if ((Ctlsp_FormulaReadClass(formula->left) == Ctlsp_LTLformula_c) ||
2004        (Ctlsp_FormulaReadClass(formula->left) == Ctlsp_propformula_c)) {
2005      return 1;
2006      }
2007    else {
2008      return 0;
2009    }
2010  }
2011  return 0;
2012} /* Ctlsp_isLtlFormula() */
2013
2014/**Function********************************************************************
2015
2016  Synopsis    [Negate an LTL formula]
2017
2018  Description [This function returns an abbreviation-free LTL formula
2019               of the negation of the input LTL formula. The returned
2020               formula share absolutely nothing with the input LTL
2021               formula.]
2022
2023  Comment     []
2024
2025  SideEffects []
2026
2027  SeeAlso     []
2028
2029******************************************************************************/
2030Ctlsp_Formula_t *
2031Ctlsp_LtllFormulaNegate(
2032  Ctlsp_Formula_t *ltlFormula)
2033{
2034  Ctlsp_Formula_t *negLtlFormula, *tmpLtlFormula;
2035
2036  negLtlFormula = Ctlsp_FormulaCreate(Ctlsp_NOT_c, ltlFormula, NIL(Ctlsp_Formula_t));
2037  tmpLtlFormula = Ctlsp_LtlFormulaExpandAbbreviation(negLtlFormula);
2038  FREE(negLtlFormula);
2039  negLtlFormula = Ctlsp_LtlFormulaNegationNormalForm(tmpLtlFormula);
2040  if(negLtlFormula != tmpLtlFormula) {
2041    Ctlsp_FormulaFree(tmpLtlFormula);
2042  }
2043  tmpLtlFormula = Ctlsp_LtlFormulaSimpleRewriting(negLtlFormula);
2044  Ctlsp_FormulaFree(negLtlFormula);
2045  Ctlsp_LtlSetClass(tmpLtlFormula);
2046
2047  return tmpLtlFormula;
2048} /* Ctlsp_LtllFormulaNegate() */
2049
2050/**Function********************************************************************
2051
2052  Synopsis    [Set the class of the LTL formula]
2053
2054  Description [This function recursively sets the class of LTL subformula. For
2055  leave nodes, by default the class sets to Ctlsp_propformula_c when the node
2056  is created.]
2057
2058  Comment     [The class filed of an LTL subformula will not be set if the
2059  programmer uses FormulaCreateWithType() and then later he adds its children.
2060  The correct way of creating a new node knowing its childeren is by using
2061  Ctlsp_FormulaCreate()]
2062
2063  SideEffects []
2064
2065  SeeAlso     [ctlspInt.h Ctlsp_FormulaCreate]
2066
2067******************************************************************************/
2068void
2069Ctlsp_LtlSetClass(
2070  Ctlsp_Formula_t *formula)
2071{
2072  Ctlsp_Formula_t *left, *right;
2073
2074  if (formula == NIL(Ctlsp_Formula_t)){
2075    return;
2076  }
2077  if (formula->type == Ctlsp_ID_c){
2078    return;
2079  }
2080  if (formula->type == Ctlsp_TRUE_c){
2081    return;
2082  }
2083  if (formula->type == Ctlsp_FALSE_c){
2084    return;
2085  }
2086  left  = formula->left;
2087  right = formula->right;
2088
2089  Ctlsp_LtlSetClass(left);
2090  Ctlsp_LtlSetClass(right);
2091
2092  switch(formula->type) {
2093    case Ctlsp_OR_c:
2094    case Ctlsp_AND_c:
2095    case Ctlsp_THEN_c:
2096    case Ctlsp_XOR_c:
2097    case Ctlsp_EQ_c:
2098      Ctlsp_FormulaSetClass(formula, table1(Ctlsp_FormulaReadClass(left),Ctlsp_FormulaReadClass(right)));
2099      break;
2100    case Ctlsp_NOT_c:
2101      Ctlsp_FormulaSetClass(formula, Ctlsp_FormulaReadClass(left));
2102      break;
2103    case Ctlsp_E_c:
2104    case Ctlsp_A_c:
2105      Ctlsp_FormulaSetClass(formula, Ctlsp_stateformula_c);
2106      break;
2107    case Ctlsp_G_c:
2108    case Ctlsp_F_c:
2109      Ctlsp_FormulaSetClass(formula, table2(Ctlsp_FormulaReadClass(left)));
2110      break;
2111    case Ctlsp_U_c:
2112    case Ctlsp_R_c:
2113    case Ctlsp_W_c:
2114      Ctlsp_FormulaSetClass(formula, table3(Ctlsp_FormulaReadClass(left),Ctlsp_FormulaReadClass(right)));
2115      break;
2116    case Ctlsp_X_c:
2117      Ctlsp_FormulaSetClass(formula, table2(Ctlsp_FormulaReadClass(left)));
2118      break;
2119    default:
2120      break;
2121  }
2122  return;
2123}
2124
2125/**Function********************************************************************
2126
2127  Synopsis    [Return TRUE iff formula is a "GF(propositional formula)".]
2128
2129  Description [GFp = FALSE R (TRUE U p) in abbreviation-free LTL formulae.]
2130
2131  SideEffects []
2132
2133  SeeAlso     []
2134
2135******************************************************************************/
2136int
2137Ctlsp_LtlFormulaIsGFp(
2138  Ctlsp_Formula_t *formula)
2139{
2140 Ctlsp_Formula_t *rightChild;
2141 Ctlsp_Formula_t *leftChild;
2142
2143 assert(formula != NIL(Ctlsp_Formula_t));
2144
2145 if (Ctlsp_FormulaReadType(formula) == Ctlsp_R_c) {
2146   rightChild = Ctlsp_FormulaReadRightChild(formula);
2147   leftChild  = Ctlsp_FormulaReadLeftChild(formula);
2148
2149   if ((Ctlsp_FormulaReadType(leftChild) == Ctlsp_FALSE_c) &&
2150       (Ctlsp_FormulaReadType(rightChild) == Ctlsp_U_c)){
2151     if ((Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(rightChild)) == Ctlsp_TRUE_c) &&
2152         (Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadRightChild(rightChild)))) {
2153       return TRUE;
2154     }
2155   }
2156 }
2157
2158 return FALSE;
2159}/* Ctlsp_LtlFormulaIsGFp() */
2160
2161
2162/**Function********************************************************************
2163
2164  Synopsis    [Return TRUE iff formula is a "G(propositional formula)".]
2165
2166  Description [G(p) = FALSE R p in abbreviation-free LTL formulae.]
2167
2168  SideEffects []
2169
2170  SeeAlso     [Ctlsp_isPropositionalFormula]
2171
2172******************************************************************************/
2173boolean
2174Ctlsp_LtlFormulaIsGp(
2175  Ctlsp_Formula_t *formula)
2176{
2177  assert(formula != NIL(Ctlsp_Formula_t));
2178
2179  if ((Ctlsp_FormulaReadType(formula)== Ctlsp_G_c) &&
2180       Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadLeftChild(formula))){
2181    return TRUE;
2182  }
2183  if (Ctlsp_FormulaReadType(formula) == Ctlsp_R_c) {
2184    if ((Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(formula)) == Ctlsp_FALSE_c) &&
2185        (Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadRightChild(formula)))) {
2186      return TRUE;
2187    }
2188  }
2189  return FALSE;
2190} /* Ctlsp_LtlFormulaIsGp */
2191
2192/**Function********************************************************************
2193
2194  Synopsis    [Return TRUE iff formula is a "F(propositional formula)".]
2195
2196  Description [F(p) = TRUE U p in abbreviation-free LTL formulae.]
2197
2198  SideEffects []
2199
2200  SeeAlso     [Ctlsp_isPropositionalFormula]
2201
2202******************************************************************************/
2203boolean
2204Ctlsp_LtlFormulaIsFp(
2205  Ctlsp_Formula_t *formula)
2206{
2207  assert(formula != NIL(Ctlsp_Formula_t));
2208
2209  if ((Ctlsp_FormulaReadType(formula)== Ctlsp_F_c) &&
2210      Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadLeftChild(formula))){
2211    return TRUE;
2212  }
2213  if (Ctlsp_FormulaReadType(formula) == Ctlsp_U_c) {
2214    if ((Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(formula)) == Ctlsp_TRUE_c) &&
2215        Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadRightChild(formula))) {
2216      return TRUE;
2217    }
2218  }
2219  return FALSE;
2220} /* Ctlsp_LtlFormulaIsFp */
2221
2222#if 0
2223/**Function********************************************************************
2224
2225  Synopsis    [Return TRUE iff formula is a safety property.]
2226
2227  Description [ The characterization of LTL formula as a safety formula is
2228  taken from the paper by A. Prasad Sistla: Safety, Liveness and Fairness in
2229  Temporal Logic.
2230  Theorm 3.1 page 8: (For positive LTL formula: formula in Negation Normal Form).
2231    - Every propositional formula is a safety formula.
2232    - If f, g are safety formula, then so are
2233      - f AND g.
2234      - f OR  g.
2235      - X(f).
2236      - f W g. (unless temporal operator).
2237      - G(f).
2238
2239  This function can only be applied to abbreviation-free LTL formulae. The
2240  formula must be in Negation Normal Form.]
2241
2242  SideEffects []
2243
2244  SeeAlso     []
2245
2246******************************************************************************/
2247boolean
2248Ctlsp_LtlFormulaIsSafety(
2249  Ctlsp_Formula_t *formula)
2250{
2251  assert(formula != NIL(Ctlsp_Formula_t));
2252
2253  if (Ctlsp_isPropositionalFormula(formula)){
2254    return TRUE;
2255  }
2256  if (Ctlsp_LtlFormulaIsW(formula)){
2257    return Ctlsp_LtlFormulaIsSafety(Ctlsp_FormulaReadLeftChild(formula)) &&
2258      Ctlsp_LtlFormulaIsSafety(Ctlsp_FormulaReadRightChild(formula));
2259  }
2260  swtich (Ctlsp_FormulaReadType(formula)){
2261  case Ctlsp_AND_c:
2262  case Ctlsp_OR_c:
2263    return Ctlsp_LtlFormulaIsSafety(Ctlsp_FormulaReadLeftChild(formula)) &&
2264           Ctlsp_LtlFormulaIsSafety(Ctlsp_FormulaReadRightChild(formula));
2265  case Ctlsp_X_c:
2266    return Ctlsp_LtlFormulaIsSafety(Ctlsp_FormulaReadLeftChild(formula));
2267  case Ctlsp_NOT_c:
2268  case Ctlsp_U_c:
2269  case Ctlsp_R_c:
2270    return FALSE;
2271  default:
2272    fail("unexpected node type in abbreviation-free formula\n");
2273    return FALSE; /* not reached */
2274  }
2275
2276  /*    == Ctlsp_F_c) &&
2277      Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadLeftChild(formula))){
2278    return TRUE;
2279    } */
2280  if (Ctlsp_FormulaReadType(formula) == Ctlsp_U_c) {
2281    if (Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(formula) == Ctlsp_TRUE_c) &&
2282        Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadRightChild(formula))) {
2283      return TRUE;
2284    }
2285  }
2286  return FALSE;
2287} /* Ctlsp_LtlFormulaIsSafety */
2288#endif
2289
2290
2291/**Function********************************************************************
2292
2293  Synopsis    [Add fairness constraints to an array of LTL formulae.]
2294
2295  Description [This function modifies an array of LTL formulae by adding to
2296  each of them a fairness constraint.  This fairness constraint is the
2297  conjunction of all fairness constraints in constraintArray.  For consistency
2298  with what done throughout VIS, each line in the file is interpreted as a
2299  condition that must hold infinitely often.  The function assumes that the
2300  incoming array only contains LTL formulae.  The returned formulae are not
2301  normalized and not converted to DAGs.]
2302
2303  SideEffects [formulaArray is modified]
2304
2305  SeeAlso []
2306
2307******************************************************************************/
2308void
2309Ctlsp_FormulaArrayAddLtlFairnessConstraints(
2310  array_t *formulaArray     /* array of LTL formulae */,
2311  array_t *constraintArray /* array of fairness constraints */)
2312{
2313  Ctlsp_Formula_t *formula;     /* a generic LTL formula */
2314  Ctlsp_Formula_t *fairness;    /* a generic fairness constraint */
2315  int i;                        /* iteration variable */
2316
2317  assert(formulaArray != NIL(array_t));
2318  assert(constraintArray != NIL(array_t));
2319  /*
2320   * Create the overall fairness constraints.  If the given constraints
2321   * are C_1, C_2, ..., C_k, build the formula /\_i GF C_i.
2322   */
2323  fairness = NIL(Ctlsp_Formula_t);
2324  arrayForEachItem(Ctlsp_Formula_t *, constraintArray, i, formula) {
2325    Ctlsp_Formula_t *finally;
2326    Ctlsp_Formula_t *globally;
2327    finally =  Ctlsp_FormulaCreate(Ctlsp_F_c, formula, NIL(Ctlsp_Formula_t));
2328    globally = Ctlsp_FormulaCreate(Ctlsp_G_c, finally, NIL(Ctlsp_Formula_t));
2329    if (i == 0) {
2330      fairness = globally;
2331    } else {
2332      fairness = Ctlsp_FormulaCreate(Ctlsp_AND_c, fairness, globally);
2333    }
2334  }
2335  /* Empty fairness constraint files are forbidden. */
2336  assert(fairness != NIL(Ctlsp_Formula_t));
2337
2338  /*
2339   * Add fairness to each given formula: Replace f_i by (fairness -> f_i).
2340   */
2341  arrayForEachItem(Ctlsp_Formula_t *, formulaArray, i, formula) {
2342    Ctlsp_Formula_t *modified;
2343    modified = Ctlsp_FormulaCreate(Ctlsp_THEN_c,
2344                                   Ctlsp_FormulaDup(fairness), formula);
2345    array_insert(Ctlsp_Formula_t *, formulaArray, i, modified);
2346  }
2347  Ctlsp_FormulaFree(fairness);
2348
2349} /* Ctlsp_FormulaArrayAddLtlFairnessConstraints */
2350
2351
2352/**Function********************************************************************
2353
2354  Synopsis    [Translate a CTL formula into a CTL* formula.]
2355
2356  Description [Translate a CTL formula into a CTL* formula.]
2357
2358  SideEffects []
2359
2360  SeeAlso     []
2361
2362******************************************************************************/
2363Ctlsp_Formula_t *
2364Ctlsp_CtlFormulaToCtlsp(Ctlp_Formula_t *F)
2365{
2366    Ctlsp_Formula_t *Fsp;
2367    Ctlp_FormulaType Ftype;
2368    Ctlsp_FormulaType Fsptype;
2369
2370    if (F == NIL(Ctlp_Formula_t))
2371        return NIL(Ctlsp_Formula_t);
2372
2373    Ftype = Ctlp_FormulaReadType(F);
2374    Fsptype = (Ctlsp_FormulaType) Ftype;
2375
2376    if (Ftype == Ctlp_TRUE_c) {
2377        Fsp = Ctlsp_FormulaCreate(Ctlsp_TRUE_c, NIL(Ctlsp_Formula_t),
2378                                  NIL(Ctlsp_Formula_t));
2379    }else if (Ftype == Ctlp_FALSE_c) {
2380        Fsp = Ctlsp_FormulaCreate(Ctlsp_FALSE_c, NIL(Ctlsp_Formula_t),
2381                                  NIL(Ctlsp_Formula_t));
2382    }else if (Ftype == Ctlp_ID_c) {
2383        char *nameString = Ctlp_FormulaReadVariableName(F);
2384        char *valueString = Ctlp_FormulaReadValueName(F);
2385        Fsp = Ctlsp_FormulaCreate(Ctlsp_ID_c,
2386                                  util_strsav(nameString),
2387                                  util_strsav(valueString));
2388    }else {
2389        Ctlp_Formula_t *Fleft = Ctlp_FormulaReadLeftChild(F);
2390        Ctlp_Formula_t *Fright = Ctlp_FormulaReadRightChild(F);
2391        Ctlsp_Formula_t *Fspleft, *Fspright;
2392        Fspleft = Ctlsp_CtlFormulaToCtlsp(Fleft);
2393        Fspright = Ctlsp_CtlFormulaToCtlsp(Fright);
2394        switch(Ftype) {
2395        case Ctlp_NOT_c:
2396            Fsptype = Ctlsp_NOT_c;
2397            break;
2398        case Ctlp_AND_c:
2399            Fsptype = Ctlsp_AND_c;
2400            break;
2401        case Ctlp_OR_c:
2402            Fsptype = Ctlsp_OR_c;
2403            break;
2404        case Ctlp_THEN_c:
2405            Fsptype = Ctlsp_THEN_c;
2406            break;
2407        case Ctlp_EQ_c:
2408            Fsptype = Ctlsp_EQ_c;
2409            break;
2410        case Ctlp_XOR_c:
2411            Fsptype = Ctlsp_XOR_c;
2412            break;
2413        default:
2414            assert(0);
2415        }
2416        if (Fspleft)
2417            CtlspFormulaIncrementRefCount(Fspleft);
2418        if (Fspright)
2419            CtlspFormulaIncrementRefCount(Fspright);
2420        Fsp = Ctlsp_FormulaCreate(Fsptype, Fspleft, Fspright);
2421    }
2422
2423    return Fsp;
2424}
2425
2426
2427/**Function********************************************************************
2428
2429  Synopsis    [Return a LTL formula with the abbreviations expanded.]
2430
2431  Description [The input must be a legal LTL formula. The result shares
2432  nothing with the input, not even a string; The result itself  does not share
2433  sub-formulae. The translation rule is:
2434    Ctlsp_THEN_c        a->b  :   !a + b
2435    Ctlsp_EQ_c          a<->b :   a*b +!a*!b
2436    Ctlsp_XOR_c         a^b   :   a*!b + !a*b
2437    Ctlsp_F_c           Fa    :   true U a
2438    Ctlsp_G_c           Ga    :   false R a
2439    Ctlsp_A_c           Aa    :   a
2440    ]
2441
2442  SideEffects []
2443
2444  SeeAlso     []
2445
2446******************************************************************************/
2447Ctlsp_Formula_t *
2448Ctlsp_LtlFormulaExpandAbbreviation(
2449  Ctlsp_Formula_t *formula)
2450{
2451  Ctlsp_Formula_t *new_;
2452
2453  if (formula == NIL(Ctlsp_Formula_t))
2454    return formula;
2455
2456  switch (formula->type) {
2457  case Ctlsp_THEN_c:
2458    /* a -> b  :: !a + b */
2459    new_ = FormulaCreateWithType(Ctlsp_OR_c);
2460    new_->left = FormulaCreateWithType(Ctlsp_NOT_c);
2461    new_->left->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
2462    new_->right = Ctlsp_LtlFormulaExpandAbbreviation(formula->right);
2463    break;
2464  case Ctlsp_EQ_c:
2465    /* a <-> b  :: a*b + !a*!b */
2466    new_ = FormulaCreateWithType(Ctlsp_OR_c);
2467    new_->left = FormulaCreateWithType(Ctlsp_AND_c);
2468    new_->right= FormulaCreateWithType(Ctlsp_AND_c);
2469    new_->left->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
2470    new_->left->right= Ctlsp_LtlFormulaExpandAbbreviation(formula->right);
2471    new_->right->left = FormulaCreateWithType(Ctlsp_NOT_c);
2472    new_->right->left->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
2473    new_->right->right= FormulaCreateWithType(Ctlsp_NOT_c);
2474    new_->right->right->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->right);
2475    break;
2476  case Ctlsp_XOR_c:
2477    /* a ^ b  :: a*!b + !a*b */
2478    new_ = FormulaCreateWithType(Ctlsp_OR_c);
2479    new_->left = FormulaCreateWithType(Ctlsp_AND_c);
2480    new_->left->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
2481    new_->left->right= FormulaCreateWithType(Ctlsp_NOT_c);
2482    new_->left->right->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->right);
2483    new_->right = FormulaCreateWithType(Ctlsp_AND_c);
2484    new_->right->left= FormulaCreateWithType(Ctlsp_NOT_c);
2485    new_->right->left->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
2486    new_->right->right = Ctlsp_LtlFormulaExpandAbbreviation(formula->right);
2487    break;
2488  case Ctlsp_F_c:
2489    /* F a  :: true U a */
2490    new_ = FormulaCreateWithType(Ctlsp_U_c);
2491    new_->left = FormulaCreateWithType(Ctlsp_TRUE_c);
2492    new_->right= Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
2493    break;
2494  case Ctlsp_G_c:
2495    /* G a  :: false R a */
2496    new_ = FormulaCreateWithType(Ctlsp_R_c);
2497    new_->left = FormulaCreateWithType(Ctlsp_FALSE_c);
2498    new_->right= Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
2499    break;
2500  case Ctlsp_W_c:
2501    /* a W b :: b R (a+b) */
2502    new_ = FormulaCreateWithType(Ctlsp_R_c);
2503    new_->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->right);
2504    new_->right = FormulaCreateWithType(Ctlsp_OR_c);
2505    new_->right->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->right);
2506    new_->right->right = Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
2507    break;
2508  case Ctlsp_ID_c:
2509    /* Make a copy of the name, and create a new formula. */
2510    new_ = FormulaCreateWithType(Ctlsp_ID_c);
2511    new_->left = (Ctlsp_Formula_t *) util_strsav((char *)(formula->left));
2512    new_->right= (Ctlsp_Formula_t *) util_strsav((char *)(formula->right));
2513    break;
2514  case Ctlsp_A_c:
2515    /* Ignore A */
2516    new_ = Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
2517    break;
2518  default:
2519    /* These are already in the correct form.  Just convert subformulas. */
2520    new_ = FormulaCreateWithType(formula->type);
2521    new_->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
2522    new_->right= Ctlsp_LtlFormulaExpandAbbreviation(formula->right);
2523  }
2524
2525  return new_;
2526}
2527
2528/**Function********************************************************************
2529
2530  Synopsis    [Return the Negation Normal Form (NNF) of a LTL formula.]
2531
2532  Description [The negation is pushed to the bottom (only ahead fo atomic
2533  formulae). The result shares nothing with the input, not even a string;
2534  subformulae in the result are not shared either.
2535
2536  Assume the formula is abbreviation-free, and there are only the following
2537  types of formulae before translation:
2538    TRUE/ FALSE/ ID/ AND/ OR/ U/ R/ X/ !  .]
2539
2540  SideEffects []
2541
2542  SeeAlso     []
2543
2544******************************************************************************/
2545Ctlsp_Formula_t *
2546Ctlsp_LtlFormulaNegationNormalForm(
2547  Ctlsp_Formula_t *formula)
2548{
2549  Ctlsp_Formula_t *new_, *left, *right;
2550#if 0
2551  Ctlsp_Formula_t  *negRight, *negLeft;
2552#endif
2553  Ctlsp_FormulaType dual;
2554
2555  if (formula == NIL(Ctlsp_Formula_t))
2556    return formula;
2557
2558  if (formula->type == Ctlsp_TRUE_c || formula->type == Ctlsp_FALSE_c) {
2559    new_ = FormulaCreateWithType(formula->type);
2560    return new_;
2561  }
2562
2563  if (formula->type == Ctlsp_ID_c) {
2564    new_ = FormulaCreateWithType(formula->type);
2565    new_->left =(Ctlsp_Formula_t *)util_strsav((char *)(formula->left));
2566    new_->right=(Ctlsp_Formula_t *)util_strsav((char *)(formula->right));
2567    return new_;
2568  }
2569
2570  if (formula->type != Ctlsp_NOT_c) {
2571    new_ = FormulaCreateWithType(formula->type);
2572    new_->left = Ctlsp_LtlFormulaNegationNormalForm(formula->left);
2573    new_->right= Ctlsp_LtlFormulaNegationNormalForm(formula->right);
2574    return new_;
2575  }
2576
2577  /* In the following, formula->type == Ctlsp_NOT_c */
2578  if (formula->left->type == Ctlsp_NOT_c)
2579    return Ctlsp_LtlFormulaNegationNormalForm(formula->left->left);
2580
2581  if (formula->left->type == Ctlsp_ID_c) {
2582    new_ = FormulaCreateWithType(formula->type);
2583    new_->left = Ctlsp_LtlFormulaNegationNormalForm(formula->left);
2584    return new_;
2585  }
2586#if 0
2587  if (formula->left->type == Ctlsp_THEN_c ) {
2588    left  = Ctlsp_LtlFormulaNegationNormalForm(formula->left->left);
2589    right = Ctlsp_FormulaCreate(Ctlsp_NOT_c, formula->left->right, NIL(Ctlsp_Formula_t));
2590    right = Ctlsp_LtlFormulaNegationNormalForm(right);
2591    new_   = Ctlsp_FormulaCreate(Ctlsp_AND_c, left, right);
2592    return new_;
2593  }
2594  if (formula->left->type == Ctlsp_EQ_c ) {
2595    left  = Ctlsp_LtlFormulaNegationNormalForm(formula->left->left);
2596    right = Ctlsp_LtlFormulaNegationNormalForm(formula->left->right);
2597    negRight = Ctlsp_FormulaCreate(Ctlsp_NOT_c, right, NIL(Ctlsp_Formula_t));
2598    negLeft  = Ctlsp_FormulaCreate(Ctlsp_NOT_c, left, NIL(Ctlsp_Formula_t));
2599    left     = right= Ctlsp_FormulaCreate(Ctlsp_AND_c, left, negRight);
2600    right    = right= Ctlsp_FormulaCreate(Ctlsp_AND_c, negLeft, right);
2601    new_      = Ctlsp_FormulaCreate(Ctlsp_OR_c, left, right);
2602    return Ctlsp_LtlFormulaNegationNormalForm(new_);
2603  }
2604#endif
2605  /* for TRUE/ FALSE/ AND/ OR/ U/ R/ X/ F/ G */
2606  switch (formula->left->type) {
2607  case Ctlsp_TRUE_c:
2608    dual = Ctlsp_FALSE_c;
2609    break;
2610  case Ctlsp_FALSE_c:
2611    dual = Ctlsp_TRUE_c;
2612    break;
2613  case Ctlsp_AND_c:
2614    dual = Ctlsp_OR_c;
2615    break;
2616  case Ctlsp_OR_c:
2617    dual = Ctlsp_AND_c;
2618    break;
2619  case Ctlsp_U_c:
2620    dual = Ctlsp_R_c;
2621    break;
2622  case Ctlsp_R_c:
2623    dual = Ctlsp_U_c;
2624    break;
2625  case Ctlsp_X_c:
2626    dual = Ctlsp_X_c;
2627    break;
2628  case Ctlsp_F_c:
2629    dual = Ctlsp_G_c;
2630    break;
2631  case Ctlsp_G_c:
2632    dual = Ctlsp_F_c;
2633    break;
2634  default:
2635    fail("Unexpected type");
2636  }
2637
2638  /* alloc temporary formulae (! left) and (! right) */
2639  left = Ctlsp_FormulaCreate(Ctlsp_NOT_c, formula->left->left, NIL(Ctlsp_Formula_t));
2640  right= Ctlsp_FormulaCreate(Ctlsp_NOT_c, formula->left->right, NIL(Ctlsp_Formula_t));
2641
2642  /* create the new formula */
2643  new_ = FormulaCreateWithType(dual);
2644  if ((dual == Ctlsp_X_c) ||
2645      (dual == Ctlsp_F_c) ||
2646      (dual == Ctlsp_G_c) ){
2647    new_->left = Ctlsp_LtlFormulaNegationNormalForm(left);
2648  }else if (dual != Ctlsp_TRUE_c && dual != Ctlsp_FALSE_c) {
2649    new_->left = Ctlsp_LtlFormulaNegationNormalForm(left);
2650    new_->right= Ctlsp_LtlFormulaNegationNormalForm(right);
2651  }
2652  FREE(left);
2653  FREE(right);
2654
2655  return new_;
2656}
2657
2658/**Function********************************************************************
2659
2660Synopsis    [Hash the LTL formula and its sub-formulae into uniquetable.]
2661
2662Description [It is possible that 'F' is freed, in which case a new 'F' is
2663returned.]
2664
2665SideEffects []
2666
2667SeeAlso     []
2668
2669******************************************************************************/
2670
2671Ctlsp_Formula_t *
2672Ctlsp_LtlFormulaHashIntoUniqueTable(
2673  Ctlsp_Formula_t *F,
2674  st_table *uniqueTable)
2675{
2676  Ctlsp_Formula_t *uniqueFormula;
2677
2678  uniqueFormula = FormulaHashIntoUniqueTable(F, uniqueTable);
2679
2680  /* If there is a copy 'uniqueFormula' in the uniqueTable, free F and
2681     increment the refCount of 'uniqueFormula' */
2682  if(uniqueFormula != F) {
2683    CtlspFormulaDecrementRefCount(F);
2684    CtlspFormulaIncrementRefCount(uniqueFormula);
2685  }
2686
2687  return uniqueFormula;
2688}
2689
2690/**Function********************************************************************
2691
2692Synopsis    [Clear the '.marked' field of the LTL formula.]
2693
2694Description [Recursively clear the .marked field for all its sub-formulae.]
2695
2696SideEffects []
2697
2698SeeAlso     []
2699
2700******************************************************************************/
2701void
2702Ctlsp_LtlFormulaClearMarks(
2703  Ctlsp_Formula_t *F)
2704{
2705  if(F) {
2706    F->marked = 0;
2707    if (F->type != Ctlsp_ID_c) {
2708      Ctlsp_LtlFormulaClearMarks(F->left);
2709      Ctlsp_LtlFormulaClearMarks(F->right);
2710    }
2711  }
2712}
2713
2714/**Function********************************************************************
2715
2716Synopsis    [Clear the '.marked' field of the LTL formula.]
2717
2718Description [Recursively clear the .marked field for all its sub-formulae.]
2719
2720SideEffects []
2721
2722SeeAlso     []
2723
2724******************************************************************************/
2725int
2726Ctlsp_LtlFormulaCountNumber(
2727  Ctlsp_Formula_t *F)
2728{
2729  int result = 1;
2730
2731  if (!F)
2732    return 0;
2733
2734  if (F->marked)
2735    return 0;
2736
2737  F->marked = 1;
2738  if (F->type == Ctlsp_TRUE_c ||
2739      F->type == Ctlsp_FALSE_c ||
2740      F->type == Ctlsp_ID_c)
2741    return 1;
2742
2743  result += Ctlsp_LtlFormulaCountNumber(F->left);
2744  result += Ctlsp_LtlFormulaCountNumber(F->right);
2745
2746  return result;
2747}
2748
2749/**Function********************************************************************
2750
2751  Synopsis    [Alloc a unqiue table for formulae.]
2752
2753  Description [Use FormulaHash and formulaCompare.]
2754
2755  SideEffects []
2756
2757  SeeAlso     []
2758
2759******************************************************************************/
2760st_table *
2761Ctlsp_LtlFormulaCreateUniqueTable( void )
2762{
2763  return st_init_table(FormulaCompare, FormulaHash);
2764}
2765
2766/**Function********************************************************************
2767
2768  Synopsis    [Return True iff formula is an "elementary formula".]
2769
2770  Description [Return True iff formula is an elementary formula. This is the
2771  original definition used in "Wring": it's a TRUE/FALSE/literal/X-formula.]
2772
2773  SideEffects []
2774
2775  SeeAlso     []
2776
2777******************************************************************************/
2778int
2779Ctlsp_LtlFormulaIsElementary2(
2780  Ctlsp_Formula_t *F)
2781{
2782  assert(F != 0);
2783
2784  return (F->type == Ctlsp_X_c || Ctlsp_LtlFormulaIsAtomicPropositional(F) );
2785}
2786
2787/**Function********************************************************************
2788
2789  Synopsis    [Return True iff formula is an "elementary formula".]
2790
2791  Description [Return True iff the formula is an elementary formula. The
2792  definition of 'elementary formula' is slightly different from the one in
2793  "Wring":  it's a TRUE/FALSE/Atomic Propositions/X-formula.]
2794
2795  SideEffects []
2796
2797  SeeAlso     []
2798
2799******************************************************************************/
2800int
2801Ctlsp_LtlFormulaIsElementary(
2802  Ctlsp_Formula_t *F)
2803{
2804  assert(F != NIL(Ctlsp_Formula_t));
2805
2806  return (F->type == Ctlsp_X_c || Ctlsp_LtlFormulaIsPropositional(F) );
2807}
2808
2809/**Function********************************************************************
2810
2811  Synopsis    [Return TRUE iff abbreviation-free LTL formula is bounded.]
2812
2813  Description [A bounded LTL formula is one that contains only atomic
2814  propositions, Boolean connectives, and the next-time (X) operator.
2815  The depth of a bounded formula is the maximum number of Xs along a
2816  path of its parse tree.  This function can only be applied to
2817  abbreviation-free LTL formulae.]
2818
2819  SideEffects [The depth is returned as a side effect.  (Only if the function
2820  returns TRUE.)]
2821
2822  SeeAlso     [Ctlsp_LtlFormulaExpandAbbreviation,
2823               Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe]
2824
2825******************************************************************************/
2826boolean
2827Ctlsp_LtlFormulaTestIsBounded(
2828  Ctlsp_Formula_t *formula,
2829  int *depth)
2830{
2831  Ctlsp_Formula_t *leftChild;
2832  Ctlsp_Formula_t *rightChild;
2833  int leftDepth, rightDepth;
2834
2835  assert(formula != NIL(Ctlsp_Formula_t));
2836
2837  switch (Ctlsp_FormulaReadType(formula)) {
2838  case Ctlsp_TRUE_c:
2839  case Ctlsp_FALSE_c:
2840  case Ctlsp_ID_c:
2841    *depth = 0;
2842    return TRUE;
2843  case Ctlsp_AND_c:
2844  case Ctlsp_OR_c:
2845    leftChild = Ctlsp_FormulaReadLeftChild(formula);
2846    if (Ctlsp_LtlFormulaTestIsBounded(leftChild, &leftDepth)) {
2847      rightChild = Ctlsp_FormulaReadRightChild(formula);
2848      if (Ctlsp_LtlFormulaTestIsBounded(rightChild, &rightDepth)) {
2849        *depth = leftDepth > rightDepth ? leftDepth : rightDepth;
2850        return TRUE;
2851      } else {
2852        return FALSE;
2853      }
2854    } else {
2855      return FALSE;
2856    }
2857  case Ctlsp_NOT_c:
2858  case Ctlsp_X_c:
2859    leftChild = Ctlsp_FormulaReadLeftChild(formula);
2860    if (Ctlsp_LtlFormulaTestIsBounded(leftChild, &leftDepth)) {
2861      if (Ctlsp_FormulaReadType(formula) == Ctlsp_X_c) leftDepth++;
2862      *depth = leftDepth;
2863      return TRUE;
2864    } else {
2865      return FALSE;
2866    }
2867  case Ctlsp_U_c:
2868  case Ctlsp_R_c:
2869    return FALSE;
2870  default:
2871    fail("unexpected node type in abbreviation-free formula\n");
2872    return FALSE; /* not reached */
2873  }
2874} /* Ctlsp_LtlFormulaTestIsBounded */
2875
2876/**Function********************************************************************
2877
2878  Synopsis    [Return the depth of abbreviation-free LTL formula.]
2879
2880  Description [The depth of the LTL formula f is the maximum level of
2881  nesting of temporal operators in f.  This function can only be applied
2882  to abbreviation-free LTL formulae.]
2883
2884  SideEffects []
2885
2886  SeeAlso     [Ctlsp_LtlFormulaExpandAbbreviation]
2887
2888******************************************************************************/
2889int
2890Ctlsp_LtlFormulaDepth(
2891  Ctlsp_Formula_t *formula)
2892{
2893  int leftDepth, rightDepth;
2894
2895  assert(formula != NIL(Ctlsp_Formula_t));
2896
2897  switch (Ctlsp_FormulaReadType(formula)) {
2898  case Ctlsp_TRUE_c:
2899  case Ctlsp_FALSE_c:
2900  case Ctlsp_ID_c:
2901    return 0;
2902  case Ctlsp_AND_c:
2903  case Ctlsp_OR_c:
2904    leftDepth  = Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadLeftChild(formula));
2905    rightDepth = Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadRightChild(formula));
2906    return leftDepth > rightDepth ? leftDepth : rightDepth;
2907  case Ctlsp_NOT_c:
2908    return Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadLeftChild(formula));
2909  case Ctlsp_X_c:
2910    return 1+Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadLeftChild(formula));
2911  case Ctlsp_U_c:
2912  case Ctlsp_R_c:
2913    leftDepth  = Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadLeftChild(formula));
2914    rightDepth = Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadRightChild(formula));
2915    return 1+(leftDepth > rightDepth ? leftDepth : rightDepth);
2916  default:
2917    fail("unexpected node type in abbreviation-free formula\n");
2918    return 0; /* not reached */
2919  }
2920} /* Ctlsp_LtlFormulaDepth */
2921
2922/**Function********************************************************************
2923
2924  Synopsis    [Return TRUE iff LTL formula in negation normal form is
2925  syntactically co-safe.]
2926
2927  Description [A syntactically co-safe LTL formula is a formula in
2928  negation normal form that contains no release (R) operators.  This
2929  function can only be applied to abbreviation-free LTL formulae in
2930  negation normal form.  We test co-safety because this function is
2931  meant to be called on the negation of the given formula.]
2932
2933  SideEffects [none]
2934
2935  SeeAlso     [Ctlsp_LtlFormulaNegationNormalForm,
2936               Ctlsp_LtlFormulaTestIsBounded]
2937
2938******************************************************************************/
2939boolean
2940Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(Ctlsp_Formula_t *formula)
2941{
2942  Ctlsp_Formula_t *leftChild;
2943  Ctlsp_Formula_t *rightChild;
2944
2945  assert(formula != NIL(Ctlsp_Formula_t));
2946
2947  /*
2948    Check for unless temporal operator. a W b = (a U b) OR (FALSE R a)
2949                     its negation = (!a R !b) AND (TRUE U !a)
2950   */
2951  if(Ctlsp_FormulaReadType(formula) ==  Ctlsp_AND_c){
2952    leftChild  = Ctlsp_FormulaReadLeftChild(formula);
2953    rightChild = Ctlsp_FormulaReadRightChild(formula);
2954    if((Ctlsp_FormulaReadType(leftChild)  == Ctlsp_R_c) &&
2955       (Ctlsp_FormulaReadType(rightChild) == Ctlsp_U_c)){
2956      if(Ctlsp_FormulaReadLeftChild(leftChild) == Ctlsp_FormulaReadRightChild(rightChild)){
2957        if(Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(rightChild)) == Ctlsp_TRUE_c){
2958          return Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(
2959                            Ctlsp_FormulaReadLeftChild(leftChild)) &&
2960                 Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(
2961                            Ctlsp_FormulaReadRightChild(leftChild));
2962        }
2963      }
2964    }
2965    /*
2966       a W b = (FALSE R a) OR (a U b)
2967       its negation = (TRUE U !a) AND (!a R !b)
2968   */
2969    if((Ctlsp_FormulaReadType(rightChild) == Ctlsp_R_c) &&
2970       (Ctlsp_FormulaReadType(leftChild) == Ctlsp_U_c)){
2971      if(Ctlsp_FormulaReadLeftChild(rightChild) == Ctlsp_FormulaReadRightChild(leftChild)){
2972        if(Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(leftChild)) == Ctlsp_TRUE_c){
2973          return Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(
2974            Ctlsp_FormulaReadLeftChild(rightChild)) &&
2975            Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(
2976              Ctlsp_FormulaReadRightChild(rightChild));
2977        }
2978      }
2979    }
2980  }
2981  switch (Ctlsp_FormulaReadType(formula)) {
2982  case Ctlsp_TRUE_c:
2983  case Ctlsp_FALSE_c:
2984  case Ctlsp_ID_c:
2985    return TRUE;
2986  case Ctlsp_AND_c:
2987  case Ctlsp_OR_c:
2988  case Ctlsp_U_c:
2989    leftChild = Ctlsp_FormulaReadLeftChild(formula);
2990    if (Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(leftChild)) {
2991      rightChild = Ctlsp_FormulaReadRightChild(formula);
2992      return Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(rightChild);
2993    } else {
2994      return FALSE;
2995    }
2996  case Ctlsp_NOT_c:
2997    leftChild = Ctlsp_FormulaReadLeftChild(formula);
2998    /* The formula is in negation normal form. */
2999    assert(Ctlsp_FormulaReadType(leftChild) == Ctlsp_ID_c);
3000    return TRUE;
3001  case Ctlsp_X_c:
3002    leftChild = Ctlsp_FormulaReadLeftChild(formula);
3003    return Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(leftChild);
3004  case Ctlsp_R_c:
3005    return FALSE;
3006  default:
3007    fail("unexpected node type in abbreviation-free formula\n");
3008    return FALSE; /* not reached */
3009  }
3010} /* Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe */
3011
3012/**Function********************************************************************
3013
3014  Synopsis [Tests if each formula in an array of LTL formulae is
3015  propositional]
3016
3017  Description [This function tests each LTL formula in negation normal
3018  form to see if it is a propositional formula.  Return TRUE if all formulae
3019  are propositional formulae.]
3020
3021  SideEffects [none]
3022
3023  SeeAlso     [Ctlsp_LtlFormulaIsPropositional]
3024
3025******************************************************************************/
3026int
3027Ctlsp_LtlFormulaArrayIsPropositional(
3028  array_t * formulaArray)
3029{
3030  int             i;
3031  Ctlsp_Formula_t *formula;
3032
3033  for (i = 0; i < array_n(formulaArray); i++) {
3034    formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i);
3035    if(!Ctlsp_isPropositionalFormula(formula)){
3036      /*if(Ctlsp_LtlFormulaIsPropositional(formula) == 0){*/
3037      return 0;
3038    }
3039  }
3040  return 1;
3041
3042} /* Ctlsp_LtlFormulaArrayIsPropositional */
3043
3044
3045/**Function********************************************************************
3046
3047  Synopsis    [Return T iff formula is a "propositional formula".]
3048
3049  Description [This function tests an LTL formula in negation normal
3050  form to see if it is a propositional formula.  A propositional
3051  formula contains only Boolean connectives, TRUE, FALSE, and
3052  literals.  A literal is an atomic proposition or the negation of an
3053  atomic popposition.]
3054
3055  SideEffects [none]
3056
3057  SeeAlso     [Ctlsp_LtlFormulaIsAtomicPropositional]
3058
3059******************************************************************************/
3060int
3061Ctlsp_LtlFormulaIsPropositional(
3062  Ctlsp_Formula_t *F)
3063{
3064  int result;
3065
3066  assert(F !=  NIL(Ctlsp_Formula_t));
3067
3068  switch (F->type) {
3069  case Ctlsp_TRUE_c:
3070  case Ctlsp_FALSE_c:
3071  case Ctlsp_ID_c:
3072    result = 1;
3073    break;
3074  case Ctlsp_NOT_c: /* negation only appears ahead of AP */
3075    if (F->left->type == Ctlsp_ID_c)
3076      result = 1;
3077    else
3078      result = 0;
3079    break;
3080  case Ctlsp_AND_c:
3081  case Ctlsp_OR_c:
3082    result = (Ctlsp_LtlFormulaIsPropositional(F->left) &&
3083              Ctlsp_LtlFormulaIsPropositional(F->right));
3084    break;
3085  default:
3086    result = 0;
3087  }
3088
3089  return result;
3090} /* Ctlsp_LtlFormulaIsPropositional() */
3091
3092/**Function********************************************************************
3093
3094  Synopsis    [Return T iff formula is an "atomic propositional formula".]
3095
3096  Description [TRUE/FALSE/literal.  literal: an atomic proposition or the
3097  negation of an atomic popposition.]
3098
3099  SideEffects [none]
3100
3101  SeeAlso     [Ctlsp_LtlFormulaIsPropositional]
3102
3103******************************************************************************/
3104int
3105Ctlsp_LtlFormulaIsAtomicPropositional(
3106  Ctlsp_Formula_t *F)
3107{
3108  int result;
3109
3110  assert(F != 0);
3111
3112  switch (F->type) {
3113  case Ctlsp_TRUE_c:
3114  case Ctlsp_FALSE_c:
3115  case Ctlsp_ID_c:
3116    result = 1;
3117    break;
3118  case Ctlsp_NOT_c: /* negation only appears ahead of AP */
3119    if (F->left->type == Ctlsp_ID_c)
3120      result = 1;
3121    else
3122      result = 0;
3123    break;
3124  default:
3125    result = 0;
3126  }
3127
3128  return result;
3129}
3130
3131/**Function********************************************************************
3132
3133  Synopsis    [Return T iff formula is a "FG formula".]
3134
3135  Description [TRUE U (FALSE R p).]
3136
3137  SideEffects []
3138
3139  SeeAlso     [Ctlsp_LtlFormulaIsGF, Ctlsp_LtlFormulaIsFGorGF]
3140
3141******************************************************************************/
3142int
3143Ctlsp_LtlFormulaIsFG(
3144  Ctlsp_Formula_t *F)
3145{
3146  int result = 0;
3147
3148  if (F->type == Ctlsp_U_c) {
3149    if (F->left->type == Ctlsp_TRUE_c && F->right->type == Ctlsp_R_c) {
3150      result = (F->right->left->type == Ctlsp_FALSE_c);
3151    }
3152  }
3153
3154  return result;
3155}
3156
3157
3158/**Function********************************************************************
3159
3160  Synopsis    [Return T iff formula is a "GF formula".]
3161
3162  Description [FALSE R (TRUE U p).]
3163
3164  SideEffects []
3165
3166  SeeAlso     [Ctlsp_LtlFormulaIsFG, Ctlsp_LtlFormulaIsFGorGF]
3167
3168******************************************************************************/
3169int
3170Ctlsp_LtlFormulaIsGF(
3171  Ctlsp_Formula_t *F)
3172{
3173  int result = 0;
3174
3175  if (F->type == Ctlsp_R_c) {
3176      if (F->left->type == Ctlsp_FALSE_c && F->right->type == Ctlsp_U_c) {
3177          result = (F->right->left->type == Ctlsp_TRUE_c);
3178      }
3179  }
3180
3181  return result;
3182}
3183
3184/**Function********************************************************************
3185
3186  Synopsis    [Return T iff formula is a "FG or GF formula".]
3187
3188  Description [TRUE U (FALSE R p).]
3189
3190  SideEffects []
3191
3192  SeeAlso     [Ctlsp_LtlFormulaIsGF, Ctlsp_LtlFormulaIsFG]
3193
3194******************************************************************************/
3195int
3196Ctlsp_LtlFormulaIsFGorGF(
3197  Ctlsp_Formula_t *F)
3198{
3199  return (Ctlsp_LtlFormulaIsFG(F) || Ctlsp_LtlFormulaIsGF(F));
3200}
3201
3202
3203/**Function********************************************************************
3204
3205  Synopsis    [Return T iff (form -> to).]
3206
3207  Description [Since determine '->' is hard, we only consider easy case which
3208  can be determined syntatically.
3209
3210  Notice that, before calling this function, 'from' and 'to' are hashed into
3211  the same UniqueTable (This helps in identifying "from==to").]
3212
3213  SideEffects []
3214
3215  SeeAlso     []
3216
3217******************************************************************************/
3218int
3219Ctlsp_LtlFormulaSimplyImply(
3220  Ctlsp_Formula_t *from,
3221  Ctlsp_Formula_t *to)
3222{
3223
3224#if 0
3225  fprintf(vis_stdout, "\n------------------------\n");
3226  Ctlsp_FormulaPrint(vis_stdout, from);
3227  fprintf(vis_stdout, "\n   ==>\n");
3228  Ctlsp_FormulaPrint(vis_stdout, to);
3229  fprintf(vis_stdout, "\n------------------------\n");
3230#endif
3231
3232  /* from -> from   :  1 */
3233  if (from == to)
3234    return 1;
3235
3236  /* from -> TRUE   :  1 */
3237  if (to->type == Ctlsp_TRUE_c)
3238    return 1;
3239
3240  /* FALSE -> to    :  1 */
3241  if (from->type == Ctlsp_FALSE_c)
3242    return 1;
3243
3244
3245  if (to->type == Ctlsp_U_c) {
3246    /* from -> tL U tR: (from->tR)? */
3247    if (Ctlsp_LtlFormulaSimplyImply(from, to->right))
3248      return 1;
3249
3250    /* (fL U fR) -> (tl U tR) : (fL->tL)? && (fR->tR)? */
3251    if (from->type == Ctlsp_U_c)
3252      return (Ctlsp_LtlFormulaSimplyImply(from->left, to->left) &&
3253              Ctlsp_LtlFormulaSimplyImply(from->right, to->right));
3254  }
3255
3256  if (to->type == Ctlsp_R_c) {
3257    /* from -> tL R tR: (from->tL)? && (from->tR)? */
3258    if (Ctlsp_LtlFormulaSimplyImply(from, to->left) &&
3259        Ctlsp_LtlFormulaSimplyImply(from, to->right))
3260      return 1;
3261
3262    /* (fL R fR) -> (tL R tR) : (fL->tL)? && (fR->tR)? */
3263    if (from->type == Ctlsp_R_c)
3264      return (Ctlsp_LtlFormulaSimplyImply(from->left, to->left) &&
3265              Ctlsp_LtlFormulaSimplyImply(from->right, to->right));
3266  }
3267
3268  /* (fL U fR) -> to :: (fL->to)? && (fR->to)? */
3269  if (from->type == Ctlsp_U_c) {
3270    if (Ctlsp_LtlFormulaSimplyImply(from->left, to) &&
3271        Ctlsp_LtlFormulaSimplyImply(from->right,to) )
3272      return 1;
3273  }
3274
3275  /* (fL R fR) -> to :: (fR->to)? */
3276  if (from->type == Ctlsp_R_c) {
3277    if (Ctlsp_LtlFormulaSimplyImply(from->right,to))
3278      return 1;
3279  }
3280
3281  /*************************************************************************
3282   * (1) If we unwinding every propositional formula, sometimes it will
3283   * become really hard. This is due to the feature of the CTL* parser.
3284   * For example, "state[1024]=0" would be parsed into 1024 subformulae
3285   *
3286   * (2) Without unwinding, some possible simplification cases can not be
3287   * detected. For example, "p + !p", "p * !p" (while p and the left
3288   * subformula in !p are syntatically different.
3289   ************************************************************************/
3290  if (!Ctlsp_LtlFormulaIsPropositional(to)) {
3291
3292    /* form -> tL*tR  : (from->tL)? && (from->rR)? */
3293    if (to->type == Ctlsp_AND_c)
3294      return (Ctlsp_LtlFormulaSimplyImply(from, to->left) &&
3295              Ctlsp_LtlFormulaSimplyImply(from, to->right));
3296
3297    /* from -> tL+tR  : (from->tL)? || (from->rR)? */
3298    if (to->type == Ctlsp_OR_c)
3299      return (Ctlsp_LtlFormulaSimplyImply(from, to->left) ||
3300              Ctlsp_LtlFormulaSimplyImply(from, to->right) );
3301  }
3302
3303  if (!Ctlsp_LtlFormulaIsPropositional(from)) {
3304
3305    /* (fL * fR) -> to :: (fL->to)? || (fR->to)? */
3306    if (from->type == Ctlsp_AND_c)
3307      return (Ctlsp_LtlFormulaSimplyImply(from->left, to) ||
3308              Ctlsp_LtlFormulaSimplyImply(from->right,to) );
3309
3310
3311    /* (fL + fR) -> to :: (fL->to)? && (fR->to)? */
3312    if (from->type == Ctlsp_OR_c)
3313      return (Ctlsp_LtlFormulaSimplyImply(from->left, to) &&
3314              Ctlsp_LtlFormulaSimplyImply(from->right,to) );
3315  }
3316
3317  return 0;
3318}
3319
3320
3321/**Function********************************************************************
3322
3323  Synopsis    [Translate LTL formula into Separated Normal Form (SNF)]
3324
3325  Description [Translate LTL formula into Separated Normal Form (SNF).
3326  Each LTL formula is translated into a set of rules in the form (p
3327  --> f(q)), where p and q are propositional and f(q) contains at most
3328  one temporal operator which is either X or F.]
3329
3330  SideEffects []
3331
3332  SeeAlso     [Ctlsp_LtlTranslateIntoSNFRecursive]
3333
3334******************************************************************************/
3335array_t *
3336Ctlsp_LtlTranslateIntoSNF(
3337  Ctlsp_Formula_t *formula)
3338{
3339  Ctlsp_Formula_t *leftNode;
3340  int             index, i;
3341  array_t         *formulaArray = array_alloc(Ctlsp_Formula_t *, 0);
3342
3343  /*
3344    rule#1: an LTL formula must hold at an initial state.
3345   */
3346
3347  leftNode  = Ctlsp_FormulaCreate(Ctlsp_ID_c, (void *)util_strsav(" SNFstart"), (void *)util_strsav("1"));
3348  /*
3349    rightNode = Ctlsp_FormulaCreate(Ctlsp_ID_c, (void *)util_strsav("SNFx_0"),   (void *)util_strsav("1"));
3350    newNode = Ctlsp_FormulaCreate(Ctlsp_THEN_c, leftNode, rightNode);
3351  */
3352
3353  index = 0;
3354  Ctlsp_LtlTranslateIntoSNFRecursive(leftNode, formula, formulaArray, &index);
3355
3356  fprintf(vis_stdout, "The SNF rules are:\n");
3357  for (i = 0; i < array_n(formulaArray); i++) {
3358    Ctlsp_Formula_t *ltlFormula     = array_fetch(Ctlsp_Formula_t *, formulaArray, i);
3359
3360    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
3361    fprintf(vis_stdout, "\n");
3362  }
3363
3364  return formulaArray;
3365}
3366
3367/**Function********************************************************************
3368
3369  Synopsis    [Trnalate LTL formula into Separated Normal Form (SNF)]
3370
3371  Description [Recursively trnaslate LTL formula into SNF
3372
3373  Assume the formula is abbreviation-free NNF, and there are only the
3374  following types of formulae before translation: TRUE FALSE ID AND OR
3375  U R X !  .]
3376
3377  SideEffects []
3378
3379  SeeAlso     []
3380
3381******************************************************************************/
3382void
3383Ctlsp_LtlTranslateIntoSNFRecursive(
3384  Ctlsp_Formula_t *propNode,
3385  Ctlsp_Formula_t *formula,
3386  array_t         *formulaArray,
3387  int             *index)
3388{
3389
3390  Ctlsp_Formula_t *leftNode, *rightNode, *newNode, *result;
3391
3392  if(formula == NIL(Ctlsp_Formula_t)){
3393    return;
3394  }
3395  if(Ctlsp_LtlFormulaIsPropositional(formula)){
3396    newNode = CtlspFunctionThen(propNode, formula);
3397    CtlspFormulaIncrementRefCount(newNode);
3398    array_insert_last(Ctlsp_Formula_t *, formulaArray, newNode);
3399    return;
3400  }
3401  switch (Ctlsp_FormulaReadType(formula)) {
3402  case Ctlsp_AND_c:
3403    leftNode  = Ctlsp_FormulaReadLeftChild(formula);
3404    rightNode = Ctlsp_FormulaReadRightChild(formula);
3405
3406    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, leftNode, formulaArray, index);
3407    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, rightNode, formulaArray, index);
3408
3409    break;
3410  case Ctlsp_OR_c:
3411    leftNode  = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index);
3412    rightNode = createSNFnode(Ctlsp_FormulaReadRightChild(formula), formulaArray, index);
3413    newNode   = CtlspFunctionOr(leftNode, rightNode);
3414    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, newNode, formulaArray, index);
3415
3416    break;
3417  case Ctlsp_THEN_c:
3418    leftNode  = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index);
3419    rightNode = createSNFnode(Ctlsp_FormulaReadRightChild(formula), formulaArray, index);
3420    newNode   = CtlspFunctionOr(
3421      Ctlsp_FormulaCreate(Ctlsp_NOT_c, leftNode, NIL(Ctlsp_Formula_t))
3422      , rightNode);
3423    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, newNode, formulaArray, index);
3424    break;
3425  case Ctlsp_NOT_c:
3426    if (!Ctlsp_isPropositionalFormula(formula)){
3427      fprintf(vis_stderr,"SNF error: the LTL formula is not in NNF\n");
3428    }
3429    break;
3430  case Ctlsp_X_c:
3431    /*
3432      propNode -> X leftNode
3433     */
3434    leftNode = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index);
3435
3436    newNode = Ctlsp_FormulaCreate(Ctlsp_X_c, leftNode, NIL(Ctlsp_Formula_t));
3437    newNode = CtlspFunctionThen(propNode, newNode);
3438     CtlspFormulaIncrementRefCount(newNode);
3439    array_insert_last(Ctlsp_Formula_t *, formulaArray, newNode);
3440
3441    break;
3442  case Ctlsp_F_c:
3443    /*
3444      propNode -> F leftNode
3445     */
3446    leftNode = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index);
3447
3448    newNode  = Ctlsp_FormulaCreate(Ctlsp_F_c, leftNode, NIL(Ctlsp_Formula_t));
3449    newNode  = CtlspFunctionThen(propNode, newNode);
3450     CtlspFormulaIncrementRefCount(newNode);
3451    array_insert_last(Ctlsp_Formula_t *, formulaArray, newNode);
3452
3453    break;
3454  case Ctlsp_G_c:
3455    /*
3456      propNode -> G leftNode
3457    */
3458    leftNode = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index);
3459
3460    newNode  = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strcat3(" SNFx","_", util_inttostr((*index)++)),
3461                                   (void *)util_strsav("1"));
3462
3463    result  = CtlspFunctionAnd(leftNode, newNode);
3464    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, result, formulaArray, index);
3465    result   = Ctlsp_FormulaCreate(Ctlsp_X_c, result, NIL(Ctlsp_Formula_t));
3466    Ctlsp_LtlTranslateIntoSNFRecursive(newNode, result, formulaArray, index);
3467
3468    break;
3469  case Ctlsp_U_c:
3470    /*
3471      x --> a U b = x --> b + a*y
3472                    y --> X(b + a*y)
3473                    x --> F(b)
3474    */
3475    newNode = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strcat3(" SNFx","_", util_inttostr((*index)++)),
3476                                  (void *)util_strsav("1"));
3477
3478    leftNode  = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index);
3479    rightNode = createSNFnode(Ctlsp_FormulaReadRightChild(formula), formulaArray, index);
3480
3481    result  = CtlspFunctionAnd(leftNode, newNode);
3482    result  = CtlspFunctionOr(rightNode, result);
3483
3484    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, result, formulaArray, index);
3485
3486    result   = Ctlsp_FormulaCreate(Ctlsp_X_c, result, NIL(Ctlsp_Formula_t));
3487    Ctlsp_LtlTranslateIntoSNFRecursive(newNode, result, formulaArray, index);
3488
3489    result   = Ctlsp_FormulaCreate(Ctlsp_F_c, rightNode, NIL(Ctlsp_Formula_t));
3490    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, result, formulaArray, index);
3491    break;
3492  case Ctlsp_W_c:
3493    /*
3494      x --> a W b = x --> b + a*y
3495                    y --> X(b + a*y)
3496    */
3497    newNode = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strcat3(" SNFx","_", util_inttostr((*index)++)),
3498                                  (void *)util_strsav("1"));
3499
3500    leftNode  = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index);
3501    rightNode = createSNFnode(Ctlsp_FormulaReadRightChild(formula), formulaArray, index);
3502
3503    result  = CtlspFunctionAnd(leftNode, newNode);
3504    result  = CtlspFunctionOr(rightNode, result);
3505
3506    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, result, formulaArray, index);
3507
3508    result   = Ctlsp_FormulaCreate(Ctlsp_X_c, result, NIL(Ctlsp_Formula_t));
3509    Ctlsp_LtlTranslateIntoSNFRecursive(newNode, result, formulaArray, index);
3510    break;
3511  case Ctlsp_R_c:
3512    /*
3513      x --> left R right = x --> left*right + right*y
3514                           y --> X(left*rigt* + right*y)
3515     */
3516    newNode = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strcat3(" SNFx","_", util_inttostr((*index)++)),
3517                                  (void *)util_strsav("1"));
3518    leftNode  = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index);
3519    rightNode = createSNFnode(Ctlsp_FormulaReadRightChild(formula), formulaArray, index);
3520
3521    leftNode  = CtlspFunctionAnd(leftNode, rightNode);
3522
3523    result = CtlspFunctionAnd(rightNode, newNode);
3524    result = CtlspFunctionOr(leftNode, result);
3525
3526    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, result, formulaArray, index);
3527
3528    result = Ctlsp_FormulaCreate(Ctlsp_X_c, result, NIL(Ctlsp_Formula_t));
3529    Ctlsp_LtlTranslateIntoSNFRecursive(newNode, result, formulaArray, index);
3530
3531    break;
3532  default:
3533    fail("unexpected node type in abbreviation-free formula\n");
3534    return; /* not reached */
3535  }
3536}
3537
3538
3539/**Function********************************************************************
3540
3541  Synopsis    [Perform simple rewriting of a formula.]
3542
3543  Description [We return a formula which shares nothing with the input formula]
3544
3545  SideEffects []
3546
3547  SeeAlso     []
3548
3549******************************************************************************/
3550Ctlsp_Formula_t *
3551Ctlsp_LtlFormulaSimpleRewriting(
3552  Ctlsp_Formula_t *formula)
3553{
3554  Ctlsp_Formula_t *F, *newF;
3555  st_table *Utable = st_init_table(FormulaCompare, FormulaHash);
3556  st_generator *stGen;
3557  char *key;
3558
3559  /* copy the input formula (so that they share nothing) */
3560  F = Ctlsp_LtlFormulaNegationNormalForm(formula);
3561
3562  /* hash into the 'Utable' */
3563  F = Ctlsp_LtlFormulaHashIntoUniqueTable(F, Utable);
3564
3565  /* simple rewriting */
3566  F = CtlspLtlFormulaSimpleRewriting_Aux(F, Utable);
3567
3568  /* copy F into 'newF' (they shares nothing) */
3569  newF = Ctlsp_LtlFormulaNegationNormalForm(F);
3570
3571  /* free formulae in st_table */
3572  st_foreach_item(Utable, stGen, &key, &F) {
3573    if (F->type == Ctlsp_ID_c) {
3574      FREE(F->left);
3575      FREE(F->right);
3576    }
3577    FREE(F);
3578  }
3579  st_free_table(Utable);
3580
3581  return (newF);
3582}
3583
3584
3585/*---------------------------------------------------------------------------*/
3586/* Definition of internal functions                                          */
3587/*---------------------------------------------------------------------------*/
3588
3589
3590/**Function********************************************************************
3591
3592  Synopsis    [Rewriting the LTL formula recursively.]
3593
3594  Description [Recursive call, used in Ctlsp_LtlFormulaSimpleRewriting() only.]
3595
3596  SideEffects [The given formula F might be freed (hence unrecoverable)]
3597
3598  SeeAlso     [Ctlsp_LtlFormulaSimpleRewriting]
3599
3600******************************************************************************/
3601Ctlsp_Formula_t *
3602CtlspLtlFormulaSimpleRewriting_Aux(
3603  Ctlsp_Formula_t *F,
3604  st_table *Utable)
3605{
3606  Ctlsp_Formula_t *left, *right;
3607  Ctlsp_Formula_t *tmpf1, *tmpf2;
3608  Ctlsp_Formula_t *True, *False;
3609
3610  if (F == NIL(Ctlsp_Formula_t))
3611    return F;
3612
3613  if (F->type == Ctlsp_ID_c || F->type == Ctlsp_TRUE_c ||
3614      F->type == Ctlsp_FALSE_c) {
3615    F = Ctlsp_LtlFormulaHashIntoUniqueTable(F, Utable);
3616    return F;
3617  }
3618
3619#if 0
3620  fprintf(vis_stdout, "\nRewriting ...\n");
3621  Ctlsp_FormulaPrint(vis_stdout, F);
3622  fprintf(vis_stdout, "\n");
3623#endif
3624
3625  /* First of all, rewrite F->left, F->right */
3626  left = CtlspLtlFormulaSimpleRewriting_Aux(F->left, Utable);
3627#if 0
3628  fprintf(vis_stdout, "\n... Rewriting(left)\n");
3629  Ctlsp_FormulaPrint(vis_stdout, left);
3630  fprintf(vis_stdout, "\n");
3631#endif
3632
3633  right = CtlspLtlFormulaSimpleRewriting_Aux(F->right, Utable);
3634#if 0
3635  fprintf(vis_stdout, "\n... Rewriting(right)\n");
3636  Ctlsp_FormulaPrint(vis_stdout, right);
3637  fprintf(vis_stdout, "\n");
3638#endif
3639
3640  /* in case we want to use TRUE/FALSE */
3641  True = Ctlsp_LtlFormulaHashIntoUniqueTable(FormulaCreateWithType(Ctlsp_TRUE_c), Utable);
3642  False = Ctlsp_LtlFormulaHashIntoUniqueTable(FormulaCreateWithType(Ctlsp_FALSE_c), Utable);
3643
3644  switch (F->type) {
3645  case Ctlsp_AND_c:
3646
3647    /* r -> l :  l*r == r */
3648    if (Ctlsp_LtlFormulaSimplyImply(right, left))
3649      return right;
3650
3651    /* l -> r, l*r == l */
3652    if (Ctlsp_LtlFormulaSimplyImply(left, right))
3653      return left;
3654
3655    /* r -> !l, l*r == FALSE*/
3656    tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
3657    tmpf1->left = left;
3658    tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
3659    FREE(tmpf1);
3660    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3661    if (Ctlsp_LtlFormulaSimplyImply(right, tmpf2))
3662      return False;
3663
3664    /* l -> !r, l*r == FALSE*/
3665    tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
3666    tmpf1->left = right;
3667    tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
3668    FREE(tmpf1);
3669    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3670    if (Ctlsp_LtlFormulaSimplyImply(left, tmpf2))
3671      return False;
3672
3673    /* (ll R lr) * (ll R rr) == (ll) R (lr*rr) */
3674    if (left->type == Ctlsp_R_c && right->type == Ctlsp_R_c) {
3675      if (left->left == right->left) {
3676        tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
3677        tmpf1->left = left->right;
3678        tmpf1->right = right->right;
3679        CtlspFormulaIncrementRefCount(left->right);
3680        CtlspFormulaIncrementRefCount(right->right);
3681        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
3682
3683        tmpf2 = FormulaCreateWithType(Ctlsp_R_c);
3684        tmpf2->left = left->left;
3685        tmpf2->right = tmpf1;
3686        CtlspFormulaIncrementRefCount(left->left);
3687        CtlspFormulaIncrementRefCount(tmpf1);
3688        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3689        return tmpf2;
3690      }
3691    }
3692
3693    /* (ll U lr) * (rl U lr) == (ll * rl) U (lr) */
3694    if (left->type == Ctlsp_U_c && right->type == Ctlsp_U_c) {
3695      if (left->right == right->right) {
3696        tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
3697        tmpf1->left = left->left;
3698        tmpf1->right = right->left;
3699        CtlspFormulaIncrementRefCount(left->left);
3700        CtlspFormulaIncrementRefCount(right->left);
3701        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
3702
3703        tmpf2 = FormulaCreateWithType(Ctlsp_U_c);
3704        tmpf2->left = tmpf1;
3705        tmpf2->right = left->right;
3706        CtlspFormulaIncrementRefCount(tmpf1);
3707        CtlspFormulaIncrementRefCount(left->right);
3708        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3709        return tmpf2;
3710      }
3711    }
3712
3713    /* (X ll)*(X rl) == X (ll*rl) */
3714    if (left->type == Ctlsp_X_c && right->type == Ctlsp_X_c) {
3715      tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
3716      tmpf1->left = left->left;
3717      tmpf1->right = right->left;
3718      CtlspFormulaIncrementRefCount(left->left);
3719      CtlspFormulaIncrementRefCount(right->left);
3720      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
3721
3722      tmpf2 = FormulaCreateWithType(Ctlsp_X_c);
3723      tmpf2->left = tmpf1;
3724      CtlspFormulaIncrementRefCount(tmpf1);
3725      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3726      return tmpf2;
3727    }
3728
3729    /* (ll R lr) * (rl U ll)   ==  ( (X lr * rl) U ll) * lr */
3730    if (left->type == Ctlsp_R_c && right->type == Ctlsp_U_c) {
3731      if (left->left == right->right) {
3732        tmpf1 = FormulaCreateWithType(Ctlsp_X_c);
3733        tmpf1->left = left->right;
3734        CtlspFormulaIncrementRefCount(left->right);
3735        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
3736
3737        if (right->left->type != Ctlsp_TRUE_c) {
3738          tmpf2 = FormulaCreateWithType(Ctlsp_AND_c);
3739          tmpf2->left = tmpf1;
3740          tmpf2->right = right->left;
3741          CtlspFormulaIncrementRefCount(tmpf1);
3742          CtlspFormulaIncrementRefCount(right->left);
3743          tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3744        }
3745
3746        tmpf2 = FormulaCreateWithType(Ctlsp_U_c);
3747        tmpf2->left = tmpf1;
3748        tmpf2->right = left->left;
3749        CtlspFormulaIncrementRefCount(tmpf1);
3750        CtlspFormulaIncrementRefCount(left->left);
3751        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3752
3753        tmpf2 = FormulaCreateWithType(Ctlsp_AND_c);
3754        tmpf2->left = tmpf1;
3755        tmpf2->right = left->right;
3756        CtlspFormulaIncrementRefCount(tmpf1);
3757        CtlspFormulaIncrementRefCount(left->right);
3758        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3759
3760        return tmpf2;
3761      }
3762    }
3763    /* (ll U lr) * (lr R rr)   ==  ( (X rr * ll) U rl) * rr */
3764    if (left->type == Ctlsp_U_c && right->type == Ctlsp_R_c) {
3765      if (left->right == right->left) {
3766        tmpf1 = FormulaCreateWithType(Ctlsp_X_c);
3767        tmpf1->left = right->right;
3768        CtlspFormulaIncrementRefCount(right->right);
3769        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
3770
3771        if (left->left->type != Ctlsp_TRUE_c) {
3772          tmpf2 = FormulaCreateWithType(Ctlsp_AND_c);
3773          tmpf2->left = tmpf1;
3774          tmpf2->right = left->left;
3775          CtlspFormulaIncrementRefCount(tmpf1);
3776          CtlspFormulaIncrementRefCount(left->left);
3777          tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3778        }
3779
3780        tmpf2 = FormulaCreateWithType(Ctlsp_U_c);
3781        tmpf2->left = tmpf1;
3782        tmpf2->right = right->left;
3783        CtlspFormulaIncrementRefCount(tmpf1);
3784        CtlspFormulaIncrementRefCount(right->left);
3785        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3786
3787        tmpf2 = FormulaCreateWithType(Ctlsp_AND_c);
3788        tmpf2->left = tmpf1;
3789        tmpf2->right = right->right;
3790        CtlspFormulaIncrementRefCount(tmpf1);
3791        CtlspFormulaIncrementRefCount(right->right);
3792        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3793
3794        return tmpf2;
3795      }
3796    }
3797
3798    /* (ll R lr) * r, r=>ll  == lr *r */
3799    if (left->type == Ctlsp_R_c &&
3800        Ctlsp_LtlFormulaSimplyImply(right, left->left)) {
3801      tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
3802      tmpf1->left = left->right;
3803      tmpf1->right = right;
3804      CtlspFormulaIncrementRefCount(left->right);
3805      CtlspFormulaIncrementRefCount(right);
3806      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
3807      return tmpf2;
3808    }
3809    /* l *(rl R rr), l=>rl  == l * rr */
3810    if (right->type == Ctlsp_R_c &&
3811        Ctlsp_LtlFormulaSimplyImply(left, right->left)) {
3812      tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
3813      tmpf1->left = left;
3814      tmpf1->right = right->right;
3815      CtlspFormulaIncrementRefCount(left);
3816      CtlspFormulaIncrementRefCount(right->right);
3817      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
3818      return tmpf2;
3819    }
3820
3821    /* (ll U lr) * r, r=>!ll   == lr * r */
3822    if (left->type == Ctlsp_U_c) {
3823      tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
3824      tmpf1->left = left->left;
3825      tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
3826      FREE(tmpf1);
3827      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3828
3829      if (Ctlsp_LtlFormulaSimplyImply(right, tmpf1)) {
3830        tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
3831        tmpf1->left = left->right;
3832        tmpf1->right = right;
3833        CtlspFormulaIncrementRefCount(left->right);
3834        CtlspFormulaIncrementRefCount(right);
3835        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
3836        return tmpf2;
3837      }
3838    }
3839    /* l * (rl U rr), l=>!rl   == l * rr */
3840    if (right->type == Ctlsp_U_c) {
3841      tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
3842      tmpf1->left = right->left;
3843      tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
3844      FREE(tmpf1);
3845      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3846
3847      if (Ctlsp_LtlFormulaSimplyImply(left, tmpf1)) {
3848        tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
3849        tmpf1->left = left;
3850        tmpf1->right = right->right;
3851        CtlspFormulaIncrementRefCount(left);
3852        CtlspFormulaIncrementRefCount(right->right);
3853        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
3854        return tmpf2;
3855      }
3856    }
3857
3858    /* FG lrr * FG rrr = FG (lrr * rrr) */
3859    if (Ctlsp_LtlFormulaIsFG(left) && Ctlsp_LtlFormulaIsFG(right)) {
3860      tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
3861      tmpf1->left = left->right->right;
3862      tmpf1->right = right->right->right;
3863      CtlspFormulaIncrementRefCount(left->right->right);
3864      CtlspFormulaIncrementRefCount(right->right->right);
3865      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
3866
3867      tmpf2 = FormulaCreateWithType(Ctlsp_R_c);
3868      tmpf2->left = False;
3869      tmpf2->right = tmpf1;
3870      CtlspFormulaIncrementRefCount(False);
3871      CtlspFormulaIncrementRefCount(tmpf1);
3872      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3873
3874      tmpf2 = FormulaCreateWithType(Ctlsp_U_c);
3875      tmpf2->left = True;
3876      tmpf2->right = tmpf1;
3877      CtlspFormulaIncrementRefCount(True);
3878      CtlspFormulaIncrementRefCount(tmpf1);
3879      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3880      return tmpf2;
3881    }
3882
3883    /* return  (l * r) */
3884    tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
3885    tmpf1->left = left;
3886    tmpf1->right = right;
3887    CtlspFormulaIncrementRefCount(left);
3888    CtlspFormulaIncrementRefCount(right);
3889    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
3890    return tmpf2;
3891
3892  case Ctlsp_OR_c:
3893
3894    /* r -> l, l+r == l */
3895    if (Ctlsp_LtlFormulaSimplyImply(right, left))
3896      return left;
3897
3898    /* l -> r, l+r == r */
3899    if (Ctlsp_LtlFormulaSimplyImply(left, right))
3900      return right;
3901
3902    /* !r -> l, l+r == TRUE*/
3903    tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
3904    tmpf1->left = right;
3905    tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
3906    FREE(tmpf1);
3907    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3908    if (Ctlsp_LtlFormulaSimplyImply(tmpf2, left))
3909      return True;
3910
3911    /* !l -> r, l+r == TRUE*/
3912    tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
3913    tmpf1->left = left;
3914    tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
3915    FREE(tmpf1);
3916    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3917    if (Ctlsp_LtlFormulaSimplyImply(tmpf2, right))
3918      return True;
3919
3920    /* (ll U lr) + (ll U rr) == (ll) U (lr+rr) */
3921    if (left->type == Ctlsp_U_c && right->type == Ctlsp_U_c) {
3922      if (left->left == right->left) {
3923        tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
3924        tmpf1->left = left->right;
3925        tmpf1->right = right->right;
3926        CtlspFormulaIncrementRefCount(left->right);
3927        CtlspFormulaIncrementRefCount(right->right);
3928        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
3929
3930        tmpf2 = FormulaCreateWithType(Ctlsp_U_c);
3931        tmpf2->left = left->left;
3932        tmpf2->right = tmpf1;
3933        CtlspFormulaIncrementRefCount(left->left);
3934        CtlspFormulaIncrementRefCount(tmpf1);
3935        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3936        return tmpf2;
3937      }
3938    }
3939
3940    /* (ll R lr) + (rl R lr) == (ll+rl) R (lr) */
3941    if (left->type == Ctlsp_R_c && right->type == Ctlsp_R_c) {
3942      if (left->right == right->right) {
3943        tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
3944        tmpf1->left = left->left;
3945        tmpf1->right = right->left;
3946        CtlspFormulaIncrementRefCount(left->left);
3947        CtlspFormulaIncrementRefCount(right->left);
3948        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
3949
3950        tmpf2 = FormulaCreateWithType(Ctlsp_R_c);
3951        tmpf2->left = tmpf1;
3952        tmpf2->right = left->right;
3953        CtlspFormulaIncrementRefCount(tmpf1);
3954        CtlspFormulaIncrementRefCount(left->right);
3955        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3956        return tmpf2;
3957      }
3958    }
3959
3960    /* (X ll) + (X rl) == X (ll+rl) */
3961    if (left->type == Ctlsp_X_c && right->type == Ctlsp_X_c) {
3962      tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
3963      tmpf1->left = left->left;
3964      tmpf1->right = right->left;
3965      CtlspFormulaIncrementRefCount(left->left);
3966      CtlspFormulaIncrementRefCount(right->left);
3967      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
3968
3969      tmpf2 = FormulaCreateWithType(Ctlsp_X_c);
3970      tmpf2->left = tmpf1;
3971      CtlspFormulaIncrementRefCount(tmpf1);
3972      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3973      return tmpf2;
3974    }
3975
3976    /* ll U lr  + rl R ll  == ((Xlr + rl) R ll) +lr */
3977    if (left->type == Ctlsp_U_c && right->type == Ctlsp_R_c) {
3978      if (left->left == right->right) {
3979        tmpf1 = FormulaCreateWithType(Ctlsp_X_c);
3980        tmpf1->left = left->right;
3981        CtlspFormulaIncrementRefCount(left->right);
3982        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
3983
3984        if (right->left->type != Ctlsp_FALSE_c) {
3985          tmpf2 = FormulaCreateWithType(Ctlsp_OR_c);
3986          tmpf2->left = tmpf1;
3987          tmpf2->right = right->left;
3988          CtlspFormulaIncrementRefCount(tmpf1);
3989          CtlspFormulaIncrementRefCount(right->left);
3990          tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3991        }
3992
3993        tmpf2 = FormulaCreateWithType(Ctlsp_R_c);
3994        tmpf2->left = tmpf1;
3995        tmpf2->right = left->left;
3996        CtlspFormulaIncrementRefCount(tmpf1);
3997        CtlspFormulaIncrementRefCount(left->left);
3998        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
3999
4000        tmpf2 = FormulaCreateWithType(Ctlsp_OR_c);
4001        tmpf2->left = tmpf1;
4002        tmpf2->right = left->right;
4003        CtlspFormulaIncrementRefCount(tmpf1);
4004        CtlspFormulaIncrementRefCount(left->right);
4005        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4006
4007        return tmpf2;
4008      }
4009    }
4010
4011    /* ll R lr  + lr U rr  == ((Xrr + ll) R lr) + rr */
4012    if (left->type == Ctlsp_R_c && right->type == Ctlsp_U_c) {
4013      if (left->right == right->left) {
4014        tmpf1 = FormulaCreateWithType(Ctlsp_X_c);
4015        tmpf1->left = right->right;
4016        CtlspFormulaIncrementRefCount(right->right);
4017        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4018
4019        if (left->left->type != Ctlsp_FALSE_c) {
4020          tmpf2 = FormulaCreateWithType(Ctlsp_OR_c);
4021          tmpf2->left = tmpf1;
4022          tmpf2->right = left->left;
4023          CtlspFormulaIncrementRefCount(tmpf1);
4024          CtlspFormulaIncrementRefCount(left->left);
4025          tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4026        }
4027
4028        tmpf2 = FormulaCreateWithType(Ctlsp_R_c);
4029        tmpf2->left = tmpf1;
4030        tmpf2->right = left->right;
4031        CtlspFormulaIncrementRefCount(tmpf1);
4032        CtlspFormulaIncrementRefCount(left->right);
4033        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4034
4035        tmpf2 = FormulaCreateWithType(Ctlsp_OR_c);
4036        tmpf2->left = tmpf1;
4037        tmpf2->right = right->right;
4038        CtlspFormulaIncrementRefCount(tmpf1);
4039        CtlspFormulaIncrementRefCount(right->right);
4040        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4041
4042        return tmpf2;
4043      }
4044    }
4045
4046    /* ll U lr + r , ll =>r  ==  lr + r ??? */
4047    if (left->type == Ctlsp_U_c) {
4048      if (Ctlsp_LtlFormulaSimplyImply(left->left, right)) {
4049        tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
4050        tmpf1->left = left->right;
4051        tmpf1->right = right;
4052        CtlspFormulaIncrementRefCount(left->right);
4053        CtlspFormulaIncrementRefCount(right);
4054        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4055        return tmpf2;
4056      }
4057    }
4058
4059    /* l + rl U rr ,  rl => l   ==  rr + l */
4060    if (right->type == Ctlsp_U_c) {
4061      if (Ctlsp_LtlFormulaSimplyImply(right->left, left)) {
4062        tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
4063        tmpf1->left = left;
4064        tmpf1->right = right->right;
4065        CtlspFormulaIncrementRefCount(left);
4066        CtlspFormulaIncrementRefCount(right->right);
4067        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4068        return tmpf2;
4069      }
4070    }
4071
4072    /* ll R lr + r ,  !ll => r   ==  lr + r */
4073    if (left->type == Ctlsp_R_c) {
4074      tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
4075      tmpf1->left = left->left;
4076      tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
4077      FREE(tmpf1);
4078      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4079      if (Ctlsp_LtlFormulaSimplyImply(tmpf2, right)) {
4080        tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
4081        tmpf1->left = left->right;
4082        tmpf1->right = right;
4083        CtlspFormulaIncrementRefCount(left->right);
4084        CtlspFormulaIncrementRefCount(right);
4085        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4086        return tmpf2;
4087      }
4088    }
4089
4090    /* l + rl R rr ,  !rl => l   ==  rr + l */
4091    if (right->type == Ctlsp_R_c) {
4092      tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
4093      tmpf1->left = right->left;
4094      tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
4095      FREE(tmpf1);
4096      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4097      if (Ctlsp_LtlFormulaSimplyImply(tmpf2, left)) {
4098        tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
4099        tmpf1->left = left;
4100        tmpf1->right = right->right;
4101        CtlspFormulaIncrementRefCount(left);
4102        CtlspFormulaIncrementRefCount(right->right);
4103        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4104        return tmpf2;
4105      }
4106    }
4107
4108    /* GF lrr + GF rrr = GF (lrr + rrr) */
4109    if (Ctlsp_LtlFormulaIsGF(left) && Ctlsp_LtlFormulaIsGF(right)) {
4110      tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
4111      tmpf1->left = left->right->right;
4112      tmpf1->right = right->right->right;
4113      CtlspFormulaIncrementRefCount(left->right->right);
4114      CtlspFormulaIncrementRefCount(right->right->right);
4115      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4116
4117      tmpf2 = FormulaCreateWithType(Ctlsp_U_c);
4118      tmpf2->left = True;
4119      tmpf2->right = tmpf1;
4120      CtlspFormulaIncrementRefCount(True);
4121      CtlspFormulaIncrementRefCount(tmpf1);
4122      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4123
4124      tmpf2 = FormulaCreateWithType(Ctlsp_R_c);
4125      tmpf2->left = False;
4126      tmpf2->right = tmpf1;
4127      CtlspFormulaIncrementRefCount(False);
4128      CtlspFormulaIncrementRefCount(tmpf1);
4129      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4130      return tmpf2;
4131    }
4132
4133    /* return  (l + r) */
4134    tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
4135    tmpf1->left = left;
4136    tmpf1->right = right;
4137    CtlspFormulaIncrementRefCount(left);
4138    CtlspFormulaIncrementRefCount(right);
4139    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4140    return tmpf2;
4141
4142  case Ctlsp_U_c:
4143
4144    /* l -> r : l U r == r */
4145    if (Ctlsp_LtlFormulaSimplyImply(left, right))
4146      return right;
4147
4148    /* l U FALSE = FALSE */
4149    if (right->type == Ctlsp_FALSE_c)
4150      return False;
4151
4152    /* (X ll) U (X rl) == X (ll U rl) */
4153    if (left->type == Ctlsp_X_c && right->type == Ctlsp_X_c) {
4154      tmpf1 = FormulaCreateWithType(Ctlsp_U_c);
4155      tmpf1->left = left->left;
4156      tmpf1->right = right->left;
4157      CtlspFormulaIncrementRefCount(left->left);
4158      CtlspFormulaIncrementRefCount(right->left);
4159      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4160
4161      tmpf2 = FormulaCreateWithType(Ctlsp_X_c);
4162      tmpf2->left = tmpf1;
4163      CtlspFormulaIncrementRefCount(tmpf1);
4164      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4165      return tmpf2;
4166    }
4167
4168    /* TRUE U (X rl) == X( TRUE U rl ) */
4169    if (left->type == Ctlsp_TRUE_c && right->type == Ctlsp_X_c) {
4170      tmpf1 = FormulaCreateWithType(Ctlsp_U_c);
4171      tmpf1->left = True;
4172      tmpf1->right = right->left;
4173      CtlspFormulaIncrementRefCount(True);
4174      CtlspFormulaIncrementRefCount(right->left);
4175      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4176
4177      tmpf2 = FormulaCreateWithType(Ctlsp_X_c);
4178      tmpf2->left = tmpf1;
4179      CtlspFormulaIncrementRefCount(tmpf1);
4180      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4181      return tmpf2;
4182    }
4183
4184    /* l->rl : l U (rl U rr) == rl U rr */
4185    if (right->type == Ctlsp_U_c) {
4186      if (Ctlsp_LtlFormulaSimplyImply(left, right->left)) {
4187        return right;
4188      }
4189    }
4190
4191    /* (TRUE or anything) U (FG rrr) == FG rrr */
4192    /* (TRUE or anything) U (GF rrr) == GF rrr */
4193    if (/*left->type == Ctlsp_TRUE_c &&*/ Ctlsp_LtlFormulaIsFGorGF(right))
4194      return right;
4195
4196    /* TRUE U (rl * FG rrrr) = F(rl) * FG(rrrr) */
4197    /* TRUE U (rl * GF rrrr) = F(rl) * GF(rrrr) */
4198    if (left->type == Ctlsp_TRUE_c && right->type == Ctlsp_AND_c) {
4199      if (Ctlsp_LtlFormulaIsFGorGF(right->right)) {
4200        tmpf1 = FormulaCreateWithType(Ctlsp_U_c);
4201        tmpf1->left = True;
4202        tmpf1->right = right->left;
4203        CtlspFormulaIncrementRefCount(True);
4204        CtlspFormulaIncrementRefCount(right->left);
4205        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4206
4207        tmpf2 = FormulaCreateWithType(Ctlsp_AND_c);
4208        tmpf2->left = tmpf1;
4209        tmpf2->right = right->right;
4210        CtlspFormulaIncrementRefCount(tmpf1);
4211        CtlspFormulaIncrementRefCount(right->right);
4212        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4213        return tmpf2;
4214      }
4215    }
4216
4217    /* TRUE U (FG rlrr * rr) == (FG rlrr) * F(rr) */
4218    /* TRUE U (GF rlrr * rr) == (GF rlrr) * F(rr) */
4219    if (left->type == Ctlsp_TRUE_c && right->type == Ctlsp_AND_c) {
4220      if (Ctlsp_LtlFormulaIsFGorGF(right->left)) {
4221        tmpf1 = FormulaCreateWithType(Ctlsp_U_c);
4222        tmpf1->left = True;
4223        tmpf1->right = right->right;
4224        CtlspFormulaIncrementRefCount(True);
4225        CtlspFormulaIncrementRefCount(right->right);
4226        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4227
4228        tmpf2 = FormulaCreateWithType(Ctlsp_AND_c);
4229        tmpf2->left = right->left;
4230        tmpf2->right = tmpf1;
4231        CtlspFormulaIncrementRefCount(right->left);
4232        CtlspFormulaIncrementRefCount(tmpf1);
4233        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4234        return tmpf2;
4235      }
4236    }
4237
4238    /* !r -> l : (l U r) == TRUE U r */
4239    tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
4240    tmpf1->left = right;
4241    tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
4242    FREE(tmpf1);
4243    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4244    if (Ctlsp_LtlFormulaSimplyImply(tmpf2, left)) {
4245      tmpf1 = FormulaCreateWithType(Ctlsp_U_c);
4246      tmpf1->left = True;
4247      tmpf1->right = right;
4248      CtlspFormulaIncrementRefCount(True);
4249      CtlspFormulaIncrementRefCount(right);
4250      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4251      return tmpf2;
4252    }
4253
4254    /* (ll + lr) U r,  ll => r   == (lr U r) */
4255    if (left->type == Ctlsp_OR_c) {
4256      if (Ctlsp_LtlFormulaSimplyImply(left->left, right)) {
4257        tmpf1 = FormulaCreateWithType(Ctlsp_U_c);
4258        tmpf1->left = left->right;
4259        tmpf1->right = right;
4260        CtlspFormulaIncrementRefCount(left->right);
4261        CtlspFormulaIncrementRefCount(right);
4262        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4263        return tmpf2;
4264      }
4265    }
4266
4267    /* (ll + lr) U r,  lr => r   == (ll U r) */
4268    if (left->type == Ctlsp_OR_c) {
4269      if (Ctlsp_LtlFormulaSimplyImply(left->right, right)) {
4270        tmpf1 = FormulaCreateWithType(Ctlsp_U_c);
4271        tmpf1->left = left->left;
4272        tmpf1->right = right;
4273        CtlspFormulaIncrementRefCount(left->left);
4274        CtlspFormulaIncrementRefCount(right);
4275        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4276        return tmpf2;
4277      }
4278    }
4279
4280
4281    /* return  (left U right) */
4282    tmpf1 = FormulaCreateWithType(Ctlsp_U_c);
4283    tmpf1->left = left;
4284    tmpf1->right = right;
4285    CtlspFormulaIncrementRefCount(left);
4286    CtlspFormulaIncrementRefCount(right);
4287    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4288    return tmpf2;
4289
4290  case Ctlsp_R_c:
4291
4292    /* r -> l : l R r == r */
4293    if (Ctlsp_LtlFormulaSimplyImply(right,left))
4294      return right;
4295
4296    /* l R TRUE == TRUE */
4297    if (right->type == Ctlsp_TRUE_c)
4298      return True;
4299
4300    /* (X ll) R (X rl) == X (ll R rl) */
4301    if (left->type == Ctlsp_X_c && right->type == Ctlsp_X_c) {
4302      tmpf1 = FormulaCreateWithType(Ctlsp_R_c);
4303      tmpf1->left = left->left;
4304      tmpf1->right = right->left;
4305      CtlspFormulaIncrementRefCount(left->left);
4306      CtlspFormulaIncrementRefCount(right->left);
4307      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4308
4309      tmpf2 = FormulaCreateWithType(Ctlsp_X_c);
4310      tmpf2->left = tmpf1;
4311      CtlspFormulaIncrementRefCount(tmpf1);
4312      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4313      return tmpf2;
4314    }
4315
4316    /* FALSE R (X rl) == X( FALSE R rl) */
4317    if (left->type == Ctlsp_TRUE_c && right->type == Ctlsp_X_c) {
4318      tmpf1 = FormulaCreateWithType(Ctlsp_R_c);
4319      tmpf1->left = False;
4320      tmpf1->right = right->left;
4321      CtlspFormulaIncrementRefCount(False);
4322      CtlspFormulaIncrementRefCount(right->left);
4323      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4324
4325      tmpf2 = FormulaCreateWithType(Ctlsp_X_c);
4326      tmpf2->left = tmpf1;
4327      CtlspFormulaIncrementRefCount(tmpf1);
4328      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4329      return tmpf2;
4330    }
4331
4332    /* rl->l :  l R (rl R rr) == (rl R rr) */
4333    if (right->type == Ctlsp_R_c)
4334      if (Ctlsp_LtlFormulaSimplyImply(right->left, left))
4335        return right;
4336
4337    /* (FALSE or anything) R (FG rrr) == FG rrr */
4338    /* (FALSE or anything) R (GF rrr) == GF rrr */
4339    if (/*left->type == Ctlsp_FALSE_c &&*/ Ctlsp_LtlFormulaIsFGorGF(right))
4340      return right;
4341
4342    /* FALSE R (rl + FG rrrr) = G(rl) + FG(rrrr) */
4343    /* FALSE R (rl + GF rrrr) = G(rl) + GF(rrrr) */
4344    if (left->type == Ctlsp_FALSE_c && right->type == Ctlsp_OR_c) {
4345      if (Ctlsp_LtlFormulaIsFGorGF(right->right)) {
4346        tmpf1 = FormulaCreateWithType(Ctlsp_R_c);
4347        tmpf1->left = False;
4348        tmpf1->right = right->left;
4349        CtlspFormulaIncrementRefCount(False);
4350        CtlspFormulaIncrementRefCount(right->left);
4351        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4352
4353        tmpf2 = FormulaCreateWithType(Ctlsp_OR_c);
4354        tmpf2->left = tmpf1;
4355        tmpf2->right = right->right;
4356        CtlspFormulaIncrementRefCount(tmpf1);
4357        CtlspFormulaIncrementRefCount(right->right);
4358        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4359        return tmpf2;
4360      }
4361    }
4362
4363    /* FALSE R (FG rlrr + rr) = FG(rlrr) + G(rr) */
4364    /* FALSE R (GF rlrr + rr) = GF(rlrr) + G(rr) */
4365    if (left->type == Ctlsp_FALSE_c && right->type == Ctlsp_OR_c) {
4366      if (Ctlsp_LtlFormulaIsFGorGF(right->left)) {
4367        tmpf1 = FormulaCreateWithType(Ctlsp_R_c);
4368        tmpf1->left = False;
4369        tmpf1->right = right->right;
4370        CtlspFormulaIncrementRefCount(False);
4371        CtlspFormulaIncrementRefCount(right->right);
4372        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4373
4374        tmpf2 = FormulaCreateWithType(Ctlsp_OR_c);
4375        tmpf2->left = tmpf1;
4376        tmpf2->right = right->left;
4377        CtlspFormulaIncrementRefCount(tmpf1);
4378        CtlspFormulaIncrementRefCount(right->left);
4379        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4380        return tmpf2;
4381      }
4382    }
4383
4384    /* r -> !l : (l R r) == FALSE R r */
4385    tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
4386    tmpf1->left = left;
4387    tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
4388    FREE(tmpf1);
4389    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4390    if (Ctlsp_LtlFormulaSimplyImply(right, tmpf2)) {
4391      tmpf1 = FormulaCreateWithType(Ctlsp_R_c);
4392      tmpf1->left = False;
4393      tmpf1->right = right;
4394      CtlspFormulaIncrementRefCount(False);
4395      CtlspFormulaIncrementRefCount(right);
4396      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4397      return tmpf2;
4398    }
4399
4400    /* r=>ll : (ll * lr) R r  ==  lr R r */
4401    if (left->type == Ctlsp_AND_c) {
4402      if (Ctlsp_LtlFormulaSimplyImply(right, left->left)) {
4403        tmpf1 = FormulaCreateWithType(Ctlsp_R_c);
4404        tmpf1->left = left->right;
4405        tmpf1->right = right;
4406        CtlspFormulaIncrementRefCount(left->right);
4407        CtlspFormulaIncrementRefCount(right);
4408        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4409        return tmpf2;
4410      }
4411    }
4412
4413    /* r=>lr : (ll * lr) R r  ==  ll R r */
4414    if (left->type == Ctlsp_AND_c) {
4415      if (Ctlsp_LtlFormulaSimplyImply(right, left->right)) {
4416        tmpf1 = FormulaCreateWithType(Ctlsp_R_c);
4417        tmpf1->left = left->left;
4418        tmpf1->right = right;
4419        CtlspFormulaIncrementRefCount(left->left);
4420        CtlspFormulaIncrementRefCount(right);
4421        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4422        return tmpf2;
4423      }
4424    }
4425
4426
4427    /* return  (left R right) */
4428    tmpf1 = FormulaCreateWithType(Ctlsp_R_c);
4429    tmpf1->left = left;
4430    tmpf1->right = right;
4431    CtlspFormulaIncrementRefCount(left);
4432    CtlspFormulaIncrementRefCount(right);
4433    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4434    return tmpf2;
4435
4436  case Ctlsp_X_c:
4437
4438    /* X(TRUE) == TRUE */
4439    /* X(FALSE) == FALSE */
4440    if (left->type == Ctlsp_TRUE_c || left->type == Ctlsp_FALSE_c)
4441      return left;
4442
4443    /* X(FGorGF) == FGorGF */
4444    if (Ctlsp_LtlFormulaIsFGorGF(left))
4445      return left;
4446
4447    /* X(ll + FGorGF lrrr) == X(ll) + FGorGF lrrr */
4448    /* X(ll * FGorGF lrrr) == X(ll) * FGorGF lrrr */
4449    if (left->type == Ctlsp_AND_c || left->type == Ctlsp_OR_c) {
4450      if (Ctlsp_LtlFormulaIsFGorGF(left->right)) {
4451        tmpf1 = FormulaCreateWithType(Ctlsp_X_c);
4452        tmpf1->left = left->left;
4453        CtlspFormulaIncrementRefCount(left->left);
4454        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4455
4456        tmpf2 = FormulaCreateWithType(left->type);
4457        tmpf2->left = tmpf1;
4458        tmpf2->right = left->right;
4459        CtlspFormulaIncrementRefCount(tmpf1);
4460        CtlspFormulaIncrementRefCount(left->right);
4461        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4462        return tmpf2;
4463      }
4464    }
4465
4466    /* X(FGorGF llrr + lr) ==  FGorGF llrr + X(lr) */
4467    /* X(FGorGF llrr * lr) ==  FGorGF llrr * X(lr) */
4468    if (left->type == Ctlsp_AND_c || left->type == Ctlsp_OR_c) {
4469      if (Ctlsp_LtlFormulaIsFGorGF(left->left)) {
4470        tmpf1 = FormulaCreateWithType(Ctlsp_X_c);
4471        tmpf1->left = left->right;
4472        CtlspFormulaIncrementRefCount(left->right);
4473        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4474
4475        tmpf2 = FormulaCreateWithType(left->type);
4476        tmpf2->left = left->left;
4477        tmpf2->right = tmpf1;
4478        CtlspFormulaIncrementRefCount(left->left);
4479        CtlspFormulaIncrementRefCount(tmpf1);
4480        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
4481        return tmpf2;
4482      }
4483    }
4484
4485    /* return X(left) */
4486    tmpf1 = FormulaCreateWithType(Ctlsp_X_c);
4487    tmpf1->left = left;
4488    CtlspFormulaIncrementRefCount(left);
4489    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4490    return tmpf2;
4491
4492  case Ctlsp_NOT_c:
4493
4494    /* return !(left) */
4495    tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
4496    tmpf1->left = left;
4497    CtlspFormulaIncrementRefCount(left);
4498    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
4499    return tmpf2;
4500
4501  default:
4502    assert(0);
4503  }
4504  return NIL(Ctlsp_Formula_t);
4505}
4506
4507/**Function********************************************************************
4508
4509  Synopsis    [Increments the reference count of a formula.]
4510
4511  Description [The function increments the reference count of a formula. If
4512  the formula is NULL, the function does nothing.]
4513
4514  SideEffects []
4515
4516  SeeAlso     []
4517
4518******************************************************************************/
4519void
4520CtlspFormulaIncrementRefCount(
4521  Ctlsp_Formula_t *formula)
4522{
4523  if(formula!=NIL(Ctlsp_Formula_t)) {
4524    ++(formula->refCount);
4525  }
4526}
4527
4528/**Function********************************************************************
4529
4530  Synopsis    [Decrements the reference count of a formula.]
4531
4532  Description [The function decrements the reference count of formula and if
4533  the reference count reaches 0, the formula is freed. If the formula is NULL,
4534  the function does nothing. It is an error to decrement the reference count
4535  below 0.]
4536
4537  SideEffects []
4538
4539  SeeAlso     []
4540
4541******************************************************************************/
4542void
4543CtlspFormulaDecrementRefCount(
4544  Ctlsp_Formula_t *formula)
4545{
4546  if(formula!=NIL(Ctlsp_Formula_t)) {
4547    assert(formula->refCount>0);
4548    if(--(formula->refCount) == 0)
4549      CtlspFormulaFree(formula);
4550  }
4551}
4552/**Function********************************************************************
4553
4554  Synopsis    [Adds formula to the end of globalFormulaArray.]
4555
4556  SideEffects [Manipulates the global variable globalFormulaArray.]
4557
4558  SeeAlso     [CtlspYyparse]
4559
4560******************************************************************************/
4561void
4562CtlspFormulaAddToGlobalArray(
4563  Ctlsp_Formula_t * formula)
4564{
4565  array_insert_last(Ctlsp_Formula_t *, globalFormulaArray, formula);
4566}
4567
4568/**Function********************************************************************
4569
4570  Synopsis    [Frees a CTL* formula.]
4571
4572  Description [The function frees all memory associated with the formula,
4573  including all MDDs and all character strings (however, does not free
4574  dbgInfo.originalFormula). It also decrements the reference counts of its two
4575  chidren. The function does nothing if formula is NULL.]
4576
4577  SideEffects []
4578
4579  SeeAlso     [Ctlsp_FormulaArrayFree]
4580
4581******************************************************************************/
4582void
4583CtlspFormulaFree(
4584  Ctlsp_Formula_t * formula)
4585{
4586  if (formula != NIL(Ctlsp_Formula_t)) {
4587
4588    /*
4589     * Free any fields that are not NULL.
4590     */
4591
4592    if (formula->type == Ctlsp_ID_c){
4593      FREE(formula->left);
4594      FREE(formula->right);
4595    }
4596    else {
4597      if (formula->left  != NIL(Ctlsp_Formula_t)) {
4598        CtlspFormulaDecrementRefCount(formula->left);
4599      }
4600      if (formula->right != NIL(Ctlsp_Formula_t)) {
4601        CtlspFormulaDecrementRefCount(formula->right);
4602      }
4603    }
4604
4605    if (formula->states != NIL(mdd_t))
4606      mdd_free(formula->states);
4607    if (formula->underapprox != NIL(mdd_t))
4608      mdd_free(formula->underapprox);
4609    if (formula->overapprox != NIL(mdd_t))
4610      mdd_free(formula->overapprox);
4611
4612    if (formula->dbgInfo.data != NIL(void)){
4613      (*formula->dbgInfo.freeFn)(formula);
4614    }
4615
4616    FREE(formula);
4617  }
4618}
4619
4620
4621/**Function********************************************************************
4622
4623  Synopsis    [Create a binary string of given value with size of interval.]
4624
4625  Description [The value is a binary string starting with 'b', a
4626  hexadecimal string starting with 'x', or an integer string.  If value
4627  does not fit the interval, or the binary string is not of the
4628  correct length, 0 is return.  Otherwise 1 is returned.  The result
4629  string is saved at given pointer.]
4630
4631  SideEffects []
4632
4633  SeeAlso     []
4634
4635******************************************************************************/
4636int
4637CtlspStringChangeValueStrToBinString(
4638  char *value,
4639  char *binValueStr,
4640  int  interval)
4641{
4642  int i;
4643  long int num, mask;
4644  double maxNum;
4645  char *ptr;
4646
4647  mask = 1;
4648  maxNum = pow(2.0,(double)interval);
4649  errno = 0;
4650
4651  if(value[0] == 'b'){
4652    if ((int)strlen(value)-1 == interval){
4653                        for(i=1;i<=interval;i++){
4654        if (value[i] == '0' || value[i] == '1'){
4655          binValueStr[i-1] =  value[i];
4656        }else{
4657          return 0;
4658        }
4659      }
4660      binValueStr[interval] = '\0';
4661    }else{
4662      return 0;
4663    }
4664  }else if (value[0] == 'x'){
4665    for(i=1; i < (int)strlen(value); i++){
4666      if (!isxdigit((int)value[i])){
4667        return 0;
4668      }
4669    }
4670    num = strtol(++value,&ptr,16);
4671    if (errno) return 0;
4672    if (num >= maxNum) return 0;
4673    for(i=0;i<interval;i++){
4674      if(num & (mask<<i)) binValueStr[interval-i-1] = '1';
4675      else binValueStr[interval-i-1] = '0';
4676    }
4677    binValueStr[interval] = '\0';
4678  }else{
4679    for(i=0;i<(int)strlen(value);i++){
4680      if (!isdigit((int)value[i])){
4681        return 0;
4682      }
4683    }
4684    num = strtol(value,&ptr,0);
4685    if (errno) return 0;
4686    if (num >= maxNum) return 0;
4687    mask = 1;
4688    for(i=0;i<interval;i++){
4689      if(num & (mask<<i)) binValueStr[interval-i-1] = '1';
4690      else binValueStr[interval-i-1] = '0';
4691    }
4692    binValueStr[interval] = '\0';
4693  }
4694
4695  return(1);
4696}
4697
4698
4699/**Function********************************************************************
4700
4701  Synopsis    [Change [] to <>]
4702
4703  Description []
4704
4705  SideEffects [The input string contains ...[num] and this function changes it
4706  to ...<num>.]
4707
4708  SeeAlso     []
4709
4710******************************************************************************/
4711void
4712CtlspChangeBracket(
4713  char *inStr)
4714{
4715  int i, j;
4716  char *str;
4717
4718  j = 0;
4719  for (i=0;i<(int)strlen(inStr)+1;i++){
4720    if (inStr[i] != ' '){
4721      inStr[i-j] = inStr[i];
4722    }else{
4723      j++;
4724    }
4725  }
4726
4727  if (changeBracket == 0)
4728    return;
4729
4730  str = strchr(inStr,'[');
4731  if (str == NULL) return;
4732
4733  *str = '<';
4734  str = strchr(inStr,']');
4735  *str = '>';
4736}
4737
4738
4739/**Function********************************************************************
4740
4741  Synopsis    [Parse a given vector string.]
4742
4743  Description [Parse given vector string of the form of var<i:j> and
4744  string var is returned. Other information such as i, j, interval between
4745  i and j, and increment or decrement from i to j are saved.]
4746
4747  SideEffects []
4748
4749  SeeAlso     []
4750
4751******************************************************************************/
4752char *
4753CtlspGetVectorInfoFromStr(
4754  char *str,
4755  int  *start,
4756  int  *end,
4757  int  *interval,
4758  int  *inc)
4759{
4760  char *str1, *str2, *str3;
4761  char *startStr, *endStr;
4762  char *name, *ptr;
4763
4764  str1 = strchr(str,'[');
4765  str2 = strchr(str,':');
4766  str3 = strchr(str,']');
4767  startStr = ALLOC(char, str2-str1);
4768  endStr = ALLOC(char, str3-str2);
4769  name = ALLOC(char, str1-str+1);
4770
4771  (void) strncpy(name, str, str1-str);
4772  (void) strncpy(startStr, str1+1, str2-str1-1);
4773  (void) strncpy(endStr, str2+1, str3-str2-1);
4774
4775  startStr[str2-str1-1] = '\0';
4776  endStr[str3-str2-1] = '\0';
4777  name[str1-str] = '\0';
4778  *start = strtol(startStr,&ptr,0);
4779  *end = strtol(endStr,&ptr,0);
4780  if(*start > *end){
4781      *inc = -1;
4782      *interval = *start - *end + 1;
4783  } else {
4784      *inc = 1;
4785      *interval = *end - *start + 1;
4786  }
4787  FREE(startStr);
4788  FREE(endStr);
4789  return name;
4790}
4791
4792/**Function********************************************************************
4793
4794  Synopsis    [Insert macro formula into symbol table.]
4795
4796  Description [If the name is already in table return 0, otherwise insert the
4797  formula into the table and return 1]
4798
4799  SideEffects []
4800
4801  SeeAlso     []
4802
4803******************************************************************************/
4804int
4805CtlspFormulaAddToTable(
4806  char *name,
4807  Ctlsp_Formula_t *formula,
4808  st_table *macroTable)
4809{
4810  if(macroTable == NIL(st_table)){
4811    macroTable = st_init_table(strcmp, st_strhash);
4812  }
4813  if(st_is_member(macroTable, name)){
4814    return 0;
4815  }
4816  st_insert(macroTable, name, (char *)formula);
4817  return 1;
4818}
4819
4820
4821/**Function********************************************************************
4822
4823  Synopsis    [Get macro formula from symbol table]
4824
4825  Description [If macro string is not found in table, NULL pointer is returned]
4826
4827  SideEffects []
4828
4829  SeeAlso     []
4830
4831******************************************************************************/
4832Ctlsp_Formula_t *
4833CtlspFormulaFindInTable(
4834  char *name,
4835  st_table *macroTable)
4836{
4837  Ctlsp_Formula_t *formula;
4838  if (st_lookup(macroTable, name, &formula)){
4839    return (Ctlsp_FormulaDup(formula));
4840  }else{
4841    return NIL(Ctlsp_Formula_t);
4842  }
4843}
4844
4845/**Function********************************************************************
4846
4847  Synopsis    []
4848
4849  Description []
4850
4851  SideEffects []
4852
4853  SeeAlso [FormulaTestIsForallQuantifier]
4854
4855******************************************************************************/
4856Ctlsp_FormulaClass
4857CtlspCheckClassOfExistentialFormulaRecur(
4858  Ctlsp_Formula_t *formula,
4859  boolean parity)
4860{
4861  Ctlsp_FormulaClass result;
4862
4863  Ctlsp_FormulaType formulaType = Ctlsp_FormulaReadType(formula);
4864  Ctlsp_Formula_t *rightFormula, *leftFormula;
4865  Ctlsp_FormulaClass resultLeft, resultRight, tempResult, currentClass;
4866
4867  /* Depending on the formula type, create result or recur */
4868  switch (formulaType) {
4869  case Ctlsp_E_c:
4870    leftFormula = Ctlsp_FormulaReadLeftChild(formula);
4871    resultLeft = CtlspCheckClassOfExistentialFormulaRecur(leftFormula, parity);
4872      resultRight = Ctlsp_QuantifierFree_c;
4873    tempResult = CtlspResolveClass(resultLeft, resultRight);
4874    if (!parity){
4875      currentClass = Ctlsp_ECTL_c;
4876    }else{
4877      currentClass = Ctlsp_ACTL_c;
4878    }
4879    result = CtlspResolveClass(currentClass, tempResult);
4880    break;
4881  case Ctlsp_A_c:
4882    /* The formula is supposed to be only existential */
4883    error_append("Inconsistency detected in function ");
4884    error_append("FormulaTestIsForallQuantifier\n");
4885    result = Ctlsp_invalid_c;
4886    break;
4887  case Ctlsp_OR_c:
4888  case Ctlsp_AND_c:
4889    rightFormula = Ctlsp_FormulaReadRightChild(formula);
4890    leftFormula = Ctlsp_FormulaReadLeftChild(formula);
4891    resultLeft = CtlspCheckClassOfExistentialFormulaRecur(leftFormula, parity);
4892    resultRight = CtlspCheckClassOfExistentialFormulaRecur(rightFormula, parity);
4893    result = CtlspResolveClass(resultLeft, resultRight);
4894    break;
4895  case Ctlsp_NOT_c:
4896    parity = !parity;
4897    leftFormula = Ctlsp_FormulaReadLeftChild(formula);
4898    result = CtlspCheckClassOfExistentialFormulaRecur(leftFormula, parity);
4899    break;
4900  case Ctlsp_ID_c:
4901  case Ctlsp_TRUE_c:
4902  case Ctlsp_FALSE_c:
4903     result = Ctlsp_QuantifierFree_c;
4904     break;
4905  case Ctlsp_Cmp_c:
4906    result = Ctlsp_Mixed_c;
4907    break;
4908  default:
4909    error_append("Unexpected operator detected.");
4910    result = Ctlsp_invalid_c;
4911    break;
4912  }
4913
4914  return result;
4915
4916} /* End of FormulaTestIsForallQuantifier */
4917
4918/**Function********************************************************************
4919
4920  Synopsis    []
4921
4922  Description []
4923
4924  SideEffects []
4925
4926  SeeAlso []
4927
4928******************************************************************************/
4929Ctlsp_FormulaClass
4930CtlspResolveClass(
4931  Ctlsp_FormulaClass class1,
4932  Ctlsp_FormulaClass class2)
4933{
4934  Ctlsp_FormulaClass result;
4935
4936  if ((class1 == Ctlsp_Mixed_c) || (class2 == Ctlsp_Mixed_c)){
4937    result = Ctlsp_Mixed_c;
4938  }else if (class1 == Ctlsp_QuantifierFree_c){
4939    result = class2;
4940  }else if (class2 == Ctlsp_QuantifierFree_c){
4941    result = class1;
4942  }else if (class1 == class2){
4943    result = class1;
4944  }else{
4945    result = Ctlsp_Mixed_c;
4946  }
4947  return result;
4948}
4949
4950/**Function********************************************************************
4951
4952  Synopsis    [Performs a recursive step of Ctlsp_FormulaConvertToCTL() ]
4953
4954  Description []
4955
4956  SideEffects []
4957
4958  Remarks []
4959
4960  SeeAlso []
4961
4962******************************************************************************/
4963Ctlp_Formula_t *
4964CtlspFormulaConvertToCTL(
4965  Ctlsp_Formula_t *formula)
4966{
4967  Ctlp_Formula_t *newNode, *leftNode, *rightNode;
4968  Ctlsp_Formula_t *childNode;
4969  char *variableNameCopy, *valueNameCopy;
4970
4971  if (formula == NIL(Ctlsp_Formula_t)) {
4972    return NIL(Ctlp_Formula_t);
4973  }
4974  /*
4975   * Recursively convert each subformula.
4976   */
4977  switch(formula->type) {
4978  case Ctlsp_E_c:
4979    childNode = formula->left;
4980    switch(childNode->type) {
4981    case Ctlsp_X_c:
4982      newNode = Ctlp_FormulaCreate(Ctlp_EX_c,
4983                                   CtlspFormulaConvertToCTL(childNode->left),
4984                                   NIL(Ctlsp_Formula_t));
4985      break;
4986    case Ctlsp_F_c:
4987      newNode = Ctlp_FormulaCreate(Ctlp_EF_c,
4988                                   CtlspFormulaConvertToCTL(childNode->left),
4989                                   NIL(Ctlsp_Formula_t));
4990      break;
4991    case Ctlsp_U_c:
4992      newNode = Ctlp_FormulaCreate(Ctlp_EU_c,
4993                                   CtlspFormulaConvertToCTL(childNode->left),
4994                                   CtlspFormulaConvertToCTL(childNode->right));
4995      break;
4996    case Ctlsp_R_c:
4997      /* E(f R g) => !A( !f U !g) */
4998
4999      leftNode  =  Ctlp_FormulaCreate(Ctlp_NOT_c,
5000                   CtlspFormulaConvertToCTL(childNode->left),
5001                   NIL(Ctlsp_Formula_t));
5002      rightNode =  Ctlp_FormulaCreate(Ctlp_NOT_c,
5003                   CtlspFormulaConvertToCTL(childNode->right),
5004                   NIL(Ctlsp_Formula_t));
5005
5006      newNode = Ctlp_FormulaCreate(Ctlp_AU_c, leftNode, rightNode);
5007      newNode = Ctlp_FormulaCreate(Ctlp_NOT_c, newNode, NIL(Ctlsp_Formula_t));
5008
5009      break;
5010    case Ctlsp_W_c:
5011      /* E(f W g) => !A(!g U !(f + g)) */
5012
5013      leftNode  =  Ctlp_FormulaCreate(Ctlp_NOT_c,
5014                   CtlspFormulaConvertToCTL(childNode->right),
5015                   NIL(Ctlsp_Formula_t));
5016      rightNode =  Ctlp_FormulaCreate(Ctlp_OR_c,
5017                   CtlspFormulaConvertToCTL(childNode->left),
5018                   CtlspFormulaConvertToCTL(childNode->right));
5019      rightNode =  Ctlp_FormulaCreate(Ctlp_NOT_c, rightNode,
5020                   NIL(Ctlsp_Formula_t));
5021
5022      newNode = Ctlp_FormulaCreate(Ctlp_AU_c, leftNode, rightNode);
5023      newNode = Ctlp_FormulaCreate(Ctlp_NOT_c, newNode, NIL(Ctlsp_Formula_t));
5024
5025      break;
5026    case Ctlsp_G_c:
5027      newNode = Ctlp_FormulaCreate(Ctlp_EG_c,
5028                                   CtlspFormulaConvertToCTL(childNode->left),
5029                                   NIL(Ctlsp_Formula_t));
5030      break;
5031    default:
5032      fail("Unexpected type");
5033    } /* switch: childNode->type */
5034    break;
5035  case Ctlsp_A_c:
5036    childNode = formula->left;
5037    switch(childNode->type) {
5038    case Ctlsp_X_c:
5039      newNode = Ctlp_FormulaCreate(Ctlp_AX_c,
5040                                   CtlspFormulaConvertToCTL(childNode->left),
5041                                   NIL(Ctlsp_Formula_t));
5042      break;
5043    case Ctlsp_F_c:
5044      newNode = Ctlp_FormulaCreate(Ctlp_AF_c,
5045                                   CtlspFormulaConvertToCTL(childNode->left),
5046                                   NIL(Ctlsp_Formula_t));
5047      break;
5048    case Ctlsp_U_c:
5049      newNode = Ctlp_FormulaCreate(Ctlp_AU_c,
5050                                   CtlspFormulaConvertToCTL(childNode->left),
5051                                   CtlspFormulaConvertToCTL(childNode->right));
5052      break;
5053    case Ctlsp_R_c:
5054      /* A(f R g) => !E( !f U !g) */
5055
5056      leftNode  =  Ctlp_FormulaCreate(Ctlp_NOT_c,
5057                   CtlspFormulaConvertToCTL(childNode->left),
5058                   NIL(Ctlsp_Formula_t));
5059      rightNode =  Ctlp_FormulaCreate(Ctlp_NOT_c,
5060                   CtlspFormulaConvertToCTL(childNode->right),
5061                   NIL(Ctlsp_Formula_t));
5062
5063      newNode = Ctlp_FormulaCreate(Ctlp_EU_c, leftNode, rightNode);
5064      newNode = Ctlp_FormulaCreate(Ctlp_NOT_c, newNode, NIL(Ctlsp_Formula_t));
5065
5066      break;
5067    case Ctlsp_W_c:
5068      /* A(f W g) => !E(!g U !(f + g)) */
5069
5070      leftNode  =  Ctlp_FormulaCreate(Ctlp_NOT_c,
5071                   CtlspFormulaConvertToCTL(childNode->right),
5072                   NIL(Ctlsp_Formula_t));
5073      rightNode =  Ctlp_FormulaCreate(Ctlp_OR_c,
5074                   CtlspFormulaConvertToCTL(childNode->left),
5075                   CtlspFormulaConvertToCTL(childNode->right));
5076      rightNode =  Ctlp_FormulaCreate(Ctlp_NOT_c, rightNode,
5077                   NIL(Ctlsp_Formula_t));
5078
5079      newNode = Ctlp_FormulaCreate(Ctlp_EU_c, leftNode, rightNode);
5080      newNode = Ctlp_FormulaCreate(Ctlp_NOT_c, newNode, NIL(Ctlsp_Formula_t));
5081
5082      break;
5083    case Ctlsp_G_c:
5084      newNode = Ctlp_FormulaCreate(Ctlp_AG_c,
5085                                   CtlspFormulaConvertToCTL(childNode->left),
5086                                   NIL(Ctlsp_Formula_t));
5087      break;
5088    default:
5089      fail("Unexpected type");
5090    } /* switch: childNode->type */
5091    break;
5092
5093  case Ctlsp_ID_c:
5094    /* Make a copy of the name, and create a new formula. */
5095    variableNameCopy = util_strsav((char *)(formula->left));
5096    valueNameCopy = util_strsav((char *)(formula->right));
5097    newNode = Ctlp_FormulaCreate(Ctlp_ID_c, variableNameCopy, valueNameCopy);
5098    break;
5099
5100  case Ctlsp_THEN_c:
5101    newNode = Ctlp_FormulaCreate(Ctlp_THEN_c,
5102                                 CtlspFormulaConvertToCTL(formula->left) ,
5103                                 CtlspFormulaConvertToCTL(formula->right) );
5104    break;
5105  case Ctlsp_OR_c:
5106    newNode = Ctlp_FormulaCreate(Ctlp_OR_c,
5107                                 CtlspFormulaConvertToCTL(formula->left) ,
5108                                 CtlspFormulaConvertToCTL(formula->right) );
5109    break;
5110  case Ctlsp_AND_c:
5111    newNode = Ctlp_FormulaCreate(Ctlp_AND_c,
5112                                 CtlspFormulaConvertToCTL(formula->left) ,
5113                                 CtlspFormulaConvertToCTL(formula->right) );
5114    break;
5115  case Ctlsp_NOT_c:
5116    newNode = Ctlp_FormulaCreate(Ctlp_NOT_c,
5117                                 CtlspFormulaConvertToCTL(formula->left) ,
5118                                 CtlspFormulaConvertToCTL(formula->right) );
5119    break;
5120  case Ctlsp_XOR_c:
5121    newNode = Ctlp_FormulaCreate(Ctlp_XOR_c,
5122                                 CtlspFormulaConvertToCTL(formula->left) ,
5123                                 CtlspFormulaConvertToCTL(formula->right) );
5124    break;
5125  case Ctlsp_EQ_c:
5126    newNode = Ctlp_FormulaCreate(Ctlp_EQ_c,
5127                                 CtlspFormulaConvertToCTL(formula->left) ,
5128                                 CtlspFormulaConvertToCTL(formula->right) );
5129    break;
5130  case Ctlsp_TRUE_c:
5131    newNode = Ctlp_FormulaCreate(Ctlp_TRUE_c,
5132                                 CtlspFormulaConvertToCTL(formula->left) ,
5133                                 CtlspFormulaConvertToCTL(formula->right) );
5134    break;
5135  case Ctlsp_FALSE_c:
5136    newNode = Ctlp_FormulaCreate(Ctlp_FALSE_c,
5137                                 CtlspFormulaConvertToCTL(formula->left) ,
5138                                 CtlspFormulaConvertToCTL(formula->right) );
5139    break;
5140  default:
5141    fail("Unexpected type");
5142  }
5143
5144  return newNode;
5145} /* CtlspFormulaConvertToCTL() */
5146
5147
5148/**Function********************************************************************
5149
5150  Synopsis    [Performs OR function]
5151
5152  Description []
5153
5154  SideEffects []
5155
5156  SeeAlso     []
5157
5158******************************************************************************/
5159Ctlsp_Formula_t *
5160CtlspFunctionOr(
5161  Ctlsp_Formula_t *left,
5162  Ctlsp_Formula_t *right)
5163{
5164  Ctlsp_Formula_t *result;
5165
5166  if((Ctlsp_FormulaReadType(left)  == Ctlsp_TRUE_c) ||
5167     (Ctlsp_FormulaReadType(right) == Ctlsp_TRUE_c)){
5168    result = Ctlsp_FormulaCreate(Ctlsp_TRUE_c, NIL(Ctlsp_Formula_t),
5169                                 NIL(Ctlsp_Formula_t));;
5170  } else
5171    if(Ctlsp_FormulaReadType(left) == Ctlsp_FALSE_c){
5172      result = right;
5173    } else
5174      if(Ctlsp_FormulaReadType(right) == Ctlsp_FALSE_c){
5175        result = left;
5176      } else
5177        result = Ctlsp_FormulaCreate(Ctlsp_OR_c, left, right);
5178
5179  return result;
5180}
5181
5182/**Function********************************************************************
5183
5184  Synopsis    [Performs And function]
5185
5186  Description []
5187
5188  SideEffects []
5189
5190  SeeAlso     []
5191
5192******************************************************************************/
5193Ctlsp_Formula_t *
5194CtlspFunctionAnd(
5195  Ctlsp_Formula_t *left,
5196  Ctlsp_Formula_t *right)
5197{
5198  Ctlsp_Formula_t *result;
5199
5200  if((Ctlsp_FormulaReadType(left)  == Ctlsp_FALSE_c) ||
5201     (Ctlsp_FormulaReadType(right) == Ctlsp_FALSE_c)){
5202    result = Ctlsp_FormulaCreate(Ctlsp_FALSE_c, NIL(Ctlsp_Formula_t),
5203                                 NIL(Ctlsp_Formula_t));;
5204  } else
5205    if(Ctlsp_FormulaReadType(left) == Ctlsp_TRUE_c){
5206      result = right;
5207    } else
5208      if(Ctlsp_FormulaReadType(right) == Ctlsp_TRUE_c){
5209        result = left;
5210      } else
5211        result = Ctlsp_FormulaCreate(Ctlsp_AND_c, left, right);
5212
5213  return result;
5214}
5215
5216/**Function********************************************************************
5217
5218  Synopsis    [Performs Then(Imply) function]
5219
5220  Description []
5221
5222  SideEffects []
5223
5224  SeeAlso     []
5225
5226******************************************************************************/
5227Ctlsp_Formula_t *
5228CtlspFunctionThen(
5229  Ctlsp_Formula_t *left,
5230  Ctlsp_Formula_t *right)
5231{
5232  Ctlsp_Formula_t *result;
5233
5234  if((Ctlsp_FormulaReadType(left)  == Ctlsp_TRUE_c) &&
5235     (Ctlsp_FormulaReadType(right) == Ctlsp_FALSE_c)){
5236    result = Ctlsp_FormulaCreate(Ctlsp_FALSE_c, NIL(Ctlsp_Formula_t),
5237                                 NIL(Ctlsp_Formula_t));
5238  } else
5239    if(Ctlsp_FormulaReadType(left) == Ctlsp_FALSE_c){
5240      result = Ctlsp_FormulaCreate(Ctlsp_TRUE_c, NIL(Ctlsp_Formula_t),
5241                                   NIL(Ctlsp_Formula_t));
5242    } else
5243      if((Ctlsp_FormulaReadType(left)  == Ctlsp_TRUE_c) &&
5244         (Ctlsp_FormulaReadType(right) == Ctlsp_TRUE_c)){
5245        result = Ctlsp_FormulaCreate(Ctlsp_TRUE_c, NIL(Ctlsp_Formula_t),
5246                                     NIL(Ctlsp_Formula_t));
5247      } else
5248        result = Ctlsp_FormulaCreate(Ctlsp_THEN_c, left, right);
5249
5250  return result;
5251}
5252
5253/*---------------------------------------------------------------------------*/
5254/* Definition of static functions                                            */
5255/*---------------------------------------------------------------------------*/
5256
5257/**Function********************************************************************
5258
5259  Synopsis    [Creates a CTL* formula with just the type set.]
5260
5261  Description [Calls Ctlsp_FormulaCreate with type, and all other fields NULL.]
5262
5263  SideEffects []
5264
5265  SeeAlso     [Ctlsp_FormulaCreate]
5266
5267******************************************************************************/
5268static Ctlsp_Formula_t *
5269FormulaCreateWithType(
5270  Ctlsp_FormulaType type)
5271{
5272  return (Ctlsp_FormulaCreate(type, NIL(Ctlsp_Formula_t), NIL(Ctlsp_Formula_t)));
5273}
5274
5275
5276/**Function********************************************************************
5277
5278  Synopsis    [The comparison function for the formula unique table.]
5279
5280  Description [The function takes as parameters two CTL* formulae. It compares
5281  the formula type, the left child and the right child, and returns 0 if they
5282  match. Otherwise, it returns -1.]
5283
5284  SideEffects []
5285
5286  SeeAlso     [FormulaHash]
5287
5288******************************************************************************/
5289static int
5290FormulaCompare(
5291  const char *key1,
5292  const char *key2)
5293{
5294  Ctlsp_Formula_t *formula1 = (Ctlsp_Formula_t *) key1;
5295  Ctlsp_Formula_t *formula2 = (Ctlsp_Formula_t *) key2;
5296
5297  assert(key1 != NIL(char));
5298  assert(key2 != NIL(char));
5299
5300
5301  if(formula1->type != formula2->type) {
5302    return -1;
5303  }
5304  if(formula1->type == Ctlsp_ID_c) {
5305    if(strcmp((char *) (formula1->left), (char *) (formula2->left)) ||
5306       strcmp((char *) (formula1->right), (char *) (formula2->right))) {
5307      return -1;
5308    } else
5309      return 0;
5310  } else {
5311    if(formula1->left != formula2->left)
5312      return -1;
5313    if(formula1->right != formula2->right)
5314      return -1;
5315    if (formula1->type == Ctlsp_Cmp_c &&
5316        formula1->compareValue != formula2->compareValue) {
5317      return -1;
5318    }
5319    return 0;
5320  }
5321}
5322
5323/**Function********************************************************************
5324
5325  Synopsis    [The hash function for the formula unique table.]
5326
5327  Description [The function takes as parameter a CTL* formula. If the formula
5328  type is Ctlsp_ID_c, st_strhash is used with a concatenation of left and
5329  right children as the key string. Otherwise, something very similar to
5330  st_ptrhash is done.]
5331
5332  SideEffects []
5333
5334  SeeAlso     [FormulaCompare]
5335
5336******************************************************************************/
5337static int
5338FormulaHash(
5339  char *key,
5340  int modulus)
5341{
5342  char *hashString;
5343  int hashValue;
5344  Ctlsp_Formula_t *formula = (Ctlsp_Formula_t *) key;
5345
5346  if(formula->type==Ctlsp_ID_c) {
5347    hashString = util_strcat3((char *) (formula->left), (char *)
5348                              (formula->right), "");
5349    hashValue = st_strhash(hashString, modulus);
5350    FREE(hashString);
5351    return hashValue;
5352  }
5353  return (int) ((((unsigned long) formula->left >>2) +
5354                 ((unsigned long) formula->right >>2)) % modulus);
5355}
5356
5357/**Function********************************************************************
5358
5359  Synopsis    [Hashes the formula into the unique table.]
5360
5361  Description [The function takes a formula and hashes it and all its
5362  subformulae into a unique table. It returns the unique formula identical to
5363  the formula being hashed. The formula returned will have maximum sharing
5364  with the formulae that are already present in uniqueTable. It returns
5365  NIL(Ctlsp_Formula_t) if the formula is NIL(Ctlsp_Formula_t).]
5366
5367  SideEffects [If a copy of some subformula of formula is present in
5368  uniqueTable then the copy is substituted for it and the reference count of
5369  the subformula is decremented.]
5370
5371  SeeAlso     [FormulaCompare]
5372
5373******************************************************************************/
5374static Ctlsp_Formula_t *
5375FormulaHashIntoUniqueTable(
5376  Ctlsp_Formula_t *formula,
5377  st_table *uniqueTable)
5378{
5379  Ctlsp_Formula_t *uniqueFormula, *uniqueLeft, *uniqueRight;
5380
5381  if(formula == NIL(Ctlsp_Formula_t))
5382    return NIL(Ctlsp_Formula_t);
5383  if(st_lookup(uniqueTable, formula, &uniqueFormula)) {
5384    return uniqueFormula;
5385  }
5386  else {
5387    if(formula->type == Ctlsp_ID_c) {
5388      st_insert(uniqueTable, (char *) formula, (char *) formula);
5389      return formula;
5390    }
5391    else {
5392      uniqueLeft = FormulaHashIntoUniqueTable(formula->left, uniqueTable);
5393      if(uniqueLeft != NIL(Ctlsp_Formula_t))
5394        if(uniqueLeft != formula->left) {
5395          CtlspFormulaDecrementRefCount(formula->left);
5396          formula->left = uniqueLeft;
5397          CtlspFormulaIncrementRefCount(formula->left);
5398        }
5399      uniqueRight = FormulaHashIntoUniqueTable(formula->right, uniqueTable);
5400      if(uniqueRight != NIL(Ctlsp_Formula_t))
5401        if(uniqueRight != formula->right) {
5402          CtlspFormulaDecrementRefCount(formula->right);
5403          formula->right = uniqueRight;
5404          CtlspFormulaIncrementRefCount(formula->right);
5405        }
5406      if(st_lookup(uniqueTable, formula, &uniqueFormula)) {
5407        return uniqueFormula;
5408      }
5409      else {
5410        st_insert(uniqueTable, (char *) formula, (char *) formula);
5411        return formula;
5412      }
5413    }
5414  }
5415}
5416
5417/**Function********************************************************************
5418
5419  Synopsis [Create SNF propositional variable if the passed formula is
5420  not propositional]
5421
5422  Description [If formula is not propositional, generate SNF for the
5423  formula first and returned the renamed variable]
5424
5425  SideEffects [Add the new generated SNF rule to formulaArray]
5426
5427  SeeAlso     [Ctlsp_LtlTranslateIntoSNFRecursive]
5428
5429******************************************************************************/
5430static Ctlsp_Formula_t *
5431createSNFnode(
5432  Ctlsp_Formula_t *formula,
5433  array_t         *formulaArray,
5434  int             *index)
5435{
5436  Ctlsp_Formula_t *newNode;
5437
5438  if(!Ctlsp_LtlFormulaIsPropositional(formula)){
5439    newNode  = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strcat3(" SNFx","_", util_inttostr((*index)++)),
5440                                   (void *)util_strsav("1"));
5441    Ctlsp_LtlTranslateIntoSNFRecursive(newNode, formula, formulaArray, index);
5442    return newNode;
5443  } else {
5444    return Ctlsp_FormulaDup(formula);
5445  }
5446
5447}
Note: See TracBrowser for help on using the repository browser.