VIS
Functions | Variables

src/ctlsp/ctlspUtil.c File Reference

#include "ctlspInt.h"
#include "errno.h"
#include "ntk.h"
Include dependency graph for ctlspUtil.c:

Go to the source code of this file.

Functions

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)
array_t * Ctlsp_FileParseFormulaArray (FILE *fp)
array_t * Ctlsp_FileParseCTLFormulaArray (FILE *fp)
char * Ctlsp_FormulaConvertToString (Ctlsp_Formula_t *formula)
void Ctlsp_FormulaPrint (FILE *fp, Ctlsp_Formula_t *formula)
Ctlsp_FormulaType Ctlsp_FormulaReadType (Ctlsp_Formula_t *formula)
int Ctlsp_FormulaReadCompareValue (Ctlsp_Formula_t *formula)
char * Ctlsp_FormulaReadVariableName (Ctlsp_Formula_t *formula)
char * Ctlsp_FormulaReadValueName (Ctlsp_Formula_t *formula)
Ctlsp_Formula_t * Ctlsp_FormulaReadLeftChild (Ctlsp_Formula_t *formula)
Ctlsp_Formula_t * Ctlsp_FormulaReadRightChild (Ctlsp_Formula_t *formula)
mdd_t * Ctlsp_FormulaObtainStates (Ctlsp_Formula_t *formula)
mdd_t * Ctlsp_FormulaObtainApproxStates (Ctlsp_Formula_t *formula, Ctlsp_Approx_t approx)
void Ctlsp_FormulaSetStates (Ctlsp_Formula_t *formula, mdd_t *states)
void Ctlsp_FormulaSetApproxStates (Ctlsp_Formula_t *formula, mdd_t *states, Ctlsp_Approx_t approx)
void Ctlsp_FormulaSetDbgInfo (Ctlsp_Formula_t *formula, void *data, Ctlsp_DbgInfoFreeFn freeFn)
void * Ctlsp_FormulaReadDebugData (Ctlsp_Formula_t *formula)
boolean Ctlsp_FormulaTestIsConverted (Ctlsp_Formula_t *formula)
boolean Ctlsp_FormulaTestIsQuantifierFree (Ctlsp_Formula_t *formula)
Ctlsp_Formula_t * Ctlsp_FormulaReadOriginalFormula (Ctlsp_Formula_t *formula)
int Ctlsp_FormulaReadABIndex (Ctlsp_Formula_t *formula)
void Ctlsp_FormulaSetABIndex (Ctlsp_Formula_t *formula, int ab_idx)
int Ctlsp_FormulaReadLabelIndex (Ctlsp_Formula_t *formula)
void Ctlsp_FormulaSetLabelIndex (Ctlsp_Formula_t *formula, int label_idx)
char Ctlsp_FormulaReadRhs (Ctlsp_Formula_t *formula)
void Ctlsp_FormulaSetRhs (Ctlsp_Formula_t *formula)
void Ctlsp_FormulaResetRhs (Ctlsp_Formula_t *formula)
char Ctlsp_FormulaReadMarked (Ctlsp_Formula_t *formula)
void Ctlsp_FormulaSetMarked (Ctlsp_Formula_t *formula)
void Ctlsp_FormulaResetMarked (Ctlsp_Formula_t *formula)
void Ctlsp_FormulaFree (Ctlsp_Formula_t *formula)
void Ctlsp_FlushStates (Ctlsp_Formula_t *formula)
Ctlsp_Formula_t * Ctlsp_FormulaDup (Ctlsp_Formula_t *formula)
void Ctlsp_FormulaArrayFree (array_t *formulaArray)
array_t * Ctlsp_FormulaArrayConvertToDAG (array_t *formulaArray)
Ctlsp_Formula_t * Ctlsp_FormulaCreate (Ctlsp_FormulaType type, void *left_, void *right_)
Ctlsp_Formula_t * Ctlsp_FormulaCreateOr (char *name, char *valueStr)
Ctlsp_Formula_t * Ctlsp_FormulaCreateVectorAnd (char *nameVector, char *value)
Ctlsp_Formula_t * Ctlsp_FormulaCreateVectorOr (char *nameVector, char *valueStr)
Ctlsp_Formula_t * Ctlsp_FormulaCreateEquiv (char *left, char *right)
Ctlsp_Formula_t * Ctlsp_FormulaCreateVectorEquiv (char *left, char *right)
Ctlsp_Formula_t * Ctlsp_FormulaCreateXMult (char *string, Ctlsp_Formula_t *formula)
Ctlsp_Formula_t * Ctlsp_FormulaCreateEXMult (char *string, Ctlsp_Formula_t *formula)
Ctlsp_Formula_t * Ctlsp_FormulaCreateAXMult (char *string, Ctlsp_Formula_t *formula)
char * Ctlsp_FormulaGetTypeString (Ctlsp_Formula_t *formula)
Ctlsp_FormulaClass Ctlsp_CheckClassOfExistentialFormula (Ctlsp_Formula_t *formula)
Ctlsp_FormulaClass Ctlsp_CheckClassOfExistentialFormulaArray (array_t *formulaArray)
Ctlsp_ClassOfFormula Ctlsp_FormulaReadClass (Ctlsp_Formula_t *formula)
void Ctlsp_FormulaSetClass (Ctlsp_Formula_t *formula, Ctlsp_ClassOfFormula newClass)
Ctlsp_ClassOfCTLFormula Ctlsp_FormulaReadClassOfCTL (Ctlsp_Formula_t *formula)
void Ctlsp_FormulaSetClassOfCTL (Ctlsp_Formula_t *formula, Ctlsp_ClassOfCTLFormula newCTLclass)
array_t * Ctlsp_FormulaArrayConvertToLTL (array_t *formulaArray)
array_t * Ctlsp_FormulaArrayConvertToCTL (array_t *formulaArray)
Ctlp_Formula_t * Ctlsp_FormulaConvertToCTL (Ctlsp_Formula_t *formula)
Ctlp_Formula_t * Ctlsp_PropositionalFormulaToCTL (Ctlsp_Formula_t *formula)
int Ctlsp_isPropositionalFormula (Ctlsp_Formula_t *formula)
int Ctlsp_isCtlFormula (Ctlsp_Formula_t *formula)
int Ctlsp_isLtlFormula (Ctlsp_Formula_t *formula)
Ctlsp_Formula_t * Ctlsp_LtllFormulaNegate (Ctlsp_Formula_t *ltlFormula)
void Ctlsp_LtlSetClass (Ctlsp_Formula_t *formula)
int Ctlsp_LtlFormulaIsGFp (Ctlsp_Formula_t *formula)
boolean Ctlsp_LtlFormulaIsGp (Ctlsp_Formula_t *formula)
boolean Ctlsp_LtlFormulaIsFp (Ctlsp_Formula_t *formula)
void Ctlsp_FormulaArrayAddLtlFairnessConstraints (array_t *formulaArray, array_t *constraintArray)
Ctlsp_Formula_t * Ctlsp_CtlFormulaToCtlsp (Ctlp_Formula_t *F)
Ctlsp_Formula_t * Ctlsp_LtlFormulaExpandAbbreviation (Ctlsp_Formula_t *formula)
Ctlsp_Formula_t * Ctlsp_LtlFormulaNegationNormalForm (Ctlsp_Formula_t *formula)
Ctlsp_Formula_t * Ctlsp_LtlFormulaHashIntoUniqueTable (Ctlsp_Formula_t *F, st_table *uniqueTable)
void Ctlsp_LtlFormulaClearMarks (Ctlsp_Formula_t *F)
int Ctlsp_LtlFormulaCountNumber (Ctlsp_Formula_t *F)
st_table * Ctlsp_LtlFormulaCreateUniqueTable (void)
int Ctlsp_LtlFormulaIsElementary2 (Ctlsp_Formula_t *F)
int Ctlsp_LtlFormulaIsElementary (Ctlsp_Formula_t *F)
boolean Ctlsp_LtlFormulaTestIsBounded (Ctlsp_Formula_t *formula, int *depth)
int Ctlsp_LtlFormulaDepth (Ctlsp_Formula_t *formula)
boolean Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe (Ctlsp_Formula_t *formula)
int Ctlsp_LtlFormulaArrayIsPropositional (array_t *formulaArray)
int Ctlsp_LtlFormulaIsPropositional (Ctlsp_Formula_t *F)
int Ctlsp_LtlFormulaIsAtomicPropositional (Ctlsp_Formula_t *F)
int Ctlsp_LtlFormulaIsFG (Ctlsp_Formula_t *F)
int Ctlsp_LtlFormulaIsGF (Ctlsp_Formula_t *F)
int Ctlsp_LtlFormulaIsFGorGF (Ctlsp_Formula_t *F)
int Ctlsp_LtlFormulaSimplyImply (Ctlsp_Formula_t *from, Ctlsp_Formula_t *to)
array_t * Ctlsp_LtlTranslateIntoSNF (Ctlsp_Formula_t *formula)
void Ctlsp_LtlTranslateIntoSNFRecursive (Ctlsp_Formula_t *propNode, Ctlsp_Formula_t *formula, array_t *formulaArray, int *index)
Ctlsp_Formula_t * Ctlsp_LtlFormulaSimpleRewriting (Ctlsp_Formula_t *formula)
Ctlsp_Formula_t * CtlspLtlFormulaSimpleRewriting_Aux (Ctlsp_Formula_t *F, st_table *Utable)
void CtlspFormulaIncrementRefCount (Ctlsp_Formula_t *formula)
void CtlspFormulaDecrementRefCount (Ctlsp_Formula_t *formula)
void CtlspFormulaAddToGlobalArray (Ctlsp_Formula_t *formula)
void CtlspFormulaFree (Ctlsp_Formula_t *formula)
int CtlspStringChangeValueStrToBinString (char *value, char *binValueStr, int interval)
void CtlspChangeBracket (char *inStr)
char * CtlspGetVectorInfoFromStr (char *str, int *start, int *end, int *interval, int *inc)
int CtlspFormulaAddToTable (char *name, Ctlsp_Formula_t *formula, st_table *macroTable)
Ctlsp_Formula_t * CtlspFormulaFindInTable (char *name, st_table *macroTable)
Ctlsp_FormulaClass CtlspCheckClassOfExistentialFormulaRecur (Ctlsp_Formula_t *formula, boolean parity)
Ctlsp_FormulaClass CtlspResolveClass (Ctlsp_FormulaClass class1, Ctlsp_FormulaClass class2)
Ctlp_Formula_t * CtlspFormulaConvertToCTL (Ctlsp_Formula_t *formula)
Ctlsp_Formula_t * CtlspFunctionOr (Ctlsp_Formula_t *left, Ctlsp_Formula_t *right)
Ctlsp_Formula_t * CtlspFunctionAnd (Ctlsp_Formula_t *left, Ctlsp_Formula_t *right)
Ctlsp_Formula_t * CtlspFunctionThen (Ctlsp_Formula_t *left, Ctlsp_Formula_t *right)

