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

  FileName    [absTranslate.c]

  PackageName [abs]

  Synopsis    [Functions to translate CTL formulas to mu-calculus graphs.]

  Author      [Abelardo Pardo <abel@vlsi.colorado.edu>]

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

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

#include "absInt.h" 

static char rcsid[] UNUSED = "$Id: absTranslate.c,v 1.14 2002/09/04 14:58:18 fabio Exp $";


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


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

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

static AbsVertexInfo_t * TranslateCtlSubFormula(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
static AbsVertexInfo_t * ComputeFairPredicate(AbsVertexCatalog_t *catalog, AbsVertexInfo_t *atomicPredicate, array_t *fairArray, int polarity, int *uniqueIds);
static AbsVertexInfo_t * TranslateCtlID(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, int polarity);
static AbsVertexInfo_t * TranslateCtlEU(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
static AbsVertexInfo_t * TranslateCtlEG(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, int polarity, int *uniqueIds);
static AbsVertexInfo_t * TranslateCtlEGFair(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
static AbsVertexInfo_t * TranslateCtlEX(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
static AbsVertexInfo_t * TranslateCtlNOT(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
static AbsVertexInfo_t * TranslateCtlTHEN(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
static AbsVertexInfo_t * TranslateCtlAND(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
static AbsVertexInfo_t * TranslateCtlOR(AbsVertexCatalog_t *catalog, Ctlp_Formula_t *formula, array_t *fairArray, AbsVertexInfo_t *fairPositive, AbsVertexInfo_t *fairNegative, int polarity, int *uniqueIds);
static AbsVertexInfo_t * CreateConjunctionChain(AbsVertexCatalog_t *catalog, array_t *conjunctions, int polarity);

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


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

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

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

  Synopsis [Translate an array of CTL formulas to an array of labeled
  operational graphs. The graphs may share vertices among them.]

  SideEffects        []

  SeeAlso            [TranslateCtlSubFormula]

******************************************************************************/
array_t *
AbsCtlFormulaArrayTranslate(
  Abs_VerificationInfo_t *verInfo,
  array_t *formulaArray,
  array_t *fairArray)
{
  AbsVertexCatalog_t *catalog;
  Ctlp_Formula_t  *formulaPtr;
  AbsVertexInfo_t *fairPositive;
  AbsVertexInfo_t *fairNegative;
  array_t         *result;
  boolean         initialPolarity;
  int             uniqueIds;
  int             i;

  if (formulaArray == NIL(array_t)) {
    return NIL(array_t);
  }

  /* Initialize certain variables */
  catalog = AbsVerificationInfoReadCatalog(verInfo);
  uniqueIds = 0;

  if (fairArray != NIL(array_t)) {
    fairPositive = ComputeFairPredicate(catalog, NIL(AbsVertexInfo_t),
					fairArray, TRUE, &uniqueIds);

    fairNegative = ComputeFairPredicate(catalog, NIL(AbsVertexInfo_t), 
					fairArray, FALSE, &uniqueIds);
  }
  else {
    fairPositive = NIL(AbsVertexInfo_t);
    fairNegative = NIL(AbsVertexInfo_t);
  }

  if (AbsOptionsReadNegateFormula(AbsVerificationInfoReadOptions(verInfo))) {
    initialPolarity = TRUE;
  }
  else {
    initialPolarity = FALSE;
  }

  /* Create the result */
  result = array_alloc(AbsVertexInfo_t *, array_n(formulaArray));

  arrayForEachItem(Ctlp_Formula_t *, formulaArray, i, formulaPtr) {
    AbsVertexInfo_t *resultPtr;

    /* Translate the formula */
    resultPtr = TranslateCtlSubFormula(AbsVerificationInfoReadCatalog(verInfo),
				       formulaPtr,      /* Formula */
				       fairArray,       /* Fairness 
							   constraints */
				       fairPositive,    /* Predicate fair 
							   with positive 
							   polarity */
				       fairNegative,    /* Predicate fair
							   with negative
							   polarity */
				       initialPolarity, /* Initial polarity */
				       &uniqueIds);     /* Unique id counter */

    /* Negate the formula if needed */
    if (AbsOptionsReadNegateFormula(AbsVerificationInfoReadOptions(verInfo))) {
      AbsVertexInfo_t *newResult;

      /* If the formula's top vertex is a negation, eliminate the redundancy */
      if (AbsVertexReadType(resultPtr) == not_c) {
	
	newResult = AbsVertexReadLeftKid(resultPtr);
	AbsVertexReadRefs(newResult)++;
	AbsVertexFree(catalog, resultPtr, NIL(AbsVertexInfo_t));
	
	resultPtr =  newResult;
      }
      else {
	/* Create the not vertex */
	newResult = AbsVertexCatalogFindOrAdd(catalog, not_c, FALSE, 
					      resultPtr,
					      NIL(AbsVertexInfo_t), 0, 
					      NIL(char), 
					      NIL(char));
	if (AbsVertexReadType(newResult) == false_c) {
	  AbsVertexSetPolarity(newResult, FALSE);
	  AbsVertexSetDepth(newResult, AbsVertexReadDepth(resultPtr) + 1);
	  AbsVertexSetType(newResult, not_c);
	  AbsVertexSetLeftKid(newResult, resultPtr);
	  AbsVertexSetParent(resultPtr, newResult);
	}
	else {
	  AbsVertexFree(catalog, resultPtr, NIL(AbsVertexInfo_t));
	}
	resultPtr = newResult;
      }
    } /* If the formula needs to be negated */

    /* Set the constant bit */
    AbsFormulaSetConstantBit(resultPtr);

    array_insert(AbsVertexInfo_t *, result, i, resultPtr);
  }

  /* Clean up */
  if (fairPositive != NIL(AbsVertexInfo_t)) {
    AbsVertexFree(catalog, fairPositive, NIL(AbsVertexInfo_t));
  }
  if (fairNegative != NIL(AbsVertexInfo_t)) {
    AbsVertexFree(catalog, fairNegative, NIL(AbsVertexInfo_t));
  }

#ifndef NDEBUG
  {
    AbsVertexInfo_t *operationGraph;
    st_table *rootTable = st_init_table(st_ptrcmp, st_ptrhash);
    arrayForEachItem(AbsVertexInfo_t *, result, i, operationGraph) {
      st_insert(rootTable, (char *) operationGraph, NIL(char));
    }
    arrayForEachItem(AbsVertexInfo_t *, result, i, operationGraph) {
      assert(AbsFormulaSanityCheck(operationGraph, rootTable));
    }
    st_free_table(rootTable);
  }
#endif

  return result;
} /* End of AbsCtlFormulaArrayTranslate */


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

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

  Synopsis [Recursive formula to translate a formula to its operational graph]

  Description [This function is just a case to call the specific translation
  routines for the different types of sub-formulas]

  SideEffects        []

  SeeAlso [TranslateCtlId, TranslateCtlEG, TranslateCtlEGFair, TranslateCtlEU,
  TranslateCtlEX, TranslateCtlNOT, TranslateCtlTHEN, TranslateCtlAND,
  TranslateCtlOR]

******************************************************************************/
static AbsVertexInfo_t *
TranslateCtlSubFormula(
  AbsVertexCatalog_t *catalog,
  Ctlp_Formula_t *formula,
  array_t *fairArray,
  AbsVertexInfo_t *fairPositive,
  AbsVertexInfo_t *fairNegative,
  int polarity,
  int *uniqueIds)
{
  AbsVertexInfo_t *result;

  result = NIL(AbsVertexInfo_t);

  switch (Ctlp_FormulaReadType(formula)) {
    case Ctlp_TRUE_c:
    case Ctlp_FALSE_c: {
      (void) fprintf(vis_stderr, "** abs error: Error in TranslateCtlSubFormula. ");
      (void) fprintf(vis_stderr, "TRUE/FALSE constant found.\n");
      result = NIL(AbsVertexInfo_t);
      break;
    }
    case Ctlp_ID_c: {
      result = TranslateCtlID(catalog, formula, polarity);
      break;
    }
    case Ctlp_EG_c: {
      if (fairArray == NIL(array_t)) {
	result = TranslateCtlEG(catalog, formula, polarity, uniqueIds);
      }
      else {
	result = TranslateCtlEGFair(catalog, formula, fairArray, fairPositive, 
				    fairNegative, polarity, uniqueIds);
      }
      break;
    }
    case Ctlp_EU_c: {
      result = TranslateCtlEU(catalog, formula, fairArray, fairPositive, 
			      fairNegative, polarity, uniqueIds);
      break;
    }
    case Ctlp_EX_c: {
      result = TranslateCtlEX(catalog, formula, fairArray, fairPositive, 
			      fairNegative, polarity, uniqueIds);
      break;
    }
    case Ctlp_NOT_c: {
      result = TranslateCtlNOT(catalog, formula, fairArray, fairPositive, 
			       fairNegative, polarity, uniqueIds);
      break;
    }
    case Ctlp_THEN_c:  {
      result = TranslateCtlTHEN(catalog, formula, fairArray, fairPositive, 
				fairNegative, polarity, uniqueIds);
      break;
    }
    case Ctlp_EQ_c:
    case Ctlp_XOR_c: {
      /* Non-monotonic operators should have been replaced before
       * reaching this point.
       */
      fail("Encountered unexpected type of CTL formula\n");
      break;
    }
    case Ctlp_AND_c: {
      result = TranslateCtlAND(catalog, formula, fairArray, fairPositive, 
			       fairNegative, polarity, uniqueIds);
      break;
    }
    case Ctlp_OR_c: {
      result = TranslateCtlOR(catalog, formula, fairArray, fairPositive, 
			      fairNegative, polarity, uniqueIds);
      break;
    }
    default: fail("Encountered unknown type of CTL formula\n");
  }

  return result;
} /* End of TranslateCtlSubFormula */

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

  Synopsis [Computes the operational graph representation of the predicate
  "fair"]

  Description [Given a set of formulas f_1,...,f_n compute the predicate fair
  which is computed as follows: fair(p) = nu(x).(p * Product(i=1,n)(EX[E[p U (x
  * f_i)]])). The final graph will have in its top vertex the polarity given as
  a parameter to the routine.]

  SideEffects        []

  SeeAlso            [AbsCtlFormulaArrayTranslate]

******************************************************************************/
static AbsVertexInfo_t *
ComputeFairPredicate(
  AbsVertexCatalog_t *catalog,
  AbsVertexInfo_t *atomicPredicate,
  array_t *fairArray,
  int polarity,
  int *uniqueIds)
{
  Ctlp_Formula_t *ctlPtr;
  AbsVertexInfo_t *mainVarVertex;
  AbsVertexInfo_t *mainVarNotVertex;
  AbsVertexInfo_t *vertexPtr;
  AbsVertexInfo_t *aux1;
  AbsVertexInfo_t *aux2;
  AbsVertexInfo_t *aux3;
  array_t *conjunctions;
  array_t *constraintArray;
  int     mainVarId;
  int     i;
  
  /* Obtain the representation of the fairness predicates */
  constraintArray = array_alloc(AbsVertexInfo_t *, array_n(fairArray));
  arrayForEachItem(Ctlp_Formula_t *, fairArray, i, ctlPtr) {
    array_insert(AbsVertexInfo_t *, constraintArray, i, 
		 TranslateCtlSubFormula(catalog, ctlPtr, NIL(array_t), 
					NIL(AbsVertexInfo_t), 
					NIL(AbsVertexInfo_t), polarity,  
					uniqueIds));
  }

  /* Create the vertex representing the variable of the greatest fixed point */
  mainVarId = (*uniqueIds)++;

  aux1 = AbsVertexCatalogFindOrAdd(catalog, variable_c, !polarity, 
				   NIL(AbsVertexInfo_t), 
				   NIL(AbsVertexInfo_t),
				   mainVarId, NIL(char), NIL(char));
  if (AbsVertexReadType(aux1) == false_c) {
    AbsVertexSetPolarity(aux1, !polarity);
    AbsVertexSetDepth(aux1, 1);
    AbsVertexSetType(aux1, variable_c);
    AbsVertexSetVarId(aux1, mainVarId);
  }
  mainVarVertex = aux1;

  mainVarNotVertex = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux1,
					       NIL(AbsVertexInfo_t), 0, 
					       NIL(char), NIL(char));
  if (AbsVertexReadType(mainVarNotVertex) == false_c) {
    AbsVertexSetPolarity(mainVarNotVertex, polarity);
    AbsVertexSetDepth(mainVarNotVertex, 2);
    AbsVertexSetType(mainVarNotVertex, not_c);
    AbsVertexSetLeftKid(mainVarNotVertex, aux1);
    AbsVertexSetParent(mainVarVertex, mainVarNotVertex);
  }
  else {
    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
  }

  /* Create the predicates EX[E[f U z * f_i]] */
  conjunctions = array_alloc(AbsVertexInfo_t *, array_n(fairArray));
  arrayForEachItem(AbsVertexInfo_t *, constraintArray, i, vertexPtr) {
    AbsVertexInfo_t *varVertex;
    int variableId;

    /* Create the conjunction between z and f_i */
    AbsVertexReadRefs(mainVarNotVertex)++;
    aux1 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, vertexPtr, 
				     mainVarNotVertex, 0, NIL(char), 
				     NIL(char));
    if (AbsVertexReadType(aux1) == false_c) {
      AbsVertexSetPolarity(aux1, polarity);
      if (AbsVertexReadDepth(vertexPtr) > 2) {
	AbsVertexSetDepth(aux1, AbsVertexReadDepth(vertexPtr) + 1);
      }
      else {
	AbsVertexSetDepth(aux1, 3);
      }
      AbsVertexSetType(aux1, and_c);
      AbsVertexSetLeftKid(aux1, vertexPtr);
      AbsVertexSetRightKid(aux1, mainVarNotVertex);
      AbsVertexSetParent(vertexPtr, aux1);
      AbsVertexSetParent(mainVarNotVertex, aux1);
    }
    else {
      /* Cache hit */
      AbsVertexFree(catalog, vertexPtr, NIL(AbsVertexInfo_t));
      AbsVertexFree(catalog, mainVarNotVertex, NIL(AbsVertexInfo_t));
    }

    /* Create the vertex negating the previous conjunction */
    aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux1, 
				     NIL(AbsVertexInfo_t), 0, NIL(char), 
				     NIL(char));
    if (AbsVertexReadType(aux2) == false_c) {
      AbsVertexSetPolarity(aux2, !polarity);
      AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
      AbsVertexSetType(aux2, not_c);
      AbsVertexSetLeftKid(aux2, aux1);
      AbsVertexSetParent(aux1, aux2);
    }
    else {
      /* Cache hit */
      AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
    }

    /* Create the variable of the fixed point in the EU sub-formula*/
    variableId = (*uniqueIds)++;
    aux1 = AbsVertexCatalogFindOrAdd(catalog, variable_c, polarity,
				     NIL(AbsVertexInfo_t), 
				     NIL(AbsVertexInfo_t), variableId, 
				     NIL(char), NIL(char));
    if (AbsVertexReadType(aux1) == false_c) {
      AbsVertexSetPolarity(aux1, polarity);
      AbsVertexSetDepth(aux1, 1);
      AbsVertexSetType(aux1, variable_c);
      AbsVertexSetVarId(aux1, variableId);
    }
    varVertex = aux1;

    /* Create the vertex storing the preimage sub-formula */
    aux3 = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
				     aux1, NIL(AbsVertexInfo_t),
				     0, NIL(char), NIL(char));
    if (AbsVertexReadType(aux3) == false_c) {
      AbsVertexSetPolarity(aux3, polarity);
      AbsVertexSetDepth(aux3, 2);
      AbsVertexSetType(aux3, preImage_c);
      AbsVertexSetLeftKid(aux3, aux1);
      AbsVertexSetParent(aux1, aux3);
    }
    else {
      /* Cache hit */
      AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
    }
  
    if (atomicPredicate != NIL(AbsVertexInfo_t)) {
      AbsVertexReadRefs(atomicPredicate)++;
      /* Create the vertex representing the and */
      aux1 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity,
				       atomicPredicate, aux3, 0, NIL(char), 
				       NIL(char));
      if (AbsVertexReadType(aux1) == false_c) {
	AbsVertexSetPolarity(aux1, polarity);
	if (AbsVertexReadDepth(atomicPredicate) > 2) {
	  AbsVertexSetDepth(aux1, AbsVertexReadDepth(atomicPredicate) + 1);
	}
	else {
	  AbsVertexSetDepth(aux1, 3);
	}
	AbsVertexSetType(aux1, and_c);
	AbsVertexSetLeftKid(aux1, atomicPredicate);
	AbsVertexSetRightKid(aux1, aux3);
	AbsVertexSetParent(atomicPredicate, aux1);
	AbsVertexSetParent(aux3, aux1);
      }
      else {
	/* Cache hit */
	AbsVertexFree(catalog, aux3, NIL(AbsVertexInfo_t));
	AbsVertexFree(catalog, atomicPredicate, NIL(AbsVertexInfo_t));
      }
    }
    else {
      aux1 = aux3;
    }

    /* Create the not vertex on top of the conjunction */
    aux3 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux1, 
				     NIL(AbsVertexInfo_t), 0, NIL(char), 
				     NIL(char));
    if (AbsVertexReadType(aux3) == false_c) {
      AbsVertexSetPolarity(aux3, !polarity);
      AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux1) + 1);
      AbsVertexSetType(aux3, not_c);
      AbsVertexSetLeftKid(aux3, aux1);
      AbsVertexSetParent(aux1, aux3);
    }
    else {
      /* Cache hit */
      AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
    }
    
    /* Vertex taking the conjunction */
    aux1 = AbsVertexCatalogFindOrAdd(catalog, and_c, !polarity, aux2, aux3,
				     0, NIL(char), NIL(char));
    if (AbsVertexReadType(aux1) == false_c) {
      AbsVertexSetPolarity(aux1, !polarity);
      if (AbsVertexReadDepth(aux2) > AbsVertexReadDepth(aux3)) {
	AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
      }
      else {
	AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux3) + 1);
      }
      AbsVertexSetType(aux1, and_c);
      AbsVertexSetLeftKid(aux1, aux2);
      AbsVertexSetRightKid(aux1, aux3);
      AbsVertexSetParent(aux3, aux1);
      AbsVertexSetParent(aux2, aux1);
    }
    else {
      AbsVertexFree(catalog, aux3, NIL(AbsVertexInfo_t));
      AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
    }
    
    /* negation of the conjunction */
    aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux1,
				     NIL(AbsVertexInfo_t), 0, NIL(char), 
				     NIL(char));
    if (AbsVertexReadType(aux2) == false_c) {
      AbsVertexSetPolarity(aux2, polarity);
      AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
      AbsVertexSetType(aux2, not_c);
      AbsVertexSetLeftKid(aux2, aux1);
      AbsVertexSetParent(aux1, aux2);
    }
    else {
      AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
    }
  
    /* Create the lfp vertex for the EU operator */
    aux1 = AbsVertexCatalogFindOrAdd(catalog, fixedPoint_c, polarity, aux2,
				     NIL(AbsVertexInfo_t), 0, NIL(char),
				     NIL(char));
    if (AbsVertexReadType(aux1) == false_c) {
      AbsVertexSetPolarity(aux1, polarity);
      AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
      AbsVertexSetType(aux1, fixedPoint_c);
      AbsVertexSetLeftKid(aux1, aux2);
      AbsVertexSetFpVar(aux1, varVertex);
      AbsVertexSetUseExtraCareSet(aux1, TRUE);
      AbsVertexSetParent(aux2, aux1);
    }
    else {
      AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
    }
    
    /* Create the final EX vertex on top of the EU */
    aux2 = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
				     aux1, NIL(AbsVertexInfo_t), 0, NIL(char),
				     NIL(char));
    if (AbsVertexReadType(aux2) == false_c) {
      AbsVertexSetPolarity(aux2, polarity);
      AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
      AbsVertexSetType(aux2, preImage_c);
      AbsVertexSetLeftKid(aux2, aux1);
      AbsVertexSetParent(aux1, aux2);
    }
    else {
      AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
    }

    array_insert(AbsVertexInfo_t *, conjunctions, i, aux2);
  } /* End of the loop iterating over the fairness constraints */
  AbsVertexReadRefs(mainVarNotVertex)--;

  /* Create the chain of ands for the conjunctions */
  aux1 = CreateConjunctionChain(catalog, conjunctions, polarity);

  /* Create the and with the atomic predicate if required */
  if (atomicPredicate != NIL(AbsVertexInfo_t)) {
    aux2 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, atomicPredicate, 
				     aux1, 0, NIL(char), NIL(char));
    if (AbsVertexReadType(aux2) == false_c) {
      AbsVertexSetPolarity(aux2, polarity);
      if (AbsVertexReadDepth(aux1) > AbsVertexReadDepth(atomicPredicate)) {
	AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
      }
      else {
	AbsVertexSetDepth(aux2, AbsVertexReadDepth(atomicPredicate) + 1);
      }
      AbsVertexSetType(aux2, and_c);
      AbsVertexSetLeftKid(aux2, atomicPredicate);
      AbsVertexSetRightKid(aux2, aux1);
      AbsVertexSetParent(atomicPredicate, aux2);
      AbsVertexSetParent(aux1, aux2);
    }
    else {
      AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
      AbsVertexFree(catalog, atomicPredicate, NIL(AbsVertexInfo_t));
    }
  }
  else {
    aux2 = aux1;
  }

  /* Create the not vertex on top of the conjunction */
  aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux2, 
				   NIL(AbsVertexInfo_t), 0, NIL(char), 
				   NIL(char));
  if (AbsVertexReadType(aux1) == false_c) {
    AbsVertexSetPolarity(aux1, !polarity);
    AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
    AbsVertexSetType(aux1, not_c);
    AbsVertexSetLeftKid(aux1, aux2);
    AbsVertexSetParent(aux2, aux1);
  }
  else {
    AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
  }
  
  /* Create the top most fixed point vertex */
  aux2 = AbsVertexCatalogFindOrAdd(catalog, fixedPoint_c, !polarity, aux1,
				   NIL(AbsVertexInfo_t), mainVarId,
				   NIL(char), NIL(char));
  if (AbsVertexReadType(aux2) == false_c) {
    AbsVertexSetPolarity(aux2, !polarity);
    AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
    AbsVertexSetType(aux2, fixedPoint_c);
    AbsVertexSetVarId(aux2, mainVarId);
    AbsVertexSetLeftKid(aux2, aux1);
    AbsVertexSetFpVar(aux2, mainVarVertex);
    AbsVertexSetUseExtraCareSet(aux2, FALSE);
    AbsVertexSetParent(aux1, aux2);
  }
  else {
    AbsVertexSetUseExtraCareSet(aux2, FALSE);
    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
  }
  
  /* Create the top most vertex */
  aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux2, 
				   NIL(AbsVertexInfo_t), 0, NIL(char), 
				   NIL(char));
  if (AbsVertexReadType(aux1) == false_c) {
    AbsVertexSetPolarity(aux1, polarity);
    AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
    AbsVertexSetType(aux1, not_c);
    AbsVertexSetLeftKid(aux1, aux2);
    AbsVertexSetParent(aux2, aux1);
  }
  else {
    AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
  }
  
  /* Clean up */
  array_free(constraintArray);
  arrayForEachItem(AbsVertexInfo_t *, conjunctions, i, vertexPtr) {
    AbsVertexFree(catalog, vertexPtr, NIL(AbsVertexInfo_t));
  }
  array_free(conjunctions);

  return aux1;
} /* End of ComputeFairPredicate */

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

  Synopsis [Computes the operational grarph representation of an atomic
  predicate]

  SideEffects        []

  SeeAlso            [TranslateCtlSubFormula]

