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

/**CFile***********************************************************************

  FileName    [ctlspUtil.c]

  PackageName [ctlsp]

  Synopsis    [Routines for manipulating CTL* formulas.]

  Description [This file contains routines for accessing the fields of the CTL*
  formula data structure, for printing CTL* formulas, for reading CTL* formulas
  from a file, and for converting formulas to the existential form.]

  Author      [Mohammad Awedh, Chao Wang]

  Copyright   [This file was created at the University of Colorado at Boulder.
  The University of Colorado at Boulder makes no warranty about the suitability
  of this software for any purpose.  It is presented on an AS IS basis.]

******************************************************************************/

#include "ctlspInt.h"
#include "errno.h"
#include "ntk.h"

static char rcsid[] UNUSED = "$Id: ctlspUtil.c,v 1.64 2009/04/11 18:25:55 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/**Variable********************************************************************

  Synopsis    [Array of CTL* formulas (Ctlsp_Formula_t) read from a file.]

  SeeAlso     [Ctlsp_FormulaArrayFree]

******************************************************************************/
static array_t *globalFormulaArray;
static int      changeBracket = 1;

/* see ctlspInt.h for documentation */
int CtlspGlobalError;
Ctlsp_Formula_t *CtlspGlobalFormula;
st_table *CtlspMacroTable;

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static Ctlsp_Formula_t * FormulaCreateWithType(Ctlsp_FormulaType type);
static int FormulaCompare(const char *key1, const char *key2);
static int FormulaHash(char *key, int modulus);
static Ctlsp_Formula_t * FormulaHashIntoUniqueTable(Ctlsp_Formula_t *formula, st_table *uniqueTable);
static Ctlsp_Formula_t * createSNFnode(Ctlsp_Formula_t *formula, array_t *formulaArray, int *index);

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [Parses a file containing a set of CTL* formulas.]

  Description [Parses a file containing a set of semicolon-ending CTL*
  formulas, and returns an array of Ctlsp_Formula_t representing those
  formulas.  If an error is detected while parsing the file, the routine frees
  any allocated memory and returns NULL.]

  SideEffects [Manipulates the global variables globalFormulaArray,
  CtlspGlobalError and CtlspGlobalFormula.]

  SeeAlso     [Ctlsp_FormulaArrayFree Ctlsp_FormulaPrint]

******************************************************************************/
array_t *
Ctlsp_FileParseFormulaArray(
  FILE * fp)
{
  st_generator *stGen;
  char *name;
  Ctlsp_Formula_t *formula;
  char *flagValue;
  /*
   * Initialize the global variables.
   */
  globalFormulaArray = array_alloc(Ctlsp_Formula_t *, 0);
  CtlspGlobalError = 0;
  CtlspGlobalFormula = NIL(Ctlsp_Formula_t);
  CtlspMacroTable = st_init_table(strcmp,st_strhash);
  CtlspFileSetup(fp);
  /*
   * Check if changing "[] -> <>" is disabled.
   */
  flagValue = Cmd_FlagReadByName("ctl_change_bracket");
  if (flagValue != NIL(char)) {
    if (strcmp(flagValue, "yes") == 0)
      changeBracket = 1;
    else if (strcmp(flagValue, "no") == 0)
      changeBracket = 0;
    else {
      fprintf(vis_stderr,
        "** ctl error : invalid value %s for ctl_change_bracket[yes/no]. ***\n",
        flagValue);
    }
  }

  (void)CtlspYyparse();
  st_foreach_item(CtlspMacroTable,stGen,&name, &formula){
     FREE(name);
     CtlspFormulaFree(formula);
  }
  st_free_table(CtlspMacroTable);

  /*
   * Clean up if there was an error, otherwise return the array.
   */
  if (CtlspGlobalError){
    Ctlsp_FormulaArrayFree(globalFormulaArray);
    return NIL(array_t);
  }
  else {
    return globalFormulaArray;
  }
}


/**Function********************************************************************

  Synopsis    [Parses a file containing a set of CTL formulas.]

  Description [Parses a file containing a set of semicolon-terminated CTL
  formulae, and returns an array of Ctlp_Formula_t representing those
  formulae.  If an error is detected while parsing the file, the routine frees
  any allocated memory and returns NULL.]

  SideEffects [Manipulates the global variables globalFormulaArray,
  CtlspGlobalError and CtlspGlobalFormula.]

  SeeAlso     [Ctlsp_FileParseFormulaArray]

******************************************************************************/
array_t *
Ctlsp_FileParseCTLFormulaArray(
  FILE *fp)
{
  array_t *ctlsArray = Ctlsp_FileParseFormulaArray(fp);
  array_t *ctlArray;

  if (ctlsArray == NIL(array_t)) return NIL(array_t);
  ctlArray = Ctlsp_FormulaArrayConvertToCTL(ctlsArray);
  Ctlsp_FormulaArrayFree(ctlsArray);
  return ctlArray;
  
} /* Ctlsp_FileParseCTLFormulaArray */

/**Function********************************************************************

  Synopsis    [Returns a character string represents the CTL* formula]

  Description [Returns formula as a character string. All subformulas are
  delimited by parenthesis. Does nothing if passed a NULL formula.]

  SideEffects []

******************************************************************************/
char *
Ctlsp_FormulaConvertToString(
  Ctlsp_Formula_t * formula)
{
  char *s1        = NIL(char);
  char *s2        = NIL(char);
  char *tmpString = NIL(char);
  char *result;


  if (formula == NIL(Ctlsp_Formula_t)) {
    return NIL(char);
  }

  /* leaf node */
  if (formula->type == Ctlsp_ID_c){
  result = util_strcat3((char *)(formula->left), "=",(char *)(formula->right));
  /*
  tmpString = util_strcat3("[", util_inttostr(formula->CTLclass),"]");
  return util_strcat3(result, " ",tmpString);
  */
  return result;
  }

  /* If the formula is a non-leaf, the function is called recursively */
  s1 = Ctlsp_FormulaConvertToString(formula->left);
  s2 = Ctlsp_FormulaConvertToString(formula->right);

  switch(formula->type) {
    /*
     * The cases are listed in rough order of their expected frequency.
     */
    case Ctlsp_OR_c:
      tmpString = util_strcat3(s1, " + ",s2);
      result    = util_strcat3("(", tmpString, ")");
      break;
    case Ctlsp_AND_c:
      tmpString = util_strcat3(s1, " * ", s2);
      result    = util_strcat3("(", tmpString, ")");
      break;
    case Ctlsp_THEN_c:
      tmpString = util_strcat3(s1, " -> ", s2);
      result    = util_strcat3("(", tmpString, ")");
      break;
    case Ctlsp_XOR_c:
      tmpString = util_strcat3(s1, " ^ ", s2);
      result    = util_strcat3("(", tmpString, ")");
      break;
    case Ctlsp_EQ_c:
      tmpString = util_strcat3(s1, " <-> ", s2);
      result    = util_strcat3("(", tmpString, ")");
      break;
    case Ctlsp_NOT_c:
      tmpString = util_strcat3("(", s1, ")");
      result    = util_strcat3("!", tmpString, "");
      break;
    case Ctlsp_E_c:
      result = util_strcat3("E(", s1, ")");
      FREE(s1);
      break;
    case Ctlsp_G_c:
      result = util_strcat3("G(", s1, ")");
      break;
    case Ctlsp_F_c:
      result = util_strcat3("F(", s1, ")");
      break;
    case Ctlsp_U_c:
      tmpString = util_strcat3("(", s1, " U ");
      result    = util_strcat3(tmpString, s2, ")");
      break;
    case Ctlsp_R_c:
      tmpString = util_strcat3("(", s1, " R ");
      result    = util_strcat3(tmpString, s2, ")");
      break;
    case Ctlsp_W_c:
      tmpString = util_strcat3("(", s1, " W ");
      result    = util_strcat3(tmpString, s2, ")");
      break;
    case Ctlsp_X_c:
      result = util_strcat3("X(", s1, ")");
      break;
    case Ctlsp_A_c:
      result = util_strcat3("A(", s1, ")");
      break;;
    case Ctlsp_TRUE_c:
      result = util_strsav("TRUE");
      break;
    case Ctlsp_FALSE_c:
      result = util_strsav("FALSE");
      break;
    case Ctlsp_Init_c:
      result = util_strsav("Init");
      break;
    case Ctlsp_Cmp_c:
      if (formula->compareValue == 0)
        tmpString = util_strcat3("[", s1, "] = ");
      else
        tmpString = util_strcat3("[", s1, "] != ");
      result    = util_strcat3(tmpString, s2, "");
      break;
    case Ctlsp_Fwd_c:
      tmpString = util_strcat3("FwdG(", s1, ",");
      result    = util_strcat3(tmpString, s2, ")");
      break;
      /*   case Ctlsp_EY_c:
      result = util_strcat3("EY(", s1, ")");
      break;*/
    default:
      fail("Unexpected type");

  }
  if (s1 != NIL(char)) {
    FREE(s1);
  }
  if (s2 != NIL(char)) {
    FREE(s2);
  }
  if (tmpString != NIL(char)) {
    FREE(tmpString);
  }

  return result;
}


/**Function********************************************************************

  Synopsis    [Prints a formula to a file.]

  Description [Prints a formula to a file. All subformulas are delimited by
  parenthesis. The syntax used is the same as used by the CTL* parser.  Does
  nothing if passed a NULL formula.]

  SideEffects []

******************************************************************************/
void
Ctlsp_FormulaPrint(
  FILE * fp,
  Ctlsp_Formula_t * formula)
{
  char *tmpString;
  if (formula == NIL(Ctlsp_Formula_t)) {
    return;
  }
  tmpString = Ctlsp_FormulaConvertToString(formula);
  (void) fprintf(fp, "%s", tmpString);
  FREE(tmpString);
}


/**Function********************************************************************

  Synopsis    [Gets the type of a formula.]

  Description [Gets the type of a formula. See ctlsp.h for all the types. It is
  an error to call this function on a NULL formula.]

  SideEffects []

  SeeAlso     [ctlsp.h]

******************************************************************************/
Ctlsp_FormulaType
Ctlsp_FormulaReadType(
  Ctlsp_Formula_t * formula)
{
  return (formula->type);
}


/**Function********************************************************************

  Synopsis    [Gets the compare value of a formula.]

  Description [Gets the compare value of a formula. See ctlsp.h for all the
  types. It is an error to call this function on a NULL formula.]

  SideEffects []

  SeeAlso     [ctlsp.h]

******************************************************************************/
int
Ctlsp_FormulaReadCompareValue(
  Ctlsp_Formula_t * formula)
{
  int value;
  value = formula->compareValue;
  return (value);
}


/**Function********************************************************************

  Synopsis    [Reads the variable name of a leaf formula.]

  Description [Reads the variable name of a leaf formula.
  It is an error to call this function on a non-leaf formula.]

  SideEffects []

******************************************************************************/
char *
Ctlsp_FormulaReadVariableName(
  Ctlsp_Formula_t * formula)
{
  if (formula->type != Ctlsp_ID_c){
    fail("Ctlsp_FormulaReadVariableName() was called on a non-leaf formula.");
  }
  return ((char *)(formula->left));
}


/**Function********************************************************************

  Synopsis    [Reads the value name of a leaf formula.]

  Description [Reads the value name of a leaf formula.
  It is an error to call this function on a non-leaf formula.]

  SideEffects []

******************************************************************************/
char *
Ctlsp_FormulaReadValueName(
  Ctlsp_Formula_t * formula)
{
  if (formula->type != Ctlsp_ID_c){
    fail("Ctlsp_FormulaReadValueName() was called on a non-leaf formula.");
  }
  return ((char *)(formula->right));
}

/**Function********************************************************************

  Synopsis    [Gets the left child of a formula.]

  Description [Gets the left child of a formula.  User must not free this
  formula. If a formula is a leaf formula, NIL(Ctlsp_Formula_t) is returned.]

  SideEffects []

  SeeAlso     [Ctlsp_FormulaReadRightChild]

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_FormulaReadLeftChild(
  Ctlsp_Formula_t * formula)
{
  if (formula->type != Ctlsp_ID_c){
    return (formula->left);
  }
  return NIL(Ctlsp_Formula_t);
}


/**Function********************************************************************

  Synopsis    [Gets the right child of a formula.]

  Description [Gets the right child of a formula.  User must not free this
  formula. If a formula is a leaf formula, NIL(Ctlsp_Formula_t) is returned.]

  SideEffects []

  SeeAlso     [Ctlsp_FormulaReadLeftChild]

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_FormulaReadRightChild(
  Ctlsp_Formula_t * formula)
{
  if (formula->type != Ctlsp_ID_c){
    return (formula->right);
  }
  return NIL(Ctlsp_Formula_t);
}


/**Function********************************************************************

  Synopsis [Gets a copy of the set of states for which this formula is
  true.]

  Description [Gets a copy of the MDD representing the set of states for which
  this formula is true.  It is the user's responsibility to free this MDD. If
  the set of states has not yet been computed, then a NULL mdd_t is
  returned. It is an error to call this function on a NULL formula.]

  SideEffects []

  SeeAlso     [Ctlsp_FormulaSetStates]

******************************************************************************/
mdd_t *
Ctlsp_FormulaObtainStates(
  Ctlsp_Formula_t * formula)
{
  if (formula->states == NIL(mdd_t)) {
    return NIL(mdd_t);
  }
  else {
    return mdd_dup(formula->states);
  }
}
/**Function********************************************************************

  Synopsis [Gets (a copy of) an approximation of the satisfying set]

  Description [Gets the required approximation of the satisfying set.  If the
  exact set is available, it will return that.  If neither is available, or
  approx is Ctlsp_Incomparable_c, it will return NULL.]

  SideEffects []

  SeeAlso     [Ctlsp_FormulaSetStates]

******************************************************************************/
mdd_t *
Ctlsp_FormulaObtainApproxStates(
  Ctlsp_Formula_t *formula,
  Ctlsp_Approx_t approx)
{
  if(approx == Ctlsp_Incomparable_c)
    return NIL(mdd_t);

  if (formula->states != NIL(mdd_t))
    return mdd_dup(formula->states);

  if(approx == Ctlsp_Exact_c)
    return NIL(mdd_t);

  if(approx == Ctlsp_Overapprox_c){
    if(formula->overapprox == NIL(mdd_t))
      return NIL(mdd_t);
    else
      return mdd_dup(formula->overapprox);
  }

  if(approx == Ctlsp_Underapprox_c){
    if(formula->underapprox == NIL(mdd_t))
      return NIL(mdd_t);
    else
      return mdd_dup(formula->underapprox);
  }

  assert(0);  /* we should never get here */
  return NIL(mdd_t);
}


/**Function********************************************************************

  Synopsis    [Stores the set of states with the formula.]

  Description [Stores the MDD with the formula (a copy is not made,
  and hence, the caller should not later free this MDD). This MDD is
  intended to represent the set of states for which the formula is
  true. It is an error to call this function on a NULL formula.]

  SideEffects []

  SeeAlso     [Ctlsp_FormulaObtainStates]

******************************************************************************/
void
Ctlsp_FormulaSetStates(
  Ctlsp_Formula_t * formula,
  mdd_t * states)
{
  /* RB: added the next two lines.  Given the Description, this was a
     bug */
    if(formula->states != NIL(mdd_t))
      mdd_free(formula->states);
    formula->states = states;
}


/**Function********************************************************************

  Synopsis [Stores (an approximation of) the set of states with the
  formula.]

  Description [Sets the set of states or an under or overapproximation thereof,
  depending on the approx flag.  If there is already an under or
  overapproximation, it is overwritten.  If the exact set is given, the approx
  fields are cleared.  Setting an incomparable approximation results in no
  action being taken.  A copy of the bdd is not made, so the caller should not
  free it.  ]

  SideEffects []

  SeeAlso     [Ctlsp_FormulaObtainStates]

******************************************************************************/
void
Ctlsp_FormulaSetApproxStates(
  Ctlsp_Formula_t * formula,
  mdd_t * states,
  Ctlsp_Approx_t approx)
{
  if(approx == Ctlsp_Incomparable_c){
    mdd_free(states);
    return;
  }

  if(approx == Ctlsp_Exact_c){
    if(formula->states != NIL(mdd_t))
      mdd_free(formula->states);
    formula->states = states;

    if(formula->underapprox != NIL(mdd_t)){
      mdd_free(formula->underapprox);
      formula->underapprox = NIL(mdd_t);
    }

    if(formula->overapprox != NIL(mdd_t)){
      mdd_free(formula->overapprox);
      formula->overapprox = NIL(mdd_t);
    }
  }

  if( approx == Ctlsp_Underapprox_c){
    /* you could perform a union instead, but typical use will
       have monotonically increasing underapproximations */
    if(formula->underapprox != NIL(mdd_t))
      mdd_free(formula->underapprox);
    formula->underapprox = states;
  }

  if( approx == Ctlsp_Overapprox_c){
    /* you could perform an intersaection instead */
    if(formula->overapprox != NIL(mdd_t))
      mdd_free(formula->overapprox);
    formula->overapprox = states;
  }

  return;
}



/**Function********************************************************************

  Synopsis    [Sets the debug information of a formula.]

  Description [Sets the debug information of a CTL formula.  The data is
  uninterpreted.  FreeFn is a pointer to a function that takes a formula as
  input and returns void.  FreeFn should free all the memory associated with
  the debug data; it is called when this formula is freed.]

  SideEffects []

  SeeAlso     [Ctlsp_FormulaReadDebugData]

******************************************************************************/
void
Ctlsp_FormulaSetDbgInfo(
  Ctlsp_Formula_t * formula,
  void *data,
  Ctlsp_DbgInfoFreeFn freeFn)
{
  formula->dbgInfo.data   = data;
  formula->dbgInfo.freeFn = freeFn;
}


/**Function********************************************************************

  Synopsis    [Returns the debug data associated with a formula.]

  Description [Returns the debug data associated with a formula.  This data is
  uninterpreted by the ctlsp package.]

  SideEffects []

  SeeAlso     [Ctlsp_FormulaSetDbgInfo]

******************************************************************************/
void *
Ctlsp_FormulaReadDebugData(
  Ctlsp_Formula_t * formula)
{
  return formula->dbgInfo.data;
}


/**Function********************************************************************

  Synopsis    [Returns TRUE if formula was converted, else FALSE.]
  from AX/AG/AU/AF]

  Description [Returns TRUE if formula was converted from a formula of type
  AG, AX, AU, AF, or EF via a call to
  Ctlsp_FormulaConvertToExistentialFormTree or
  Ctlsp_FormulaConvertToExistentialFormDAG. Otherwise, returns FALSE.]

  SideEffects []

******************************************************************************/
boolean
Ctlsp_FormulaTestIsConverted(
  Ctlsp_Formula_t * formula)
{
  return formula->dbgInfo.convertedFlag;
}


/**Function********************************************************************

  Synopsis    [Returns TRUE if formula contains no path quantifiers.]

  Description [Test if a CTL* formula has any path quantifiers in it;
  if so return false, else true.  For a CTL* formula, being quantifier-free
  and being propositional are not equivalent.]

  SideEffects []

******************************************************************************/
boolean
Ctlsp_FormulaTestIsQuantifierFree(
  Ctlsp_Formula_t *formula)
{
  boolean lCheck;
  boolean rCheck;
  Ctlsp_Formula_t *leftChild;
  Ctlsp_Formula_t *rightChild;
  Ctlsp_FormulaType type;

  if ( formula == NIL( Ctlsp_Formula_t ) ) {
    return TRUE;
  }

  type = Ctlsp_FormulaReadType( formula );

  if ( ( type == Ctlsp_ID_c ) ||
       ( type == Ctlsp_TRUE_c ) ||
       ( type == Ctlsp_FALSE_c ) ) {
    return TRUE;
  }

  if ( ( type == Ctlsp_E_c ) || ( type == Ctlsp_A_c ) ) {
    return FALSE;
  }

  leftChild = Ctlsp_FormulaReadLeftChild( formula );
  lCheck = Ctlsp_FormulaTestIsQuantifierFree( leftChild );

  if (lCheck == FALSE)
    return FALSE;

  rightChild = Ctlsp_FormulaReadRightChild( formula );
  rCheck = Ctlsp_FormulaTestIsQuantifierFree( rightChild );

  return rCheck;
}


/**Function********************************************************************

  Synopsis    [Returns original formula corresponding to converted formula.]

  SideEffects []

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_FormulaReadOriginalFormula(
  Ctlsp_Formula_t * formula)
{
  return formula->dbgInfo.originalFormula;
}


/**Function********************************************************************

  Synopsis    [Returns the Alpha-Beta Index. used for LTL->AUT]

  SideEffects []

******************************************************************************/
int
Ctlsp_FormulaReadABIndex(
  Ctlsp_Formula_t * formula)
{
  return formula->ab_idx;
}

/**Function********************************************************************

  Synopsis    [Set the Alpha-Beta Index. used for LTL->AUT]

  SideEffects []

******************************************************************************/
void
Ctlsp_FormulaSetABIndex(
  Ctlsp_Formula_t * formula,
  int ab_idx)
{
  formula->ab_idx = ab_idx;
}


/**Function********************************************************************

  Synopsis    [Returns the Label Index. used for LTL->AUT]

  SideEffects []

******************************************************************************/
int
Ctlsp_FormulaReadLabelIndex(
  Ctlsp_Formula_t * formula)
{
  return formula->label_idx;
}