Variables

static char rcsid[] UNUSED = "$Id: ctlspUtil.c,v 1.64 2009/04/11 18:25:55 fabio Exp $"
static array_t * globalFormulaArray
static int changeBracket = 1
int CtlspGlobalError
Ctlsp_Formula_t * CtlspGlobalFormula
st_table * CtlspMacroTable

Function Documentation

static Ctlsp_Formula_t * createSNFnode ( Ctlsp_Formula_t *  formula,
array_t *  formulaArray,
int *  index 
) [static]

Function********************************************************************

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

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

SideEffects [Add the new generated SNF rule to formulaArray]

SeeAlso [Ctlsp_LtlTranslateIntoSNFRecursive]

Definition at line 5431 of file ctlspUtil.c.

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

}

Here is the call graph for this function:

Here is the caller graph for this function:

Ctlsp_FormulaClass Ctlsp_CheckClassOfExistentialFormula ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

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

SideEffects []

SeeAlso []

Definition at line 1687 of file ctlspUtil.c.

{
  Ctlsp_FormulaClass result;

  result = CtlspCheckClassOfExistentialFormulaRecur(formula, FALSE);

  return result;
} /* End of Ctlsp_CheckTypeOfExistentialFormula */

Here is the call graph for this function:

Here is the caller graph for this function:

Ctlsp_FormulaClass Ctlsp_CheckClassOfExistentialFormulaArray ( array_t *  formulaArray)

Function********************************************************************

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

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

SideEffects []

SeeAlso [Ctlsp_CheckClassOfExistentialFormula]

Definition at line 1713 of file ctlspUtil.c.

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

Here is the call graph for this function:

Ctlsp_Formula_t* Ctlsp_CtlFormulaToCtlsp ( Ctlp_Formula_t *  F)

Function********************************************************************

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

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

SideEffects []

SeeAlso []

Definition at line 2364 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

array_t* Ctlsp_FileParseCTLFormulaArray ( FILE *  fp)

Function********************************************************************

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

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

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

SeeAlso [Ctlsp_FileParseFormulaArray]

Definition at line 153 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

array_t* Ctlsp_FileParseFormulaArray ( FILE *  fp)

AutomaticEnd Function********************************************************************

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

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

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

SeeAlso [Ctlsp_FormulaArrayFree Ctlsp_FormulaPrint]

Definition at line 86 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void Ctlsp_FlushStates ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

Description []

SideEffects []

SeeAlso [Ctlsp_FormulaFree]

Definition at line 927 of file ctlspUtil.c.

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

  }

}
void Ctlsp_FormulaArrayAddLtlFairnessConstraints ( array_t *  formulaArray,
array_t *  constraintArray 
)

Function********************************************************************

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

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

SideEffects [formulaArray is modified]

SeeAlso []

Definition at line 2309 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

array_t* Ctlsp_FormulaArrayConvertToCTL ( array_t *  formulaArray)

Function********************************************************************

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

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

SideEffects []

SeeAlso [Ctlsp_FormulaConvertToCTL]

Definition at line 1868 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

array_t* Ctlsp_FormulaArrayConvertToDAG ( array_t *  formulaArray)

Function********************************************************************

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

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

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

RB: What does that mean?

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

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

SeeAlso []

Definition at line 1079 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

array_t* Ctlsp_FormulaArrayConvertToLTL ( array_t *  formulaArray)

Function********************************************************************

Synopsis [Returns an array of LTL formulae.]

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

SideEffects []

SeeAlso []

Definition at line 1825 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void Ctlsp_FormulaArrayFree ( array_t *  formulaArray)

Function********************************************************************

Synopsis [Frees an array of CTL* formulas.]

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

SideEffects []

SeeAlso [Ctlsp_FormulaFree]

Definition at line 1027 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Ctlp_Formula_t* Ctlsp_FormulaConvertToCTL ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Convert an CTL* formula to CTL formula]

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

SideEffects []

SeeAlso [Ctlsp_FormulaArrayConvertToCTL]

Definition at line 1912 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

char* Ctlsp_FormulaConvertToString ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

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

SideEffects []

Definition at line 177 of file ctlspUtil.c.

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

Here is the caller graph for this function:

Ctlsp_Formula_t* Ctlsp_FormulaCreate ( Ctlsp_FormulaType  type,
void *  left_,
void *  right_ 
)

Function********************************************************************

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

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

Comment []

SideEffects []