******************************************************************************/
static AbsVertexInfo_t *
TranslateCtlID(
  AbsVertexCatalog_t *catalog,
  Ctlp_Formula_t *formula,	       
  int polarity)
{
  AbsVertexInfo_t *result;

  result = AbsVertexCatalogFindOrAdd(catalog,
				     identifier_c,
				     polarity,
				     NIL(AbsVertexInfo_t),
				     NIL(AbsVertexInfo_t),
				     0,
				     Ctlp_FormulaReadVariableName(formula),
				     Ctlp_FormulaReadValueName(formula));
  if (AbsVertexReadType(result) == false_c) {
    AbsVertexSetPolarity(result, polarity);
    AbsVertexSetDepth(result, 1);
    AbsVertexSetType(result, identifier_c);
    AbsVertexSetName(result, 
		     util_strsav(Ctlp_FormulaReadVariableName(formula)));
    AbsVertexSetValue(result,
		      util_strsav(Ctlp_FormulaReadValueName(formula)));
  }
  
  return result;
} /* End of TranslateCtlID */

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

  Synopsis [Computes the operational graph representation of a formula of the
  form E(pUq)]

  SideEffects        []

  SeeAlso            [TranslateCtlSubFormula]

******************************************************************************/
static AbsVertexInfo_t *
TranslateCtlEU(
  AbsVertexCatalog_t *catalog,
  Ctlp_Formula_t *formula,
  array_t *fairArray,
  AbsVertexInfo_t *fairPositive,
  AbsVertexInfo_t *fairNegative,
  int polarity,
  int *uniqueIds)
{
  AbsVertexInfo_t *result;
  AbsVertexInfo_t *leftResult;
  AbsVertexInfo_t *rightResult;
  AbsVertexInfo_t *aux1;
  AbsVertexInfo_t *aux2;
  AbsVertexInfo_t *aux3;
  AbsVertexInfo_t *varVertex;
  int variableId;
  
  /* Allocate a unique id for the fixed point */
  variableId = (*uniqueIds)++;
  
  /* Create the vertex storing the fixed point variable */
  aux1 = AbsVertexCatalogFindOrAdd(catalog, variable_c, polarity,
				   NIL(AbsVertexInfo_t), 
				   NIL(AbsVertexInfo_t), variableId, 
				   NIL(char), NIL(char));
  if (AbsVertexReadType(aux1) == false_c) {
    AbsVertexSetPolarity(aux1, polarity);
    AbsVertexSetDepth(aux1, 1);
    AbsVertexSetType(aux1, variable_c);
    AbsVertexSetVarId(aux1, variableId);
  }
  varVertex = aux1;
  
  /* Create the vertex storing the preimage sub-formula */
  aux2 = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
				   aux1, NIL(AbsVertexInfo_t),
				   0, NIL(char), NIL(char));
  if (AbsVertexReadType(aux2) == false_c) {
    AbsVertexSetPolarity(aux2, polarity);
    AbsVertexSetDepth(aux2, 2);
    AbsVertexSetType(aux2, preImage_c);
    AbsVertexSetLeftKid(aux2, aux1);
    AbsVertexSetParent(aux1, aux2);
  }
  else {
    /* Cache hit */
    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
  }
  
  if (Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(formula)) != Ctlp_TRUE_c) {
    /* Compute the value of the sub-formula */
    leftResult = TranslateCtlSubFormula(catalog,
					Ctlp_FormulaReadLeftChild(formula),
					fairArray, fairPositive, fairNegative,
					polarity, uniqueIds);
    
    /* Create the vertex representing the and */
    aux1 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, leftResult, aux2,
				     0, NIL(char), 
				     NIL(char));
    if (AbsVertexReadType(aux1) == false_c) {
      AbsVertexSetPolarity(aux1, polarity);
      if (AbsVertexReadDepth(leftResult) > 2) {
	AbsVertexSetDepth(aux1, AbsVertexReadDepth(leftResult) + 1);
      }
      else {
	AbsVertexSetDepth(aux1, 3);
      }
      AbsVertexSetType(aux1, and_c);
      AbsVertexSetLeftKid(aux1, leftResult);
      AbsVertexSetRightKid(aux1, aux2);
      AbsVertexSetParent(leftResult, aux1);
      AbsVertexSetParent(aux2, aux1);
    }
    else {
      /* Cache hit */
      AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
      AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
    }
  } /* if type is TRUE */
  else {
    aux1 = aux2;
  }
  
  /* Create the not vertex on top of the conjunction */
  aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux1, 
				   NIL(AbsVertexInfo_t), 0, NIL(char), 
				   NIL(char));
  if (AbsVertexReadType(aux2) == false_c) {
    AbsVertexSetPolarity(aux2, !polarity);
    AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
    AbsVertexSetType(aux2, not_c);
    AbsVertexSetLeftKid(aux2, aux1);
    AbsVertexSetParent(aux1, aux2);
  }
  else {
    /* Cache hit */
    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
  }
  
  /* Evaluate the right operand of the EU */
  rightResult= TranslateCtlSubFormula(catalog,
				      Ctlp_FormulaReadRightChild(formula),
				      fairArray, fairPositive, fairNegative,
				      polarity, uniqueIds);
  
  /* check if there are fairness constraints */
  if (fairPositive != NIL(AbsVertexInfo_t)) {
    AbsVertexInfo_t *fairness;
    AbsVertexInfo_t *conjunction;

    /* The negative polarity version of the fairness must be present as well */
    assert(fairNegative != NIL(AbsVertexInfo_t));

    /* Select the apropriate representation of the fairness constraint */
    if (polarity) {
      fairness = fairPositive;
    }
    else {
      fairness = fairNegative;
    }
    AbsVertexReadRefs(fairness)++;

    conjunction = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity,
					    rightResult, fairness, 0, NIL(char),
					    NIL(char));

    if (AbsVertexReadType(conjunction) == false_c) {
      int leftDepth;
      int rightDepth;

      leftDepth = AbsVertexReadDepth(rightResult);
      rightDepth = AbsVertexReadDepth(fairness);

      AbsVertexSetPolarity(conjunction, polarity);
      if (leftDepth > rightDepth) {
	AbsVertexSetDepth(conjunction, leftDepth + 1);
      }
      else {
	AbsVertexSetDepth(conjunction, rightDepth + 1);
      }
      AbsVertexSetType(conjunction, and_c);
      AbsVertexSetLeftKid(conjunction, rightResult);
      AbsVertexSetRightKid(conjunction, fairness);
      AbsVertexSetParent(rightResult, conjunction);
      AbsVertexSetParent(fairness, conjunction);
    }
    else {
      AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
      AbsVertexFree(catalog, fairness, NIL(AbsVertexInfo_t));
    }
    rightResult = conjunction;
  }

  /* If the sub-formula's top vertex is a negation, eliminate the redundancy */
  if (AbsVertexReadType(rightResult) == not_c) {
    AbsVertexInfo_t *newResult;


    newResult = AbsVertexReadLeftKid(rightResult);
    AbsVertexReadRefs(newResult)++;
    AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
    aux1 = newResult;
  }
  else {
    /* Vertex negating second operand */
    aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, rightResult, 
				     NIL(AbsVertexInfo_t), 0, NIL(char), 
				     NIL(char));
    if (AbsVertexReadType(aux1) == false_c) {
      AbsVertexSetPolarity(aux1, !polarity);
      AbsVertexSetDepth(aux1, AbsVertexReadDepth(rightResult) + 1);
      AbsVertexSetType(aux1, not_c);
      AbsVertexSetLeftKid(aux1, rightResult);
      AbsVertexSetParent(rightResult, aux1);
    }
    else {
      AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
    }
  }
  
  /* Vertex taking the conjunction */
  aux3 = AbsVertexCatalogFindOrAdd(catalog, and_c, !polarity, aux1, aux2,
				   0, NIL(char), NIL(char));
  if (AbsVertexReadType(aux3) == false_c) {
    AbsVertexSetPolarity(aux3, !polarity);
    if (AbsVertexReadDepth(aux1) > AbsVertexReadDepth(aux2)) {
      AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux1) + 1);
    }
    else {
      AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux2) + 1);
    }
    AbsVertexSetType(aux3, and_c);
    AbsVertexSetLeftKid(aux3, aux1);
    AbsVertexSetRightKid(aux3, aux2);
    AbsVertexSetParent(aux1, aux3);
    AbsVertexSetParent(aux2, aux3);
  }
  else {
    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
    AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
  }
  
  /* negation of the conjunction */
  aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux3,
				   NIL(AbsVertexInfo_t), 0, NIL(char), 
				   NIL(char));
  if (AbsVertexReadType(aux1) == false_c) {
    AbsVertexSetPolarity(aux1, polarity);
    AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux3) + 1);
    AbsVertexSetType(aux1, not_c);
    AbsVertexSetLeftKid(aux1, aux3);
    AbsVertexSetParent(aux3, aux1);
  }
  else {
    AbsVertexFree(catalog, aux3, NIL(AbsVertexInfo_t));
  }
  
  /* Top vertex fixed point operator */
  result = AbsVertexCatalogFindOrAdd(catalog, fixedPoint_c, polarity, aux1,
				     NIL(AbsVertexInfo_t), 0, NIL(char), 
				     NIL(char));
  if (AbsVertexReadType(result) == false_c) {
    AbsVertexSetPolarity(result, polarity);
    AbsVertexSetDepth(result, AbsVertexReadDepth(aux1) + 1);
    AbsVertexSetType(result, fixedPoint_c);
    AbsVertexSetLeftKid(result, aux1);
    AbsVertexSetFpVar(result, varVertex);
    AbsVertexSetUseExtraCareSet(result, TRUE);
    AbsVertexSetParent(aux1, result);
  }
  else {
    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
  }
  
  return result;
} /* End of TranslateCtlEU */

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

  Synopsis [Computes the operational graph representation of a formula of the
  form EG(p)]

  SideEffects        []

  SeeAlso            [TranslateCtlSubFormula]