/**Function********************************************************************

  Synopsis    [Set the Label Index. used for LTL->AUT]

  SideEffects []

******************************************************************************/
void
Ctlsp_FormulaSetLabelIndex(
  Ctlsp_Formula_t * formula,
  int label_idx)
{
  formula->label_idx = label_idx;
}


/**Function********************************************************************

  Synopsis    [Returns the RHS. used for LTL->AUT]

  SideEffects []

******************************************************************************/
char
Ctlsp_FormulaReadRhs(
  Ctlsp_Formula_t * formula)
{
  return formula->rhs;
}

/**Function********************************************************************

  Synopsis    [Set the RHS. used for LTL->AUT]

  SideEffects []

******************************************************************************/
void
Ctlsp_FormulaSetRhs(
  Ctlsp_Formula_t * formula)
{
  formula->rhs = 1;
}

/**Function********************************************************************

  Synopsis    [Reset the RHS. used for LTL->AUT]

  SideEffects []

******************************************************************************/
void
Ctlsp_FormulaResetRhs(
  Ctlsp_Formula_t * formula)
{
  formula->rhs = 0;
}

/**Function********************************************************************

  Synopsis    [Returns the marked. used for LTL->AUT]

  SideEffects []

******************************************************************************/
char
Ctlsp_FormulaReadMarked(
  Ctlsp_Formula_t * formula)
{
  return formula->marked;
}

/**Function********************************************************************

  Synopsis    [Set the Alpha-Beta Index. used for LTL->AUT]

  SideEffects []

******************************************************************************/
void
Ctlsp_FormulaSetMarked(
  Ctlsp_Formula_t * formula)
{
  formula->marked = 1;
}

/**Function********************************************************************

  Synopsis    [Reset the Alpha-Beta Index. used for LTL->AUT]

  SideEffects []

******************************************************************************/
void
Ctlsp_FormulaResetMarked(
  Ctlsp_Formula_t * formula)
{
  formula->marked = 0;
}

/**Function********************************************************************

  Synopsis    [Frees a formula if no other formula refers to it as a
  sub-formula.]

  Description [The function decrements the refCount of the formula. As a
  consequence, if the refCount becomes 0, the formula is freed.]

  SideEffects []

  SeeAlso     [CtlspFormulaFree, CtlspDecrementRefCount]

******************************************************************************/
void
Ctlsp_FormulaFree(
  Ctlsp_Formula_t *formula)
{
  CtlspFormulaDecrementRefCount(formula);
}

/**Function********************************************************************

  Synopsis [Recursively frees states, underapprox and overapprox fields of
  Ctlsp_Formula_t, and the debug data]

  Description []

  SideEffects []

  SeeAlso     [Ctlsp_FormulaFree]

******************************************************************************/
void
Ctlsp_FlushStates(
  Ctlsp_Formula_t * formula)
{
  if (formula != NIL(Ctlsp_Formula_t)) {

    if (formula->type != Ctlsp_ID_c){
      if (formula->left  != NIL(Ctlsp_Formula_t)) {
        Ctlsp_FlushStates(formula->left);
      }
      if (formula->right != NIL(Ctlsp_Formula_t)) {
        Ctlsp_FlushStates(formula->right);
      }
    }

    if (formula->states != NIL(mdd_t)){
      mdd_free(formula->states);
      formula->states = NIL(mdd_t);
    }
    if (formula->underapprox != NIL(mdd_t)){
      mdd_free(formula->underapprox);
      formula->underapprox = NIL(mdd_t);
    }
    if (formula->overapprox != NIL(mdd_t)){
      mdd_free(formula->overapprox);
      formula->overapprox = NIL(mdd_t);
    }

    if (formula->dbgInfo.data != NIL(void)){
      (*formula->dbgInfo.freeFn)(formula);
      formula->dbgInfo.data = NIL(void);
    }

  }

}

/**Function********************************************************************


  Synopsis    [Duplicates a CTL* formula.]

  Description [Recursively duplicate a formula. Does nothing if the formula
  is NIL. Does not copy mdd for states, underapprox, overapprox, dbgInfo.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_FormulaDup(
  Ctlsp_Formula_t * formula)
{
  Ctlsp_Formula_t *result = NIL(Ctlsp_Formula_t);

  if ( formula == NIL(Ctlsp_Formula_t)) {
        return NIL(Ctlsp_Formula_t);
  }

  result = ALLOC(Ctlsp_Formula_t, 1);

  result->type                    = formula->type;
  result->class_                  = formula->class_;
  result->CTLclass                = formula->CTLclass;
  result->states                  = NIL(mdd_t);
  result->underapprox             = NIL(mdd_t);
  result->overapprox              = NIL(mdd_t);
  result->refCount                = 1;
  result->dbgInfo.data            = NIL(void);
  result->dbgInfo.freeFn          = (Ctlsp_DbgInfoFreeFn) NULL;
  result->dbgInfo.convertedFlag   = FALSE;
  result->dbgInfo.originalFormula = NIL(Ctlsp_Formula_t);

  if ( formula->type != Ctlsp_ID_c )  {
    result->left  = Ctlsp_FormulaDup(formula->left);
    result->right = Ctlsp_FormulaDup(formula->right);
  }
  else {
    result->left  = (Ctlsp_Formula_t *) util_strsav((char *)formula->left );
    result->right = (Ctlsp_Formula_t *) util_strsav((char *)formula->right );
  }

  return result;
}

/**Function********************************************************************

  Synopsis    [Frees an array of CTL* formulas.]

  Description [Calls CtlspFormulaDecrementRefCount on each formula in
  formulaArray, and then frees the array itself. It is okay to call this
  function with an empty array, but it is an error to call it with a NULL
  array.]

  SideEffects []

  SeeAlso     [Ctlsp_FormulaFree]

******************************************************************************/
void
Ctlsp_FormulaArrayFree(
  array_t * formulaArray /* of Ctlsp_Formula_t  */)
{
  int i;
  int numFormulas = array_n(formulaArray);

  for (i = 0; i < numFormulas; i++) {
    Ctlsp_Formula_t *formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i);

    CtlspFormulaDecrementRefCount(formula);
  }

  array_free(formulaArray);
}
/**Function********************************************************************

  Synopsis    [Converts an array of CTL formulae to a multi-rooted DAG.]

  Description [The function hashes each subformula of a formula
  (including the formula itself) into a uniqueTable.  It returns an
  array containing the roots of the multi-rooted DAG thus created by
  the sharing of the subformulae.  It is okay to call this function
  with an empty array (in which case an empty array is returned), but
  it is an error to call it with a NULL array.]

  SideEffects [A formula in formulaArray might be freed if it had been
  encountered as a subformula of some other formula. Other formulae in
  formulaArray might be present in the returned array. Therefore, the
  formulae in formulaArray should not be freed. Only formulaArray
  itself should be freed.



  RB:  What does that mean?

  I understand this as follows.  Copies of the formulae are not made,
  but rather pointers to the argument subformulae are kept.  Hence, not only
  should the formulae in the result not be freed, but also you cannot free the
  argument before you are done with the result.  Furthermore, by invocation of
  this function, the argument gets altered.  It is still valid, but pointers
  may have changed.  Is this correct?


  RB rewrite: A formula in formulaArray is freed if it is encountered as a
  subformula of some other formula. Other formulae in formulaArray might be
  present in the returned array. Therefore, the formulae in formulaArray should
  not be freed. Only formulaArray itself should be freed.]

  SeeAlso     []

******************************************************************************/
array_t *
Ctlsp_FormulaArrayConvertToDAG(
  array_t *formulaArray)
{
  int i;
  Ctlsp_Formula_t *formula, *uniqueFormula;
  st_table *uniqueTable = st_init_table(FormulaCompare, FormulaHash);
  int numFormulae = array_n(formulaArray);
  array_t *rootsOfFormulaDAG = array_alloc(Ctlsp_Formula_t *, numFormulae);

  for(i=0; i < numFormulae; i++) {
    formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i);
    uniqueFormula = FormulaHashIntoUniqueTable(formula, uniqueTable);
    if(uniqueFormula != formula) {
      CtlspFormulaDecrementRefCount(formula);
      CtlspFormulaIncrementRefCount(uniqueFormula);
      array_insert(Ctlsp_Formula_t *, rootsOfFormulaDAG, i, uniqueFormula);
    }
    else
      array_insert(Ctlsp_Formula_t *, rootsOfFormulaDAG, i, formula);
  }
  st_free_table(uniqueTable);
  return rootsOfFormulaDAG;
}

/**Function********************************************************************

  Synopsis    [Creates a CTL formula with the specified fields.]

  Description [Allocates a Ctlsp_Formula_t, and sets the 2 fields given as
  arguments.  If the type is Ctlsp_ID_c, then the left and right fields
  should contain a pointer to a variable name and a pointer to a value
  respectively. Otherwise, the two fields point to subformulas. refCount is
  set to 1. The states field is set to NULL, the converted flag is set to
  FALSE, and the originalFormula field is set to NULL.]

  Comment     []

  SideEffects []

  SeeAlso     [CtlspFormulaDecrementRefCount]

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_FormulaCreate(
  Ctlsp_FormulaType  type,
  void * left_,
  void * right_)
{
  Ctlsp_Formula_t *formula = ALLOC(Ctlsp_Formula_t, 1);
  Ctlsp_Formula_t *left    = (Ctlsp_Formula_t *) left_;
  Ctlsp_Formula_t *right   = (Ctlsp_Formula_t *) right_;

  formula->type                    = type;
  formula->left                    = left;
  formula->right                   = right;
  formula->states                  = NIL(mdd_t);
  formula->underapprox             = NIL(mdd_t);
  formula->overapprox              = NIL(mdd_t);
  formula->refCount                = 1;
  formula->dbgInfo.data            = NIL(void);
  formula->dbgInfo.freeFn          = (Ctlsp_DbgInfoFreeFn) NULL;
  formula->dbgInfo.convertedFlag   = FALSE;
  formula->dbgInfo.originalFormula = NIL(Ctlsp_Formula_t);
  formula->top                     = 0;
  formula->compareValue            = 0;
  formula->class_                  = Ctlsp_propformula_c;
  formula->CTLclass                = Ctlsp_CTL_c;
  formula->rhs                     = 0;

  if (left == NIL(Ctlsp_Formula_t)){
    return formula;
  }

  switch(formula->type) {
    case Ctlsp_OR_c:
    case Ctlsp_AND_c:
    case Ctlsp_THEN_c:
    case Ctlsp_XOR_c:
    case Ctlsp_EQ_c:
      Ctlsp_FormulaSetClass(formula, table1(Ctlsp_FormulaReadClass(left),Ctlsp_FormulaReadClass(right)));
      if ((Ctlsp_FormulaReadClassOfCTL(left)  ==  Ctlsp_CTL_c) &&
          (Ctlsp_FormulaReadClassOfCTL(right) == Ctlsp_CTL_c)){
        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_CTL_c);
      } else {
        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_NotCTL_c);
      }
      break;
    case Ctlsp_NOT_c:
      Ctlsp_FormulaSetClass(formula, Ctlsp_FormulaReadClass(left));
      Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_FormulaReadClassOfCTL(left));
      break;
    case Ctlsp_E_c:
    case Ctlsp_A_c:
      Ctlsp_FormulaSetClass(formula, Ctlsp_stateformula_c);
      if (Ctlsp_FormulaReadClassOfCTL(left) ==  Ctlsp_PathCTL_c) {
        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_CTL_c);
      } else {
        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_NotCTL_c);
      }
      break;
    case Ctlsp_G_c:
    case Ctlsp_F_c:
      Ctlsp_FormulaSetClass(formula, table2(Ctlsp_FormulaReadClass(left)));
      if (Ctlsp_FormulaReadClassOfCTL(left) ==  Ctlsp_CTL_c){
        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_PathCTL_c);
      } else {
        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_NotCTL_c);
      }
      break;
    case Ctlsp_U_c:
    case Ctlsp_R_c:
    case Ctlsp_W_c:
      Ctlsp_FormulaSetClass(formula, table3(Ctlsp_FormulaReadClass(left),Ctlsp_FormulaReadClass(right)));
      if ((Ctlsp_FormulaReadClassOfCTL(left) ==  Ctlsp_CTL_c) &&
          (Ctlsp_FormulaReadClassOfCTL(right) == Ctlsp_CTL_c)) {
        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_PathCTL_c);
      } else {
        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_NotCTL_c);
      }
      break;
    case Ctlsp_X_c:
      Ctlsp_FormulaSetClass(formula, table2(Ctlsp_FormulaReadClass(left)));
      if (Ctlsp_FormulaReadClassOfCTL(left) ==  Ctlsp_CTL_c){

        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_PathCTL_c);
      }  else {
        Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_NotCTL_c);
      }
      break;
    default:
      break;
  }
  return formula;
}

/**Function********************************************************************

  Synopsis    [Creates a CTL* formula with disjunction of atomic propositions]

  Description [This function returns Ctlsp_Formula_t for name = {v1,v2,...}.
  In case of failure, a NULL pointer is returned.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_FormulaCreateOr(
  char *name,
  char *valueStr)
{
  Ctlsp_Formula_t *formula, *tempFormula;
  char *preStr;

  preStr = strtok(valueStr,",");
  formula = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(name),
                               util_strsav(preStr));
  if (formula == NIL(Ctlsp_Formula_t)) {
     return NIL(Ctlsp_Formula_t);
  }
  while ((preStr = strtok(NIL(char),",")) != NIL(char)) {
    tempFormula = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(name),
                                     util_strsav(preStr));
    if (tempFormula == NIL(Ctlsp_Formula_t)) {
      Ctlsp_FormulaFree(formula);
      return NIL(Ctlsp_Formula_t);
    }
    formula = Ctlsp_FormulaCreate(Ctlsp_OR_c,formula,tempFormula);
  }
  return formula;
}


/**Function********************************************************************

  Synopsis    [Creates a CTL* formula with conjunction of atomic propositions]

  Description [This function returns Ctlsp_Formula_t for nameVector =
  value, nameVector is a form of var[i:j] or var<j:j> and value is any
  integer n or binary string starting with 'b' or 'x', for instance,
  b0011 or x100. If n does not fit in var[i:j] or the size of the binary
  string is not matched with var[i:j], NULL pointer is returned]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_FormulaCreateVectorAnd(
  char *nameVector,
  char *value)
{
  Ctlsp_Formula_t *formula, *tempFormula;
  int startValue, endValue, inc, i,j, interval,startInd;
  char *binValueStr, *varName, *name;
  char *bitValue;

  varName = CtlspGetVectorInfoFromStr(nameVector,&startValue,&endValue,&interval,&inc);
  binValueStr = ALLOC(char,interval+1);
  if (!CtlspStringChangeValueStrToBinString(value,binValueStr,interval) ){
     FREE(varName);
     FREE(binValueStr);
     return NIL(Ctlsp_Formula_t);
  }

  name = ALLOC(char,MAX_LENGTH_OF_VAR_NAME);
  (void) sprintf(name,"%s[%d]",varName,startValue);
  (void) CtlspChangeBracket(name);

  bitValue = ALLOC(char,2);
  bitValue[0] = binValueStr[0];
  bitValue[1] = '\0';

  formula = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(name),
                               util_strsav(bitValue));
  j = 0;
  startInd = startValue;
  for(i=startValue;i!=endValue;i=i+inc){
     startInd += inc;
     j++;
     (void) sprintf(name,"%s[%d]",varName,startInd);
     (void) CtlspChangeBracket(name);
     bitValue[0] = binValueStr[j];
     tempFormula = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(name),
                                      util_strsav(bitValue));
     formula = Ctlsp_FormulaCreate(Ctlsp_AND_c,formula,tempFormula);
  }
  FREE(varName);
  FREE(name);
  FREE(binValueStr);
  FREE(bitValue);
  return formula;
}


/**Function********************************************************************

  Synopsis    [Creates a CTL formula with OR of Vector AND]

  Description [This function returns Ctlsp_Formula_t for nameVector = valueStr,
  nameVector is a form of var[i:j] or var<j:j>, valueStr is "k,l,...,q",
  and k,l,...,q is either integer or binary string.  Binary string starting
  with 'b', for instance, b0011. If n is not fitted in var[i:j] or size of
  binary string is not matched with var[i:j], NULL pointer is returned]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_FormulaCreateVectorOr(
  char *nameVector,
  char *valueStr)
{
  Ctlsp_Formula_t *formula,*tempFormula;
  char *preStr;

  preStr = strtok(valueStr,",");
  formula = Ctlsp_FormulaCreateVectorAnd(nameVector,preStr);
  if ( formula == NIL(Ctlsp_Formula_t)){
     Ctlsp_FormulaFree(formula);
     return NIL(Ctlsp_Formula_t);
  }
  while( (preStr = strtok(NIL(char),",")) != NIL(char) ){
     tempFormula = Ctlsp_FormulaCreateVectorAnd(nameVector,preStr);
     if ( tempFormula == NIL(Ctlsp_Formula_t)){
        Ctlsp_FormulaFree(formula);
        return NIL(Ctlsp_Formula_t);
     }
     formula = Ctlsp_FormulaCreate(Ctlsp_OR_c,formula,tempFormula);
  }
  return formula;
}


/**Function********************************************************************

  Synopsis    [Creates a CTL formula for equivalent property]

  Description [This function assumes that each child is defined in binary
  domain. Enumerate type is not supported]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_FormulaCreateEquiv(
  char *left,
  char *right)
{
  Ctlsp_Formula_t *formula,*formula1,*formula2;

  char *one;
  char *zero;

  one = "1";
  zero = "0";

  formula1 = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(left),
                                 util_strsav(one));
  formula2 = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(right),
                                 util_strsav(zero));
  formula = Ctlsp_FormulaCreate(Ctlsp_XOR_c,formula1,formula2);
  return formula;
}

/**Function********************************************************************

  Synopsis    [Creates a CTL formula for equivalent of vector]

  Description [This function returns a formula, which is the AND of a bitwise
  equivalence]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_FormulaCreateVectorEquiv(
  char *left,
  char *right)
{
  Ctlsp_Formula_t *formula,*tempFormula;
  char *leftName,*rightName;
  char *leftVar, *rightVar;
  int  leftStart,leftEnd,rightStart,rightEnd,leftInterval,rightInterval;
  int  leftInc,rightInc,leftInd,rightInd,i;

  leftName  = CtlspGetVectorInfoFromStr(left,&leftStart,&leftEnd,&leftInterval,&leftInc);
  rightName = CtlspGetVectorInfoFromStr(right,&rightStart,&rightEnd,&rightInterval,&rightInc);
  if (leftInterval != rightInterval){
     return NIL(Ctlsp_Formula_t);
  }
  leftVar = ALLOC(char,MAX_LENGTH_OF_VAR_NAME);
  (void) sprintf(leftVar,"%s[%d]",leftName,leftStart);
  (void) CtlspChangeBracket(leftVar);
  rightVar = ALLOC(char,MAX_LENGTH_OF_VAR_NAME);
  (void) sprintf(rightVar,"%s[%d]",rightName,rightStart);
  (void) CtlspChangeBracket(rightVar);

  formula = Ctlsp_FormulaCreateEquiv(leftVar,rightVar);
  leftInd  = leftStart;
  rightInd = rightStart;
  for(i=leftStart;i!=leftEnd;i+=leftInc){
     leftInd  += leftInc;
     rightInd += rightInc;
     (void) sprintf(leftVar,"%s[%d]",leftName,leftInd);
     (void) CtlspChangeBracket(leftVar);
     (void) sprintf(rightVar,"%s[%d]",rightName,rightInd);
     (void) CtlspChangeBracket(rightVar);
     tempFormula = Ctlsp_FormulaCreateEquiv(leftVar,rightVar);
     formula = Ctlsp_FormulaCreate(Ctlsp_AND_c,formula,tempFormula);
  }
  FREE(leftName);
  FREE(rightName);
  FREE(leftVar);
  FREE(rightVar);
  return formula;
}


/**Function********************************************************************

  Synopsis    [Creates a CTL formula for multiple X]

  Description [This function returns a formula, which is the multiple
  times of AX. The given string includes the number of depth]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_FormulaCreateXMult(
  char *string,
  Ctlsp_Formula_t *formula)
{
  int i,num;
  char *str, *ptr;
  Ctlsp_Formula_t *result = NIL(Ctlsp_Formula_t);
  str = strchr(string,':');
  if ( str == NULL) return(NIL(Ctlsp_Formula_t));
  str++;

  num = strtol(str,&ptr,0);

  for(i=0;i<num;i++){
    result = Ctlsp_FormulaCreate(Ctlsp_X_c, formula, NIL(Ctlsp_Formula_t));
    Ctlsp_FormulaSetClass(result, table2(Ctlsp_FormulaReadClass(formula)));
    if (Ctlsp_FormulaReadClassOfCTL(formula) ==  Ctlsp_CTL_c){
      Ctlsp_FormulaSetClassOfCTL(result, Ctlsp_PathCTL_c);
     }
    else{
      Ctlsp_FormulaSetClassOfCTL(result, Ctlsp_NotCTL_c);
     }
    formula = result;
    }
  return result;
}

/**Function********************************************************************

  Synopsis    [Creates a CTL* formula for multiple EX]

  Description [This function returns a formula, which is the multiple
  times of EX. The given string includes the number of depth]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_FormulaCreateEXMult(
  char *string,
  Ctlsp_Formula_t *formula)
{
  int i,num;
  char *str, *ptr;
  Ctlsp_Formula_t *result = NIL(Ctlsp_Formula_t);

  str = strchr(string,':');
  if ( str == NULL) return(NIL(Ctlsp_Formula_t));
  str++;

  num = strtol(str,&ptr,0);

  for(i=0;i<num;i++){
    result = Ctlsp_FormulaCreate(Ctlsp_X_c, formula, NIL(Ctlsp_Formula_t));
    Ctlsp_FormulaSetClass(result, table2(Ctlsp_FormulaReadClass(formula)));
    result = Ctlsp_FormulaCreate(Ctlsp_E_c, result, NIL(Ctlsp_Formula_t));
    Ctlsp_FormulaSetClass(result, Ctlsp_stateformula_c);
    if (Ctlsp_FormulaReadClassOfCTL(formula) ==  Ctlsp_CTL_c)
    {
      Ctlsp_FormulaSetClassOfCTL(result, Ctlsp_CTL_c);
    }
    else
    {
      Ctlsp_FormulaSetClassOfCTL(result, Ctlsp_NotCTL_c);
    }
    formula = result;
  }

  return result;
}

/**Function********************************************************************

  Synopsis    [Creates a CTL* formula for multiple AX]

  Description [This function returns a formula, which is the multiple
  times of AX. The given string includes the number of depth]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_FormulaCreateAXMult(
  char *string,
  Ctlsp_Formula_t *formula)
{
  int i,num;
  char *str, *ptr;
  Ctlsp_Formula_t *result = NIL(Ctlsp_Formula_t);

  str = strchr(string,':');
  if ( str == NULL) return(NIL(Ctlsp_Formula_t));
  str++;

  num = strtol(str,&ptr,0);

  for(i=0;i<num;i++){
    result = Ctlsp_FormulaCreate(Ctlsp_X_c, formula, NIL(Ctlsp_Formula_t));
    Ctlsp_FormulaSetClass(result, table2(Ctlsp_FormulaReadClass(formula)));
    result = Ctlsp_FormulaCreate(Ctlsp_A_c, result, NIL(Ctlsp_Formula_t));
    Ctlsp_FormulaSetClass(result, Ctlsp_stateformula_c);
    if (Ctlsp_FormulaReadClassOfCTL(formula) ==  Ctlsp_CTL_c)
    {
      Ctlsp_FormulaSetClassOfCTL(result, Ctlsp_CTL_c);
    }
    else
    {
      Ctlsp_FormulaSetClassOfCTL(result, Ctlsp_NotCTL_c);
    }
    formula = result;
  }

  return result;
}


/**Function********************************************************************

  Synopsis    [Returns a string for each formula type.]

  Description [Returns a string for each formula type.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
char *
Ctlsp_FormulaGetTypeString(Ctlsp_Formula_t *formula)
{
  char *result;

  switch(formula->type) {
    /*
     * The cases are listed in rough order of their expected frequency.
     */
    case Ctlsp_ID_c:
      result = util_strsav("ID");
      break;
    case Ctlsp_OR_c:
      result = util_strsav("OR");
      break;
    case Ctlsp_AND_c:
      result = util_strsav("AND");
      break;
    case Ctlsp_THEN_c:
      result = util_strsav("THEN");
      break;
    case Ctlsp_XOR_c:
      result = util_strsav("XOR");
      break;
    case Ctlsp_EQ_c:
      result = util_strsav("EQ");
      break;
    case Ctlsp_NOT_c:
      result = util_strsav("NOT");
      break;
    case Ctlsp_E_c:
      result = util_strsav("E");
      break;
    case Ctlsp_G_c:
      result = util_strsav("G");
      break;
    case Ctlsp_F_c:
      result = util_strsav("F");
      break;
    case Ctlsp_U_c:
      result = util_strsav("U");
      break;
    case Ctlsp_R_c:
      result = util_strsav("R");
      break;
    case Ctlsp_W_c:
      result = util_strsav("W");
      break;
    case Ctlsp_X_c:
      result = util_strsav("X");
      break;
    case Ctlsp_A_c:
      result = util_strsav("A");
      break;
    case Ctlsp_TRUE_c:
      result = util_strsav("TRUE");
      break;
    case Ctlsp_FALSE_c:
      result = util_strsav("FALSE");
      break;
    case Ctlsp_Init_c:
      result = util_strsav("Init");
      break;
    case Ctlsp_Cmp_c:
      result = util_strsav("Cmp");
      break;
    case Ctlsp_Fwd_c:
      result = util_strsav("Fwd");
      break;
      /*    case Ctlsp_EY_c:
      result = util_strsav("EY");
      break;*/
      /*  case Ctlsp_EH_c:
      result = util_strsav("EH");
      break;
      break;*/
    default:
      fail("Unexpected type");
  }
  return(result);
}