SeeAlso [CtlspFormulaDecrementRefCount]

Definition at line 1122 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Ctlsp_Formula_t* Ctlsp_FormulaCreateAXMult ( char *  string,
Ctlsp_Formula_t *  formula 
)

Function********************************************************************

Synopsis [Creates a CTL* formula for multiple AX]

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

SideEffects []

SeeAlso []

Definition at line 1545 of file ctlspUtil.c.

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

Here is the call graph for this function:

Ctlsp_Formula_t* Ctlsp_FormulaCreateEquiv ( char *  left,
char *  right 
)

Function********************************************************************

Synopsis [Creates a CTL formula for equivalent property]

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

SideEffects []

SeeAlso []

Definition at line 1370 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Ctlsp_Formula_t* Ctlsp_FormulaCreateEXMult ( char *  string,
Ctlsp_Formula_t *  formula 
)

Function********************************************************************

Synopsis [Creates a CTL* formula for multiple EX]

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

SideEffects []

SeeAlso []

Definition at line 1499 of file ctlspUtil.c.

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

Here is the call graph for this function:

Ctlsp_Formula_t* Ctlsp_FormulaCreateOr ( char *  name,
char *  valueStr 
)

Function********************************************************************

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

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

SideEffects []

SeeAlso []

Definition at line 1227 of file ctlspUtil.c.

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

Here is the call graph for this function:

Ctlsp_Formula_t* Ctlsp_FormulaCreateVectorAnd ( char *  nameVector,
char *  value 
)

Function********************************************************************

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

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

SideEffects []

SeeAlso []

Definition at line 1269 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Ctlsp_Formula_t* Ctlsp_FormulaCreateVectorEquiv ( char *  left,
char *  right 
)

Function********************************************************************

Synopsis [Creates a CTL formula for equivalent of vector]

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

SideEffects []

SeeAlso []

Definition at line 1403 of file ctlspUtil.c.

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

Here is the call graph for this function:

Ctlsp_Formula_t* Ctlsp_FormulaCreateVectorOr ( char *  nameVector,
char *  valueStr 
)

Function********************************************************************

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

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

SideEffects []

SeeAlso []

Definition at line 1332 of file ctlspUtil.c.

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

Here is the call graph for this function:

Ctlsp_Formula_t* Ctlsp_FormulaCreateXMult ( char *  string,
Ctlsp_Formula_t *  formula 
)

Function********************************************************************

Synopsis [Creates a CTL formula for multiple X]

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

SideEffects []

SeeAlso []

Definition at line 1459 of file ctlspUtil.c.

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

Here is the call graph for this function:

Ctlsp_Formula_t* Ctlsp_FormulaDup ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Duplicates a CTL* formula.]

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

SideEffects []

SeeAlso []

Definition at line 977 of file ctlspUtil.c.

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

Here is the caller graph for this function:

void Ctlsp_FormulaFree ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

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

SideEffects []

SeeAlso [CtlspFormulaFree, CtlspDecrementRefCount]

Definition at line 908 of file ctlspUtil.c.

{
  CtlspFormulaDecrementRefCount(formula);
}

Here is the call graph for this function:

Here is the caller graph for this function:

char* Ctlsp_FormulaGetTypeString ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Returns a string for each formula type.]

Description [Returns a string for each formula type.]

SideEffects []

SeeAlso []

Definition at line 1591 of file ctlspUtil.c.

{
  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);
}
mdd_t* Ctlsp_FormulaObtainApproxStates ( Ctlsp_Formula_t *  formula,
Ctlsp_Approx_t  approx 
)

Function********************************************************************

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

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

SideEffects []

SeeAlso [Ctlsp_FormulaSetStates]

Definition at line 496 of file ctlspUtil.c.

{
  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);
}
mdd_t* Ctlsp_FormulaObtainStates ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

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

SideEffects []

SeeAlso [Ctlsp_FormulaSetStates]

Definition at line 472 of file ctlspUtil.c.

{
  if (formula->states == NIL(mdd_t)) {
    return NIL(mdd_t);
  }
  else {
    return mdd_dup(formula->states);
  }
}
void Ctlsp_FormulaPrint ( FILE *  fp,
Ctlsp_Formula_t *  formula 
)

Function********************************************************************

Synopsis [Prints a formula to a file.]

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

SideEffects []

Definition at line 313 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

int Ctlsp_FormulaReadABIndex ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

SideEffects []

Definition at line 758 of file ctlspUtil.c.

{
  return formula->ab_idx;
}

Here is the caller graph for this function:

Ctlsp_ClassOfFormula Ctlsp_FormulaReadClass ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Get the class of a formula]

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

SideEffects []

SeeAlso []

Definition at line 1743 of file ctlspUtil.c.

{
  return formula->class_;
}

Here is the caller graph for this function:

Ctlsp_ClassOfCTLFormula Ctlsp_FormulaReadClassOfCTL ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Get the type of a CTL formula]

Description []

SideEffects []

SeeAlso []

Definition at line 1782 of file ctlspUtil.c.

{
  return formula->CTLclass;
}

Here is the caller graph for this function:

int Ctlsp_FormulaReadCompareValue ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Gets the compare value of a formula.]

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

SideEffects []