******************************************************************************/
static AbsVertexInfo_t *
TranslateCtlEG(
  AbsVertexCatalog_t *catalog,
  Ctlp_Formula_t *formula,
  int polarity,
  int *uniqueIds)
{
  AbsVertexInfo_t *result;
  AbsVertexInfo_t *varVertex;
  AbsVertexInfo_t *aux1;
  AbsVertexInfo_t *aux2;
  AbsVertexInfo_t *childResult;
  int variableId;
  
  /* Allocate a unique id for the fixed point */
  variableId = (*uniqueIds)++;
  
  /* Create the vertex storing the fixed point variable */
  aux1 = AbsVertexCatalogFindOrAdd(catalog, variable_c, !polarity,
				   NIL(AbsVertexInfo_t), 
				   NIL(AbsVertexInfo_t),
				   variableId, NIL(char), NIL(char));
  if (AbsVertexReadType(aux1) == false_c) {
    AbsVertexSetPolarity(aux1, !polarity);
    AbsVertexSetDepth(aux1, 1);
    AbsVertexSetType(aux1, variable_c);
    AbsVertexSetVarId(aux1, variableId);
  }
  varVertex = aux1;
  
  /* Create the vertex to negate the variable of the fixed point */
  aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux1, 
				   NIL(AbsVertexInfo_t), 0, NIL(char), 
				   NIL(char));
  if (AbsVertexReadType(aux2) == false_c) {
    AbsVertexSetPolarity(aux2, polarity);
    AbsVertexSetDepth(aux2, 2);
    AbsVertexSetType(aux2, not_c);
    AbsVertexSetLeftKid(aux2, aux1);
    AbsVertexSetParent(aux1, aux2);
  }
  else {
    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
  }

  /* Create the vertex storing the preimage sub-formula */
  aux1 = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity,
				   aux1, NIL(AbsVertexInfo_t),
				   0, NIL(char), NIL(char));
  if (AbsVertexReadType(aux1) == false_c) {
    AbsVertexSetPolarity(aux1, polarity);
    AbsVertexSetDepth(aux1, 3);
    AbsVertexSetType(aux1, preImage_c);
    AbsVertexSetLeftKid(aux1, aux2);
    AbsVertexSetParent(aux2, aux1);
  }
  else {
    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
  }
  
  if (Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(formula)) != Ctlp_TRUE_c) {
    /* Create the vertex representing the sub-formula of EG */
    childResult = TranslateCtlSubFormula(catalog, 
					 Ctlp_FormulaReadLeftChild(formula),
					 NIL(array_t), NIL(AbsVertexInfo_t), 
					 NIL(AbsVertexInfo_t), polarity, 
					 uniqueIds);
    
    /* Create the vertex representing the and */
    aux2 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, childResult, 
				     aux1, 0, NIL(char), 
				     NIL(char));
    if (AbsVertexReadType(aux2) == false_c) {
      AbsVertexSetPolarity(aux2, polarity);
      if (AbsVertexReadDepth(childResult) > 2) {
	AbsVertexSetDepth(aux2, AbsVertexReadDepth(childResult) + 1);
      }
      else {
	AbsVertexSetDepth(aux2, 4);
      }
      AbsVertexSetType(aux2, and_c);
      AbsVertexSetLeftKid(aux2, childResult);
      AbsVertexSetRightKid(aux2, aux1);
      AbsVertexSetParent(childResult, aux2);
      AbsVertexSetParent(aux1, aux2);
    }
    else {
      AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
      AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
    }
  }
  else {
    aux2 = aux1;
  }
  
  /* Create the not vertex on top of the conjunction */
  aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, aux2, 
				   NIL(AbsVertexInfo_t), 0, NIL(char), 
				   NIL(char));
  if (AbsVertexReadType(aux1) == false_c) {
    AbsVertexSetPolarity(aux1, !polarity);
    AbsVertexSetDepth(aux1, AbsVertexReadDepth(aux2) + 1);
    AbsVertexSetType(aux1, not_c);
    AbsVertexSetLeftKid(aux1, aux2);
    AbsVertexSetParent(aux2, aux1);
  }
  else {
    AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
  }
  
  /* Create the fixedpoint_c vertex */
  aux2 = AbsVertexCatalogFindOrAdd(catalog, fixedPoint_c, !polarity, aux1,
				   NIL(AbsVertexInfo_t), variableId,
				   NIL(char), NIL(char));
  if (AbsVertexReadType(aux2) == false_c) {
    AbsVertexSetPolarity(aux2, !polarity);
    AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
    AbsVertexSetType(aux2, fixedPoint_c);
    AbsVertexSetVarId(aux2, variableId);
    AbsVertexSetLeftKid(aux2, aux1);
    AbsVertexSetFpVar(aux2, varVertex);
    AbsVertexSetUseExtraCareSet(aux2, FALSE);
    AbsVertexSetParent(aux1, aux2);
  }
  else {
    AbsVertexSetUseExtraCareSet(aux2, FALSE);
    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
  }
  
  /* Create the top most not vertex  */
  result = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux2, 
				     NIL(AbsVertexInfo_t), 0, NIL(char), 
				     NIL(char));
  if (AbsVertexReadType(result) == false_c) {
    AbsVertexSetPolarity(result, polarity);
    AbsVertexSetDepth(result, AbsVertexReadDepth(aux2) + 1);
    AbsVertexSetType(result, not_c);
    AbsVertexSetLeftKid(result, aux2);
    AbsVertexSetParent(aux2, result);
  }
  else {
    AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
  }
  
  return result;
} /* End of TranslateCtlEG */

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

  Synopsis [Computes the operational graph representation of a predicate of the
  form EGfair(f)]

  SideEffects        []

  SeeAlso            [TranslateCtlSubFormula]