/**Function********************************************************************

  Synopsis           [Tests if a formula is a ACTL, ECTL or mixed formula.]

  Description        [Tests if a formula is a ACTL, ECTL or mixed formula. '0'
  for ECTL, '1' for ACTL and '2' for a mixed formula. If a formula doesn't have
  any path quantifier, '3' is returned.]

  SideEffects        []

  SeeAlso            []

******************************************************************************/
Ctlsp_FormulaClass
Ctlsp_CheckClassOfExistentialFormula(
  Ctlsp_Formula_t *formula)
{
  Ctlsp_FormulaClass result;

  result = CtlspCheckClassOfExistentialFormulaRecur(formula, FALSE);

  return result;
} /* End of Ctlsp_CheckTypeOfExistentialFormula */

/**Function********************************************************************

  Synopsis [Tests if an array of simple existential formulae has only
  ACTL, only ECTL or mixture of formula.]

  Description        [Returns Ctlsp_ECTL_c if the array contains only
  ECTL formulae, Ctlsp_ACTL_c if it contains only ACTL formulae,
  Ctlsp_QuantifierFree_c if there are no quantifiers in any formulae,
  and Ctlsp_Mixed otherwise.]

  SideEffects        []

  SeeAlso            [Ctlsp_CheckClassOfExistentialFormula]

******************************************************************************/
Ctlsp_FormulaClass
Ctlsp_CheckClassOfExistentialFormulaArray(
  array_t *formulaArray)
{
  Ctlsp_FormulaClass result;
  Ctlsp_Formula_t *formula;
  int formulanr;

  result = Ctlsp_QuantifierFree_c;
  arrayForEachItem(Ctlsp_Formula_t *, formulaArray, formulanr, formula){
    Ctlsp_FormulaClass  formulaType;
    formulaType = Ctlsp_CheckClassOfExistentialFormula(formula);
    result = CtlspResolveClass(result, formulaType);
    if(result == Ctlsp_Mixed_c)
      return result;
  }
  return result;
} /* End of Ctlsp_CheckTypeOfExistentialFormulaArray */

/**Function********************************************************************

  Synopsis    [Get the class of a formula]

  Description [Get the current class of a CTL* sub-formula]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_ClassOfFormula
Ctlsp_FormulaReadClass(Ctlsp_Formula_t *formula)
{
  return formula->class_;
}

/**Function********************************************************************

  Synopsis    [Set the class of a formula]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
Ctlsp_FormulaSetClass(Ctlsp_Formula_t *formula, Ctlsp_ClassOfFormula newClass)
{
  if (formula == NIL(Ctlsp_Formula_t)){
    return;
  }
  formula->class_ = newClass;
}


/**Function********************************************************************

  Synopsis    [Get the type of a CTL formula]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/

Ctlsp_ClassOfCTLFormula
Ctlsp_FormulaReadClassOfCTL(Ctlsp_Formula_t *formula)
{
  return formula->CTLclass;
}

/**Function********************************************************************

  Synopsis    [Set the class of CTL]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
Ctlsp_FormulaSetClassOfCTL(
  Ctlsp_Formula_t *formula,
  Ctlsp_ClassOfCTLFormula newCTLclass)
{
  if (formula == NIL(Ctlsp_Formula_t)){
    return;
  }
  formula->CTLclass = newCTLclass;
}

/**Function********************************************************************

  Synopsis    [Returns an array of LTL formulae.]

  Description [Returns an array of LTL formulae given the array of CTL*
               formulae.
               If any of the CTL* formula is not LTL formula, retuns NIL.
               The return LTL formulae share absolutely nothing with the
               original CTL* formulae (not even a string).]

  SideEffects []

  SeeAlso     []

******************************************************************************/
array_t *
Ctlsp_FormulaArrayConvertToLTL(
   array_t *formulaArray)
{
  array_t *ltlFormulaArray;
  int i;

  ltlFormulaArray = array_alloc(Ctlsp_Formula_t *, 0);

  /* Check if all CTL* formulas are LTL formulas */
  for (i = 0; i < array_n(formulaArray); i++) {
    Ctlsp_Formula_t *formula, *ltlFormula;

    formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i);

    if (!Ctlsp_isLtlFormula(formula)){
     Ctlsp_FormulaArrayFree(ltlFormulaArray);
     return NIL(array_t);
    }
    ltlFormula = Ctlsp_FormulaDup(formula);
    array_insert_last(Ctlsp_Formula_t *, ltlFormulaArray, ltlFormula);

   } /* For Loop */
  return ltlFormulaArray;
} /*  Ctlsp_FormulaArrayConvertToLTL() */

/**Function********************************************************************

  Synopsis [Returns an array of CTL formulas from the parsed array of
  CTL* formulas]

  Description [This function takes an array of CTL* formulae and returns
               an array of CTL formulae if applicable.  Function
               returns NIL if any CTL * formula can't be converted to
               CTL formula.  The returned CTL formulae share absolutely
               nothing with the original CTL* formulae (not even a
               string).]

  SideEffects []

  SeeAlso     [Ctlsp_FormulaConvertToCTL]

******************************************************************************/
array_t *
Ctlsp_FormulaArrayConvertToCTL(
  array_t *formulaArray)
{
  array_t *CtlFormulaArray;
  int i;

  CtlFormulaArray = array_alloc(Ctlp_Formula_t *, 0);

  /* Convert each formula in the array to CTL */
  for (i = 0; i < array_n(formulaArray); i++) {
    Ctlsp_Formula_t *formula;
    Ctlp_Formula_t *newFormula;

    formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i);
    newFormula = Ctlsp_FormulaConvertToCTL(formula);

    if (newFormula !=  NIL(Ctlp_Formula_t)){
       array_insert_last(Ctlp_Formula_t *, CtlFormulaArray, newFormula);
    }
    else{
       (void) fprintf(vis_stderr, "** ctl* error : Can't Convert CTL* No. %d to CTL formula\n\n", i);
       Ctlp_FormulaArrayFree(CtlFormulaArray);
       return NIL(array_t);
    }
   } /* For Loop */
  return CtlFormulaArray;
} /*  Ctlsp_FormulaArrayConvertToCTL() */

/**Function********************************************************************

  Synopsis    [Convert an CTL* formula to CTL formula]

  Description [This function takes a formula in CTL* and returns a CTL formula
  if applicable.  CTL* consists of two formula classes: state formulas and
  path formulas. CTL formula is a state formula.  CTL* formula can be
  converted to CTL formula if the CTL* formula is state formula.
  Note: This function must be called for each formula in a given array.]

  SideEffects []

  SeeAlso     [Ctlsp_FormulaArrayConvertToCTL]

******************************************************************************/
Ctlp_Formula_t *
Ctlsp_FormulaConvertToCTL(
  Ctlsp_Formula_t *formula)
{
  if (Ctlsp_FormulaReadClassOfCTL(formula) ==  Ctlsp_CTL_c) {/* CTL* can be converted to CTL */
    return CtlspFormulaConvertToCTL(formula);
  }
  else{
    return NIL(Ctlp_Formula_t);
  }
} /*  Ctlsp_FormulaConvertToCTL() */

/**Function********************************************************************
  Synopsis    [Convert a propositional CTL* formula to CTL formula]

  Description [A wrapper to CtlspFormulaConvertToCTL]

  SideEffects []

  SeeAlso     [Ctlsp_FormulaArrayConvertToCTL]

******************************************************************************/
Ctlp_Formula_t *
Ctlsp_PropositionalFormulaToCTL(
  Ctlsp_Formula_t *formula)
{
    return CtlspFormulaConvertToCTL(formula);
}


/**Function********************************************************************

  Synopsis    [Return true if CTL* formula is a propositional formula.]

  Description []

  SideEffects []

  SeeAlso     [Ctlsp_FormulaReadClass()]

******************************************************************************/
int
Ctlsp_isPropositionalFormula(
  Ctlsp_Formula_t *formula)
{
  return (Ctlsp_FormulaReadClass(formula) == Ctlsp_propformula_c);
} /* Ctlsp_isPropositionalFormula() */

/**Function********************************************************************

  Synopsis    [Return true if CTL* formula is an CTL formula.]

  Description []

  SideEffects []

  SeeAlso     [Ctlsp_FormulaReadClassOfCTL()]

******************************************************************************/
int
Ctlsp_isCtlFormula(
  Ctlsp_Formula_t *formula)
{
  return (Ctlsp_FormulaReadClassOfCTL(formula) ==  Ctlsp_CTL_c);
} /* Ctlsp_isCtlFormula() */

/**Function********************************************************************

  Synopsis    [Return true if CTL* formula is an LTL formula.]

  Description [a formula is LTL formul if its one of the following:
               - Its class is Ctlsp_LTLformula_c
               - it is in the form A(Ctlsp_LTLformula_c).
               - Its class is Ctlsp_propformula_c.
               - it is in the form A(Ctlsp_propformula_c)
              ]
  SideEffects []

  SeeAlso     [Ctlsp_FormulaReadClass()]

******************************************************************************/
int
Ctlsp_isLtlFormula(
  Ctlsp_Formula_t *formula)
{
  if (Ctlsp_FormulaReadClass(formula) == Ctlsp_LTLformula_c){
    return 1;
  }
  if (Ctlsp_FormulaReadClass(formula) == Ctlsp_propformula_c){
    return 1;
  }
  if (formula->type ==  Ctlsp_A_c) {
    if ((Ctlsp_FormulaReadClass(formula->left) == Ctlsp_LTLformula_c) ||
        (Ctlsp_FormulaReadClass(formula->left) == Ctlsp_propformula_c)) {
      return 1;
      }
    else {
      return 0;
    }
  }
  return 0;
} /* Ctlsp_isLtlFormula() */

/**Function********************************************************************

  Synopsis    [Negate an LTL formula]

  Description [This function returns an abbreviation-free LTL formula
               of the negation of the input LTL formula. The returned
               formula share absolutely nothing with the input LTL
               formula.]

  Comment     []

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_LtllFormulaNegate(
  Ctlsp_Formula_t *ltlFormula)
{
  Ctlsp_Formula_t *negLtlFormula, *tmpLtlFormula;

  negLtlFormula = Ctlsp_FormulaCreate(Ctlsp_NOT_c, ltlFormula, NIL(Ctlsp_Formula_t));
  tmpLtlFormula = Ctlsp_LtlFormulaExpandAbbreviation(negLtlFormula);
  FREE(negLtlFormula);
  negLtlFormula = Ctlsp_LtlFormulaNegationNormalForm(tmpLtlFormula);
  if(negLtlFormula != tmpLtlFormula) {
    Ctlsp_FormulaFree(tmpLtlFormula);
  }
  tmpLtlFormula = Ctlsp_LtlFormulaSimpleRewriting(negLtlFormula);
  Ctlsp_FormulaFree(negLtlFormula);
  Ctlsp_LtlSetClass(tmpLtlFormula);

  return tmpLtlFormula;
} /* Ctlsp_LtllFormulaNegate() */

/**Function********************************************************************

  Synopsis    [Set the class of the LTL formula]

  Description [This function recursively sets the class of LTL subformula. For
  leave nodes, by default the class sets to Ctlsp_propformula_c when the node
  is created.]

  Comment     [The class filed of an LTL subformula will not be set if the
  programmer uses FormulaCreateWithType() and then later he adds its children.
  The correct way of creating a new node knowing its childeren is by using
  Ctlsp_FormulaCreate()]

  SideEffects []

  SeeAlso     [ctlspInt.h Ctlsp_FormulaCreate]

******************************************************************************/
void
Ctlsp_LtlSetClass(
  Ctlsp_Formula_t *formula)
{
  Ctlsp_Formula_t *left, *right;

  if (formula == NIL(Ctlsp_Formula_t)){
    return;
  }
  if (formula->type == Ctlsp_ID_c){
    return;
  }
  if (formula->type == Ctlsp_TRUE_c){
    return;
  }
  if (formula->type == Ctlsp_FALSE_c){
    return;
  }
  left  = formula->left;
  right = formula->right;

  Ctlsp_LtlSetClass(left);
  Ctlsp_LtlSetClass(right);

  switch(formula->type) {
    case Ctlsp_OR_c:
    case Ctlsp_AND_c:
    case Ctlsp_THEN_c:
    case Ctlsp_XOR_c:
    case Ctlsp_EQ_c:
      Ctlsp_FormulaSetClass(formula, table1(Ctlsp_FormulaReadClass(left),Ctlsp_FormulaReadClass(right)));
      break;
    case Ctlsp_NOT_c:
      Ctlsp_FormulaSetClass(formula, Ctlsp_FormulaReadClass(left));
      break;
    case Ctlsp_E_c:
    case Ctlsp_A_c:
      Ctlsp_FormulaSetClass(formula, Ctlsp_stateformula_c);
      break;
    case Ctlsp_G_c:
    case Ctlsp_F_c:
      Ctlsp_FormulaSetClass(formula, table2(Ctlsp_FormulaReadClass(left)));
      break;
    case Ctlsp_U_c:
    case Ctlsp_R_c:
    case Ctlsp_W_c:
      Ctlsp_FormulaSetClass(formula, table3(Ctlsp_FormulaReadClass(left),Ctlsp_FormulaReadClass(right)));
      break;
    case Ctlsp_X_c:
      Ctlsp_FormulaSetClass(formula, table2(Ctlsp_FormulaReadClass(left)));
      break;
    default:
      break;
  }
  return;
}

/**Function********************************************************************

  Synopsis    [Return TRUE iff formula is a "GF(propositional formula)".]

  Description [GFp = FALSE R (TRUE U p) in abbreviation-free LTL formulae.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
Ctlsp_LtlFormulaIsGFp(
  Ctlsp_Formula_t *formula)
{
 Ctlsp_Formula_t *rightChild;
 Ctlsp_Formula_t *leftChild;

 assert(formula != NIL(Ctlsp_Formula_t));

 if (Ctlsp_FormulaReadType(formula) == Ctlsp_R_c) {
   rightChild = Ctlsp_FormulaReadRightChild(formula);
   leftChild  = Ctlsp_FormulaReadLeftChild(formula);

   if ((Ctlsp_FormulaReadType(leftChild) == Ctlsp_FALSE_c) &&
       (Ctlsp_FormulaReadType(rightChild) == Ctlsp_U_c)){
     if ((Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(rightChild)) == Ctlsp_TRUE_c) &&
         (Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadRightChild(rightChild)))) {
       return TRUE;
     }
   }
 }

 return FALSE;
}/* Ctlsp_LtlFormulaIsGFp() */


/**Function********************************************************************

  Synopsis    [Return TRUE iff formula is a "G(propositional formula)".]

  Description [G(p) = FALSE R p in abbreviation-free LTL formulae.]

  SideEffects []

  SeeAlso     [Ctlsp_isPropositionalFormula]

******************************************************************************/
boolean
Ctlsp_LtlFormulaIsGp(
  Ctlsp_Formula_t *formula)
{
  assert(formula != NIL(Ctlsp_Formula_t));

  if ((Ctlsp_FormulaReadType(formula)== Ctlsp_G_c) &&
       Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadLeftChild(formula))){
    return TRUE;
  }
  if (Ctlsp_FormulaReadType(formula) == Ctlsp_R_c) {
    if ((Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(formula)) == Ctlsp_FALSE_c) &&
        (Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadRightChild(formula)))) {
      return TRUE;
    }
  }
  return FALSE;
} /* Ctlsp_LtlFormulaIsGp */

/**Function********************************************************************

  Synopsis    [Return TRUE iff formula is a "F(propositional formula)".]

  Description [F(p) = TRUE U p in abbreviation-free LTL formulae.]

  SideEffects []

  SeeAlso     [Ctlsp_isPropositionalFormula]

******************************************************************************/
boolean
Ctlsp_LtlFormulaIsFp(
  Ctlsp_Formula_t *formula)
{
  assert(formula != NIL(Ctlsp_Formula_t));

  if ((Ctlsp_FormulaReadType(formula)== Ctlsp_F_c) &&
      Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadLeftChild(formula))){
    return TRUE;
  }
  if (Ctlsp_FormulaReadType(formula) == Ctlsp_U_c) {
    if ((Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(formula)) == Ctlsp_TRUE_c) &&
        Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadRightChild(formula))) {
      return TRUE;
    }
  }
  return FALSE;
} /* Ctlsp_LtlFormulaIsFp */