SeeAlso [ctlsp.h]

Definition at line 360 of file ctlspUtil.c.

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

Function********************************************************************

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

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

SideEffects []

SeeAlso [Ctlsp_FormulaSetDbgInfo]

Definition at line 657 of file ctlspUtil.c.

{
  return formula->dbgInfo.data;
}
int Ctlsp_FormulaReadLabelIndex ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

SideEffects []

Definition at line 788 of file ctlspUtil.c.

{
  return formula->label_idx;
}

Here is the caller graph for this function:

Ctlsp_Formula_t* Ctlsp_FormulaReadLeftChild ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Gets the left child of a formula.]

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

SideEffects []

SeeAlso [Ctlsp_FormulaReadRightChild]

Definition at line 423 of file ctlspUtil.c.

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

Here is the caller graph for this function:

char Ctlsp_FormulaReadMarked ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

SideEffects []

Definition at line 860 of file ctlspUtil.c.

{
  return formula->marked;
}

Here is the caller graph for this function:

Ctlsp_Formula_t* Ctlsp_FormulaReadOriginalFormula ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Returns original formula corresponding to converted formula.]

SideEffects []

Definition at line 743 of file ctlspUtil.c.

{
  return formula->dbgInfo.originalFormula;
}

Here is the caller graph for this function:

char Ctlsp_FormulaReadRhs ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

SideEffects []

Definition at line 818 of file ctlspUtil.c.

{
  return formula->rhs;
}

Here is the caller graph for this function:

Ctlsp_Formula_t* Ctlsp_FormulaReadRightChild ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Gets the right child of a formula.]

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

SideEffects []

SeeAlso [Ctlsp_FormulaReadLeftChild]

Definition at line 446 of file ctlspUtil.c.

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

Here is the caller graph for this function:

Ctlsp_FormulaType Ctlsp_FormulaReadType ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Gets the type of a formula.]

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

SideEffects []

SeeAlso [ctlsp.h]

Definition at line 340 of file ctlspUtil.c.

{
  return (formula->type);
}

Here is the caller graph for this function:

char* Ctlsp_FormulaReadValueName ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

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

SideEffects []

Definition at line 401 of file ctlspUtil.c.

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

Here is the caller graph for this function:

char* Ctlsp_FormulaReadVariableName ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

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

SideEffects []

Definition at line 380 of file ctlspUtil.c.

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

Here is the caller graph for this function:

void Ctlsp_FormulaResetMarked ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

SideEffects []

Definition at line 888 of file ctlspUtil.c.

{
  formula->marked = 0;
}

Here is the caller graph for this function:

void Ctlsp_FormulaResetRhs ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

SideEffects []

Definition at line 846 of file ctlspUtil.c.

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

Function********************************************************************

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

SideEffects []

Definition at line 772 of file ctlspUtil.c.

{
  formula->ab_idx = ab_idx;
}

Here is the caller graph for this function:

void Ctlsp_FormulaSetApproxStates ( Ctlsp_Formula_t *  formula,
mdd_t *  states,
Ctlsp_Approx_t  approx 
)

Function********************************************************************

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

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

SideEffects []

SeeAlso [Ctlsp_FormulaObtainStates]

Definition at line 573 of file ctlspUtil.c.