******************************************************************************/
static AbsVertexInfo_t *
TranslateCtlEGFair(
  AbsVertexCatalog_t *catalog,
  Ctlp_Formula_t *formula,
  array_t *fairArray,
  AbsVertexInfo_t *fairPositive,
  AbsVertexInfo_t *fairNegative,
  int polarity,
  int *uniqueIds)
{
  AbsVertexInfo_t *result;
  AbsVertexInfo_t *childResult;

  if (Ctlp_FormulaReadType(Ctlp_FormulaReadLeftChild(formula)) == Ctlp_TRUE_c) {
    if (polarity) {
      result = fairPositive;
      AbsVertexReadRefs(fairPositive)++;
    }
    else {
      result = fairNegative;
      AbsVertexReadRefs(fairNegative)++;
    }
  }
  else {
    childResult = TranslateCtlSubFormula(catalog,
					 Ctlp_FormulaReadLeftChild(formula),
					 fairArray, fairPositive, fairNegative,
					 polarity, uniqueIds);

    result = ComputeFairPredicate(catalog, childResult, fairArray, polarity,
				  uniqueIds);
  }

  return result;
} /* End of TranslateCtlEGFair */

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

  Synopsis [Computes the operational graph representation of the predicate
  EX(p)]

  SideEffects        []

  SeeAlso            [TranslateCtlSubFormula]