#if 0
/**Function********************************************************************

  Synopsis    [Return TRUE iff formula is a safety property.]

  Description [ The characterization of LTL formula as a safety formula is
  taken from the paper by A. Prasad Sistla: Safety, Liveness and Fairness in
  Temporal Logic.
  Theorm 3.1 page 8: (For positive LTL formula: formula in Negation Normal Form).
    - Every propositional formula is a safety formula.
    - If f, g are safety formula, then so are
      - f AND g.
      - f OR  g.
      - X(f).
      - f W g. (unless temporal operator).
      - G(f).

  This function can only be applied to abbreviation-free LTL formulae. The
  formula must be in Negation Normal Form.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
boolean
Ctlsp_LtlFormulaIsSafety(
  Ctlsp_Formula_t *formula)
{
  assert(formula != NIL(Ctlsp_Formula_t));

  if (Ctlsp_isPropositionalFormula(formula)){
    return TRUE;
  }
  if (Ctlsp_LtlFormulaIsW(formula)){
    return Ctlsp_LtlFormulaIsSafety(Ctlsp_FormulaReadLeftChild(formula)) &&
      Ctlsp_LtlFormulaIsSafety(Ctlsp_FormulaReadRightChild(formula));
  }
  swtich (Ctlsp_FormulaReadType(formula)){
  case Ctlsp_AND_c:
  case Ctlsp_OR_c:
    return Ctlsp_LtlFormulaIsSafety(Ctlsp_FormulaReadLeftChild(formula)) &&
           Ctlsp_LtlFormulaIsSafety(Ctlsp_FormulaReadRightChild(formula));
  case Ctlsp_X_c:
    return Ctlsp_LtlFormulaIsSafety(Ctlsp_FormulaReadLeftChild(formula));
  case Ctlsp_NOT_c:
  case Ctlsp_U_c:
  case Ctlsp_R_c:
    return FALSE;
  default:
    fail("unexpected node type in abbreviation-free formula\n");
    return FALSE; /* not reached */
  }

  /*    == Ctlsp_F_c) &&
      Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadLeftChild(formula))){
    return TRUE;
    } */
  if (Ctlsp_FormulaReadType(formula) == Ctlsp_U_c) {
    if (Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(formula) == Ctlsp_TRUE_c) &&
        Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadRightChild(formula))) {
      return TRUE;
    }
  }
  return FALSE;
} /* Ctlsp_LtlFormulaIsSafety */
#endif


/**Function********************************************************************

  Synopsis    [Add fairness constraints to an array of LTL formulae.]

  Description [This function modifies an array of LTL formulae by adding to
  each of them a fairness constraint.  This fairness constraint is the
  conjunction of all fairness constraints in constraintArray.  For consistency
  with what done throughout VIS, each line in the file is interpreted as a
  condition that must hold infinitely often.  The function assumes that the
  incoming array only contains LTL formulae.  The returned formulae are not
  normalized and not converted to DAGs.]

  SideEffects [formulaArray is modified]

  SeeAlso []

******************************************************************************/
void
Ctlsp_FormulaArrayAddLtlFairnessConstraints(
  array_t *formulaArray     /* array of LTL formulae */,
  array_t *constraintArray /* array of fairness constraints */)
{
  Ctlsp_Formula_t *formula;     /* a generic LTL formula */
  Ctlsp_Formula_t *fairness;    /* a generic fairness constraint */
  int i;                        /* iteration variable */

  assert(formulaArray != NIL(array_t));
  assert(constraintArray != NIL(array_t));
  /*
   * Create the overall fairness constraints.  If the given constraints
   * are C_1, C_2, ..., C_k, build the formula /\_i GF C_i.
   */
  fairness = NIL(Ctlsp_Formula_t);
  arrayForEachItem(Ctlsp_Formula_t *, constraintArray, i, formula) {
    Ctlsp_Formula_t *finally;
    Ctlsp_Formula_t *globally;
    finally =  Ctlsp_FormulaCreate(Ctlsp_F_c, formula, NIL(Ctlsp_Formula_t));
    globally = Ctlsp_FormulaCreate(Ctlsp_G_c, finally, NIL(Ctlsp_Formula_t));
    if (i == 0) {
      fairness = globally;
    } else {
      fairness = Ctlsp_FormulaCreate(Ctlsp_AND_c, fairness, globally);
    }
  }
  /* Empty fairness constraint files are forbidden. */
  assert(fairness != NIL(Ctlsp_Formula_t));

  /*
   * Add fairness to each given formula: Replace f_i by (fairness -> f_i).
   */
  arrayForEachItem(Ctlsp_Formula_t *, formulaArray, i, formula) {
    Ctlsp_Formula_t *modified;
    modified = Ctlsp_FormulaCreate(Ctlsp_THEN_c,
                                   Ctlsp_FormulaDup(fairness), formula);
    array_insert(Ctlsp_Formula_t *, formulaArray, i, modified);
  }
  Ctlsp_FormulaFree(fairness);

} /* Ctlsp_FormulaArrayAddLtlFairnessConstraints */


/**Function********************************************************************

  Synopsis    [Translate a CTL formula into a CTL* formula.]

  Description [Translate a CTL formula into a CTL* formula.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_CtlFormulaToCtlsp(Ctlp_Formula_t *F)
{
    Ctlsp_Formula_t *Fsp;
    Ctlp_FormulaType Ftype;
    Ctlsp_FormulaType Fsptype;

    if (F == NIL(Ctlp_Formula_t))
        return NIL(Ctlsp_Formula_t);

    Ftype = Ctlp_FormulaReadType(F);
    Fsptype = (Ctlsp_FormulaType) Ftype;

    if (Ftype == Ctlp_TRUE_c) {
        Fsp = Ctlsp_FormulaCreate(Ctlsp_TRUE_c, NIL(Ctlsp_Formula_t),
                                  NIL(Ctlsp_Formula_t));
    }else if (Ftype == Ctlp_FALSE_c) {
        Fsp = Ctlsp_FormulaCreate(Ctlsp_FALSE_c, NIL(Ctlsp_Formula_t),
                                  NIL(Ctlsp_Formula_t));
    }else if (Ftype == Ctlp_ID_c) {
        char *nameString = Ctlp_FormulaReadVariableName(F);
        char *valueString = Ctlp_FormulaReadValueName(F);
        Fsp = Ctlsp_FormulaCreate(Ctlsp_ID_c,
                                  util_strsav(nameString),
                                  util_strsav(valueString));
    }else {
        Ctlp_Formula_t *Fleft = Ctlp_FormulaReadLeftChild(F);
        Ctlp_Formula_t *Fright = Ctlp_FormulaReadRightChild(F);
        Ctlsp_Formula_t *Fspleft, *Fspright;
        Fspleft = Ctlsp_CtlFormulaToCtlsp(Fleft);
        Fspright = Ctlsp_CtlFormulaToCtlsp(Fright);
        switch(Ftype) {
        case Ctlp_NOT_c:
            Fsptype = Ctlsp_NOT_c;
            break;
        case Ctlp_AND_c:
            Fsptype = Ctlsp_AND_c;
            break;
        case Ctlp_OR_c:
            Fsptype = Ctlsp_OR_c;
            break;
        case Ctlp_THEN_c:
            Fsptype = Ctlsp_THEN_c;
            break;
        case Ctlp_EQ_c:
            Fsptype = Ctlsp_EQ_c;
            break;
        case Ctlp_XOR_c:
            Fsptype = Ctlsp_XOR_c;
            break;
        default:
            assert(0);
        }
        if (Fspleft)
            CtlspFormulaIncrementRefCount(Fspleft);
        if (Fspright)
            CtlspFormulaIncrementRefCount(Fspright);
        Fsp = Ctlsp_FormulaCreate(Fsptype, Fspleft, Fspright);
    }

    return Fsp;
}


/**Function********************************************************************

  Synopsis    [Return a LTL formula with the abbreviations expanded.]

  Description [The input must be a legal LTL formula. The result shares
  nothing with the input, not even a string; The result itself  does not share
  sub-formulae. The translation rule is:
    Ctlsp_THEN_c        a->b  :   !a + b
    Ctlsp_EQ_c          a<->b :   a*b +!a*!b
    Ctlsp_XOR_c         a^b   :   a*!b + !a*b
    Ctlsp_F_c           Fa    :   true U a
    Ctlsp_G_c           Ga    :   false R a
    Ctlsp_A_c           Aa    :   a
    ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_LtlFormulaExpandAbbreviation(
  Ctlsp_Formula_t *formula)
{
  Ctlsp_Formula_t *new_;

  if (formula == NIL(Ctlsp_Formula_t))
    return formula;

  switch (formula->type) {
  case Ctlsp_THEN_c:
    /* a -> b  :: !a + b */
    new_ = FormulaCreateWithType(Ctlsp_OR_c);
    new_->left = FormulaCreateWithType(Ctlsp_NOT_c);
    new_->left->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
    new_->right = Ctlsp_LtlFormulaExpandAbbreviation(formula->right);
    break;
  case Ctlsp_EQ_c:
    /* a <-> b  :: a*b + !a*!b */
    new_ = FormulaCreateWithType(Ctlsp_OR_c);
    new_->left = FormulaCreateWithType(Ctlsp_AND_c);
    new_->right= FormulaCreateWithType(Ctlsp_AND_c);
    new_->left->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
    new_->left->right= Ctlsp_LtlFormulaExpandAbbreviation(formula->right);
    new_->right->left = FormulaCreateWithType(Ctlsp_NOT_c);
    new_->right->left->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
    new_->right->right= FormulaCreateWithType(Ctlsp_NOT_c);
    new_->right->right->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->right);
    break;
  case Ctlsp_XOR_c:
    /* a ^ b  :: a*!b + !a*b */
    new_ = FormulaCreateWithType(Ctlsp_OR_c);
    new_->left = FormulaCreateWithType(Ctlsp_AND_c);
    new_->left->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
    new_->left->right= FormulaCreateWithType(Ctlsp_NOT_c);
    new_->left->right->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->right);
    new_->right = FormulaCreateWithType(Ctlsp_AND_c);
    new_->right->left= FormulaCreateWithType(Ctlsp_NOT_c);
    new_->right->left->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
    new_->right->right = Ctlsp_LtlFormulaExpandAbbreviation(formula->right);
    break;
  case Ctlsp_F_c:
    /* F a  :: true U a */
    new_ = FormulaCreateWithType(Ctlsp_U_c);
    new_->left = FormulaCreateWithType(Ctlsp_TRUE_c);
    new_->right= Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
    break;
  case Ctlsp_G_c:
    /* G a  :: false R a */
    new_ = FormulaCreateWithType(Ctlsp_R_c);
    new_->left = FormulaCreateWithType(Ctlsp_FALSE_c);
    new_->right= Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
    break;
  case Ctlsp_W_c:
    /* a W b :: b R (a+b) */
    new_ = FormulaCreateWithType(Ctlsp_R_c);
    new_->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->right);
    new_->right = FormulaCreateWithType(Ctlsp_OR_c);
    new_->right->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->right);
    new_->right->right = Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
    break;
  case Ctlsp_ID_c:
    /* Make a copy of the name, and create a new formula. */
    new_ = FormulaCreateWithType(Ctlsp_ID_c);
    new_->left = (Ctlsp_Formula_t *) util_strsav((char *)(formula->left));
    new_->right= (Ctlsp_Formula_t *) util_strsav((char *)(formula->right));
    break;
  case Ctlsp_A_c:
    /* Ignore A */
    new_ = Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
    break;
  default:
    /* These are already in the correct form.  Just convert subformulas. */
    new_ = FormulaCreateWithType(formula->type);
    new_->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left);
    new_->right= Ctlsp_LtlFormulaExpandAbbreviation(formula->right);
  }

  return new_;
}

/**Function********************************************************************

  Synopsis    [Return the Negation Normal Form (NNF) of a LTL formula.]

  Description [The negation is pushed to the bottom (only ahead fo atomic
  formulae). The result shares nothing with the input, not even a string;
  subformulae in the result are not shared either.

  Assume the formula is abbreviation-free, and there are only the following
  types of formulae before translation:
    TRUE/ FALSE/ ID/ AND/ OR/ U/ R/ X/ !  .]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_LtlFormulaNegationNormalForm(
  Ctlsp_Formula_t *formula)
{
  Ctlsp_Formula_t *new_, *left, *right;
#if 0
  Ctlsp_Formula_t  *negRight, *negLeft;
#endif
  Ctlsp_FormulaType dual;

  if (formula == NIL(Ctlsp_Formula_t))
    return formula;

  if (formula->type == Ctlsp_TRUE_c || formula->type == Ctlsp_FALSE_c) {
    new_ = FormulaCreateWithType(formula->type);
    return new_;
  }

  if (formula->type == Ctlsp_ID_c) {
    new_ = FormulaCreateWithType(formula->type);
    new_->left =(Ctlsp_Formula_t *)util_strsav((char *)(formula->left));
    new_->right=(Ctlsp_Formula_t *)util_strsav((char *)(formula->right));
    return new_;
  }

  if (formula->type != Ctlsp_NOT_c) {
    new_ = FormulaCreateWithType(formula->type);
    new_->left = Ctlsp_LtlFormulaNegationNormalForm(formula->left);
    new_->right= Ctlsp_LtlFormulaNegationNormalForm(formula->right);
    return new_;
  }

  /* In the following, formula->type == Ctlsp_NOT_c */
  if (formula->left->type == Ctlsp_NOT_c)
    return Ctlsp_LtlFormulaNegationNormalForm(formula->left->left);

  if (formula->left->type == Ctlsp_ID_c) {
    new_ = FormulaCreateWithType(formula->type);
    new_->left = Ctlsp_LtlFormulaNegationNormalForm(formula->left);
    return new_;
  }
#if 0
  if (formula->left->type == Ctlsp_THEN_c ) {
    left  = Ctlsp_LtlFormulaNegationNormalForm(formula->left->left);
    right = Ctlsp_FormulaCreate(Ctlsp_NOT_c, formula->left->right, NIL(Ctlsp_Formula_t));
    right = Ctlsp_LtlFormulaNegationNormalForm(right);
    new_   = Ctlsp_FormulaCreate(Ctlsp_AND_c, left, right);
    return new_;
  }
  if (formula->left->type == Ctlsp_EQ_c ) {
    left  = Ctlsp_LtlFormulaNegationNormalForm(formula->left->left);
    right = Ctlsp_LtlFormulaNegationNormalForm(formula->left->right);
    negRight = Ctlsp_FormulaCreate(Ctlsp_NOT_c, right, NIL(Ctlsp_Formula_t));
    negLeft  = Ctlsp_FormulaCreate(Ctlsp_NOT_c, left, NIL(Ctlsp_Formula_t));
    left     = right= Ctlsp_FormulaCreate(Ctlsp_AND_c, left, negRight);
    right    = right= Ctlsp_FormulaCreate(Ctlsp_AND_c, negLeft, right);
    new_      = Ctlsp_FormulaCreate(Ctlsp_OR_c, left, right);
    return Ctlsp_LtlFormulaNegationNormalForm(new_);
  }
#endif
  /* for TRUE/ FALSE/ AND/ OR/ U/ R/ X/ F/ G */
  switch (formula->left->type) {
  case Ctlsp_TRUE_c:
    dual = Ctlsp_FALSE_c;
    break;
  case Ctlsp_FALSE_c:
    dual = Ctlsp_TRUE_c;
    break;
  case Ctlsp_AND_c:
    dual = Ctlsp_OR_c;
    break;
  case Ctlsp_OR_c:
    dual = Ctlsp_AND_c;
    break;
  case Ctlsp_U_c:
    dual = Ctlsp_R_c;
    break;
  case Ctlsp_R_c:
    dual = Ctlsp_U_c;
    break;
  case Ctlsp_X_c:
    dual = Ctlsp_X_c;
    break;
  case Ctlsp_F_c:
    dual = Ctlsp_G_c;
    break;
  case Ctlsp_G_c:
    dual = Ctlsp_F_c;
    break;
  default:
    fail("Unexpected type");
  }

  /* alloc temporary formulae (! left) and (! right) */
  left = Ctlsp_FormulaCreate(Ctlsp_NOT_c, formula->left->left, NIL(Ctlsp_Formula_t));
  right= Ctlsp_FormulaCreate(Ctlsp_NOT_c, formula->left->right, NIL(Ctlsp_Formula_t));

  /* create the new formula */
  new_ = FormulaCreateWithType(dual);
  if ((dual == Ctlsp_X_c) ||
      (dual == Ctlsp_F_c) ||
      (dual == Ctlsp_G_c) ){
    new_->left = Ctlsp_LtlFormulaNegationNormalForm(left);
  }else if (dual != Ctlsp_TRUE_c && dual != Ctlsp_FALSE_c) {
    new_->left = Ctlsp_LtlFormulaNegationNormalForm(left);
    new_->right= Ctlsp_LtlFormulaNegationNormalForm(right);
  }
  FREE(left);
  FREE(right);

  return new_;
}

/**Function********************************************************************

Synopsis    [Hash the LTL formula and its sub-formulae into uniquetable.]

Description [It is possible that 'F' is freed, in which case a new 'F' is
returned.]

SideEffects []

SeeAlso     []

******************************************************************************/

Ctlsp_Formula_t *
Ctlsp_LtlFormulaHashIntoUniqueTable(
  Ctlsp_Formula_t *F,
  st_table *uniqueTable)
{
  Ctlsp_Formula_t *uniqueFormula;

  uniqueFormula = FormulaHashIntoUniqueTable(F, uniqueTable);

  /* If there is a copy 'uniqueFormula' in the uniqueTable, free F and
     increment the refCount of 'uniqueFormula' */
  if(uniqueFormula != F) {
    CtlspFormulaDecrementRefCount(F);
    CtlspFormulaIncrementRefCount(uniqueFormula);
  }

  return uniqueFormula;
}

/**Function********************************************************************

Synopsis    [Clear the '.marked' field of the LTL formula.]

Description [Recursively clear the .marked field for all its sub-formulae.]

SideEffects []

SeeAlso     []

******************************************************************************/
void
Ctlsp_LtlFormulaClearMarks(
  Ctlsp_Formula_t *F)
{
  if(F) {
    F->marked = 0;
    if (F->type != Ctlsp_ID_c) {
      Ctlsp_LtlFormulaClearMarks(F->left);
      Ctlsp_LtlFormulaClearMarks(F->right);
    }
  }
}

/**Function********************************************************************

Synopsis    [Clear the '.marked' field of the LTL formula.]

Description [Recursively clear the .marked field for all its sub-formulae.]

SideEffects []

SeeAlso     []

******************************************************************************/
int
Ctlsp_LtlFormulaCountNumber(
  Ctlsp_Formula_t *F)
{
  int result = 1;

  if (!F)
    return 0;

  if (F->marked)
    return 0;

  F->marked = 1;
  if (F->type == Ctlsp_TRUE_c ||
      F->type == Ctlsp_FALSE_c ||
      F->type == Ctlsp_ID_c)
    return 1;

  result += Ctlsp_LtlFormulaCountNumber(F->left);
  result += Ctlsp_LtlFormulaCountNumber(F->right);

  return result;
}

/**Function********************************************************************

  Synopsis    [Alloc a unqiue table for formulae.]

  Description [Use FormulaHash and formulaCompare.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
st_table *
Ctlsp_LtlFormulaCreateUniqueTable( void )
{
  return st_init_table(FormulaCompare, FormulaHash);
}

/**Function********************************************************************

  Synopsis    [Return True iff formula is an "elementary formula".]

  Description [Return True iff formula is an elementary formula. This is the
  original definition used in "Wring": it's a TRUE/FALSE/literal/X-formula.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
Ctlsp_LtlFormulaIsElementary2(
  Ctlsp_Formula_t *F)
{
  assert(F != 0);

  return (F->type == Ctlsp_X_c || Ctlsp_LtlFormulaIsAtomicPropositional(F) );
}

/**Function********************************************************************

  Synopsis    [Return True iff formula is an "elementary formula".]

  Description [Return True iff the formula is an elementary formula. The
  definition of 'elementary formula' is slightly different from the one in
  "Wring":  it's a TRUE/FALSE/Atomic Propositions/X-formula.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
Ctlsp_LtlFormulaIsElementary(
  Ctlsp_Formula_t *F)
{
  assert(F != NIL(Ctlsp_Formula_t));

  return (F->type == Ctlsp_X_c || Ctlsp_LtlFormulaIsPropositional(F) );
}

/**Function********************************************************************

  Synopsis    [Return TRUE iff abbreviation-free LTL formula is bounded.]

  Description [A bounded LTL formula is one that contains only atomic
  propositions, Boolean connectives, and the next-time (X) operator.
  The depth of a bounded formula is the maximum number of Xs along a
  path of its parse tree.  This function can only be applied to
  abbreviation-free LTL formulae.]

  SideEffects [The depth is returned as a side effect.  (Only if the function
  returns TRUE.)]

  SeeAlso     [Ctlsp_LtlFormulaExpandAbbreviation,
               Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe]

******************************************************************************/
boolean
Ctlsp_LtlFormulaTestIsBounded(
  Ctlsp_Formula_t *formula,
  int *depth)
{
  Ctlsp_Formula_t *leftChild;
  Ctlsp_Formula_t *rightChild;
  int leftDepth, rightDepth;

  assert(formula != NIL(Ctlsp_Formula_t));

  switch (Ctlsp_FormulaReadType(formula)) {
  case Ctlsp_TRUE_c:
  case Ctlsp_FALSE_c:
  case Ctlsp_ID_c:
    *depth = 0;
    return TRUE;
  case Ctlsp_AND_c:
  case Ctlsp_OR_c:
    leftChild = Ctlsp_FormulaReadLeftChild(formula);
    if (Ctlsp_LtlFormulaTestIsBounded(leftChild, &leftDepth)) {
      rightChild = Ctlsp_FormulaReadRightChild(formula);
      if (Ctlsp_LtlFormulaTestIsBounded(rightChild, &rightDepth)) {
        *depth = leftDepth > rightDepth ? leftDepth : rightDepth;
        return TRUE;
      } else {
        return FALSE;
      }
    } else {
      return FALSE;
    }
  case Ctlsp_NOT_c:
  case Ctlsp_X_c:
    leftChild = Ctlsp_FormulaReadLeftChild(formula);
    if (Ctlsp_LtlFormulaTestIsBounded(leftChild, &leftDepth)) {
      if (Ctlsp_FormulaReadType(formula) == Ctlsp_X_c) leftDepth++;
      *depth = leftDepth;
      return TRUE;
    } else {
      return FALSE;
    }
  case Ctlsp_U_c:
  case Ctlsp_R_c:
    return FALSE;
  default:
    fail("unexpected node type in abbreviation-free formula\n");
    return FALSE; /* not reached */
  }
} /* Ctlsp_LtlFormulaTestIsBounded */