{
  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_FormulaSetClass ( Ctlsp_Formula_t *  formula,
Ctlsp_ClassOfFormula  newClass 
)

Function********************************************************************

Synopsis [Set the class of a formula]

Description []

SideEffects []

SeeAlso []

Definition at line 1760 of file ctlspUtil.c.

{
  if (formula == NIL(Ctlsp_Formula_t)){
    return;
  }
  formula->class_ = newClass;
}

Here is the caller graph for this function:

void Ctlsp_FormulaSetClassOfCTL ( Ctlsp_Formula_t *  formula,
Ctlsp_ClassOfCTLFormula  newCTLclass 
)

Function********************************************************************

Synopsis [Set the class of CTL]

Description []

SideEffects []

SeeAlso []

Definition at line 1799 of file ctlspUtil.c.

{
  if (formula == NIL(Ctlsp_Formula_t)){
    return;
  }
  formula->CTLclass = newCTLclass;
}

Here is the caller graph for this function:

void Ctlsp_FormulaSetDbgInfo ( Ctlsp_Formula_t *  formula,
void *  data,
Ctlsp_DbgInfoFreeFn  freeFn 
)

Function********************************************************************

Synopsis [Sets the debug information of a formula.]

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

SideEffects []

SeeAlso [Ctlsp_FormulaReadDebugData]

Definition at line 634 of file ctlspUtil.c.

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

Function********************************************************************

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

SideEffects []

Definition at line 802 of file ctlspUtil.c.

{
  formula->label_idx = label_idx;
}

Here is the caller graph for this function:

void Ctlsp_FormulaSetMarked ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

SideEffects []

Definition at line 874 of file ctlspUtil.c.

{
  formula->marked = 1;
}

Here is the caller graph for this function:

void Ctlsp_FormulaSetRhs ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

SideEffects []

Definition at line 832 of file ctlspUtil.c.

{
  formula->rhs = 1;
}

Here is the caller graph for this function:

void Ctlsp_FormulaSetStates ( Ctlsp_Formula_t *  formula,
mdd_t *  states 
)

Function********************************************************************

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

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

SideEffects []

SeeAlso [Ctlsp_FormulaObtainStates]

Definition at line 543 of file ctlspUtil.c.

{
  /* 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;
}
boolean Ctlsp_FormulaTestIsConverted ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

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

SideEffects []

Definition at line 678 of file ctlspUtil.c.

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

Function********************************************************************

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

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

SideEffects []

Definition at line 697 of file ctlspUtil.c.

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

Here is the call graph for this function:

int Ctlsp_isCtlFormula ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

Description []

SideEffects []

SeeAlso [Ctlsp_FormulaReadClassOfCTL()]

Definition at line 1971 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

int Ctlsp_isLtlFormula ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

Description [a formula is LTL formul if its one of the following:

  • Its class is Ctlsp_LTLformula_c
  • it is in the form A(Ctlsp_LTLformula_c).
  • Its class is Ctlsp_propformula_c.
  • it is in the form A(Ctlsp_propformula_c) ] SideEffects []

SeeAlso [Ctlsp_FormulaReadClass()]

Definition at line 1993 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

int Ctlsp_isPropositionalFormula ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

Description []

SideEffects []

SeeAlso [Ctlsp_FormulaReadClass()]

Definition at line 1953 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

int Ctlsp_LtlFormulaArrayIsPropositional ( array_t *  formulaArray)

Function********************************************************************

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

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

SideEffects [none]

SeeAlso [Ctlsp_LtlFormulaIsPropositional]

Definition at line 3027 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void Ctlsp_LtlFormulaClearMarks ( Ctlsp_Formula_t *  F)

Function********************************************************************

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

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

SideEffects []

SeeAlso []

Definition at line 2702 of file ctlspUtil.c.

{
  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)

Function********************************************************************

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

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

SideEffects []

SeeAlso []

Definition at line 2726 of file ctlspUtil.c.

{
  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  )

Function********************************************************************

Synopsis [Alloc a unqiue table for formulae.]

Description [Use FormulaHash and formulaCompare.]

SideEffects []

SeeAlso []

Definition at line 2761 of file ctlspUtil.c.

{
  return st_init_table(FormulaCompare, FormulaHash);
}

Here is the call graph for this function:

Here is the caller graph for this function:

int Ctlsp_LtlFormulaDepth ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

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

SideEffects []

SeeAlso [Ctlsp_LtlFormulaExpandAbbreviation]

Definition at line 2890 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Ctlsp_Formula_t* Ctlsp_LtlFormulaExpandAbbreviation ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

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

SideEffects []

SeeAlso []

Definition at line 2448 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Ctlsp_Formula_t* Ctlsp_LtlFormulaHashIntoUniqueTable ( Ctlsp_Formula_t *  F,
st_table *  uniqueTable 
)

Function********************************************************************

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

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

SideEffects []

SeeAlso []

Definition at line 2672 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

int Ctlsp_LtlFormulaIsAtomicPropositional ( Ctlsp_Formula_t *  F)

Function********************************************************************

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

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

SideEffects [none]

SeeAlso [Ctlsp_LtlFormulaIsPropositional]

Definition at line 3105 of file ctlspUtil.c.

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

Here is the caller graph for this function:

int Ctlsp_LtlFormulaIsElementary ( Ctlsp_Formula_t *  F)

Function********************************************************************

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

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

SideEffects []

SeeAlso []

Definition at line 2801 of file ctlspUtil.c.

{
  assert(F != NIL(Ctlsp_Formula_t));

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

Here is the call graph for this function:

Here is the caller graph for this function:

int Ctlsp_LtlFormulaIsElementary2 ( Ctlsp_Formula_t *  F)

Function********************************************************************

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

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

SideEffects []

SeeAlso []

Definition at line 2779 of file ctlspUtil.c.

{
  assert(F != 0);

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

Here is the call graph for this function:

int Ctlsp_LtlFormulaIsFG ( Ctlsp_Formula_t *  F)

Function********************************************************************

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

Description [TRUE U (FALSE R p).]

SideEffects []

SeeAlso [Ctlsp_LtlFormulaIsGF, Ctlsp_LtlFormulaIsFGorGF]

Definition at line 3143 of file ctlspUtil.c.

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

Here is the caller graph for this function:

int Ctlsp_LtlFormulaIsFGorGF ( Ctlsp_Formula_t *  F)

Function********************************************************************

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

Description [TRUE U (FALSE R p).]

SideEffects []

SeeAlso [Ctlsp_LtlFormulaIsGF, Ctlsp_LtlFormulaIsFG]

Definition at line 3196 of file ctlspUtil.c.

{
  return (Ctlsp_LtlFormulaIsFG(F) || Ctlsp_LtlFormulaIsGF(F));
}

Here is the call graph for this function:

Here is the caller graph for this function:

boolean Ctlsp_LtlFormulaIsFp ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

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

SideEffects []

SeeAlso [Ctlsp_isPropositionalFormula]

Definition at line 2204 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

int Ctlsp_LtlFormulaIsGF ( Ctlsp_Formula_t *  F)

Function********************************************************************

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

Description [FALSE R (TRUE U p).]

SideEffects []

SeeAlso [Ctlsp_LtlFormulaIsFG, Ctlsp_LtlFormulaIsFGorGF]

Definition at line 3170 of file ctlspUtil.c.

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

Here is the caller graph for this function:

int Ctlsp_LtlFormulaIsGFp ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

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

SideEffects []

SeeAlso []

Definition at line 2137 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

boolean Ctlsp_LtlFormulaIsGp ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

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

SideEffects []

SeeAlso [Ctlsp_isPropositionalFormula]

Definition at line 2174 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

int Ctlsp_LtlFormulaIsPropositional ( Ctlsp_Formula_t *  F)

Function********************************************************************

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

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

SideEffects [none]

SeeAlso [Ctlsp_LtlFormulaIsAtomicPropositional]

Definition at line 3061 of file ctlspUtil.c.

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

Here is the caller graph for this function:

Ctlsp_Formula_t* Ctlsp_LtlFormulaNegationNormalForm ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

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

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

SideEffects []

SeeAlso []

Definition at line 2546 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Ctlsp_Formula_t* Ctlsp_LtlFormulaSimpleRewriting ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Perform simple rewriting of a formula.]

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

SideEffects []

SeeAlso []

Definition at line 3551 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

int Ctlsp_LtlFormulaSimplyImply ( Ctlsp_Formula_t *  from,
Ctlsp_Formula_t *  to 
)

Function********************************************************************

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

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

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

SideEffects []

SeeAlso []

Definition at line 3219 of file ctlspUtil.c.

{

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

Here is the call graph for this function:

Here is the caller graph for this function:

boolean Ctlsp_LtlFormulaTestIsBounded ( Ctlsp_Formula_t *  formula,
int *  depth 
)

Function********************************************************************

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

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

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

SeeAlso [Ctlsp_LtlFormulaExpandAbbreviation, Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe]

Definition at line 2827 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

boolean Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

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

SideEffects [none]

SeeAlso [Ctlsp_LtlFormulaNegationNormalForm, Ctlsp_LtlFormulaTestIsBounded]

Definition at line 2940 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Ctlsp_Formula_t* Ctlsp_LtllFormulaNegate ( Ctlsp_Formula_t *  ltlFormula)

Function********************************************************************

Synopsis [Negate an LTL formula]

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

Comment []

SideEffects []

SeeAlso []

Definition at line 2031 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void Ctlsp_LtlSetClass ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Set the class of the LTL formula]

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

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

SideEffects []

SeeAlso [ctlspInt.h Ctlsp_FormulaCreate]

Definition at line 2069 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

array_t* Ctlsp_LtlTranslateIntoSNF ( Ctlsp_Formula_t *  formula)

Function********************************************************************

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

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

SideEffects []

SeeAlso [Ctlsp_LtlTranslateIntoSNFRecursive]

Definition at line 3336 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

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

Function********************************************************************

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

Description [Recursively trnaslate LTL formula into SNF

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

SideEffects []

SeeAlso []

Definition at line 3383 of file ctlspUtil.c.

{

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

Here is the call graph for this function:

Here is the caller graph for this function:

Ctlp_Formula_t* Ctlsp_PropositionalFormulaToCTL ( Ctlsp_Formula_t *  formula)

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

Description [A wrapper to CtlspFormulaConvertToCTL]

SideEffects []

SeeAlso [Ctlsp_FormulaArrayConvertToCTL]

Definition at line 1934 of file ctlspUtil.c.

{
    return CtlspFormulaConvertToCTL(formula);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void CtlspChangeBracket ( char *  inStr)

Function********************************************************************

Synopsis [Change [] to <>]

Description []

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

SeeAlso []

Definition at line 4712 of file ctlspUtil.c.

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

Here is the caller graph for this function:

Ctlsp_FormulaClass CtlspCheckClassOfExistentialFormulaRecur ( Ctlsp_Formula_t *  formula,
boolean  parity 
)

Function********************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso [FormulaTestIsForallQuantifier]

Definition at line 4857 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void CtlspFormulaAddToGlobalArray ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Adds formula to the end of globalFormulaArray.]

SideEffects [Manipulates the global variable globalFormulaArray.]

SeeAlso [CtlspYyparse]

Definition at line 4562 of file ctlspUtil.c.

{
  array_insert_last(Ctlsp_Formula_t *, globalFormulaArray, formula);
}
int CtlspFormulaAddToTable ( char *  name,
Ctlsp_Formula_t *  formula,
st_table *  macroTable 
)

Function********************************************************************

Synopsis [Insert macro formula into symbol table.]

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

SideEffects []

SeeAlso []

Definition at line 4805 of file ctlspUtil.c.

{
  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;
}
Ctlp_Formula_t* CtlspFormulaConvertToCTL ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Performs a recursive step of Ctlsp_FormulaConvertToCTL() ]

Description []

SideEffects []

Remarks []

SeeAlso []

Definition at line 4964 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void CtlspFormulaDecrementRefCount ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Decrements the reference count of a formula.]

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

SideEffects []

SeeAlso []

Definition at line 4543 of file ctlspUtil.c.

{
  if(formula!=NIL(Ctlsp_Formula_t)) {
    assert(formula->refCount>0);
    if(--(formula->refCount) == 0)
      CtlspFormulaFree(formula);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ctlsp_Formula_t* CtlspFormulaFindInTable ( char *  name,
st_table *  macroTable 
)

Function********************************************************************

Synopsis [Get macro formula from symbol table]

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

SideEffects []

SeeAlso []

Definition at line 4833 of file ctlspUtil.c.

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

Here is the call graph for this function:

void CtlspFormulaFree ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Frees a CTL* formula.]

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

SideEffects []

SeeAlso [Ctlsp_FormulaArrayFree]

Definition at line 4583 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void CtlspFormulaIncrementRefCount ( Ctlsp_Formula_t *  formula)

Function********************************************************************

Synopsis [Increments the reference count of a formula.]

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

SideEffects []

SeeAlso []

Definition at line 4520 of file ctlspUtil.c.

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

Here is the caller graph for this function:

Ctlsp_Formula_t* CtlspFunctionAnd ( Ctlsp_Formula_t *  left,
Ctlsp_Formula_t *  right 
)

Function********************************************************************

Synopsis [Performs And function]

Description []

SideEffects []

SeeAlso []

Definition at line 5194 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Ctlsp_Formula_t* CtlspFunctionOr ( Ctlsp_Formula_t *  left,
Ctlsp_Formula_t *  right 
)

Function********************************************************************

Synopsis [Performs OR function]

Description []

SideEffects []

SeeAlso []

Definition at line 5160 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Ctlsp_Formula_t* CtlspFunctionThen ( Ctlsp_Formula_t *  left,
Ctlsp_Formula_t *  right 
)

Function********************************************************************

Synopsis [Performs Then(Imply) function]

Description []

SideEffects []

SeeAlso []

Definition at line 5228 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

char* CtlspGetVectorInfoFromStr ( char *  str,
int *  start,
int *  end,
int *  interval,
int *  inc 
)

Function********************************************************************

Synopsis [Parse a given vector string.]

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

SideEffects []

SeeAlso []

Definition at line 4753 of file ctlspUtil.c.

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

Here is the caller graph for this function:

Ctlsp_Formula_t* CtlspLtlFormulaSimpleRewriting_Aux ( Ctlsp_Formula_t *  F,
st_table *  Utable 
)

Function********************************************************************

Synopsis [Rewriting the LTL formula recursively.]

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

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

SeeAlso [Ctlsp_LtlFormulaSimpleRewriting]

Definition at line 3602 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Ctlsp_FormulaClass CtlspResolveClass ( Ctlsp_FormulaClass  class1,
Ctlsp_FormulaClass  class2 
)

Function********************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 4930 of file ctlspUtil.c.

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

Here is the caller graph for this function:

int CtlspStringChangeValueStrToBinString ( char *  value,
char *  binValueStr,
int  interval 
)

Function********************************************************************

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

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

SideEffects []

SeeAlso []

Definition at line 4637 of file ctlspUtil.c.

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

Here is the caller graph for this function:

static int FormulaCompare ( const char *  key1,
const char *  key2 
) [static]

Function********************************************************************

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

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

SideEffects []

SeeAlso [FormulaHash]

Definition at line 5290 of file ctlspUtil.c.

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

Here is the caller graph for this function:

static Ctlsp_Formula_t * FormulaCreateWithType ( Ctlsp_FormulaType  type) [static]

AutomaticStart

Function********************************************************************

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

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

SideEffects []

SeeAlso [Ctlsp_FormulaCreate]

Definition at line 5269 of file ctlspUtil.c.

{
  return (Ctlsp_FormulaCreate(type, NIL(Ctlsp_Formula_t), NIL(Ctlsp_Formula_t)));
}

Here is the call graph for this function:

Here is the caller graph for this function:

static int FormulaHash ( char *  key,
int  modulus 
) [static]

Function********************************************************************

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

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

SideEffects []

SeeAlso [FormulaCompare]

Definition at line 5338 of file ctlspUtil.c.

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

Here is the caller graph for this function:

static Ctlsp_Formula_t * FormulaHashIntoUniqueTable ( Ctlsp_Formula_t *  formula,
st_table *  uniqueTable 
) [static]

Function********************************************************************

Synopsis [Hashes the formula into the unique table.]

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

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

SeeAlso [FormulaCompare]

Definition at line 5375 of file ctlspUtil.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Variable Documentation

int changeBracket = 1 [static]

Definition at line 39 of file ctlspUtil.c.

int CtlspGlobalError

Definition at line 42 of file ctlspUtil.c.

Ctlsp_Formula_t* CtlspGlobalFormula

Definition at line 43 of file ctlspUtil.c.

st_table* CtlspMacroTable

Definition at line 44 of file ctlspUtil.c.

array_t* globalFormulaArray [static]

Variable********************************************************************

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

SeeAlso [Ctlsp_FormulaArrayFree]

Definition at line 38 of file ctlspUtil.c.

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

CFile***********************************************************************

FileName [ctlspUtil.c]

PackageName [ctlsp]

Synopsis [Routines for manipulating CTL* formulas.]

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

Author [Mohammad Awedh, Chao Wang]

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

Definition at line 25 of file ctlspUtil.c.