******************************************************************************/
static AbsVertexInfo_t *
TranslateCtlEX(
  AbsVertexCatalog_t *catalog,
  Ctlp_Formula_t *formula,
  array_t *fairArray,
  AbsVertexInfo_t *fairPositive,
  AbsVertexInfo_t *fairNegative,
  int polarity,
  int *uniqueIds)
{
  AbsVertexInfo_t *result;
  AbsVertexInfo_t *childResult;
  
  /* Translate the sub-formula regardless */
  childResult = TranslateCtlSubFormula(catalog,
				       Ctlp_FormulaReadLeftChild(formula),
				       fairArray, fairPositive, fairNegative,
				       polarity, uniqueIds);
  
  /* check if there are fairness constraints */
  if (fairPositive != NIL(AbsVertexInfo_t)) {
    AbsVertexInfo_t *fairness;
    AbsVertexInfo_t *conjunction;

    /* The negative polarity version of the fairness must be present as well */
    assert(fairNegative != NIL(AbsVertexInfo_t));

    /* Select the apropriate representation of the fairness constraint */
    if (polarity) {
      fairness = fairPositive;
    }
    else {
      fairness = fairNegative;
    }
    AbsVertexReadRefs(fairness)++;

    conjunction = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity,
					    childResult, fairness, 0, NIL(char),
					    NIL(char));

    if (AbsVertexReadType(conjunction) == false_c) {
      int leftDepth;
      int rightDepth;

      leftDepth = AbsVertexReadDepth(childResult);
      rightDepth = AbsVertexReadDepth(fairness);

      AbsVertexSetPolarity(conjunction, polarity);
      if (leftDepth > rightDepth) {
	AbsVertexSetDepth(conjunction, leftDepth + 1);
      }
      else {
	AbsVertexSetDepth(conjunction, rightDepth + 1);
      }
      AbsVertexSetType(conjunction, and_c);
      AbsVertexSetLeftKid(conjunction, childResult);
      AbsVertexSetRightKid(conjunction, fairness);
      AbsVertexSetParent(childResult, conjunction);
      AbsVertexSetParent(fairness, conjunction);
    }
    else {
      AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
      AbsVertexFree(catalog, fairness, NIL(AbsVertexInfo_t));
    }
    childResult = conjunction;
  }

  /* Create the preImage vertex */
  result = AbsVertexCatalogFindOrAdd(catalog, preImage_c, polarity, 
				     childResult, NIL(AbsVertexInfo_t), 0, 
				     NIL(char), NIL(char));
  if (AbsVertexReadType(result) == false_c) {
    AbsVertexSetPolarity(result, polarity);
    AbsVertexSetDepth(result, AbsVertexReadDepth(childResult) + 1);
    AbsVertexSetType(result, preImage_c);
    AbsVertexSetLeftKid(result, childResult);
    AbsVertexSetParent(childResult, result);
  }
  else {
    AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
  }
							   
  return result;
} /* End of TranslateCtlEX */

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

  Synopsis [Computes the operational graph representation of the predicate
  NOT(p)]

  SideEffects        []

  SeeAlso            [TranslateCtlSubFormula]