/**Function********************************************************************

  Synopsis    [Return the depth of abbreviation-free LTL formula.]

  Description [The depth of the LTL formula f is the maximum level of
  nesting of temporal operators in f.  This function can only be applied
  to abbreviation-free LTL formulae.]

  SideEffects []

  SeeAlso     [Ctlsp_LtlFormulaExpandAbbreviation]

******************************************************************************/
int
Ctlsp_LtlFormulaDepth(
  Ctlsp_Formula_t *formula)
{
  int leftDepth, rightDepth;

  assert(formula != NIL(Ctlsp_Formula_t));

  switch (Ctlsp_FormulaReadType(formula)) {
  case Ctlsp_TRUE_c:
  case Ctlsp_FALSE_c:
  case Ctlsp_ID_c:
    return 0;
  case Ctlsp_AND_c:
  case Ctlsp_OR_c:
    leftDepth  = Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadLeftChild(formula));
    rightDepth = Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadRightChild(formula));
    return leftDepth > rightDepth ? leftDepth : rightDepth;
  case Ctlsp_NOT_c:
    return Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadLeftChild(formula));
  case Ctlsp_X_c:
    return 1+Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadLeftChild(formula));
  case Ctlsp_U_c:
  case Ctlsp_R_c:
    leftDepth  = Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadLeftChild(formula));
    rightDepth = Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadRightChild(formula));
    return 1+(leftDepth > rightDepth ? leftDepth : rightDepth);
  default:
    fail("unexpected node type in abbreviation-free formula\n");
    return 0; /* not reached */
  }
} /* Ctlsp_LtlFormulaDepth */

/**Function********************************************************************

  Synopsis    [Return TRUE iff LTL formula in negation normal form is
  syntactically co-safe.]

  Description [A syntactically co-safe LTL formula is a formula in
  negation normal form that contains no release (R) operators.  This
  function can only be applied to abbreviation-free LTL formulae in
  negation normal form.  We test co-safety because this function is
  meant to be called on the negation of the given formula.]

  SideEffects [none]

  SeeAlso     [Ctlsp_LtlFormulaNegationNormalForm,
               Ctlsp_LtlFormulaTestIsBounded]

******************************************************************************/
boolean
Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(Ctlsp_Formula_t *formula)
{
  Ctlsp_Formula_t *leftChild;
  Ctlsp_Formula_t *rightChild;

  assert(formula != NIL(Ctlsp_Formula_t));

  /*
    Check for unless temporal operator. a W b = (a U b) OR (FALSE R a)
                     its negation = (!a R !b) AND (TRUE U !a)
   */
  if(Ctlsp_FormulaReadType(formula) ==  Ctlsp_AND_c){
    leftChild  = Ctlsp_FormulaReadLeftChild(formula);
    rightChild = Ctlsp_FormulaReadRightChild(formula);
    if((Ctlsp_FormulaReadType(leftChild)  == Ctlsp_R_c) &&
       (Ctlsp_FormulaReadType(rightChild) == Ctlsp_U_c)){
      if(Ctlsp_FormulaReadLeftChild(leftChild) == Ctlsp_FormulaReadRightChild(rightChild)){
        if(Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(rightChild)) == Ctlsp_TRUE_c){
          return Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(
                            Ctlsp_FormulaReadLeftChild(leftChild)) &&
                 Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(
                            Ctlsp_FormulaReadRightChild(leftChild));
        }
      }
    }
    /*
       a W b = (FALSE R a) OR (a U b)
       its negation = (TRUE U !a) AND (!a R !b)
   */
    if((Ctlsp_FormulaReadType(rightChild) == Ctlsp_R_c) &&
       (Ctlsp_FormulaReadType(leftChild) == Ctlsp_U_c)){
      if(Ctlsp_FormulaReadLeftChild(rightChild) == Ctlsp_FormulaReadRightChild(leftChild)){
        if(Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(leftChild)) == Ctlsp_TRUE_c){
          return Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(
            Ctlsp_FormulaReadLeftChild(rightChild)) &&
            Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(
              Ctlsp_FormulaReadRightChild(rightChild));
        }
      }
    }
  }
  switch (Ctlsp_FormulaReadType(formula)) {
  case Ctlsp_TRUE_c:
  case Ctlsp_FALSE_c:
  case Ctlsp_ID_c:
    return TRUE;
  case Ctlsp_AND_c:
  case Ctlsp_OR_c:
  case Ctlsp_U_c:
    leftChild = Ctlsp_FormulaReadLeftChild(formula);
    if (Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(leftChild)) {
      rightChild = Ctlsp_FormulaReadRightChild(formula);
      return Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(rightChild);
    } else {
      return FALSE;
    }
  case Ctlsp_NOT_c:
    leftChild = Ctlsp_FormulaReadLeftChild(formula);
    /* The formula is in negation normal form. */
    assert(Ctlsp_FormulaReadType(leftChild) == Ctlsp_ID_c);
    return TRUE;
  case Ctlsp_X_c:
    leftChild = Ctlsp_FormulaReadLeftChild(formula);
    return Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(leftChild);
  case Ctlsp_R_c:
    return FALSE;
  default:
    fail("unexpected node type in abbreviation-free formula\n");
    return FALSE; /* not reached */
  }
} /* Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe */

/**Function********************************************************************

  Synopsis [Tests if each formula in an array of LTL formulae is
  propositional]

  Description [This function tests each LTL formula in negation normal
  form to see if it is a propositional formula.  Return TRUE if all formulae
  are propositional formulae.]

  SideEffects [none]

  SeeAlso     [Ctlsp_LtlFormulaIsPropositional]

******************************************************************************/
int
Ctlsp_LtlFormulaArrayIsPropositional(
  array_t * formulaArray)
{
  int             i;
  Ctlsp_Formula_t *formula;

  for (i = 0; i < array_n(formulaArray); i++) {
    formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i);
    if(!Ctlsp_isPropositionalFormula(formula)){
      /*if(Ctlsp_LtlFormulaIsPropositional(formula) == 0){*/
      return 0;
    }
  }
  return 1;

} /* Ctlsp_LtlFormulaArrayIsPropositional */


/**Function********************************************************************

  Synopsis    [Return T iff formula is a "propositional formula".]

  Description [This function tests an LTL formula in negation normal
  form to see if it is a propositional formula.  A propositional
  formula contains only Boolean connectives, TRUE, FALSE, and
  literals.  A literal is an atomic proposition or the negation of an
  atomic popposition.]

  SideEffects [none]

  SeeAlso     [Ctlsp_LtlFormulaIsAtomicPropositional]

******************************************************************************/
int
Ctlsp_LtlFormulaIsPropositional(
  Ctlsp_Formula_t *F)
{
  int result;

  assert(F !=  NIL(Ctlsp_Formula_t));

  switch (F->type) {
  case Ctlsp_TRUE_c:
  case Ctlsp_FALSE_c:
  case Ctlsp_ID_c:
    result = 1;
    break;
  case Ctlsp_NOT_c: /* negation only appears ahead of AP */
    if (F->left->type == Ctlsp_ID_c)
      result = 1;
    else
      result = 0;
    break;
  case Ctlsp_AND_c:
  case Ctlsp_OR_c:
    result = (Ctlsp_LtlFormulaIsPropositional(F->left) &&
              Ctlsp_LtlFormulaIsPropositional(F->right));
    break;
  default:
    result = 0;
  }

  return result;
} /* Ctlsp_LtlFormulaIsPropositional() */

/**Function********************************************************************

  Synopsis    [Return T iff formula is an "atomic propositional formula".]

  Description [TRUE/FALSE/literal.  literal: an atomic proposition or the
  negation of an atomic popposition.]

  SideEffects [none]

  SeeAlso     [Ctlsp_LtlFormulaIsPropositional]

******************************************************************************/
int
Ctlsp_LtlFormulaIsAtomicPropositional(
  Ctlsp_Formula_t *F)
{
  int result;

  assert(F != 0);

  switch (F->type) {
  case Ctlsp_TRUE_c:
  case Ctlsp_FALSE_c:
  case Ctlsp_ID_c:
    result = 1;
    break;
  case Ctlsp_NOT_c: /* negation only appears ahead of AP */
    if (F->left->type == Ctlsp_ID_c)
      result = 1;
    else
      result = 0;
    break;
  default:
    result = 0;
  }

  return result;
}

/**Function********************************************************************

  Synopsis    [Return T iff formula is a "FG formula".]

  Description [TRUE U (FALSE R p).]

  SideEffects []

  SeeAlso     [Ctlsp_LtlFormulaIsGF, Ctlsp_LtlFormulaIsFGorGF]

******************************************************************************/
int
Ctlsp_LtlFormulaIsFG(
  Ctlsp_Formula_t *F)
{
  int result = 0;

  if (F->type == Ctlsp_U_c) {
    if (F->left->type == Ctlsp_TRUE_c && F->right->type == Ctlsp_R_c) {
      result = (F->right->left->type == Ctlsp_FALSE_c);
    }
  }

  return result;
}


/**Function********************************************************************

  Synopsis    [Return T iff formula is a "GF formula".]

  Description [FALSE R (TRUE U p).]

  SideEffects []

  SeeAlso     [Ctlsp_LtlFormulaIsFG, Ctlsp_LtlFormulaIsFGorGF]

******************************************************************************/
int
Ctlsp_LtlFormulaIsGF(
  Ctlsp_Formula_t *F)
{
  int result = 0;

  if (F->type == Ctlsp_R_c) {
      if (F->left->type == Ctlsp_FALSE_c && F->right->type == Ctlsp_U_c) {
          result = (F->right->left->type == Ctlsp_TRUE_c);
      }
  }

  return result;
}

/**Function********************************************************************

  Synopsis    [Return T iff formula is a "FG or GF formula".]

  Description [TRUE U (FALSE R p).]

  SideEffects []

  SeeAlso     [Ctlsp_LtlFormulaIsGF, Ctlsp_LtlFormulaIsFG]

******************************************************************************/
int
Ctlsp_LtlFormulaIsFGorGF(
  Ctlsp_Formula_t *F)
{
  return (Ctlsp_LtlFormulaIsFG(F) || Ctlsp_LtlFormulaIsGF(F));
}


/**Function********************************************************************

  Synopsis    [Return T iff (form -> to).]

  Description [Since determine '->' is hard, we only consider easy case which
  can be determined syntatically.

  Notice that, before calling this function, 'from' and 'to' are hashed into
  the same UniqueTable (This helps in identifying "from==to").]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
Ctlsp_LtlFormulaSimplyImply(
  Ctlsp_Formula_t *from,
  Ctlsp_Formula_t *to)
{

#if 0
  fprintf(vis_stdout, "\n------------------------\n");
  Ctlsp_FormulaPrint(vis_stdout, from);
  fprintf(vis_stdout, "\n   ==>\n");
  Ctlsp_FormulaPrint(vis_stdout, to);
  fprintf(vis_stdout, "\n------------------------\n");
#endif

  /* from -> from   :  1 */
  if (from == to)
    return 1;

  /* from -> TRUE   :  1 */
  if (to->type == Ctlsp_TRUE_c)
    return 1;

  /* FALSE -> to    :  1 */
  if (from->type == Ctlsp_FALSE_c)
    return 1;


  if (to->type == Ctlsp_U_c) {
    /* from -> tL U tR: (from->tR)? */
    if (Ctlsp_LtlFormulaSimplyImply(from, to->right))
      return 1;

    /* (fL U fR) -> (tl U tR) : (fL->tL)? && (fR->tR)? */
    if (from->type == Ctlsp_U_c)
      return (Ctlsp_LtlFormulaSimplyImply(from->left, to->left) &&
              Ctlsp_LtlFormulaSimplyImply(from->right, to->right));
  }

  if (to->type == Ctlsp_R_c) {
    /* from -> tL R tR: (from->tL)? && (from->tR)? */
    if (Ctlsp_LtlFormulaSimplyImply(from, to->left) &&
        Ctlsp_LtlFormulaSimplyImply(from, to->right))
      return 1;

    /* (fL R fR) -> (tL R tR) : (fL->tL)? && (fR->tR)? */
    if (from->type == Ctlsp_R_c)
      return (Ctlsp_LtlFormulaSimplyImply(from->left, to->left) &&
              Ctlsp_LtlFormulaSimplyImply(from->right, to->right));
  }

  /* (fL U fR) -> to :: (fL->to)? && (fR->to)? */
  if (from->type == Ctlsp_U_c) {
    if (Ctlsp_LtlFormulaSimplyImply(from->left, to) &&
        Ctlsp_LtlFormulaSimplyImply(from->right,to) )
      return 1;
  }

  /* (fL R fR) -> to :: (fR->to)? */
  if (from->type == Ctlsp_R_c) {
    if (Ctlsp_LtlFormulaSimplyImply(from->right,to))
      return 1;
  }

  /*************************************************************************
   * (1) If we unwinding every propositional formula, sometimes it will
   * become really hard. This is due to the feature of the CTL* parser.
   * For example, "state[1024]=0" would be parsed into 1024 subformulae
   *
   * (2) Without unwinding, some possible simplification cases can not be
   * detected. For example, "p + !p", "p * !p" (while p and the left
   * subformula in !p are syntatically different.
   ************************************************************************/
  if (!Ctlsp_LtlFormulaIsPropositional(to)) {

    /* form -> tL*tR  : (from->tL)? && (from->rR)? */
    if (to->type == Ctlsp_AND_c)
      return (Ctlsp_LtlFormulaSimplyImply(from, to->left) &&
              Ctlsp_LtlFormulaSimplyImply(from, to->right));

    /* from -> tL+tR  : (from->tL)? || (from->rR)? */
    if (to->type == Ctlsp_OR_c)
      return (Ctlsp_LtlFormulaSimplyImply(from, to->left) ||
              Ctlsp_LtlFormulaSimplyImply(from, to->right) );
  }

  if (!Ctlsp_LtlFormulaIsPropositional(from)) {

    /* (fL * fR) -> to :: (fL->to)? || (fR->to)? */
    if (from->type == Ctlsp_AND_c)
      return (Ctlsp_LtlFormulaSimplyImply(from->left, to) ||
              Ctlsp_LtlFormulaSimplyImply(from->right,to) );


    /* (fL + fR) -> to :: (fL->to)? && (fR->to)? */
    if (from->type == Ctlsp_OR_c)
      return (Ctlsp_LtlFormulaSimplyImply(from->left, to) &&
              Ctlsp_LtlFormulaSimplyImply(from->right,to) );
  }

  return 0;
}


/**Function********************************************************************

  Synopsis    [Translate LTL formula into Separated Normal Form (SNF)]

  Description [Translate LTL formula into Separated Normal Form (SNF).
  Each LTL formula is translated into a set of rules in the form (p
  --> f(q)), where p and q are propositional and f(q) contains at most
  one temporal operator which is either X or F.]

  SideEffects []

  SeeAlso     [Ctlsp_LtlTranslateIntoSNFRecursive]

******************************************************************************/
array_t *
Ctlsp_LtlTranslateIntoSNF(
  Ctlsp_Formula_t *formula)
{
  Ctlsp_Formula_t *leftNode;
  int             index, i;
  array_t         *formulaArray = array_alloc(Ctlsp_Formula_t *, 0);

  /*
    rule#1: an LTL formula must hold at an initial state.
   */

  leftNode  = Ctlsp_FormulaCreate(Ctlsp_ID_c, (void *)util_strsav(" SNFstart"), (void *)util_strsav("1"));
  /*
    rightNode = Ctlsp_FormulaCreate(Ctlsp_ID_c, (void *)util_strsav("SNFx_0"),   (void *)util_strsav("1"));
    newNode = Ctlsp_FormulaCreate(Ctlsp_THEN_c, leftNode, rightNode);
  */

  index = 0;
  Ctlsp_LtlTranslateIntoSNFRecursive(leftNode, formula, formulaArray, &index);

  fprintf(vis_stdout, "The SNF rules are:\n");
  for (i = 0; i < array_n(formulaArray); i++) {
    Ctlsp_Formula_t *ltlFormula     = array_fetch(Ctlsp_Formula_t *, formulaArray, i);

    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
    fprintf(vis_stdout, "\n");
  }

  return formulaArray;
}

/**Function********************************************************************

  Synopsis    [Trnalate LTL formula into Separated Normal Form (SNF)]

  Description [Recursively trnaslate LTL formula into SNF

  Assume the formula is abbreviation-free NNF, and there are only the
  following types of formulae before translation: TRUE FALSE ID AND OR
  U R X !  .]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
Ctlsp_LtlTranslateIntoSNFRecursive(
  Ctlsp_Formula_t *propNode,
  Ctlsp_Formula_t *formula,
  array_t         *formulaArray,
  int             *index)
{

  Ctlsp_Formula_t *leftNode, *rightNode, *newNode, *result;

  if(formula == NIL(Ctlsp_Formula_t)){
    return;
  }
  if(Ctlsp_LtlFormulaIsPropositional(formula)){
    newNode = CtlspFunctionThen(propNode, formula);
    CtlspFormulaIncrementRefCount(newNode);
    array_insert_last(Ctlsp_Formula_t *, formulaArray, newNode);
    return;
  }
  switch (Ctlsp_FormulaReadType(formula)) {
  case Ctlsp_AND_c:
    leftNode  = Ctlsp_FormulaReadLeftChild(formula);
    rightNode = Ctlsp_FormulaReadRightChild(formula);

    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, leftNode, formulaArray, index);
    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, rightNode, formulaArray, index);

    break;
  case Ctlsp_OR_c:
    leftNode  = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index);
    rightNode = createSNFnode(Ctlsp_FormulaReadRightChild(formula), formulaArray, index);
    newNode   = CtlspFunctionOr(leftNode, rightNode);
    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, newNode, formulaArray, index);

    break;
  case Ctlsp_THEN_c:
    leftNode  = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index);
    rightNode = createSNFnode(Ctlsp_FormulaReadRightChild(formula), formulaArray, index);
    newNode   = CtlspFunctionOr(
      Ctlsp_FormulaCreate(Ctlsp_NOT_c, leftNode, NIL(Ctlsp_Formula_t))
      , rightNode);
    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, newNode, formulaArray, index);
    break;
  case Ctlsp_NOT_c:
    if (!Ctlsp_isPropositionalFormula(formula)){
      fprintf(vis_stderr,"SNF error: the LTL formula is not in NNF\n");
    }
    break;
  case Ctlsp_X_c:
    /*
      propNode -> X leftNode
     */
    leftNode = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index);

    newNode = Ctlsp_FormulaCreate(Ctlsp_X_c, leftNode, NIL(Ctlsp_Formula_t));
    newNode = CtlspFunctionThen(propNode, newNode);
     CtlspFormulaIncrementRefCount(newNode);
    array_insert_last(Ctlsp_Formula_t *, formulaArray, newNode);

    break;
  case Ctlsp_F_c:
    /*
      propNode -> F leftNode
     */
    leftNode = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index);

    newNode  = Ctlsp_FormulaCreate(Ctlsp_F_c, leftNode, NIL(Ctlsp_Formula_t));
    newNode  = CtlspFunctionThen(propNode, newNode);
     CtlspFormulaIncrementRefCount(newNode);
    array_insert_last(Ctlsp_Formula_t *, formulaArray, newNode);

    break;
  case Ctlsp_G_c:
    /*
      propNode -> G leftNode
    */
    leftNode = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index);

    newNode  = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strcat3(" SNFx","_", util_inttostr((*index)++)),
                                   (void *)util_strsav("1"));

    result  = CtlspFunctionAnd(leftNode, newNode);
    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, result, formulaArray, index);
    result   = Ctlsp_FormulaCreate(Ctlsp_X_c, result, NIL(Ctlsp_Formula_t));
    Ctlsp_LtlTranslateIntoSNFRecursive(newNode, result, formulaArray, index);

    break;
  case Ctlsp_U_c:
    /*
      x --> a U b = x --> b + a*y
                    y --> X(b + a*y)
                    x --> F(b)
    */
    newNode = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strcat3(" SNFx","_", util_inttostr((*index)++)),
                                  (void *)util_strsav("1"));

    leftNode  = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index);
    rightNode = createSNFnode(Ctlsp_FormulaReadRightChild(formula), formulaArray, index);

    result  = CtlspFunctionAnd(leftNode, newNode);
    result  = CtlspFunctionOr(rightNode, result);

    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, result, formulaArray, index);

    result   = Ctlsp_FormulaCreate(Ctlsp_X_c, result, NIL(Ctlsp_Formula_t));
    Ctlsp_LtlTranslateIntoSNFRecursive(newNode, result, formulaArray, index);

    result   = Ctlsp_FormulaCreate(Ctlsp_F_c, rightNode, NIL(Ctlsp_Formula_t));
    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, result, formulaArray, index);
    break;
  case Ctlsp_W_c:
    /*
      x --> a W b = x --> b + a*y
                    y --> X(b + a*y)
    */
    newNode = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strcat3(" SNFx","_", util_inttostr((*index)++)),
                                  (void *)util_strsav("1"));

    leftNode  = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index);
    rightNode = createSNFnode(Ctlsp_FormulaReadRightChild(formula), formulaArray, index);

    result  = CtlspFunctionAnd(leftNode, newNode);
    result  = CtlspFunctionOr(rightNode, result);

    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, result, formulaArray, index);

    result   = Ctlsp_FormulaCreate(Ctlsp_X_c, result, NIL(Ctlsp_Formula_t));
    Ctlsp_LtlTranslateIntoSNFRecursive(newNode, result, formulaArray, index);
    break;
  case Ctlsp_R_c:
    /*
      x --> left R right = x --> left*right + right*y
                           y --> X(left*rigt* + right*y)
     */
    newNode = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strcat3(" SNFx","_", util_inttostr((*index)++)),
                                  (void *)util_strsav("1"));
    leftNode  = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index);
    rightNode = createSNFnode(Ctlsp_FormulaReadRightChild(formula), formulaArray, index);

    leftNode  = CtlspFunctionAnd(leftNode, rightNode);

    result = CtlspFunctionAnd(rightNode, newNode);
    result = CtlspFunctionOr(leftNode, result);

    Ctlsp_LtlTranslateIntoSNFRecursive(propNode, result, formulaArray, index);

    result = Ctlsp_FormulaCreate(Ctlsp_X_c, result, NIL(Ctlsp_Formula_t));
    Ctlsp_LtlTranslateIntoSNFRecursive(newNode, result, formulaArray, index);

    break;
  default:
    fail("unexpected node type in abbreviation-free formula\n");
    return; /* not reached */
  }
}


