src/ctlsp/ctlspUtil.c

Go to the documentation of this file.

#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                                                     */
/*---------------------------------------------------------------------------*/

static array_t *globalFormulaArray;
static int      changeBracket = 1;

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

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


/*---------------------------------------------------------------------------*/
/* 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);

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

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;
  }
}


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 */

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;
}


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);
}


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


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


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));
}


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));
}

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


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


mdd_t *
Ctlsp_FormulaObtainStates(
  Ctlsp_Formula_t * formula)
{
  if (formula->states == NIL(mdd_t)) {
    return NIL(mdd_t);
  }
  else {
    return mdd_dup(formula->states);
  }
}
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);
}


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;
}


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;
}



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


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


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


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;
}


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


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

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


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

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


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

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

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

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

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

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

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

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);
    }

  }

}

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;
}

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);
}
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;
}

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;
}

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;
}


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;
}


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;
}


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;
}

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;
}


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;
}

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;
}

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;
}


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);
}


Ctlsp_FormulaClass
Ctlsp_CheckClassOfExistentialFormula(
  Ctlsp_Formula_t *formula)
{
  Ctlsp_FormulaClass result;

  result = CtlspCheckClassOfExistentialFormulaRecur(formula, FALSE);

  return result;
} /* End of Ctlsp_CheckTypeOfExistentialFormula */

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 */

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

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


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

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

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() */

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() */

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() */

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


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

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

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() */

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() */

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;
}

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() */


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 */

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

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


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 */


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;
}


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_;
}

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_;
}

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;
}

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);
    }
  }
}

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;
}

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

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

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

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

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

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 */

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 */

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 */

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 */


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() */

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;
}

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;
}


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;
}

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


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;
}


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;
}

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 */
  }
}


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                                          */
/*---------------------------------------------------------------------------*/


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);
}

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

void
CtlspFormulaDecrementRefCount(
  Ctlsp_Formula_t *formula)
{
  if(formula!=NIL(Ctlsp_Formula_t)) {
    assert(formula->refCount>0);
    if(--(formula->refCount) == 0)
      CtlspFormulaFree(formula);
  }
}
void
CtlspFormulaAddToGlobalArray(
  Ctlsp_Formula_t * formula)
{
  array_insert_last(Ctlsp_Formula_t *, globalFormulaArray, formula);
}

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);
  }
}


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);
}


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 = '>';
}


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;
}

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;
}


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);
  }
}

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 */

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;
}

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() */


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;
}

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;
}

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                                            */
/*---------------------------------------------------------------------------*/

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


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;
  }
}

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);
}

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;
      }
    }
  }
}

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);
  }

}