******************************************************************************/
static AbsVertexInfo_t *
TranslateCtlNOT(
  AbsVertexCatalog_t *catalog,
  Ctlp_Formula_t *formula,
  array_t *fairArray,
  AbsVertexInfo_t *fairPositive,
  AbsVertexInfo_t *fairNegative,
  int polarity,
  int *uniqueIds)
{
  AbsVertexInfo_t *result;
  AbsVertexInfo_t *childResult;
  
  childResult = TranslateCtlSubFormula(catalog,
				       Ctlp_FormulaReadLeftChild(formula),
				       fairArray, fairPositive, fairNegative,
				       !polarity, uniqueIds);
  
  /* If the sub-formula's top vertex is a negation, eliminate the redundancy */
  if (AbsVertexReadType(childResult) == not_c) {
    AbsVertexInfo_t *newResult;

    newResult = AbsVertexReadLeftKid(childResult);
    AbsVertexReadRefs(newResult)++;
    AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
    
    return newResult;
  }

  /* Create the not vertex */
  result = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, childResult,
				     NIL(AbsVertexInfo_t), 0, NIL(char), 
				     NIL(char));
  if (AbsVertexReadType(result) == false_c) {
    AbsVertexSetPolarity(result, polarity);
    AbsVertexSetDepth(result, AbsVertexReadDepth(childResult) + 1);
    AbsVertexSetType(result, not_c);
    AbsVertexSetLeftKid(result, childResult);
    AbsVertexSetParent(childResult, result);
  }
  else {
    AbsVertexFree(catalog, childResult, NIL(AbsVertexInfo_t));
  }
  
  return result;
} /* End of TranslateCtlNOT */

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

  Synopsis [Computes the operational graph representation of the predicate
  of the form p -> q]

  SideEffects        []

  SeeAlso            [TranslateCtlSubFormula]