/**Function********************************************************************

  Synopsis    [Perform simple rewriting of a formula.]

  Description [We return a formula which shares nothing with the input formula]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
Ctlsp_LtlFormulaSimpleRewriting(
  Ctlsp_Formula_t *formula)
{
  Ctlsp_Formula_t *F, *newF;
  st_table *Utable = st_init_table(FormulaCompare, FormulaHash);
  st_generator *stGen;
  char *key;

  /* copy the input formula (so that they share nothing) */
  F = Ctlsp_LtlFormulaNegationNormalForm(formula);

  /* hash into the 'Utable' */
  F = Ctlsp_LtlFormulaHashIntoUniqueTable(F, Utable);

  /* simple rewriting */
  F = CtlspLtlFormulaSimpleRewriting_Aux(F, Utable);

  /* copy F into 'newF' (they shares nothing) */
  newF = Ctlsp_LtlFormulaNegationNormalForm(F);

  /* free formulae in st_table */
  st_foreach_item(Utable, stGen, &key, &F) {
    if (F->type == Ctlsp_ID_c) {
      FREE(F->left);
      FREE(F->right);
    }
    FREE(F);
  }
  st_free_table(Utable);

  return (newF);
}


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [Rewriting the LTL formula recursively.]

  Description [Recursive call, used in Ctlsp_LtlFormulaSimpleRewriting() only.]

  SideEffects [The given formula F might be freed (hence unrecoverable)]

  SeeAlso     [Ctlsp_LtlFormulaSimpleRewriting]