******************************************************************************/
static AbsVertexInfo_t *
TranslateCtlTHEN(
  AbsVertexCatalog_t *catalog,
  Ctlp_Formula_t *formula,
  array_t *fairArray,
  AbsVertexInfo_t *fairPositive,
  AbsVertexInfo_t *fairNegative,
  int polarity,
  int *uniqueIds)
{
  AbsVertexInfo_t *result;
  AbsVertexInfo_t *leftResult, *rightResult;
  AbsVertexInfo_t *aux1;
  AbsVertexInfo_t *aux2;
  
  leftResult = TranslateCtlSubFormula(catalog,
				      Ctlp_FormulaReadLeftChild(formula),
				      fairArray, fairPositive, fairNegative,
				      !polarity, uniqueIds);
  rightResult= TranslateCtlSubFormula(catalog,
				      Ctlp_FormulaReadRightChild(formula),
				      fairArray, fairPositive, fairNegative,
				      polarity, uniqueIds);
  
  /* If the sub-formula's top vertex is a negation, eliminate the redundancy */
  if (AbsVertexReadType(rightResult) == not_c) {
    AbsVertexInfo_t *newResult;

    newResult = AbsVertexReadLeftKid(rightResult);
    AbsVertexReadRefs(newResult)++;
    AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
    aux1 = newResult;
  }
  else {
    /* Vertex negating first operand */
    aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, rightResult, 
				     NIL(AbsVertexInfo_t), 0, NIL(char), 
				     NIL(char));
    if (AbsVertexReadType(aux1) == false_c) {
      AbsVertexSetPolarity(aux1, !polarity);
      AbsVertexSetDepth(aux1, AbsVertexReadDepth(rightResult) + 1);
      AbsVertexSetType(aux1, not_c);
      AbsVertexSetLeftKid(aux1, rightResult);
      AbsVertexSetParent(rightResult, aux1);
    }
    else {
      AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
    }
  }
  
  /* Result node holding the and of both operands */
  aux2 = AbsVertexCatalogFindOrAdd(catalog, and_c, !polarity, leftResult, 
				   aux1, 0, NIL(char), NIL(char));
  if (AbsVertexReadType(aux2) == false_c) {
    AbsVertexSetPolarity(aux2, !polarity);
    if (AbsVertexReadDepth(leftResult) > AbsVertexReadDepth(aux1)) {
      AbsVertexSetDepth(aux2, AbsVertexReadDepth(leftResult) + 1);
    }
    else {
      AbsVertexSetDepth(aux2, AbsVertexReadDepth(aux1) + 1);
    }
    AbsVertexSetType(aux2, and_c);
    AbsVertexSetLeftKid(aux2, leftResult);
    AbsVertexSetRightKid(aux2, aux1);
    AbsVertexSetParent(aux1, aux2);
    AbsVertexSetParent(leftResult, aux2);
  }
  else {
    AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
  }
  
  /* Top vertex negation of the conjunction */
  result = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux2,
				     NIL(AbsVertexInfo_t), 0, NIL(char), 
				     NIL(char));
  if (AbsVertexReadType(result) == false_c) {
    AbsVertexSetPolarity(result, polarity);
    AbsVertexSetDepth(result, AbsVertexReadDepth(aux2) + 1);
    AbsVertexSetType(result, not_c);
    AbsVertexSetLeftKid(result, aux2);
    AbsVertexSetParent(aux2, result);
  }
  else {
    AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
  }
  
  return result;
} /* End of TranslateCtlTHEN */

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

  Synopsis [Computes the operational graph representation of the predicate of
  the form p AND q]

  SideEffects        []

  SeeAlso            [TranslateCtlSubFormula]

******************************************************************************/
static AbsVertexInfo_t *
TranslateCtlAND(
  AbsVertexCatalog_t *catalog,
  Ctlp_Formula_t *formula,
  array_t *fairArray,
  AbsVertexInfo_t *fairPositive,
  AbsVertexInfo_t *fairNegative,
  int polarity,
  int *uniqueIds)
{
  AbsVertexInfo_t *result;
  AbsVertexInfo_t *leftResult, *rightResult;
  int leftDepth;
  int rightDepth;
  
  leftResult = TranslateCtlSubFormula(catalog,
				      Ctlp_FormulaReadLeftChild(formula),
				      fairArray, fairPositive, fairNegative,
				      polarity, uniqueIds);
  rightResult= TranslateCtlSubFormula(catalog,
				      Ctlp_FormulaReadRightChild(formula),
				      fairArray, fairPositive, fairNegative,
				      polarity, uniqueIds);
  
  /* Read the depths */
  leftDepth = AbsVertexReadDepth(leftResult);
  rightDepth = AbsVertexReadDepth(rightResult);
  
  result = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, leftResult, 
				     rightResult, 0, NIL(char), NIL(char));
  if (AbsVertexReadType(result) == false_c) {
    AbsVertexSetPolarity(result, polarity);
    if (leftDepth > rightDepth) {
      AbsVertexSetDepth(result, leftDepth + 1);
    }
    else {
      AbsVertexSetDepth(result, rightDepth + 1);
    }
    AbsVertexSetType(result, and_c);
    AbsVertexSetLeftKid(result, leftResult);
    AbsVertexSetRightKid(result, rightResult);
    AbsVertexSetParent(leftResult, result);
    AbsVertexSetParent(rightResult, result);
  }
  else {
    AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
    AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
  }
  
  return result;
} /* End of TranslateCtlAND */

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

  Synopsis [Computes the operational graph representation of the predicate of
   the for p OR q]

  SideEffects        []

  SeeAlso            [TranslateCtlSubFormula]

******************************************************************************/
static AbsVertexInfo_t *
TranslateCtlOR(
  AbsVertexCatalog_t *catalog,
  Ctlp_Formula_t *formula,
  array_t *fairArray,
  AbsVertexInfo_t *fairPositive,
  AbsVertexInfo_t *fairNegative,
  int polarity,
  int *uniqueIds)
{
  AbsVertexInfo_t *result;
  AbsVertexInfo_t *leftResult, *rightResult;
  AbsVertexInfo_t *aux1;
  AbsVertexInfo_t *aux2;
  AbsVertexInfo_t *aux3;
  
  leftResult = TranslateCtlSubFormula(catalog,
				      Ctlp_FormulaReadLeftChild(formula),
				      fairArray, fairPositive, fairNegative,
				      polarity, uniqueIds);
  rightResult= TranslateCtlSubFormula(catalog,
				      Ctlp_FormulaReadRightChild(formula),
				      fairArray, fairPositive, fairNegative,
				      polarity, uniqueIds);
  
  /* If the sub-formula's top vertex is a negation, eliminate the redundancy */
  if (AbsVertexReadType(leftResult) == not_c) {
    AbsVertexInfo_t *newResult;

    newResult = AbsVertexReadLeftKid(leftResult);
    AbsVertexReadRefs(newResult)++;
    AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
    aux1 = newResult;
  }
  else {
    /* Vertex negating first operand */
    aux1 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, leftResult, 
				     NIL(AbsVertexInfo_t), 0, NIL(char), 
				     NIL(char));
    if (AbsVertexReadType(aux1) == false_c) {
      AbsVertexSetPolarity(aux1, !polarity);
      AbsVertexSetDepth(aux1, AbsVertexReadDepth(leftResult) + 1);
      AbsVertexSetType(aux1, not_c);
      AbsVertexSetLeftKid(aux1, leftResult);
      AbsVertexSetParent(leftResult, aux1);
    }
    else {
      AbsVertexFree(catalog, leftResult, NIL(AbsVertexInfo_t));
    }
  }
  
  if (AbsVertexReadType(rightResult) == not_c) {
    AbsVertexInfo_t *newResult;

    newResult = AbsVertexReadLeftKid(rightResult);
    AbsVertexReadRefs(newResult)++;
    AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
    aux2 = newResult;
  }
  else {
    /* Vertex negating second operand */
    aux2 = AbsVertexCatalogFindOrAdd(catalog, not_c, !polarity, rightResult, 
				     NIL(AbsVertexInfo_t), 0, NIL(char), 
				     NIL(char));
    if (AbsVertexReadType(aux2) == false_c) {
      AbsVertexSetPolarity(aux2, !polarity);
      AbsVertexSetDepth(aux2, AbsVertexReadDepth(rightResult) + 1);
      AbsVertexSetType(aux2, not_c);
      AbsVertexSetLeftKid(aux2, rightResult);
      AbsVertexSetParent(rightResult, aux2);
    }
    else {
      AbsVertexFree(catalog, rightResult, NIL(AbsVertexInfo_t));
    }
  }
  
  /* Vertex taking the conjunction */
  aux3 = AbsVertexCatalogFindOrAdd(catalog, and_c, !polarity, aux1, aux2,
				   0, NIL(char), NIL(char));
  if (AbsVertexReadType(aux3) == false_c) {
    AbsVertexSetPolarity(aux3, !polarity);
    if (AbsVertexReadDepth(aux1) > AbsVertexReadDepth(aux2)) {
      AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux1) + 1);
    }
    else {
      AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux2) + 1);
    }
    AbsVertexSetType(aux3, and_c);
    AbsVertexSetLeftKid(aux3, aux1);
    AbsVertexSetRightKid(aux3, aux2);
    AbsVertexSetParent(aux1, aux3);
    AbsVertexSetParent(aux2, aux3);
  }
  else {
    AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
    AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
  }
  
  /* Top vertex negation of the conjunction */
  result = AbsVertexCatalogFindOrAdd(catalog, not_c, polarity, aux3,
				     NIL(AbsVertexInfo_t), 0, NIL(char), 
				     NIL(char));
  if (AbsVertexReadType(result) == false_c) {
    AbsVertexSetPolarity(result, polarity);
    AbsVertexSetDepth(result, AbsVertexReadDepth(aux3) + 1);
    AbsVertexSetType(result, not_c);
    AbsVertexSetLeftKid(result, aux3);
    AbsVertexSetParent(aux3, result);
  }
  else {
    AbsVertexFree(catalog, aux3, NIL(AbsVertexInfo_t));
  }
  
  return result;
} /* End of TranslateCtlOR */

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

  Synopsis [Given an array containing vertices, creates the conjunction of all
  of them.]

  SideEffects        []

  SeeAlso            [ComputeFairPredicate]

******************************************************************************/
static AbsVertexInfo_t *
CreateConjunctionChain(
  AbsVertexCatalog_t *catalog,
  array_t *conjunctions,
  int polarity)
{
  AbsVertexInfo_t *aux1;
  AbsVertexInfo_t *aux2;
  AbsVertexInfo_t *aux3;
  int i;

  assert(conjunctions != NIL(array_t));

  aux1 = array_fetch(AbsVertexInfo_t *, conjunctions, 0);
  AbsVertexReadRefs(aux1)++;

  if (array_n(conjunctions) == 1) {
    return aux1;
  }

  for (i=1; i<array_n(conjunctions); i++) {
    aux2 = array_fetch(AbsVertexInfo_t *, conjunctions, i);
    AbsVertexReadRefs(aux2)++;
    
    aux3 = AbsVertexCatalogFindOrAdd(catalog, and_c, polarity, aux1, aux2, 0,
				     NIL(char), NIL(char));

    if (AbsVertexReadType(aux3) == false_c) {
      AbsVertexSetPolarity(aux3, polarity);
      if (AbsVertexReadDepth(aux1) < AbsVertexReadDepth(aux2)) {
	AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux2) + 1);
      }
      else {
	AbsVertexSetDepth(aux3, AbsVertexReadDepth(aux1) + 1);
      }
      AbsVertexSetType(aux3, and_c);
      AbsVertexSetLeftKid(aux3, aux1);
      AbsVertexSetRightKid(aux3, aux2);
      AbsVertexSetParent(aux1, aux3);
      AbsVertexSetParent(aux2, aux3);
    }
    else {
      AbsVertexFree(catalog, aux1, NIL(AbsVertexInfo_t));
      AbsVertexFree(catalog, aux2, NIL(AbsVertexInfo_t));
    }

    aux1 = aux3;
  }

  return aux1;
} /* End of CreateConjunctionChain */