******************************************************************************/
Ctlsp_Formula_t *
CtlspLtlFormulaSimpleRewriting_Aux(
  Ctlsp_Formula_t *F,
  st_table *Utable)
{
  Ctlsp_Formula_t *left, *right;
  Ctlsp_Formula_t *tmpf1, *tmpf2;
  Ctlsp_Formula_t *True, *False;

  if (F == NIL(Ctlsp_Formula_t))
    return F;

  if (F->type == Ctlsp_ID_c || F->type == Ctlsp_TRUE_c ||
      F->type == Ctlsp_FALSE_c) {
    F = Ctlsp_LtlFormulaHashIntoUniqueTable(F, Utable);
    return F;
  }

#if 0
  fprintf(vis_stdout, "\nRewriting ...\n");
  Ctlsp_FormulaPrint(vis_stdout, F);
  fprintf(vis_stdout, "\n");
#endif

  /* First of all, rewrite F->left, F->right */
  left = CtlspLtlFormulaSimpleRewriting_Aux(F->left, Utable);
#if 0
  fprintf(vis_stdout, "\n... Rewriting(left)\n");
  Ctlsp_FormulaPrint(vis_stdout, left);
  fprintf(vis_stdout, "\n");
#endif

  right = CtlspLtlFormulaSimpleRewriting_Aux(F->right, Utable);
#if 0
  fprintf(vis_stdout, "\n... Rewriting(right)\n");
  Ctlsp_FormulaPrint(vis_stdout, right);
  fprintf(vis_stdout, "\n");
#endif

  /* in case we want to use TRUE/FALSE */
  True = Ctlsp_LtlFormulaHashIntoUniqueTable(FormulaCreateWithType(Ctlsp_TRUE_c), Utable);
  False = Ctlsp_LtlFormulaHashIntoUniqueTable(FormulaCreateWithType(Ctlsp_FALSE_c), Utable);

  switch (F->type) {
  case Ctlsp_AND_c:

    /* r -> l :  l*r == r */
    if (Ctlsp_LtlFormulaSimplyImply(right, left))
      return right;

    /* l -> r, l*r == l */
    if (Ctlsp_LtlFormulaSimplyImply(left, right))
      return left;

    /* r -> !l, l*r == FALSE*/
    tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
    tmpf1->left = left;
    tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
    FREE(tmpf1);
    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
    if (Ctlsp_LtlFormulaSimplyImply(right, tmpf2))
      return False;

    /* l -> !r, l*r == FALSE*/
    tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
    tmpf1->left = right;
    tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
    FREE(tmpf1);
    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
    if (Ctlsp_LtlFormulaSimplyImply(left, tmpf2))
      return False;

    /* (ll R lr) * (ll R rr) == (ll) R (lr*rr) */
    if (left->type == Ctlsp_R_c && right->type == Ctlsp_R_c) {
      if (left->left == right->left) {
        tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
        tmpf1->left = left->right;
        tmpf1->right = right->right;
        CtlspFormulaIncrementRefCount(left->right);
        CtlspFormulaIncrementRefCount(right->right);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

        tmpf2 = FormulaCreateWithType(Ctlsp_R_c);
        tmpf2->left = left->left;
        tmpf2->right = tmpf1;
        CtlspFormulaIncrementRefCount(left->left);
        CtlspFormulaIncrementRefCount(tmpf1);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
        return tmpf2;
      }
    }

    /* (ll U lr) * (rl U lr) == (ll * rl) U (lr) */
    if (left->type == Ctlsp_U_c && right->type == Ctlsp_U_c) {
      if (left->right == right->right) {
        tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
        tmpf1->left = left->left;
        tmpf1->right = right->left;
        CtlspFormulaIncrementRefCount(left->left);
        CtlspFormulaIncrementRefCount(right->left);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

        tmpf2 = FormulaCreateWithType(Ctlsp_U_c);
        tmpf2->left = tmpf1;
        tmpf2->right = left->right;
        CtlspFormulaIncrementRefCount(tmpf1);
        CtlspFormulaIncrementRefCount(left->right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
        return tmpf2;
      }
    }

    /* (X ll)*(X rl) == X (ll*rl) */
    if (left->type == Ctlsp_X_c && right->type == Ctlsp_X_c) {
      tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
      tmpf1->left = left->left;
      tmpf1->right = right->left;
      CtlspFormulaIncrementRefCount(left->left);
      CtlspFormulaIncrementRefCount(right->left);
      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

      tmpf2 = FormulaCreateWithType(Ctlsp_X_c);
      tmpf2->left = tmpf1;
      CtlspFormulaIncrementRefCount(tmpf1);
      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
      return tmpf2;
    }

    /* (ll R lr) * (rl U ll)   ==  ( (X lr * rl) U ll) * lr */
    if (left->type == Ctlsp_R_c && right->type == Ctlsp_U_c) {
      if (left->left == right->right) {
        tmpf1 = FormulaCreateWithType(Ctlsp_X_c);
        tmpf1->left = left->right;
        CtlspFormulaIncrementRefCount(left->right);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

        if (right->left->type != Ctlsp_TRUE_c) {
          tmpf2 = FormulaCreateWithType(Ctlsp_AND_c);
          tmpf2->left = tmpf1;
          tmpf2->right = right->left;
          CtlspFormulaIncrementRefCount(tmpf1);
          CtlspFormulaIncrementRefCount(right->left);
          tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
        }

        tmpf2 = FormulaCreateWithType(Ctlsp_U_c);
        tmpf2->left = tmpf1;
        tmpf2->right = left->left;
        CtlspFormulaIncrementRefCount(tmpf1);
        CtlspFormulaIncrementRefCount(left->left);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);

        tmpf2 = FormulaCreateWithType(Ctlsp_AND_c);
        tmpf2->left = tmpf1;
        tmpf2->right = left->right;
        CtlspFormulaIncrementRefCount(tmpf1);
        CtlspFormulaIncrementRefCount(left->right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);

        return tmpf2;
      }
    }
    /* (ll U lr) * (lr R rr)   ==  ( (X rr * ll) U rl) * rr */
    if (left->type == Ctlsp_U_c && right->type == Ctlsp_R_c) {
      if (left->right == right->left) {
        tmpf1 = FormulaCreateWithType(Ctlsp_X_c);
        tmpf1->left = right->right;
        CtlspFormulaIncrementRefCount(right->right);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

        if (left->left->type != Ctlsp_TRUE_c) {
          tmpf2 = FormulaCreateWithType(Ctlsp_AND_c);
          tmpf2->left = tmpf1;
          tmpf2->right = left->left;
          CtlspFormulaIncrementRefCount(tmpf1);
          CtlspFormulaIncrementRefCount(left->left);
          tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
        }

        tmpf2 = FormulaCreateWithType(Ctlsp_U_c);
        tmpf2->left = tmpf1;
        tmpf2->right = right->left;
        CtlspFormulaIncrementRefCount(tmpf1);
        CtlspFormulaIncrementRefCount(right->left);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);

        tmpf2 = FormulaCreateWithType(Ctlsp_AND_c);
        tmpf2->left = tmpf1;
        tmpf2->right = right->right;
        CtlspFormulaIncrementRefCount(tmpf1);
        CtlspFormulaIncrementRefCount(right->right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);

        return tmpf2;
      }
    }

    /* (ll R lr) * r, r=>ll  == lr *r */
    if (left->type == Ctlsp_R_c &&
        Ctlsp_LtlFormulaSimplyImply(right, left->left)) {
      tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
      tmpf1->left = left->right;
      tmpf1->right = right;
      CtlspFormulaIncrementRefCount(left->right);
      CtlspFormulaIncrementRefCount(right);
      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
      return tmpf2;
    }
    /* l *(rl R rr), l=>rl  == l * rr */
    if (right->type == Ctlsp_R_c &&
        Ctlsp_LtlFormulaSimplyImply(left, right->left)) {
      tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
      tmpf1->left = left;
      tmpf1->right = right->right;
      CtlspFormulaIncrementRefCount(left);
      CtlspFormulaIncrementRefCount(right->right);
      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
      return tmpf2;
    }

    /* (ll U lr) * r, r=>!ll   == lr * r */
    if (left->type == Ctlsp_U_c) {
      tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
      tmpf1->left = left->left;
      tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
      FREE(tmpf1);
      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);

      if (Ctlsp_LtlFormulaSimplyImply(right, tmpf1)) {
        tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
        tmpf1->left = left->right;
        tmpf1->right = right;
        CtlspFormulaIncrementRefCount(left->right);
        CtlspFormulaIncrementRefCount(right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
        return tmpf2;
      }
    }
    /* l * (rl U rr), l=>!rl   == l * rr */
    if (right->type == Ctlsp_U_c) {
      tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
      tmpf1->left = right->left;
      tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
      FREE(tmpf1);
      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);

      if (Ctlsp_LtlFormulaSimplyImply(left, tmpf1)) {
        tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
        tmpf1->left = left;
        tmpf1->right = right->right;
        CtlspFormulaIncrementRefCount(left);
        CtlspFormulaIncrementRefCount(right->right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
        return tmpf2;
      }
    }

    /* FG lrr * FG rrr = FG (lrr * rrr) */
    if (Ctlsp_LtlFormulaIsFG(left) && Ctlsp_LtlFormulaIsFG(right)) {
      tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
      tmpf1->left = left->right->right;
      tmpf1->right = right->right->right;
      CtlspFormulaIncrementRefCount(left->right->right);
      CtlspFormulaIncrementRefCount(right->right->right);
      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

      tmpf2 = FormulaCreateWithType(Ctlsp_R_c);
      tmpf2->left = False;
      tmpf2->right = tmpf1;
      CtlspFormulaIncrementRefCount(False);
      CtlspFormulaIncrementRefCount(tmpf1);
      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);

      tmpf2 = FormulaCreateWithType(Ctlsp_U_c);
      tmpf2->left = True;
      tmpf2->right = tmpf1;
      CtlspFormulaIncrementRefCount(True);
      CtlspFormulaIncrementRefCount(tmpf1);
      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
      return tmpf2;
    }

    /* return  (l * r) */
    tmpf1 = FormulaCreateWithType(Ctlsp_AND_c);
    tmpf1->left = left;
    tmpf1->right = right;
    CtlspFormulaIncrementRefCount(left);
    CtlspFormulaIncrementRefCount(right);
    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
    return tmpf2;

  case Ctlsp_OR_c:

    /* r -> l, l+r == l */
    if (Ctlsp_LtlFormulaSimplyImply(right, left))
      return left;

    /* l -> r, l+r == r */
    if (Ctlsp_LtlFormulaSimplyImply(left, right))
      return right;

    /* !r -> l, l+r == TRUE*/
    tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
    tmpf1->left = right;
    tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
    FREE(tmpf1);
    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
    if (Ctlsp_LtlFormulaSimplyImply(tmpf2, left))
      return True;

    /* !l -> r, l+r == TRUE*/
    tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
    tmpf1->left = left;
    tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
    FREE(tmpf1);
    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
    if (Ctlsp_LtlFormulaSimplyImply(tmpf2, right))
      return True;

    /* (ll U lr) + (ll U rr) == (ll) U (lr+rr) */
    if (left->type == Ctlsp_U_c && right->type == Ctlsp_U_c) {
      if (left->left == right->left) {
        tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
        tmpf1->left = left->right;
        tmpf1->right = right->right;
        CtlspFormulaIncrementRefCount(left->right);
        CtlspFormulaIncrementRefCount(right->right);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

        tmpf2 = FormulaCreateWithType(Ctlsp_U_c);
        tmpf2->left = left->left;
        tmpf2->right = tmpf1;
        CtlspFormulaIncrementRefCount(left->left);
        CtlspFormulaIncrementRefCount(tmpf1);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
        return tmpf2;
      }
    }

    /* (ll R lr) + (rl R lr) == (ll+rl) R (lr) */
    if (left->type == Ctlsp_R_c && right->type == Ctlsp_R_c) {
      if (left->right == right->right) {
        tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
        tmpf1->left = left->left;
        tmpf1->right = right->left;
        CtlspFormulaIncrementRefCount(left->left);
        CtlspFormulaIncrementRefCount(right->left);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

        tmpf2 = FormulaCreateWithType(Ctlsp_R_c);
        tmpf2->left = tmpf1;
        tmpf2->right = left->right;
        CtlspFormulaIncrementRefCount(tmpf1);
        CtlspFormulaIncrementRefCount(left->right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
        return tmpf2;
      }
    }

    /* (X ll) + (X rl) == X (ll+rl) */
    if (left->type == Ctlsp_X_c && right->type == Ctlsp_X_c) {
      tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
      tmpf1->left = left->left;
      tmpf1->right = right->left;
      CtlspFormulaIncrementRefCount(left->left);
      CtlspFormulaIncrementRefCount(right->left);
      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

      tmpf2 = FormulaCreateWithType(Ctlsp_X_c);
      tmpf2->left = tmpf1;
      CtlspFormulaIncrementRefCount(tmpf1);
      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
      return tmpf2;
    }

    /* ll U lr  + rl R ll  == ((Xlr + rl) R ll) +lr */
    if (left->type == Ctlsp_U_c && right->type == Ctlsp_R_c) {
      if (left->left == right->right) {
        tmpf1 = FormulaCreateWithType(Ctlsp_X_c);
        tmpf1->left = left->right;
        CtlspFormulaIncrementRefCount(left->right);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

        if (right->left->type != Ctlsp_FALSE_c) {
          tmpf2 = FormulaCreateWithType(Ctlsp_OR_c);
          tmpf2->left = tmpf1;
          tmpf2->right = right->left;
          CtlspFormulaIncrementRefCount(tmpf1);
          CtlspFormulaIncrementRefCount(right->left);
          tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
        }

        tmpf2 = FormulaCreateWithType(Ctlsp_R_c);
        tmpf2->left = tmpf1;
        tmpf2->right = left->left;
        CtlspFormulaIncrementRefCount(tmpf1);
        CtlspFormulaIncrementRefCount(left->left);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);

        tmpf2 = FormulaCreateWithType(Ctlsp_OR_c);
        tmpf2->left = tmpf1;
        tmpf2->right = left->right;
        CtlspFormulaIncrementRefCount(tmpf1);
        CtlspFormulaIncrementRefCount(left->right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);

        return tmpf2;
      }
    }

    /* ll R lr  + lr U rr  == ((Xrr + ll) R lr) + rr */
    if (left->type == Ctlsp_R_c && right->type == Ctlsp_U_c) {
      if (left->right == right->left) {
        tmpf1 = FormulaCreateWithType(Ctlsp_X_c);
        tmpf1->left = right->right;
        CtlspFormulaIncrementRefCount(right->right);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

        if (left->left->type != Ctlsp_FALSE_c) {
          tmpf2 = FormulaCreateWithType(Ctlsp_OR_c);
          tmpf2->left = tmpf1;
          tmpf2->right = left->left;
          CtlspFormulaIncrementRefCount(tmpf1);
          CtlspFormulaIncrementRefCount(left->left);
          tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
        }

        tmpf2 = FormulaCreateWithType(Ctlsp_R_c);
        tmpf2->left = tmpf1;
        tmpf2->right = left->right;
        CtlspFormulaIncrementRefCount(tmpf1);
        CtlspFormulaIncrementRefCount(left->right);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);

        tmpf2 = FormulaCreateWithType(Ctlsp_OR_c);
        tmpf2->left = tmpf1;
        tmpf2->right = right->right;
        CtlspFormulaIncrementRefCount(tmpf1);
        CtlspFormulaIncrementRefCount(right->right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);

        return tmpf2;
      }
    }

    /* ll U lr + r , ll =>r  ==  lr + r ??? */
    if (left->type == Ctlsp_U_c) {
      if (Ctlsp_LtlFormulaSimplyImply(left->left, right)) {
        tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
        tmpf1->left = left->right;
        tmpf1->right = right;
        CtlspFormulaIncrementRefCount(left->right);
        CtlspFormulaIncrementRefCount(right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
        return tmpf2;
      }
    }

    /* l + rl U rr ,  rl => l   ==  rr + l */
    if (right->type == Ctlsp_U_c) {
      if (Ctlsp_LtlFormulaSimplyImply(right->left, left)) {
        tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
        tmpf1->left = left;
        tmpf1->right = right->right;
        CtlspFormulaIncrementRefCount(left);
        CtlspFormulaIncrementRefCount(right->right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
        return tmpf2;
      }
    }

    /* ll R lr + r ,  !ll => r   ==  lr + r */
    if (left->type == Ctlsp_R_c) {
      tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
      tmpf1->left = left->left;
      tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
      FREE(tmpf1);
      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
      if (Ctlsp_LtlFormulaSimplyImply(tmpf2, right)) {
        tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
        tmpf1->left = left->right;
        tmpf1->right = right;
        CtlspFormulaIncrementRefCount(left->right);
        CtlspFormulaIncrementRefCount(right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
        return tmpf2;
      }
    }

    /* l + rl R rr ,  !rl => l   ==  rr + l */
    if (right->type == Ctlsp_R_c) {
      tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
      tmpf1->left = right->left;
      tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
      FREE(tmpf1);
      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
      if (Ctlsp_LtlFormulaSimplyImply(tmpf2, left)) {
        tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
        tmpf1->left = left;
        tmpf1->right = right->right;
        CtlspFormulaIncrementRefCount(left);
        CtlspFormulaIncrementRefCount(right->right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
        return tmpf2;
      }
    }

    /* GF lrr + GF rrr = GF (lrr + rrr) */
    if (Ctlsp_LtlFormulaIsGF(left) && Ctlsp_LtlFormulaIsGF(right)) {
      tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
      tmpf1->left = left->right->right;
      tmpf1->right = right->right->right;
      CtlspFormulaIncrementRefCount(left->right->right);
      CtlspFormulaIncrementRefCount(right->right->right);
      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

      tmpf2 = FormulaCreateWithType(Ctlsp_U_c);
      tmpf2->left = True;
      tmpf2->right = tmpf1;
      CtlspFormulaIncrementRefCount(True);
      CtlspFormulaIncrementRefCount(tmpf1);
      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);

      tmpf2 = FormulaCreateWithType(Ctlsp_R_c);
      tmpf2->left = False;
      tmpf2->right = tmpf1;
      CtlspFormulaIncrementRefCount(False);
      CtlspFormulaIncrementRefCount(tmpf1);
      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
      return tmpf2;
    }

    /* return  (l + r) */
    tmpf1 = FormulaCreateWithType(Ctlsp_OR_c);
    tmpf1->left = left;
    tmpf1->right = right;
    CtlspFormulaIncrementRefCount(left);
    CtlspFormulaIncrementRefCount(right);
    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
    return tmpf2;

  case Ctlsp_U_c:

    /* l -> r : l U r == r */
    if (Ctlsp_LtlFormulaSimplyImply(left, right))
      return right;

    /* l U FALSE = FALSE */
    if (right->type == Ctlsp_FALSE_c)
      return False;

    /* (X ll) U (X rl) == X (ll U rl) */
    if (left->type == Ctlsp_X_c && right->type == Ctlsp_X_c) {
      tmpf1 = FormulaCreateWithType(Ctlsp_U_c);
      tmpf1->left = left->left;
      tmpf1->right = right->left;
      CtlspFormulaIncrementRefCount(left->left);
      CtlspFormulaIncrementRefCount(right->left);
      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

      tmpf2 = FormulaCreateWithType(Ctlsp_X_c);
      tmpf2->left = tmpf1;
      CtlspFormulaIncrementRefCount(tmpf1);
      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
      return tmpf2;
    }

    /* TRUE U (X rl) == X( TRUE U rl ) */
    if (left->type == Ctlsp_TRUE_c && right->type == Ctlsp_X_c) {
      tmpf1 = FormulaCreateWithType(Ctlsp_U_c);
      tmpf1->left = True;
      tmpf1->right = right->left;
      CtlspFormulaIncrementRefCount(True);
      CtlspFormulaIncrementRefCount(right->left);
      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

      tmpf2 = FormulaCreateWithType(Ctlsp_X_c);
      tmpf2->left = tmpf1;
      CtlspFormulaIncrementRefCount(tmpf1);
      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
      return tmpf2;
    }

    /* l->rl : l U (rl U rr) == rl U rr */
    if (right->type == Ctlsp_U_c) {
      if (Ctlsp_LtlFormulaSimplyImply(left, right->left)) {
        return right;
      }
    }

    /* (TRUE or anything) U (FG rrr) == FG rrr */
    /* (TRUE or anything) U (GF rrr) == GF rrr */
    if (/*left->type == Ctlsp_TRUE_c &&*/ Ctlsp_LtlFormulaIsFGorGF(right))
      return right;

    /* TRUE U (rl * FG rrrr) = F(rl) * FG(rrrr) */
    /* TRUE U (rl * GF rrrr) = F(rl) * GF(rrrr) */
    if (left->type == Ctlsp_TRUE_c && right->type == Ctlsp_AND_c) {
      if (Ctlsp_LtlFormulaIsFGorGF(right->right)) {
        tmpf1 = FormulaCreateWithType(Ctlsp_U_c);
        tmpf1->left = True;
        tmpf1->right = right->left;
        CtlspFormulaIncrementRefCount(True);
        CtlspFormulaIncrementRefCount(right->left);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

        tmpf2 = FormulaCreateWithType(Ctlsp_AND_c);
        tmpf2->left = tmpf1;
        tmpf2->right = right->right;
        CtlspFormulaIncrementRefCount(tmpf1);
        CtlspFormulaIncrementRefCount(right->right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
        return tmpf2;
      }
    }

    /* TRUE U (FG rlrr * rr) == (FG rlrr) * F(rr) */
    /* TRUE U (GF rlrr * rr) == (GF rlrr) * F(rr) */
    if (left->type == Ctlsp_TRUE_c && right->type == Ctlsp_AND_c) {
      if (Ctlsp_LtlFormulaIsFGorGF(right->left)) {
        tmpf1 = FormulaCreateWithType(Ctlsp_U_c);
        tmpf1->left = True;
        tmpf1->right = right->right;
        CtlspFormulaIncrementRefCount(True);
        CtlspFormulaIncrementRefCount(right->right);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

        tmpf2 = FormulaCreateWithType(Ctlsp_AND_c);
        tmpf2->left = right->left;
        tmpf2->right = tmpf1;
        CtlspFormulaIncrementRefCount(right->left);
        CtlspFormulaIncrementRefCount(tmpf1);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
        return tmpf2;
      }
    }

    /* !r -> l : (l U r) == TRUE U r */
    tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
    tmpf1->left = right;
    tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
    FREE(tmpf1);
    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
    if (Ctlsp_LtlFormulaSimplyImply(tmpf2, left)) {
      tmpf1 = FormulaCreateWithType(Ctlsp_U_c);
      tmpf1->left = True;
      tmpf1->right = right;
      CtlspFormulaIncrementRefCount(True);
      CtlspFormulaIncrementRefCount(right);
      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
      return tmpf2;
    }

    /* (ll + lr) U r,  ll => r   == (lr U r) */
    if (left->type == Ctlsp_OR_c) {
      if (Ctlsp_LtlFormulaSimplyImply(left->left, right)) {
        tmpf1 = FormulaCreateWithType(Ctlsp_U_c);
        tmpf1->left = left->right;
        tmpf1->right = right;
        CtlspFormulaIncrementRefCount(left->right);
        CtlspFormulaIncrementRefCount(right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
        return tmpf2;
      }
    }

    /* (ll + lr) U r,  lr => r   == (ll U r) */
    if (left->type == Ctlsp_OR_c) {
      if (Ctlsp_LtlFormulaSimplyImply(left->right, right)) {
        tmpf1 = FormulaCreateWithType(Ctlsp_U_c);
        tmpf1->left = left->left;
        tmpf1->right = right;
        CtlspFormulaIncrementRefCount(left->left);
        CtlspFormulaIncrementRefCount(right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
        return tmpf2;
      }
    }


    /* return  (left U right) */
    tmpf1 = FormulaCreateWithType(Ctlsp_U_c);
    tmpf1->left = left;
    tmpf1->right = right;
    CtlspFormulaIncrementRefCount(left);
    CtlspFormulaIncrementRefCount(right);
    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
    return tmpf2;

  case Ctlsp_R_c:

    /* r -> l : l R r == r */
    if (Ctlsp_LtlFormulaSimplyImply(right,left))
      return right;

    /* l R TRUE == TRUE */
    if (right->type == Ctlsp_TRUE_c)
      return True;

    /* (X ll) R (X rl) == X (ll R rl) */
    if (left->type == Ctlsp_X_c && right->type == Ctlsp_X_c) {
      tmpf1 = FormulaCreateWithType(Ctlsp_R_c);
      tmpf1->left = left->left;
      tmpf1->right = right->left;
      CtlspFormulaIncrementRefCount(left->left);
      CtlspFormulaIncrementRefCount(right->left);
      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

      tmpf2 = FormulaCreateWithType(Ctlsp_X_c);
      tmpf2->left = tmpf1;
      CtlspFormulaIncrementRefCount(tmpf1);
      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
      return tmpf2;
    }

    /* FALSE R (X rl) == X( FALSE R rl) */
    if (left->type == Ctlsp_TRUE_c && right->type == Ctlsp_X_c) {
      tmpf1 = FormulaCreateWithType(Ctlsp_R_c);
      tmpf1->left = False;
      tmpf1->right = right->left;
      CtlspFormulaIncrementRefCount(False);
      CtlspFormulaIncrementRefCount(right->left);
      tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

      tmpf2 = FormulaCreateWithType(Ctlsp_X_c);
      tmpf2->left = tmpf1;
      CtlspFormulaIncrementRefCount(tmpf1);
      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
      return tmpf2;
    }

    /* rl->l :  l R (rl R rr) == (rl R rr) */
    if (right->type == Ctlsp_R_c)
      if (Ctlsp_LtlFormulaSimplyImply(right->left, left))
        return right;

    /* (FALSE or anything) R (FG rrr) == FG rrr */
    /* (FALSE or anything) R (GF rrr) == GF rrr */
    if (/*left->type == Ctlsp_FALSE_c &&*/ Ctlsp_LtlFormulaIsFGorGF(right))
      return right;

    /* FALSE R (rl + FG rrrr) = G(rl) + FG(rrrr) */
    /* FALSE R (rl + GF rrrr) = G(rl) + GF(rrrr) */
    if (left->type == Ctlsp_FALSE_c && right->type == Ctlsp_OR_c) {
      if (Ctlsp_LtlFormulaIsFGorGF(right->right)) {
        tmpf1 = FormulaCreateWithType(Ctlsp_R_c);
        tmpf1->left = False;
        tmpf1->right = right->left;
        CtlspFormulaIncrementRefCount(False);
        CtlspFormulaIncrementRefCount(right->left);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

        tmpf2 = FormulaCreateWithType(Ctlsp_OR_c);
        tmpf2->left = tmpf1;
        tmpf2->right = right->right;
        CtlspFormulaIncrementRefCount(tmpf1);
        CtlspFormulaIncrementRefCount(right->right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
        return tmpf2;
      }
    }

    /* FALSE R (FG rlrr + rr) = FG(rlrr) + G(rr) */
    /* FALSE R (GF rlrr + rr) = GF(rlrr) + G(rr) */
    if (left->type == Ctlsp_FALSE_c && right->type == Ctlsp_OR_c) {
      if (Ctlsp_LtlFormulaIsFGorGF(right->left)) {
        tmpf1 = FormulaCreateWithType(Ctlsp_R_c);
        tmpf1->left = False;
        tmpf1->right = right->right;
        CtlspFormulaIncrementRefCount(False);
        CtlspFormulaIncrementRefCount(right->right);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

        tmpf2 = FormulaCreateWithType(Ctlsp_OR_c);
        tmpf2->left = tmpf1;
        tmpf2->right = right->left;
        CtlspFormulaIncrementRefCount(tmpf1);
        CtlspFormulaIncrementRefCount(right->left);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
        return tmpf2;
      }
    }

    /* r -> !l : (l R r) == FALSE R r */
    tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
    tmpf1->left = left;
    tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1);
    FREE(tmpf1);
    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
    if (Ctlsp_LtlFormulaSimplyImply(right, tmpf2)) {
      tmpf1 = FormulaCreateWithType(Ctlsp_R_c);
      tmpf1->left = False;
      tmpf1->right = right;
      CtlspFormulaIncrementRefCount(False);
      CtlspFormulaIncrementRefCount(right);
      tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
      return tmpf2;
    }

    /* r=>ll : (ll * lr) R r  ==  lr R r */
    if (left->type == Ctlsp_AND_c) {
      if (Ctlsp_LtlFormulaSimplyImply(right, left->left)) {
        tmpf1 = FormulaCreateWithType(Ctlsp_R_c);
        tmpf1->left = left->right;
        tmpf1->right = right;
        CtlspFormulaIncrementRefCount(left->right);
        CtlspFormulaIncrementRefCount(right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
        return tmpf2;
      }
    }

    /* r=>lr : (ll * lr) R r  ==  ll R r */
    if (left->type == Ctlsp_AND_c) {
      if (Ctlsp_LtlFormulaSimplyImply(right, left->right)) {
        tmpf1 = FormulaCreateWithType(Ctlsp_R_c);
        tmpf1->left = left->left;
        tmpf1->right = right;
        CtlspFormulaIncrementRefCount(left->left);
        CtlspFormulaIncrementRefCount(right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
        return tmpf2;
      }
    }


    /* return  (left R right) */
    tmpf1 = FormulaCreateWithType(Ctlsp_R_c);
    tmpf1->left = left;
    tmpf1->right = right;
    CtlspFormulaIncrementRefCount(left);
    CtlspFormulaIncrementRefCount(right);
    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
    return tmpf2;

  case Ctlsp_X_c:

    /* X(TRUE) == TRUE */
    /* X(FALSE) == FALSE */
    if (left->type == Ctlsp_TRUE_c || left->type == Ctlsp_FALSE_c)
      return left;

    /* X(FGorGF) == FGorGF */
    if (Ctlsp_LtlFormulaIsFGorGF(left))
      return left;

    /* X(ll + FGorGF lrrr) == X(ll) + FGorGF lrrr */
    /* X(ll * FGorGF lrrr) == X(ll) * FGorGF lrrr */
    if (left->type == Ctlsp_AND_c || left->type == Ctlsp_OR_c) {
      if (Ctlsp_LtlFormulaIsFGorGF(left->right)) {
        tmpf1 = FormulaCreateWithType(Ctlsp_X_c);
        tmpf1->left = left->left;
        CtlspFormulaIncrementRefCount(left->left);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

        tmpf2 = FormulaCreateWithType(left->type);
        tmpf2->left = tmpf1;
        tmpf2->right = left->right;
        CtlspFormulaIncrementRefCount(tmpf1);
        CtlspFormulaIncrementRefCount(left->right);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
        return tmpf2;
      }
    }

    /* X(FGorGF llrr + lr) ==  FGorGF llrr + X(lr) */
    /* X(FGorGF llrr * lr) ==  FGorGF llrr * X(lr) */
    if (left->type == Ctlsp_AND_c || left->type == Ctlsp_OR_c) {
      if (Ctlsp_LtlFormulaIsFGorGF(left->left)) {
        tmpf1 = FormulaCreateWithType(Ctlsp_X_c);
        tmpf1->left = left->right;
        CtlspFormulaIncrementRefCount(left->right);
        tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);

        tmpf2 = FormulaCreateWithType(left->type);
        tmpf2->left = left->left;
        tmpf2->right = tmpf1;
        CtlspFormulaIncrementRefCount(left->left);
        CtlspFormulaIncrementRefCount(tmpf1);
        tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable);
        return tmpf2;
      }
    }

    /* return X(left) */
    tmpf1 = FormulaCreateWithType(Ctlsp_X_c);
    tmpf1->left = left;
    CtlspFormulaIncrementRefCount(left);
    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
    return tmpf2;

  case Ctlsp_NOT_c:

    /* return !(left) */
    tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c);
    tmpf1->left = left;
    CtlspFormulaIncrementRefCount(left);
    tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable);
    return tmpf2;

  default:
    assert(0);
  }
  return NIL(Ctlsp_Formula_t);
}

/**Function********************************************************************

  Synopsis    [Increments the reference count of a formula.]

  Description [The function increments the reference count of a formula. If
  the formula is NULL, the function does nothing.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
CtlspFormulaIncrementRefCount(
  Ctlsp_Formula_t *formula)
{
  if(formula!=NIL(Ctlsp_Formula_t)) {
    ++(formula->refCount);
  }
}

/**Function********************************************************************

  Synopsis    [Decrements the reference count of a formula.]

  Description [The function decrements the reference count of formula and if
  the reference count reaches 0, the formula is freed. If the formula is NULL,
  the function does nothing. It is an error to decrement the reference count
  below 0.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
CtlspFormulaDecrementRefCount(
  Ctlsp_Formula_t *formula)
{
  if(formula!=NIL(Ctlsp_Formula_t)) {
    assert(formula->refCount>0);
    if(--(formula->refCount) == 0)
      CtlspFormulaFree(formula);
  }
}
/**Function********************************************************************

  Synopsis    [Adds formula to the end of globalFormulaArray.]

  SideEffects [Manipulates the global variable globalFormulaArray.]

  SeeAlso     [CtlspYyparse]

******************************************************************************/
void
CtlspFormulaAddToGlobalArray(
  Ctlsp_Formula_t * formula)
{
  array_insert_last(Ctlsp_Formula_t *, globalFormulaArray, formula);
}

/**Function********************************************************************

  Synopsis    [Frees a CTL* formula.]

  Description [The function frees all memory associated with the formula,
  including all MDDs and all character strings (however, does not free
  dbgInfo.originalFormula). It also decrements the reference counts of its two
  chidren. The function does nothing if formula is NULL.]

  SideEffects []

  SeeAlso     [Ctlsp_FormulaArrayFree]

******************************************************************************/
void
CtlspFormulaFree(
  Ctlsp_Formula_t * formula)
{
  if (formula != NIL(Ctlsp_Formula_t)) {

    /*
     * Free any fields that are not NULL.
     */

    if (formula->type == Ctlsp_ID_c){
      FREE(formula->left);
      FREE(formula->right);
    }
    else {
      if (formula->left  != NIL(Ctlsp_Formula_t)) {
        CtlspFormulaDecrementRefCount(formula->left);
      }
      if (formula->right != NIL(Ctlsp_Formula_t)) {
        CtlspFormulaDecrementRefCount(formula->right);
      }
    }

    if (formula->states != NIL(mdd_t))
      mdd_free(formula->states);
    if (formula->underapprox != NIL(mdd_t))
      mdd_free(formula->underapprox);
    if (formula->overapprox != NIL(mdd_t))
      mdd_free(formula->overapprox);

    if (formula->dbgInfo.data != NIL(void)){
      (*formula->dbgInfo.freeFn)(formula);
    }

    FREE(formula);
  }
}


/**Function********************************************************************

  Synopsis    [Create a binary string of given value with size of interval.]

  Description [The value is a binary string starting with 'b', a
  hexadecimal string starting with 'x', or an integer string.  If value
  does not fit the interval, or the binary string is not of the
  correct length, 0 is return.  Otherwise 1 is returned.  The result
  string is saved at given pointer.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
CtlspStringChangeValueStrToBinString(
  char *value,
  char *binValueStr,
  int  interval)
{
  int i;
  long int num, mask;
  double maxNum;
  char *ptr;

  mask = 1;
  maxNum = pow(2.0,(double)interval);
  errno = 0;

  if(value[0] == 'b'){
    if ((int)strlen(value)-1 == interval){
                        for(i=1;i<=interval;i++){
        if (value[i] == '0' || value[i] == '1'){
          binValueStr[i-1] =  value[i];
        }else{
          return 0;
        }
      }
      binValueStr[interval] = '\0';
    }else{
      return 0;
    }
  }else if (value[0] == 'x'){
    for(i=1; i < (int)strlen(value); i++){
      if (!isxdigit((int)value[i])){
        return 0;
      }
    }
    num = strtol(++value,&ptr,16);
    if (errno) return 0;
    if (num >= maxNum) return 0;
    for(i=0;i<interval;i++){
      if(num & (mask<<i)) binValueStr[interval-i-1] = '1';
      else binValueStr[interval-i-1] = '0';
    }
    binValueStr[interval] = '\0';
  }else{
    for(i=0;i<(int)strlen(value);i++){
      if (!isdigit((int)value[i])){
        return 0;
      }
    }
    num = strtol(value,&ptr,0);
    if (errno) return 0;
    if (num >= maxNum) return 0;
    mask = 1;
    for(i=0;i<interval;i++){
      if(num & (mask<<i)) binValueStr[interval-i-1] = '1';
      else binValueStr[interval-i-1] = '0';
    }
    binValueStr[interval] = '\0';
  }

  return(1);
}


/**Function********************************************************************

  Synopsis    [Change [] to <>]

  Description []

  SideEffects [The input string contains ...[num] and this function changes it
  to ...<num>.]

  SeeAlso     []

******************************************************************************/
void
CtlspChangeBracket(
  char *inStr)
{
  int i, j;
  char *str;

  j = 0;
  for (i=0;i<(int)strlen(inStr)+1;i++){
    if (inStr[i] != ' '){
      inStr[i-j] = inStr[i];
    }else{
      j++;
    }
  }

  if (changeBracket == 0)
    return;

  str = strchr(inStr,'[');
  if (str == NULL) return;

  *str = '<';
  str = strchr(inStr,']');
  *str = '>';
}


/**Function********************************************************************

  Synopsis    [Parse a given vector string.]

  Description [Parse given vector string of the form of var<i:j> and
  string var is returned. Other information such as i, j, interval between
  i and j, and increment or decrement from i to j are saved.]

  SideEffects []

  SeeAlso     []

******************************************************************************/
char *
CtlspGetVectorInfoFromStr(
  char *str,
  int  *start,
  int  *end,
  int  *interval,
  int  *inc)
{
  char *str1, *str2, *str3;
  char *startStr, *endStr;
  char *name, *ptr;

  str1 = strchr(str,'[');
  str2 = strchr(str,':');
  str3 = strchr(str,']');
  startStr = ALLOC(char, str2-str1);
  endStr = ALLOC(char, str3-str2);
  name = ALLOC(char, str1-str+1);

  (void) strncpy(name, str, str1-str);
  (void) strncpy(startStr, str1+1, str2-str1-1);
  (void) strncpy(endStr, str2+1, str3-str2-1);

  startStr[str2-str1-1] = '\0';
  endStr[str3-str2-1] = '\0';
  name[str1-str] = '\0';
  *start = strtol(startStr,&ptr,0);
  *end = strtol(endStr,&ptr,0);
  if(*start > *end){
      *inc = -1;
      *interval = *start - *end + 1;
  } else {
      *inc = 1;
      *interval = *end - *start + 1;
  }
  FREE(startStr);
  FREE(endStr);
  return name;
}

/**Function********************************************************************

  Synopsis    [Insert macro formula into symbol table.]

  Description [If the name is already in table return 0, otherwise insert the
  formula into the table and return 1]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
CtlspFormulaAddToTable(
  char *name,
  Ctlsp_Formula_t *formula,
  st_table *macroTable)
{
  if(macroTable == NIL(st_table)){
    macroTable = st_init_table(strcmp, st_strhash);
  }
  if(st_is_member(macroTable, name)){
    return 0;
  }
  st_insert(macroTable, name, (char *)formula);
  return 1;
}


/**Function********************************************************************

  Synopsis    [Get macro formula from symbol table]

  Description [If macro string is not found in table, NULL pointer is returned]

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
CtlspFormulaFindInTable(
  char *name,
  st_table *macroTable)
{
  Ctlsp_Formula_t *formula;
  if (st_lookup(macroTable, name, &formula)){
    return (Ctlsp_FormulaDup(formula));
  }else{
    return NIL(Ctlsp_Formula_t);
  }
}

/**Function********************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso [FormulaTestIsForallQuantifier]

******************************************************************************/
Ctlsp_FormulaClass
CtlspCheckClassOfExistentialFormulaRecur(
  Ctlsp_Formula_t *formula,
  boolean parity)
{
  Ctlsp_FormulaClass result;

  Ctlsp_FormulaType formulaType = Ctlsp_FormulaReadType(formula);
  Ctlsp_Formula_t *rightFormula, *leftFormula;
  Ctlsp_FormulaClass resultLeft, resultRight, tempResult, currentClass;

  /* Depending on the formula type, create result or recur */
  switch (formulaType) {
  case Ctlsp_E_c:
    leftFormula = Ctlsp_FormulaReadLeftChild(formula);
    resultLeft = CtlspCheckClassOfExistentialFormulaRecur(leftFormula, parity);
      resultRight = Ctlsp_QuantifierFree_c;
    tempResult = CtlspResolveClass(resultLeft, resultRight);
    if (!parity){
      currentClass = Ctlsp_ECTL_c;
    }else{
      currentClass = Ctlsp_ACTL_c;
    }
    result = CtlspResolveClass(currentClass, tempResult);
    break;
  case Ctlsp_A_c:
    /* The formula is supposed to be only existential */
    error_append("Inconsistency detected in function ");
    error_append("FormulaTestIsForallQuantifier\n");
    result = Ctlsp_invalid_c;
    break;
  case Ctlsp_OR_c:
  case Ctlsp_AND_c:
    rightFormula = Ctlsp_FormulaReadRightChild(formula);
    leftFormula = Ctlsp_FormulaReadLeftChild(formula);
    resultLeft = CtlspCheckClassOfExistentialFormulaRecur(leftFormula, parity);
    resultRight = CtlspCheckClassOfExistentialFormulaRecur(rightFormula, parity);
    result = CtlspResolveClass(resultLeft, resultRight);
    break;
  case Ctlsp_NOT_c:
    parity = !parity;
    leftFormula = Ctlsp_FormulaReadLeftChild(formula);
    result = CtlspCheckClassOfExistentialFormulaRecur(leftFormula, parity);
    break;
  case Ctlsp_ID_c:
  case Ctlsp_TRUE_c:
  case Ctlsp_FALSE_c:
     result = Ctlsp_QuantifierFree_c;
     break;
  case Ctlsp_Cmp_c:
    result = Ctlsp_Mixed_c;
    break;
  default:
    error_append("Unexpected operator detected.");
    result = Ctlsp_invalid_c;
    break;
  }

  return result;

} /* End of FormulaTestIsForallQuantifier */

/**Function********************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso []

******************************************************************************/
Ctlsp_FormulaClass
CtlspResolveClass(
  Ctlsp_FormulaClass class1,
  Ctlsp_FormulaClass class2)
{
  Ctlsp_FormulaClass result;

  if ((class1 == Ctlsp_Mixed_c) || (class2 == Ctlsp_Mixed_c)){
    result = Ctlsp_Mixed_c;
  }else if (class1 == Ctlsp_QuantifierFree_c){
    result = class2;
  }else if (class2 == Ctlsp_QuantifierFree_c){
    result = class1;
  }else if (class1 == class2){
    result = class1;
  }else{
    result = Ctlsp_Mixed_c;
  }
  return result;
}

/**Function********************************************************************

  Synopsis    [Performs a recursive step of Ctlsp_FormulaConvertToCTL() ]

  Description []

  SideEffects []

  Remarks []

  SeeAlso []

******************************************************************************/
Ctlp_Formula_t *
CtlspFormulaConvertToCTL(
  Ctlsp_Formula_t *formula)
{
  Ctlp_Formula_t *newNode, *leftNode, *rightNode;
  Ctlsp_Formula_t *childNode;
  char *variableNameCopy, *valueNameCopy;

  if (formula == NIL(Ctlsp_Formula_t)) {
    return NIL(Ctlp_Formula_t);
  }
  /*
   * Recursively convert each subformula.
   */
  switch(formula->type) {
  case Ctlsp_E_c:
    childNode = formula->left;
    switch(childNode->type) {
    case Ctlsp_X_c:
      newNode = Ctlp_FormulaCreate(Ctlp_EX_c,
                                   CtlspFormulaConvertToCTL(childNode->left),
                                   NIL(Ctlsp_Formula_t));
      break;
    case Ctlsp_F_c:
      newNode = Ctlp_FormulaCreate(Ctlp_EF_c,
                                   CtlspFormulaConvertToCTL(childNode->left),
                                   NIL(Ctlsp_Formula_t));
      break;
    case Ctlsp_U_c:
      newNode = Ctlp_FormulaCreate(Ctlp_EU_c,
                                   CtlspFormulaConvertToCTL(childNode->left),
                                   CtlspFormulaConvertToCTL(childNode->right));
      break;
    case Ctlsp_R_c:
      /* E(f R g) => !A( !f U !g) */

      leftNode  =  Ctlp_FormulaCreate(Ctlp_NOT_c,
                   CtlspFormulaConvertToCTL(childNode->left),
                   NIL(Ctlsp_Formula_t));
      rightNode =  Ctlp_FormulaCreate(Ctlp_NOT_c,
                   CtlspFormulaConvertToCTL(childNode->right),
                   NIL(Ctlsp_Formula_t));

      newNode = Ctlp_FormulaCreate(Ctlp_AU_c, leftNode, rightNode);
      newNode = Ctlp_FormulaCreate(Ctlp_NOT_c, newNode, NIL(Ctlsp_Formula_t));

      break;
    case Ctlsp_W_c:
      /* E(f W g) => !A(!g U !(f + g)) */

      leftNode  =  Ctlp_FormulaCreate(Ctlp_NOT_c,
                   CtlspFormulaConvertToCTL(childNode->right),
                   NIL(Ctlsp_Formula_t));
      rightNode =  Ctlp_FormulaCreate(Ctlp_OR_c,
                   CtlspFormulaConvertToCTL(childNode->left),
                   CtlspFormulaConvertToCTL(childNode->right));
      rightNode =  Ctlp_FormulaCreate(Ctlp_NOT_c, rightNode,
                   NIL(Ctlsp_Formula_t));

      newNode = Ctlp_FormulaCreate(Ctlp_AU_c, leftNode, rightNode);
      newNode = Ctlp_FormulaCreate(Ctlp_NOT_c, newNode, NIL(Ctlsp_Formula_t));

      break;
    case Ctlsp_G_c:
      newNode = Ctlp_FormulaCreate(Ctlp_EG_c,
                                   CtlspFormulaConvertToCTL(childNode->left),
                                   NIL(Ctlsp_Formula_t));
      break;
    default:
      fail("Unexpected type");
    } /* switch: childNode->type */
    break;
  case Ctlsp_A_c:
    childNode = formula->left;
    switch(childNode->type) {
    case Ctlsp_X_c:
      newNode = Ctlp_FormulaCreate(Ctlp_AX_c,
                                   CtlspFormulaConvertToCTL(childNode->left),
                                   NIL(Ctlsp_Formula_t));
      break;
    case Ctlsp_F_c:
      newNode = Ctlp_FormulaCreate(Ctlp_AF_c,
                                   CtlspFormulaConvertToCTL(childNode->left),
                                   NIL(Ctlsp_Formula_t));
      break;
    case Ctlsp_U_c:
      newNode = Ctlp_FormulaCreate(Ctlp_AU_c,
                                   CtlspFormulaConvertToCTL(childNode->left),
                                   CtlspFormulaConvertToCTL(childNode->right));
      break;
    case Ctlsp_R_c:
      /* A(f R g) => !E( !f U !g) */

      leftNode  =  Ctlp_FormulaCreate(Ctlp_NOT_c,
                   CtlspFormulaConvertToCTL(childNode->left),
                   NIL(Ctlsp_Formula_t));
      rightNode =  Ctlp_FormulaCreate(Ctlp_NOT_c,
                   CtlspFormulaConvertToCTL(childNode->right),
                   NIL(Ctlsp_Formula_t));

      newNode = Ctlp_FormulaCreate(Ctlp_EU_c, leftNode, rightNode);
      newNode = Ctlp_FormulaCreate(Ctlp_NOT_c, newNode, NIL(Ctlsp_Formula_t));

      break;
    case Ctlsp_W_c:
      /* A(f W g) => !E(!g U !(f + g)) */

      leftNode  =  Ctlp_FormulaCreate(Ctlp_NOT_c,
                   CtlspFormulaConvertToCTL(childNode->right),
                   NIL(Ctlsp_Formula_t));
      rightNode =  Ctlp_FormulaCreate(Ctlp_OR_c,
                   CtlspFormulaConvertToCTL(childNode->left),
                   CtlspFormulaConvertToCTL(childNode->right));
      rightNode =  Ctlp_FormulaCreate(Ctlp_NOT_c, rightNode,
                   NIL(Ctlsp_Formula_t));

      newNode = Ctlp_FormulaCreate(Ctlp_EU_c, leftNode, rightNode);
      newNode = Ctlp_FormulaCreate(Ctlp_NOT_c, newNode, NIL(Ctlsp_Formula_t));

      break;
    case Ctlsp_G_c:
      newNode = Ctlp_FormulaCreate(Ctlp_AG_c,
                                   CtlspFormulaConvertToCTL(childNode->left),
                                   NIL(Ctlsp_Formula_t));
      break;
    default:
      fail("Unexpected type");
    } /* switch: childNode->type */
    break;

  case Ctlsp_ID_c:
    /* Make a copy of the name, and create a new formula. */
    variableNameCopy = util_strsav((char *)(formula->left));
    valueNameCopy = util_strsav((char *)(formula->right));
    newNode = Ctlp_FormulaCreate(Ctlp_ID_c, variableNameCopy, valueNameCopy);
    break;

  case Ctlsp_THEN_c:
    newNode = Ctlp_FormulaCreate(Ctlp_THEN_c,
                                 CtlspFormulaConvertToCTL(formula->left) ,
                                 CtlspFormulaConvertToCTL(formula->right) );
    break;
  case Ctlsp_OR_c:
    newNode = Ctlp_FormulaCreate(Ctlp_OR_c,
                                 CtlspFormulaConvertToCTL(formula->left) ,
                                 CtlspFormulaConvertToCTL(formula->right) );
    break;
  case Ctlsp_AND_c:
    newNode = Ctlp_FormulaCreate(Ctlp_AND_c,
                                 CtlspFormulaConvertToCTL(formula->left) ,
                                 CtlspFormulaConvertToCTL(formula->right) );
    break;
  case Ctlsp_NOT_c:
    newNode = Ctlp_FormulaCreate(Ctlp_NOT_c,
                                 CtlspFormulaConvertToCTL(formula->left) ,
                                 CtlspFormulaConvertToCTL(formula->right) );
    break;
  case Ctlsp_XOR_c:
    newNode = Ctlp_FormulaCreate(Ctlp_XOR_c,
                                 CtlspFormulaConvertToCTL(formula->left) ,
                                 CtlspFormulaConvertToCTL(formula->right) );
    break;
  case Ctlsp_EQ_c:
    newNode = Ctlp_FormulaCreate(Ctlp_EQ_c,
                                 CtlspFormulaConvertToCTL(formula->left) ,
                                 CtlspFormulaConvertToCTL(formula->right) );
    break;
  case Ctlsp_TRUE_c:
    newNode = Ctlp_FormulaCreate(Ctlp_TRUE_c,
                                 CtlspFormulaConvertToCTL(formula->left) ,
                                 CtlspFormulaConvertToCTL(formula->right) );
    break;
  case Ctlsp_FALSE_c:
    newNode = Ctlp_FormulaCreate(Ctlp_FALSE_c,
                                 CtlspFormulaConvertToCTL(formula->left) ,
                                 CtlspFormulaConvertToCTL(formula->right) );
    break;
  default:
    fail("Unexpected type");
  }

  return newNode;
} /* CtlspFormulaConvertToCTL() */


/**Function********************************************************************

  Synopsis    [Performs OR function]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
CtlspFunctionOr(
  Ctlsp_Formula_t *left,
  Ctlsp_Formula_t *right)
{
  Ctlsp_Formula_t *result;

  if((Ctlsp_FormulaReadType(left)  == Ctlsp_TRUE_c) ||
     (Ctlsp_FormulaReadType(right) == Ctlsp_TRUE_c)){
    result = Ctlsp_FormulaCreate(Ctlsp_TRUE_c, NIL(Ctlsp_Formula_t),
                                 NIL(Ctlsp_Formula_t));;
  } else
    if(Ctlsp_FormulaReadType(left) == Ctlsp_FALSE_c){
      result = right;
    } else
      if(Ctlsp_FormulaReadType(right) == Ctlsp_FALSE_c){
        result = left;
      } else
        result = Ctlsp_FormulaCreate(Ctlsp_OR_c, left, right);

  return result;
}

/**Function********************************************************************

  Synopsis    [Performs And function]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
CtlspFunctionAnd(
  Ctlsp_Formula_t *left,
  Ctlsp_Formula_t *right)
{
  Ctlsp_Formula_t *result;

  if((Ctlsp_FormulaReadType(left)  == Ctlsp_FALSE_c) ||
     (Ctlsp_FormulaReadType(right) == Ctlsp_FALSE_c)){
    result = Ctlsp_FormulaCreate(Ctlsp_FALSE_c, NIL(Ctlsp_Formula_t),
                                 NIL(Ctlsp_Formula_t));;
  } else
    if(Ctlsp_FormulaReadType(left) == Ctlsp_TRUE_c){
      result = right;
    } else
      if(Ctlsp_FormulaReadType(right) == Ctlsp_TRUE_c){
        result = left;
      } else
        result = Ctlsp_FormulaCreate(Ctlsp_AND_c, left, right);

  return result;
}

/**Function********************************************************************

  Synopsis    [Performs Then(Imply) function]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
Ctlsp_Formula_t *
CtlspFunctionThen(
  Ctlsp_Formula_t *left,
  Ctlsp_Formula_t *right)
{
  Ctlsp_Formula_t *result;

  if((Ctlsp_FormulaReadType(left)  == Ctlsp_TRUE_c) &&
     (Ctlsp_FormulaReadType(right) == Ctlsp_FALSE_c)){
    result = Ctlsp_FormulaCreate(Ctlsp_FALSE_c, NIL(Ctlsp_Formula_t),
                                 NIL(Ctlsp_Formula_t));
  } else
    if(Ctlsp_FormulaReadType(left) == Ctlsp_FALSE_c){
      result = Ctlsp_FormulaCreate(Ctlsp_TRUE_c, NIL(Ctlsp_Formula_t),
                                   NIL(Ctlsp_Formula_t));
    } else
      if((Ctlsp_FormulaReadType(left)  == Ctlsp_TRUE_c) &&
         (Ctlsp_FormulaReadType(right) == Ctlsp_TRUE_c)){
        result = Ctlsp_FormulaCreate(Ctlsp_TRUE_c, NIL(Ctlsp_Formula_t),
                                     NIL(Ctlsp_Formula_t));
      } else
        result = Ctlsp_FormulaCreate(Ctlsp_THEN_c, left, right);

  return result;
}

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [Creates a CTL* formula with just the type set.]

  Description [Calls Ctlsp_FormulaCreate with type, and all other fields NULL.]

  SideEffects []

  SeeAlso     [Ctlsp_FormulaCreate]

******************************************************************************/
static Ctlsp_Formula_t *
FormulaCreateWithType(
  Ctlsp_FormulaType type)
{
  return (Ctlsp_FormulaCreate(type, NIL(Ctlsp_Formula_t), NIL(Ctlsp_Formula_t)));
}


/**Function********************************************************************

  Synopsis    [The comparison function for the formula unique table.]

  Description [The function takes as parameters two CTL* formulae. It compares
  the formula type, the left child and the right child, and returns 0 if they
  match. Otherwise, it returns -1.]

  SideEffects []

  SeeAlso     [FormulaHash]

******************************************************************************/
static int
FormulaCompare(
  const char *key1,
  const char *key2)
{
  Ctlsp_Formula_t *formula1 = (Ctlsp_Formula_t *) key1;
  Ctlsp_Formula_t *formula2 = (Ctlsp_Formula_t *) key2;

  assert(key1 != NIL(char));
  assert(key2 != NIL(char));


  if(formula1->type != formula2->type) {
    return -1;
  }
  if(formula1->type == Ctlsp_ID_c) {
    if(strcmp((char *) (formula1->left), (char *) (formula2->left)) ||
       strcmp((char *) (formula1->right), (char *) (formula2->right))) {
      return -1;
    } else
      return 0;
  } else {
    if(formula1->left != formula2->left)
      return -1;
    if(formula1->right != formula2->right)
      return -1;
    if (formula1->type == Ctlsp_Cmp_c &&
        formula1->compareValue != formula2->compareValue) {
      return -1;
    }
    return 0;
  }
}

/**Function********************************************************************

  Synopsis    [The hash function for the formula unique table.]

  Description [The function takes as parameter a CTL* formula. If the formula
  type is Ctlsp_ID_c, st_strhash is used with a concatenation of left and
  right children as the key string. Otherwise, something very similar to
  st_ptrhash is done.]

  SideEffects []

  SeeAlso     [FormulaCompare]

******************************************************************************/
static int
FormulaHash(
  char *key,
  int modulus)
{
  char *hashString;
  int hashValue;
  Ctlsp_Formula_t *formula = (Ctlsp_Formula_t *) key;

  if(formula->type==Ctlsp_ID_c) {
    hashString = util_strcat3((char *) (formula->left), (char *)
                              (formula->right), "");
    hashValue = st_strhash(hashString, modulus);
    FREE(hashString);
    return hashValue;
  }
  return (int) ((((unsigned long) formula->left >>2) +
                 ((unsigned long) formula->right >>2)) % modulus);
}

/**Function********************************************************************

  Synopsis    [Hashes the formula into the unique table.]

  Description [The function takes a formula and hashes it and all its
  subformulae into a unique table. It returns the unique formula identical to
  the formula being hashed. The formula returned will have maximum sharing
  with the formulae that are already present in uniqueTable. It returns
  NIL(Ctlsp_Formula_t) if the formula is NIL(Ctlsp_Formula_t).]

  SideEffects [If a copy of some subformula of formula is present in
  uniqueTable then the copy is substituted for it and the reference count of
  the subformula is decremented.]

  SeeAlso     [FormulaCompare]

******************************************************************************/
static Ctlsp_Formula_t *
FormulaHashIntoUniqueTable(
  Ctlsp_Formula_t *formula,
  st_table *uniqueTable)
{
  Ctlsp_Formula_t *uniqueFormula, *uniqueLeft, *uniqueRight;

  if(formula == NIL(Ctlsp_Formula_t))
    return NIL(Ctlsp_Formula_t);
  if(st_lookup(uniqueTable, formula, &uniqueFormula)) {
    return uniqueFormula;
  }
  else {
    if(formula->type == Ctlsp_ID_c) {
      st_insert(uniqueTable, (char *) formula, (char *) formula);
      return formula;
    }
    else {
      uniqueLeft = FormulaHashIntoUniqueTable(formula->left, uniqueTable);
      if(uniqueLeft != NIL(Ctlsp_Formula_t))
        if(uniqueLeft != formula->left) {
          CtlspFormulaDecrementRefCount(formula->left);
          formula->left = uniqueLeft;
          CtlspFormulaIncrementRefCount(formula->left);
        }
      uniqueRight = FormulaHashIntoUniqueTable(formula->right, uniqueTable);
      if(uniqueRight != NIL(Ctlsp_Formula_t))
        if(uniqueRight != formula->right) {
          CtlspFormulaDecrementRefCount(formula->right);
          formula->right = uniqueRight;
          CtlspFormulaIncrementRefCount(formula->right);
        }
      if(st_lookup(uniqueTable, formula, &uniqueFormula)) {
        return uniqueFormula;
      }
      else {
        st_insert(uniqueTable, (char *) formula, (char *) formula);
        return formula;
      }
    }
  }
}

/**Function********************************************************************

  Synopsis [Create SNF propositional variable if the passed formula is
  not propositional]

  Description [If formula is not propositional, generate SNF for the
  formula first and returned the renamed variable]

  SideEffects [Add the new generated SNF rule to formulaArray]

  SeeAlso     [Ctlsp_LtlTranslateIntoSNFRecursive]

******************************************************************************/
static Ctlsp_Formula_t *
createSNFnode(
  Ctlsp_Formula_t *formula,
  array_t         *formulaArray,
  int             *index)
{
  Ctlsp_Formula_t *newNode;

  if(!Ctlsp_LtlFormulaIsPropositional(formula)){
    newNode  = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strcat3(" SNFx","_", util_inttostr((*index)++)),
                                   (void *)util_strsav("1"));
    Ctlsp_LtlTranslateIntoSNFRecursive(newNode, formula, formulaArray, index);
    return newNode;
  } else {
    return Ctlsp_FormulaDup(formula);
  }

}