/**CFile*********************************************************************** FileName [ctlspUtil.c] PackageName [ctlsp] Synopsis [Routines for manipulating CTL* formulas.] Description [This file contains routines for accessing the fields of the CTL* formula data structure, for printing CTL* formulas, for reading CTL* formulas from a file, and for converting formulas to the existential form.] Author [Mohammad Awedh, Chao Wang] Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] ******************************************************************************/ #include "ctlspInt.h" #include "errno.h" #include "ntk.h" static char rcsid[] UNUSED = "$Id: ctlspUtil.c,v 1.64 2009/04/11 18:25:55 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /**Variable******************************************************************** Synopsis [Array of CTL* formulas (Ctlsp_Formula_t) read from a file.] SeeAlso [Ctlsp_FormulaArrayFree] ******************************************************************************/ static array_t *globalFormulaArray; static int changeBracket = 1; /* see ctlspInt.h for documentation */ int CtlspGlobalError; Ctlsp_Formula_t *CtlspGlobalFormula; st_table *CtlspMacroTable; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static Ctlsp_Formula_t * FormulaCreateWithType(Ctlsp_FormulaType type); static int FormulaCompare(const char *key1, const char *key2); static int FormulaHash(char *key, int modulus); static Ctlsp_Formula_t * FormulaHashIntoUniqueTable(Ctlsp_Formula_t *formula, st_table *uniqueTable); static Ctlsp_Formula_t * createSNFnode(Ctlsp_Formula_t *formula, array_t *formulaArray, int *index); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Parses a file containing a set of CTL* formulas.] Description [Parses a file containing a set of semicolon-ending CTL* formulas, and returns an array of Ctlsp_Formula_t representing those formulas. If an error is detected while parsing the file, the routine frees any allocated memory and returns NULL.] SideEffects [Manipulates the global variables globalFormulaArray, CtlspGlobalError and CtlspGlobalFormula.] SeeAlso [Ctlsp_FormulaArrayFree Ctlsp_FormulaPrint] ******************************************************************************/ array_t * Ctlsp_FileParseFormulaArray( FILE * fp) { st_generator *stGen; char *name; Ctlsp_Formula_t *formula; char *flagValue; /* * Initialize the global variables. */ globalFormulaArray = array_alloc(Ctlsp_Formula_t *, 0); CtlspGlobalError = 0; CtlspGlobalFormula = NIL(Ctlsp_Formula_t); CtlspMacroTable = st_init_table(strcmp,st_strhash); CtlspFileSetup(fp); /* * Check if changing "[] -> <>" is disabled. */ flagValue = Cmd_FlagReadByName("ctl_change_bracket"); if (flagValue != NIL(char)) { if (strcmp(flagValue, "yes") == 0) changeBracket = 1; else if (strcmp(flagValue, "no") == 0) changeBracket = 0; else { fprintf(vis_stderr, "** ctl error : invalid value %s for ctl_change_bracket[yes/no]. ***\n", flagValue); } } (void)CtlspYyparse(); st_foreach_item(CtlspMacroTable,stGen,&name, &formula){ FREE(name); CtlspFormulaFree(formula); } st_free_table(CtlspMacroTable); /* * Clean up if there was an error, otherwise return the array. */ if (CtlspGlobalError){ Ctlsp_FormulaArrayFree(globalFormulaArray); return NIL(array_t); } else { return globalFormulaArray; } } /**Function******************************************************************** Synopsis [Parses a file containing a set of CTL formulas.] Description [Parses a file containing a set of semicolon-terminated CTL formulae, and returns an array of Ctlp_Formula_t representing those formulae. If an error is detected while parsing the file, the routine frees any allocated memory and returns NULL.] SideEffects [Manipulates the global variables globalFormulaArray, CtlspGlobalError and CtlspGlobalFormula.] SeeAlso [Ctlsp_FileParseFormulaArray] ******************************************************************************/ array_t * Ctlsp_FileParseCTLFormulaArray( FILE *fp) { array_t *ctlsArray = Ctlsp_FileParseFormulaArray(fp); array_t *ctlArray; if (ctlsArray == NIL(array_t)) return NIL(array_t); ctlArray = Ctlsp_FormulaArrayConvertToCTL(ctlsArray); Ctlsp_FormulaArrayFree(ctlsArray); return ctlArray; } /* Ctlsp_FileParseCTLFormulaArray */ /**Function******************************************************************** Synopsis [Returns a character string represents the CTL* formula] Description [Returns formula as a character string. All subformulas are delimited by parenthesis. Does nothing if passed a NULL formula.] SideEffects [] ******************************************************************************/ char * Ctlsp_FormulaConvertToString( Ctlsp_Formula_t * formula) { char *s1 = NIL(char); char *s2 = NIL(char); char *tmpString = NIL(char); char *result; if (formula == NIL(Ctlsp_Formula_t)) { return NIL(char); } /* leaf node */ if (formula->type == Ctlsp_ID_c){ result = util_strcat3((char *)(formula->left), "=",(char *)(formula->right)); /* tmpString = util_strcat3("[", util_inttostr(formula->CTLclass),"]"); return util_strcat3(result, " ",tmpString); */ return result; } /* If the formula is a non-leaf, the function is called recursively */ s1 = Ctlsp_FormulaConvertToString(formula->left); s2 = Ctlsp_FormulaConvertToString(formula->right); switch(formula->type) { /* * The cases are listed in rough order of their expected frequency. */ case Ctlsp_OR_c: tmpString = util_strcat3(s1, " + ",s2); result = util_strcat3("(", tmpString, ")"); break; case Ctlsp_AND_c: tmpString = util_strcat3(s1, " * ", s2); result = util_strcat3("(", tmpString, ")"); break; case Ctlsp_THEN_c: tmpString = util_strcat3(s1, " -> ", s2); result = util_strcat3("(", tmpString, ")"); break; case Ctlsp_XOR_c: tmpString = util_strcat3(s1, " ^ ", s2); result = util_strcat3("(", tmpString, ")"); break; case Ctlsp_EQ_c: tmpString = util_strcat3(s1, " <-> ", s2); result = util_strcat3("(", tmpString, ")"); break; case Ctlsp_NOT_c: tmpString = util_strcat3("(", s1, ")"); result = util_strcat3("!", tmpString, ""); break; case Ctlsp_E_c: result = util_strcat3("E(", s1, ")"); FREE(s1); break; case Ctlsp_G_c: result = util_strcat3("G(", s1, ")"); break; case Ctlsp_F_c: result = util_strcat3("F(", s1, ")"); break; case Ctlsp_U_c: tmpString = util_strcat3("(", s1, " U "); result = util_strcat3(tmpString, s2, ")"); break; case Ctlsp_R_c: tmpString = util_strcat3("(", s1, " R "); result = util_strcat3(tmpString, s2, ")"); break; case Ctlsp_W_c: tmpString = util_strcat3("(", s1, " W "); result = util_strcat3(tmpString, s2, ")"); break; case Ctlsp_X_c: result = util_strcat3("X(", s1, ")"); break; case Ctlsp_A_c: result = util_strcat3("A(", s1, ")"); break;; case Ctlsp_TRUE_c: result = util_strsav("TRUE"); break; case Ctlsp_FALSE_c: result = util_strsav("FALSE"); break; case Ctlsp_Init_c: result = util_strsav("Init"); break; case Ctlsp_Cmp_c: if (formula->compareValue == 0) tmpString = util_strcat3("[", s1, "] = "); else tmpString = util_strcat3("[", s1, "] != "); result = util_strcat3(tmpString, s2, ""); break; case Ctlsp_Fwd_c: tmpString = util_strcat3("FwdG(", s1, ","); result = util_strcat3(tmpString, s2, ")"); break; /* case Ctlsp_EY_c: result = util_strcat3("EY(", s1, ")"); break;*/ default: fail("Unexpected type"); } if (s1 != NIL(char)) { FREE(s1); } if (s2 != NIL(char)) { FREE(s2); } if (tmpString != NIL(char)) { FREE(tmpString); } return result; } /**Function******************************************************************** Synopsis [Prints a formula to a file.] Description [Prints a formula to a file. All subformulas are delimited by parenthesis. The syntax used is the same as used by the CTL* parser. Does nothing if passed a NULL formula.] SideEffects [] ******************************************************************************/ void Ctlsp_FormulaPrint( FILE * fp, Ctlsp_Formula_t * formula) { char *tmpString; if (formula == NIL(Ctlsp_Formula_t)) { return; } tmpString = Ctlsp_FormulaConvertToString(formula); (void) fprintf(fp, "%s", tmpString); FREE(tmpString); } /**Function******************************************************************** Synopsis [Gets the type of a formula.] Description [Gets the type of a formula. See ctlsp.h for all the types. It is an error to call this function on a NULL formula.] SideEffects [] SeeAlso [ctlsp.h] ******************************************************************************/ Ctlsp_FormulaType Ctlsp_FormulaReadType( Ctlsp_Formula_t * formula) { return (formula->type); } /**Function******************************************************************** Synopsis [Gets the compare value of a formula.] Description [Gets the compare value of a formula. See ctlsp.h for all the types. It is an error to call this function on a NULL formula.] SideEffects [] SeeAlso [ctlsp.h] ******************************************************************************/ int Ctlsp_FormulaReadCompareValue( Ctlsp_Formula_t * formula) { int value; value = formula->compareValue; return (value); } /**Function******************************************************************** Synopsis [Reads the variable name of a leaf formula.] Description [Reads the variable name of a leaf formula. It is an error to call this function on a non-leaf formula.] SideEffects [] ******************************************************************************/ char * Ctlsp_FormulaReadVariableName( Ctlsp_Formula_t * formula) { if (formula->type != Ctlsp_ID_c){ fail("Ctlsp_FormulaReadVariableName() was called on a non-leaf formula."); } return ((char *)(formula->left)); } /**Function******************************************************************** Synopsis [Reads the value name of a leaf formula.] Description [Reads the value name of a leaf formula. It is an error to call this function on a non-leaf formula.] SideEffects [] ******************************************************************************/ char * Ctlsp_FormulaReadValueName( Ctlsp_Formula_t * formula) { if (formula->type != Ctlsp_ID_c){ fail("Ctlsp_FormulaReadValueName() was called on a non-leaf formula."); } return ((char *)(formula->right)); } /**Function******************************************************************** Synopsis [Gets the left child of a formula.] Description [Gets the left child of a formula. User must not free this formula. If a formula is a leaf formula, NIL(Ctlsp_Formula_t) is returned.] SideEffects [] SeeAlso [Ctlsp_FormulaReadRightChild] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_FormulaReadLeftChild( Ctlsp_Formula_t * formula) { if (formula->type != Ctlsp_ID_c){ return (formula->left); } return NIL(Ctlsp_Formula_t); } /**Function******************************************************************** Synopsis [Gets the right child of a formula.] Description [Gets the right child of a formula. User must not free this formula. If a formula is a leaf formula, NIL(Ctlsp_Formula_t) is returned.] SideEffects [] SeeAlso [Ctlsp_FormulaReadLeftChild] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_FormulaReadRightChild( Ctlsp_Formula_t * formula) { if (formula->type != Ctlsp_ID_c){ return (formula->right); } return NIL(Ctlsp_Formula_t); } /**Function******************************************************************** Synopsis [Gets a copy of the set of states for which this formula is true.] Description [Gets a copy of the MDD representing the set of states for which this formula is true. It is the user's responsibility to free this MDD. If the set of states has not yet been computed, then a NULL mdd_t is returned. It is an error to call this function on a NULL formula.] SideEffects [] SeeAlso [Ctlsp_FormulaSetStates] ******************************************************************************/ mdd_t * Ctlsp_FormulaObtainStates( Ctlsp_Formula_t * formula) { if (formula->states == NIL(mdd_t)) { return NIL(mdd_t); } else { return mdd_dup(formula->states); } } /**Function******************************************************************** Synopsis [Gets (a copy of) an approximation of the satisfying set] Description [Gets the required approximation of the satisfying set. If the exact set is available, it will return that. If neither is available, or approx is Ctlsp_Incomparable_c, it will return NULL.] SideEffects [] SeeAlso [Ctlsp_FormulaSetStates] ******************************************************************************/ mdd_t * Ctlsp_FormulaObtainApproxStates( Ctlsp_Formula_t *formula, Ctlsp_Approx_t approx) { if(approx == Ctlsp_Incomparable_c) return NIL(mdd_t); if (formula->states != NIL(mdd_t)) return mdd_dup(formula->states); if(approx == Ctlsp_Exact_c) return NIL(mdd_t); if(approx == Ctlsp_Overapprox_c){ if(formula->overapprox == NIL(mdd_t)) return NIL(mdd_t); else return mdd_dup(formula->overapprox); } if(approx == Ctlsp_Underapprox_c){ if(formula->underapprox == NIL(mdd_t)) return NIL(mdd_t); else return mdd_dup(formula->underapprox); } assert(0); /* we should never get here */ return NIL(mdd_t); } /**Function******************************************************************** Synopsis [Stores the set of states with the formula.] Description [Stores the MDD with the formula (a copy is not made, and hence, the caller should not later free this MDD). This MDD is intended to represent the set of states for which the formula is true. It is an error to call this function on a NULL formula.] SideEffects [] SeeAlso [Ctlsp_FormulaObtainStates] ******************************************************************************/ void Ctlsp_FormulaSetStates( Ctlsp_Formula_t * formula, mdd_t * states) { /* RB: added the next two lines. Given the Description, this was a bug */ if(formula->states != NIL(mdd_t)) mdd_free(formula->states); formula->states = states; } /**Function******************************************************************** Synopsis [Stores (an approximation of) the set of states with the formula.] Description [Sets the set of states or an under or overapproximation thereof, depending on the approx flag. If there is already an under or overapproximation, it is overwritten. If the exact set is given, the approx fields are cleared. Setting an incomparable approximation results in no action being taken. A copy of the bdd is not made, so the caller should not free it. ] SideEffects [] SeeAlso [Ctlsp_FormulaObtainStates] ******************************************************************************/ void Ctlsp_FormulaSetApproxStates( Ctlsp_Formula_t * formula, mdd_t * states, Ctlsp_Approx_t approx) { if(approx == Ctlsp_Incomparable_c){ mdd_free(states); return; } if(approx == Ctlsp_Exact_c){ if(formula->states != NIL(mdd_t)) mdd_free(formula->states); formula->states = states; if(formula->underapprox != NIL(mdd_t)){ mdd_free(formula->underapprox); formula->underapprox = NIL(mdd_t); } if(formula->overapprox != NIL(mdd_t)){ mdd_free(formula->overapprox); formula->overapprox = NIL(mdd_t); } } if( approx == Ctlsp_Underapprox_c){ /* you could perform a union instead, but typical use will have monotonically increasing underapproximations */ if(formula->underapprox != NIL(mdd_t)) mdd_free(formula->underapprox); formula->underapprox = states; } if( approx == Ctlsp_Overapprox_c){ /* you could perform an intersaection instead */ if(formula->overapprox != NIL(mdd_t)) mdd_free(formula->overapprox); formula->overapprox = states; } return; } /**Function******************************************************************** Synopsis [Sets the debug information of a formula.] Description [Sets the debug information of a CTL formula. The data is uninterpreted. FreeFn is a pointer to a function that takes a formula as input and returns void. FreeFn should free all the memory associated with the debug data; it is called when this formula is freed.] SideEffects [] SeeAlso [Ctlsp_FormulaReadDebugData] ******************************************************************************/ void Ctlsp_FormulaSetDbgInfo( Ctlsp_Formula_t * formula, void *data, Ctlsp_DbgInfoFreeFn freeFn) { formula->dbgInfo.data = data; formula->dbgInfo.freeFn = freeFn; } /**Function******************************************************************** Synopsis [Returns the debug data associated with a formula.] Description [Returns the debug data associated with a formula. This data is uninterpreted by the ctlsp package.] SideEffects [] SeeAlso [Ctlsp_FormulaSetDbgInfo] ******************************************************************************/ void * Ctlsp_FormulaReadDebugData( Ctlsp_Formula_t * formula) { return formula->dbgInfo.data; } /**Function******************************************************************** Synopsis [Returns TRUE if formula was converted, else FALSE.] from AX/AG/AU/AF] Description [Returns TRUE if formula was converted from a formula of type AG, AX, AU, AF, or EF via a call to Ctlsp_FormulaConvertToExistentialFormTree or Ctlsp_FormulaConvertToExistentialFormDAG. Otherwise, returns FALSE.] SideEffects [] ******************************************************************************/ boolean Ctlsp_FormulaTestIsConverted( Ctlsp_Formula_t * formula) { return formula->dbgInfo.convertedFlag; } /**Function******************************************************************** Synopsis [Returns TRUE if formula contains no path quantifiers.] Description [Test if a CTL* formula has any path quantifiers in it; if so return false, else true. For a CTL* formula, being quantifier-free and being propositional are not equivalent.] SideEffects [] ******************************************************************************/ boolean Ctlsp_FormulaTestIsQuantifierFree( Ctlsp_Formula_t *formula) { boolean lCheck; boolean rCheck; Ctlsp_Formula_t *leftChild; Ctlsp_Formula_t *rightChild; Ctlsp_FormulaType type; if ( formula == NIL( Ctlsp_Formula_t ) ) { return TRUE; } type = Ctlsp_FormulaReadType( formula ); if ( ( type == Ctlsp_ID_c ) || ( type == Ctlsp_TRUE_c ) || ( type == Ctlsp_FALSE_c ) ) { return TRUE; } if ( ( type == Ctlsp_E_c ) || ( type == Ctlsp_A_c ) ) { return FALSE; } leftChild = Ctlsp_FormulaReadLeftChild( formula ); lCheck = Ctlsp_FormulaTestIsQuantifierFree( leftChild ); if (lCheck == FALSE) return FALSE; rightChild = Ctlsp_FormulaReadRightChild( formula ); rCheck = Ctlsp_FormulaTestIsQuantifierFree( rightChild ); return rCheck; } /**Function******************************************************************** Synopsis [Returns original formula corresponding to converted formula.] SideEffects [] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_FormulaReadOriginalFormula( Ctlsp_Formula_t * formula) { return formula->dbgInfo.originalFormula; } /**Function******************************************************************** Synopsis [Returns the Alpha-Beta Index. used for LTL->AUT] SideEffects [] ******************************************************************************/ int Ctlsp_FormulaReadABIndex( Ctlsp_Formula_t * formula) { return formula->ab_idx; } /**Function******************************************************************** Synopsis [Set the Alpha-Beta Index. used for LTL->AUT] SideEffects [] ******************************************************************************/ void Ctlsp_FormulaSetABIndex( Ctlsp_Formula_t * formula, int ab_idx) { formula->ab_idx = ab_idx; } /**Function******************************************************************** Synopsis [Returns the Label Index. used for LTL->AUT] SideEffects [] ******************************************************************************/ int Ctlsp_FormulaReadLabelIndex( Ctlsp_Formula_t * formula) { return formula->label_idx; } /**Function******************************************************************** Synopsis [Set the Label Index. used for LTL->AUT] SideEffects [] ******************************************************************************/ void Ctlsp_FormulaSetLabelIndex( Ctlsp_Formula_t * formula, int label_idx) { formula->label_idx = label_idx; } /**Function******************************************************************** Synopsis [Returns the RHS. used for LTL->AUT] SideEffects [] ******************************************************************************/ char Ctlsp_FormulaReadRhs( Ctlsp_Formula_t * formula) { return formula->rhs; } /**Function******************************************************************** Synopsis [Set the RHS. used for LTL->AUT] SideEffects [] ******************************************************************************/ void Ctlsp_FormulaSetRhs( Ctlsp_Formula_t * formula) { formula->rhs = 1; } /**Function******************************************************************** Synopsis [Reset the RHS. used for LTL->AUT] SideEffects [] ******************************************************************************/ void Ctlsp_FormulaResetRhs( Ctlsp_Formula_t * formula) { formula->rhs = 0; } /**Function******************************************************************** Synopsis [Returns the marked. used for LTL->AUT] SideEffects [] ******************************************************************************/ char Ctlsp_FormulaReadMarked( Ctlsp_Formula_t * formula) { return formula->marked; } /**Function******************************************************************** Synopsis [Set the Alpha-Beta Index. used for LTL->AUT] SideEffects [] ******************************************************************************/ void Ctlsp_FormulaSetMarked( Ctlsp_Formula_t * formula) { formula->marked = 1; } /**Function******************************************************************** Synopsis [Reset the Alpha-Beta Index. used for LTL->AUT] SideEffects [] ******************************************************************************/ void Ctlsp_FormulaResetMarked( Ctlsp_Formula_t * formula) { formula->marked = 0; } /**Function******************************************************************** Synopsis [Frees a formula if no other formula refers to it as a sub-formula.] Description [The function decrements the refCount of the formula. As a consequence, if the refCount becomes 0, the formula is freed.] SideEffects [] SeeAlso [CtlspFormulaFree, CtlspDecrementRefCount] ******************************************************************************/ void Ctlsp_FormulaFree( Ctlsp_Formula_t *formula) { CtlspFormulaDecrementRefCount(formula); } /**Function******************************************************************** Synopsis [Recursively frees states, underapprox and overapprox fields of Ctlsp_Formula_t, and the debug data] Description [] SideEffects [] SeeAlso [Ctlsp_FormulaFree] ******************************************************************************/ void Ctlsp_FlushStates( Ctlsp_Formula_t * formula) { if (formula != NIL(Ctlsp_Formula_t)) { if (formula->type != Ctlsp_ID_c){ if (formula->left != NIL(Ctlsp_Formula_t)) { Ctlsp_FlushStates(formula->left); } if (formula->right != NIL(Ctlsp_Formula_t)) { Ctlsp_FlushStates(formula->right); } } if (formula->states != NIL(mdd_t)){ mdd_free(formula->states); formula->states = NIL(mdd_t); } if (formula->underapprox != NIL(mdd_t)){ mdd_free(formula->underapprox); formula->underapprox = NIL(mdd_t); } if (formula->overapprox != NIL(mdd_t)){ mdd_free(formula->overapprox); formula->overapprox = NIL(mdd_t); } if (formula->dbgInfo.data != NIL(void)){ (*formula->dbgInfo.freeFn)(formula); formula->dbgInfo.data = NIL(void); } } } /**Function******************************************************************** Synopsis [Duplicates a CTL* formula.] Description [Recursively duplicate a formula. Does nothing if the formula is NIL. Does not copy mdd for states, underapprox, overapprox, dbgInfo.] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_FormulaDup( Ctlsp_Formula_t * formula) { Ctlsp_Formula_t *result = NIL(Ctlsp_Formula_t); if ( formula == NIL(Ctlsp_Formula_t)) { return NIL(Ctlsp_Formula_t); } result = ALLOC(Ctlsp_Formula_t, 1); result->type = formula->type; result->class_ = formula->class_; result->CTLclass = formula->CTLclass; result->states = NIL(mdd_t); result->underapprox = NIL(mdd_t); result->overapprox = NIL(mdd_t); result->refCount = 1; result->dbgInfo.data = NIL(void); result->dbgInfo.freeFn = (Ctlsp_DbgInfoFreeFn) NULL; result->dbgInfo.convertedFlag = FALSE; result->dbgInfo.originalFormula = NIL(Ctlsp_Formula_t); if ( formula->type != Ctlsp_ID_c ) { result->left = Ctlsp_FormulaDup(formula->left); result->right = Ctlsp_FormulaDup(formula->right); } else { result->left = (Ctlsp_Formula_t *) util_strsav((char *)formula->left ); result->right = (Ctlsp_Formula_t *) util_strsav((char *)formula->right ); } return result; } /**Function******************************************************************** Synopsis [Frees an array of CTL* formulas.] Description [Calls CtlspFormulaDecrementRefCount on each formula in formulaArray, and then frees the array itself. It is okay to call this function with an empty array, but it is an error to call it with a NULL array.] SideEffects [] SeeAlso [Ctlsp_FormulaFree] ******************************************************************************/ void Ctlsp_FormulaArrayFree( array_t * formulaArray /* of Ctlsp_Formula_t */) { int i; int numFormulas = array_n(formulaArray); for (i = 0; i < numFormulas; i++) { Ctlsp_Formula_t *formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i); CtlspFormulaDecrementRefCount(formula); } array_free(formulaArray); } /**Function******************************************************************** Synopsis [Converts an array of CTL formulae to a multi-rooted DAG.] Description [The function hashes each subformula of a formula (including the formula itself) into a uniqueTable. It returns an array containing the roots of the multi-rooted DAG thus created by the sharing of the subformulae. It is okay to call this function with an empty array (in which case an empty array is returned), but it is an error to call it with a NULL array.] SideEffects [A formula in formulaArray might be freed if it had been encountered as a subformula of some other formula. Other formulae in formulaArray might be present in the returned array. Therefore, the formulae in formulaArray should not be freed. Only formulaArray itself should be freed. RB: What does that mean? I understand this as follows. Copies of the formulae are not made, but rather pointers to the argument subformulae are kept. Hence, not only should the formulae in the result not be freed, but also you cannot free the argument before you are done with the result. Furthermore, by invocation of this function, the argument gets altered. It is still valid, but pointers may have changed. Is this correct? RB rewrite: A formula in formulaArray is freed if it is encountered as a subformula of some other formula. Other formulae in formulaArray might be present in the returned array. Therefore, the formulae in formulaArray should not be freed. Only formulaArray itself should be freed.] SeeAlso [] ******************************************************************************/ array_t * Ctlsp_FormulaArrayConvertToDAG( array_t *formulaArray) { int i; Ctlsp_Formula_t *formula, *uniqueFormula; st_table *uniqueTable = st_init_table(FormulaCompare, FormulaHash); int numFormulae = array_n(formulaArray); array_t *rootsOfFormulaDAG = array_alloc(Ctlsp_Formula_t *, numFormulae); for(i=0; i < numFormulae; i++) { formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i); uniqueFormula = FormulaHashIntoUniqueTable(formula, uniqueTable); if(uniqueFormula != formula) { CtlspFormulaDecrementRefCount(formula); CtlspFormulaIncrementRefCount(uniqueFormula); array_insert(Ctlsp_Formula_t *, rootsOfFormulaDAG, i, uniqueFormula); } else array_insert(Ctlsp_Formula_t *, rootsOfFormulaDAG, i, formula); } st_free_table(uniqueTable); return rootsOfFormulaDAG; } /**Function******************************************************************** Synopsis [Creates a CTL formula with the specified fields.] Description [Allocates a Ctlsp_Formula_t, and sets the 2 fields given as arguments. If the type is Ctlsp_ID_c, then the left and right fields should contain a pointer to a variable name and a pointer to a value respectively. Otherwise, the two fields point to subformulas. refCount is set to 1. The states field is set to NULL, the converted flag is set to FALSE, and the originalFormula field is set to NULL.] Comment [] SideEffects [] SeeAlso [CtlspFormulaDecrementRefCount] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_FormulaCreate( Ctlsp_FormulaType type, void * left_, void * right_) { Ctlsp_Formula_t *formula = ALLOC(Ctlsp_Formula_t, 1); Ctlsp_Formula_t *left = (Ctlsp_Formula_t *) left_; Ctlsp_Formula_t *right = (Ctlsp_Formula_t *) right_; formula->type = type; formula->left = left; formula->right = right; formula->states = NIL(mdd_t); formula->underapprox = NIL(mdd_t); formula->overapprox = NIL(mdd_t); formula->refCount = 1; formula->dbgInfo.data = NIL(void); formula->dbgInfo.freeFn = (Ctlsp_DbgInfoFreeFn) NULL; formula->dbgInfo.convertedFlag = FALSE; formula->dbgInfo.originalFormula = NIL(Ctlsp_Formula_t); formula->top = 0; formula->compareValue = 0; formula->class_ = Ctlsp_propformula_c; formula->CTLclass = Ctlsp_CTL_c; formula->rhs = 0; if (left == NIL(Ctlsp_Formula_t)){ return formula; } switch(formula->type) { case Ctlsp_OR_c: case Ctlsp_AND_c: case Ctlsp_THEN_c: case Ctlsp_XOR_c: case Ctlsp_EQ_c: Ctlsp_FormulaSetClass(formula, table1(Ctlsp_FormulaReadClass(left),Ctlsp_FormulaReadClass(right))); if ((Ctlsp_FormulaReadClassOfCTL(left) == Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL(right) == Ctlsp_CTL_c)){ Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_CTL_c); } else { Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_NotCTL_c); } break; case Ctlsp_NOT_c: Ctlsp_FormulaSetClass(formula, Ctlsp_FormulaReadClass(left)); Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_FormulaReadClassOfCTL(left)); break; case Ctlsp_E_c: case Ctlsp_A_c: Ctlsp_FormulaSetClass(formula, Ctlsp_stateformula_c); if (Ctlsp_FormulaReadClassOfCTL(left) == Ctlsp_PathCTL_c) { Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_CTL_c); } else { Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_NotCTL_c); } break; case Ctlsp_G_c: case Ctlsp_F_c: Ctlsp_FormulaSetClass(formula, table2(Ctlsp_FormulaReadClass(left))); if (Ctlsp_FormulaReadClassOfCTL(left) == Ctlsp_CTL_c){ Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_PathCTL_c); } else { Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_NotCTL_c); } break; case Ctlsp_U_c: case Ctlsp_R_c: case Ctlsp_W_c: Ctlsp_FormulaSetClass(formula, table3(Ctlsp_FormulaReadClass(left),Ctlsp_FormulaReadClass(right))); if ((Ctlsp_FormulaReadClassOfCTL(left) == Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL(right) == Ctlsp_CTL_c)) { Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_PathCTL_c); } else { Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_NotCTL_c); } break; case Ctlsp_X_c: Ctlsp_FormulaSetClass(formula, table2(Ctlsp_FormulaReadClass(left))); if (Ctlsp_FormulaReadClassOfCTL(left) == Ctlsp_CTL_c){ Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_PathCTL_c); } else { Ctlsp_FormulaSetClassOfCTL(formula, Ctlsp_NotCTL_c); } break; default: break; } return formula; } /**Function******************************************************************** Synopsis [Creates a CTL* formula with disjunction of atomic propositions] Description [This function returns Ctlsp_Formula_t for name = {v1,v2,...}. In case of failure, a NULL pointer is returned.] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_FormulaCreateOr( char *name, char *valueStr) { Ctlsp_Formula_t *formula, *tempFormula; char *preStr; preStr = strtok(valueStr,","); formula = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(name), util_strsav(preStr)); if (formula == NIL(Ctlsp_Formula_t)) { return NIL(Ctlsp_Formula_t); } while ((preStr = strtok(NIL(char),",")) != NIL(char)) { tempFormula = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(name), util_strsav(preStr)); if (tempFormula == NIL(Ctlsp_Formula_t)) { Ctlsp_FormulaFree(formula); return NIL(Ctlsp_Formula_t); } formula = Ctlsp_FormulaCreate(Ctlsp_OR_c,formula,tempFormula); } return formula; } /**Function******************************************************************** Synopsis [Creates a CTL* formula with conjunction of atomic propositions] Description [This function returns Ctlsp_Formula_t for nameVector = value, nameVector is a form of var[i:j] or var and value is any integer n or binary string starting with 'b' or 'x', for instance, b0011 or x100. If n does not fit in var[i:j] or the size of the binary string is not matched with var[i:j], NULL pointer is returned] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_FormulaCreateVectorAnd( char *nameVector, char *value) { Ctlsp_Formula_t *formula, *tempFormula; int startValue, endValue, inc, i,j, interval,startInd; char *binValueStr, *varName, *name; char *bitValue; varName = CtlspGetVectorInfoFromStr(nameVector,&startValue,&endValue,&interval,&inc); binValueStr = ALLOC(char,interval+1); if (!CtlspStringChangeValueStrToBinString(value,binValueStr,interval) ){ FREE(varName); FREE(binValueStr); return NIL(Ctlsp_Formula_t); } name = ALLOC(char,MAX_LENGTH_OF_VAR_NAME); (void) sprintf(name,"%s[%d]",varName,startValue); (void) CtlspChangeBracket(name); bitValue = ALLOC(char,2); bitValue[0] = binValueStr[0]; bitValue[1] = '\0'; formula = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(name), util_strsav(bitValue)); j = 0; startInd = startValue; for(i=startValue;i!=endValue;i=i+inc){ startInd += inc; j++; (void) sprintf(name,"%s[%d]",varName,startInd); (void) CtlspChangeBracket(name); bitValue[0] = binValueStr[j]; tempFormula = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(name), util_strsav(bitValue)); formula = Ctlsp_FormulaCreate(Ctlsp_AND_c,formula,tempFormula); } FREE(varName); FREE(name); FREE(binValueStr); FREE(bitValue); return formula; } /**Function******************************************************************** Synopsis [Creates a CTL formula with OR of Vector AND] Description [This function returns Ctlsp_Formula_t for nameVector = valueStr, nameVector is a form of var[i:j] or var, valueStr is "k,l,...,q", and k,l,...,q is either integer or binary string. Binary string starting with 'b', for instance, b0011. If n is not fitted in var[i:j] or size of binary string is not matched with var[i:j], NULL pointer is returned] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_FormulaCreateVectorOr( char *nameVector, char *valueStr) { Ctlsp_Formula_t *formula,*tempFormula; char *preStr; preStr = strtok(valueStr,","); formula = Ctlsp_FormulaCreateVectorAnd(nameVector,preStr); if ( formula == NIL(Ctlsp_Formula_t)){ Ctlsp_FormulaFree(formula); return NIL(Ctlsp_Formula_t); } while( (preStr = strtok(NIL(char),",")) != NIL(char) ){ tempFormula = Ctlsp_FormulaCreateVectorAnd(nameVector,preStr); if ( tempFormula == NIL(Ctlsp_Formula_t)){ Ctlsp_FormulaFree(formula); return NIL(Ctlsp_Formula_t); } formula = Ctlsp_FormulaCreate(Ctlsp_OR_c,formula,tempFormula); } return formula; } /**Function******************************************************************** Synopsis [Creates a CTL formula for equivalent property] Description [This function assumes that each child is defined in binary domain. Enumerate type is not supported] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_FormulaCreateEquiv( char *left, char *right) { Ctlsp_Formula_t *formula,*formula1,*formula2; char *one; char *zero; one = "1"; zero = "0"; formula1 = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(left), util_strsav(one)); formula2 = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(right), util_strsav(zero)); formula = Ctlsp_FormulaCreate(Ctlsp_XOR_c,formula1,formula2); return formula; } /**Function******************************************************************** Synopsis [Creates a CTL formula for equivalent of vector] Description [This function returns a formula, which is the AND of a bitwise equivalence] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_FormulaCreateVectorEquiv( char *left, char *right) { Ctlsp_Formula_t *formula,*tempFormula; char *leftName,*rightName; char *leftVar, *rightVar; int leftStart,leftEnd,rightStart,rightEnd,leftInterval,rightInterval; int leftInc,rightInc,leftInd,rightInd,i; leftName = CtlspGetVectorInfoFromStr(left,&leftStart,&leftEnd,&leftInterval,&leftInc); rightName = CtlspGetVectorInfoFromStr(right,&rightStart,&rightEnd,&rightInterval,&rightInc); if (leftInterval != rightInterval){ return NIL(Ctlsp_Formula_t); } leftVar = ALLOC(char,MAX_LENGTH_OF_VAR_NAME); (void) sprintf(leftVar,"%s[%d]",leftName,leftStart); (void) CtlspChangeBracket(leftVar); rightVar = ALLOC(char,MAX_LENGTH_OF_VAR_NAME); (void) sprintf(rightVar,"%s[%d]",rightName,rightStart); (void) CtlspChangeBracket(rightVar); formula = Ctlsp_FormulaCreateEquiv(leftVar,rightVar); leftInd = leftStart; rightInd = rightStart; for(i=leftStart;i!=leftEnd;i+=leftInc){ leftInd += leftInc; rightInd += rightInc; (void) sprintf(leftVar,"%s[%d]",leftName,leftInd); (void) CtlspChangeBracket(leftVar); (void) sprintf(rightVar,"%s[%d]",rightName,rightInd); (void) CtlspChangeBracket(rightVar); tempFormula = Ctlsp_FormulaCreateEquiv(leftVar,rightVar); formula = Ctlsp_FormulaCreate(Ctlsp_AND_c,formula,tempFormula); } FREE(leftName); FREE(rightName); FREE(leftVar); FREE(rightVar); return formula; } /**Function******************************************************************** Synopsis [Creates a CTL formula for multiple X] Description [This function returns a formula, which is the multiple times of AX. The given string includes the number of depth] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_FormulaCreateXMult( char *string, Ctlsp_Formula_t *formula) { int i,num; char *str, *ptr; Ctlsp_Formula_t *result = NIL(Ctlsp_Formula_t); str = strchr(string,':'); if ( str == NULL) return(NIL(Ctlsp_Formula_t)); str++; num = strtol(str,&ptr,0); for(i=0;itype) { /* * The cases are listed in rough order of their expected frequency. */ case Ctlsp_ID_c: result = util_strsav("ID"); break; case Ctlsp_OR_c: result = util_strsav("OR"); break; case Ctlsp_AND_c: result = util_strsav("AND"); break; case Ctlsp_THEN_c: result = util_strsav("THEN"); break; case Ctlsp_XOR_c: result = util_strsav("XOR"); break; case Ctlsp_EQ_c: result = util_strsav("EQ"); break; case Ctlsp_NOT_c: result = util_strsav("NOT"); break; case Ctlsp_E_c: result = util_strsav("E"); break; case Ctlsp_G_c: result = util_strsav("G"); break; case Ctlsp_F_c: result = util_strsav("F"); break; case Ctlsp_U_c: result = util_strsav("U"); break; case Ctlsp_R_c: result = util_strsav("R"); break; case Ctlsp_W_c: result = util_strsav("W"); break; case Ctlsp_X_c: result = util_strsav("X"); break; case Ctlsp_A_c: result = util_strsav("A"); break; case Ctlsp_TRUE_c: result = util_strsav("TRUE"); break; case Ctlsp_FALSE_c: result = util_strsav("FALSE"); break; case Ctlsp_Init_c: result = util_strsav("Init"); break; case Ctlsp_Cmp_c: result = util_strsav("Cmp"); break; case Ctlsp_Fwd_c: result = util_strsav("Fwd"); break; /* case Ctlsp_EY_c: result = util_strsav("EY"); break;*/ /* case Ctlsp_EH_c: result = util_strsav("EH"); break; break;*/ default: fail("Unexpected type"); } return(result); } /**Function******************************************************************** Synopsis [Tests if a formula is a ACTL, ECTL or mixed formula.] Description [Tests if a formula is a ACTL, ECTL or mixed formula. '0' for ECTL, '1' for ACTL and '2' for a mixed formula. If a formula doesn't have any path quantifier, '3' is returned.] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_FormulaClass Ctlsp_CheckClassOfExistentialFormula( Ctlsp_Formula_t *formula) { Ctlsp_FormulaClass result; result = CtlspCheckClassOfExistentialFormulaRecur(formula, FALSE); return result; } /* End of Ctlsp_CheckTypeOfExistentialFormula */ /**Function******************************************************************** Synopsis [Tests if an array of simple existential formulae has only ACTL, only ECTL or mixture of formula.] Description [Returns Ctlsp_ECTL_c if the array contains only ECTL formulae, Ctlsp_ACTL_c if it contains only ACTL formulae, Ctlsp_QuantifierFree_c if there are no quantifiers in any formulae, and Ctlsp_Mixed otherwise.] SideEffects [] SeeAlso [Ctlsp_CheckClassOfExistentialFormula] ******************************************************************************/ Ctlsp_FormulaClass Ctlsp_CheckClassOfExistentialFormulaArray( array_t *formulaArray) { Ctlsp_FormulaClass result; Ctlsp_Formula_t *formula; int formulanr; result = Ctlsp_QuantifierFree_c; arrayForEachItem(Ctlsp_Formula_t *, formulaArray, formulanr, formula){ Ctlsp_FormulaClass formulaType; formulaType = Ctlsp_CheckClassOfExistentialFormula(formula); result = CtlspResolveClass(result, formulaType); if(result == Ctlsp_Mixed_c) return result; } return result; } /* End of Ctlsp_CheckTypeOfExistentialFormulaArray */ /**Function******************************************************************** Synopsis [Get the class of a formula] Description [Get the current class of a CTL* sub-formula] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_ClassOfFormula Ctlsp_FormulaReadClass(Ctlsp_Formula_t *formula) { return formula->class_; } /**Function******************************************************************** Synopsis [Set the class of a formula] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void Ctlsp_FormulaSetClass(Ctlsp_Formula_t *formula, Ctlsp_ClassOfFormula newClass) { if (formula == NIL(Ctlsp_Formula_t)){ return; } formula->class_ = newClass; } /**Function******************************************************************** Synopsis [Get the type of a CTL formula] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_ClassOfCTLFormula Ctlsp_FormulaReadClassOfCTL(Ctlsp_Formula_t *formula) { return formula->CTLclass; } /**Function******************************************************************** Synopsis [Set the class of CTL] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void Ctlsp_FormulaSetClassOfCTL( Ctlsp_Formula_t *formula, Ctlsp_ClassOfCTLFormula newCTLclass) { if (formula == NIL(Ctlsp_Formula_t)){ return; } formula->CTLclass = newCTLclass; } /**Function******************************************************************** Synopsis [Returns an array of LTL formulae.] Description [Returns an array of LTL formulae given the array of CTL* formulae. If any of the CTL* formula is not LTL formula, retuns NIL. The return LTL formulae share absolutely nothing with the original CTL* formulae (not even a string).] SideEffects [] SeeAlso [] ******************************************************************************/ array_t * Ctlsp_FormulaArrayConvertToLTL( array_t *formulaArray) { array_t *ltlFormulaArray; int i; ltlFormulaArray = array_alloc(Ctlsp_Formula_t *, 0); /* Check if all CTL* formulas are LTL formulas */ for (i = 0; i < array_n(formulaArray); i++) { Ctlsp_Formula_t *formula, *ltlFormula; formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i); if (!Ctlsp_isLtlFormula(formula)){ Ctlsp_FormulaArrayFree(ltlFormulaArray); return NIL(array_t); } ltlFormula = Ctlsp_FormulaDup(formula); array_insert_last(Ctlsp_Formula_t *, ltlFormulaArray, ltlFormula); } /* For Loop */ return ltlFormulaArray; } /* Ctlsp_FormulaArrayConvertToLTL() */ /**Function******************************************************************** Synopsis [Returns an array of CTL formulas from the parsed array of CTL* formulas] Description [This function takes an array of CTL* formulae and returns an array of CTL formulae if applicable. Function returns NIL if any CTL * formula can't be converted to CTL formula. The returned CTL formulae share absolutely nothing with the original CTL* formulae (not even a string).] SideEffects [] SeeAlso [Ctlsp_FormulaConvertToCTL] ******************************************************************************/ array_t * Ctlsp_FormulaArrayConvertToCTL( array_t *formulaArray) { array_t *CtlFormulaArray; int i; CtlFormulaArray = array_alloc(Ctlp_Formula_t *, 0); /* Convert each formula in the array to CTL */ for (i = 0; i < array_n(formulaArray); i++) { Ctlsp_Formula_t *formula; Ctlp_Formula_t *newFormula; formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i); newFormula = Ctlsp_FormulaConvertToCTL(formula); if (newFormula != NIL(Ctlp_Formula_t)){ array_insert_last(Ctlp_Formula_t *, CtlFormulaArray, newFormula); } else{ (void) fprintf(vis_stderr, "** ctl* error : Can't Convert CTL* No. %d to CTL formula\n\n", i); Ctlp_FormulaArrayFree(CtlFormulaArray); return NIL(array_t); } } /* For Loop */ return CtlFormulaArray; } /* Ctlsp_FormulaArrayConvertToCTL() */ /**Function******************************************************************** Synopsis [Convert an CTL* formula to CTL formula] Description [This function takes a formula in CTL* and returns a CTL formula if applicable. CTL* consists of two formula classes: state formulas and path formulas. CTL formula is a state formula. CTL* formula can be converted to CTL formula if the CTL* formula is state formula. Note: This function must be called for each formula in a given array.] SideEffects [] SeeAlso [Ctlsp_FormulaArrayConvertToCTL] ******************************************************************************/ Ctlp_Formula_t * Ctlsp_FormulaConvertToCTL( Ctlsp_Formula_t *formula) { if (Ctlsp_FormulaReadClassOfCTL(formula) == Ctlsp_CTL_c) {/* CTL* can be converted to CTL */ return CtlspFormulaConvertToCTL(formula); } else{ return NIL(Ctlp_Formula_t); } } /* Ctlsp_FormulaConvertToCTL() */ /**Function******************************************************************** Synopsis [Convert a propositional CTL* formula to CTL formula] Description [A wrapper to CtlspFormulaConvertToCTL] SideEffects [] SeeAlso [Ctlsp_FormulaArrayConvertToCTL] ******************************************************************************/ Ctlp_Formula_t * Ctlsp_PropositionalFormulaToCTL( Ctlsp_Formula_t *formula) { return CtlspFormulaConvertToCTL(formula); } /**Function******************************************************************** Synopsis [Return true if CTL* formula is a propositional formula.] Description [] SideEffects [] SeeAlso [Ctlsp_FormulaReadClass()] ******************************************************************************/ int Ctlsp_isPropositionalFormula( Ctlsp_Formula_t *formula) { return (Ctlsp_FormulaReadClass(formula) == Ctlsp_propformula_c); } /* Ctlsp_isPropositionalFormula() */ /**Function******************************************************************** Synopsis [Return true if CTL* formula is an CTL formula.] Description [] SideEffects [] SeeAlso [Ctlsp_FormulaReadClassOfCTL()] ******************************************************************************/ int Ctlsp_isCtlFormula( Ctlsp_Formula_t *formula) { return (Ctlsp_FormulaReadClassOfCTL(formula) == Ctlsp_CTL_c); } /* Ctlsp_isCtlFormula() */ /**Function******************************************************************** Synopsis [Return true if CTL* formula is an LTL formula.] Description [a formula is LTL formul if its one of the following: - Its class is Ctlsp_LTLformula_c - it is in the form A(Ctlsp_LTLformula_c). - Its class is Ctlsp_propformula_c. - it is in the form A(Ctlsp_propformula_c) ] SideEffects [] SeeAlso [Ctlsp_FormulaReadClass()] ******************************************************************************/ int Ctlsp_isLtlFormula( Ctlsp_Formula_t *formula) { if (Ctlsp_FormulaReadClass(formula) == Ctlsp_LTLformula_c){ return 1; } if (Ctlsp_FormulaReadClass(formula) == Ctlsp_propformula_c){ return 1; } if (formula->type == Ctlsp_A_c) { if ((Ctlsp_FormulaReadClass(formula->left) == Ctlsp_LTLformula_c) || (Ctlsp_FormulaReadClass(formula->left) == Ctlsp_propformula_c)) { return 1; } else { return 0; } } return 0; } /* Ctlsp_isLtlFormula() */ /**Function******************************************************************** Synopsis [Negate an LTL formula] Description [This function returns an abbreviation-free LTL formula of the negation of the input LTL formula. The returned formula share absolutely nothing with the input LTL formula.] Comment [] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_LtllFormulaNegate( Ctlsp_Formula_t *ltlFormula) { Ctlsp_Formula_t *negLtlFormula, *tmpLtlFormula; negLtlFormula = Ctlsp_FormulaCreate(Ctlsp_NOT_c, ltlFormula, NIL(Ctlsp_Formula_t)); tmpLtlFormula = Ctlsp_LtlFormulaExpandAbbreviation(negLtlFormula); FREE(negLtlFormula); negLtlFormula = Ctlsp_LtlFormulaNegationNormalForm(tmpLtlFormula); if(negLtlFormula != tmpLtlFormula) { Ctlsp_FormulaFree(tmpLtlFormula); } tmpLtlFormula = Ctlsp_LtlFormulaSimpleRewriting(negLtlFormula); Ctlsp_FormulaFree(negLtlFormula); Ctlsp_LtlSetClass(tmpLtlFormula); return tmpLtlFormula; } /* Ctlsp_LtllFormulaNegate() */ /**Function******************************************************************** Synopsis [Set the class of the LTL formula] Description [This function recursively sets the class of LTL subformula. For leave nodes, by default the class sets to Ctlsp_propformula_c when the node is created.] Comment [The class filed of an LTL subformula will not be set if the programmer uses FormulaCreateWithType() and then later he adds its children. The correct way of creating a new node knowing its childeren is by using Ctlsp_FormulaCreate()] SideEffects [] SeeAlso [ctlspInt.h Ctlsp_FormulaCreate] ******************************************************************************/ void Ctlsp_LtlSetClass( Ctlsp_Formula_t *formula) { Ctlsp_Formula_t *left, *right; if (formula == NIL(Ctlsp_Formula_t)){ return; } if (formula->type == Ctlsp_ID_c){ return; } if (formula->type == Ctlsp_TRUE_c){ return; } if (formula->type == Ctlsp_FALSE_c){ return; } left = formula->left; right = formula->right; Ctlsp_LtlSetClass(left); Ctlsp_LtlSetClass(right); switch(formula->type) { case Ctlsp_OR_c: case Ctlsp_AND_c: case Ctlsp_THEN_c: case Ctlsp_XOR_c: case Ctlsp_EQ_c: Ctlsp_FormulaSetClass(formula, table1(Ctlsp_FormulaReadClass(left),Ctlsp_FormulaReadClass(right))); break; case Ctlsp_NOT_c: Ctlsp_FormulaSetClass(formula, Ctlsp_FormulaReadClass(left)); break; case Ctlsp_E_c: case Ctlsp_A_c: Ctlsp_FormulaSetClass(formula, Ctlsp_stateformula_c); break; case Ctlsp_G_c: case Ctlsp_F_c: Ctlsp_FormulaSetClass(formula, table2(Ctlsp_FormulaReadClass(left))); break; case Ctlsp_U_c: case Ctlsp_R_c: case Ctlsp_W_c: Ctlsp_FormulaSetClass(formula, table3(Ctlsp_FormulaReadClass(left),Ctlsp_FormulaReadClass(right))); break; case Ctlsp_X_c: Ctlsp_FormulaSetClass(formula, table2(Ctlsp_FormulaReadClass(left))); break; default: break; } return; } /**Function******************************************************************** Synopsis [Return TRUE iff formula is a "GF(propositional formula)".] Description [GFp = FALSE R (TRUE U p) in abbreviation-free LTL formulae.] SideEffects [] SeeAlso [] ******************************************************************************/ int Ctlsp_LtlFormulaIsGFp( Ctlsp_Formula_t *formula) { Ctlsp_Formula_t *rightChild; Ctlsp_Formula_t *leftChild; assert(formula != NIL(Ctlsp_Formula_t)); if (Ctlsp_FormulaReadType(formula) == Ctlsp_R_c) { rightChild = Ctlsp_FormulaReadRightChild(formula); leftChild = Ctlsp_FormulaReadLeftChild(formula); if ((Ctlsp_FormulaReadType(leftChild) == Ctlsp_FALSE_c) && (Ctlsp_FormulaReadType(rightChild) == Ctlsp_U_c)){ if ((Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(rightChild)) == Ctlsp_TRUE_c) && (Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadRightChild(rightChild)))) { return TRUE; } } } return FALSE; }/* Ctlsp_LtlFormulaIsGFp() */ /**Function******************************************************************** Synopsis [Return TRUE iff formula is a "G(propositional formula)".] Description [G(p) = FALSE R p in abbreviation-free LTL formulae.] SideEffects [] SeeAlso [Ctlsp_isPropositionalFormula] ******************************************************************************/ boolean Ctlsp_LtlFormulaIsGp( Ctlsp_Formula_t *formula) { assert(formula != NIL(Ctlsp_Formula_t)); if ((Ctlsp_FormulaReadType(formula)== Ctlsp_G_c) && Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadLeftChild(formula))){ return TRUE; } if (Ctlsp_FormulaReadType(formula) == Ctlsp_R_c) { if ((Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(formula)) == Ctlsp_FALSE_c) && (Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadRightChild(formula)))) { return TRUE; } } return FALSE; } /* Ctlsp_LtlFormulaIsGp */ /**Function******************************************************************** Synopsis [Return TRUE iff formula is a "F(propositional formula)".] Description [F(p) = TRUE U p in abbreviation-free LTL formulae.] SideEffects [] SeeAlso [Ctlsp_isPropositionalFormula] ******************************************************************************/ boolean Ctlsp_LtlFormulaIsFp( Ctlsp_Formula_t *formula) { assert(formula != NIL(Ctlsp_Formula_t)); if ((Ctlsp_FormulaReadType(formula)== Ctlsp_F_c) && Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadLeftChild(formula))){ return TRUE; } if (Ctlsp_FormulaReadType(formula) == Ctlsp_U_c) { if ((Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(formula)) == Ctlsp_TRUE_c) && Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadRightChild(formula))) { return TRUE; } } return FALSE; } /* Ctlsp_LtlFormulaIsFp */ #if 0 /**Function******************************************************************** Synopsis [Return TRUE iff formula is a safety property.] Description [ The characterization of LTL formula as a safety formula is taken from the paper by A. Prasad Sistla: Safety, Liveness and Fairness in Temporal Logic. Theorm 3.1 page 8: (For positive LTL formula: formula in Negation Normal Form). - Every propositional formula is a safety formula. - If f, g are safety formula, then so are - f AND g. - f OR g. - X(f). - f W g. (unless temporal operator). - G(f). This function can only be applied to abbreviation-free LTL formulae. The formula must be in Negation Normal Form.] SideEffects [] SeeAlso [] ******************************************************************************/ boolean Ctlsp_LtlFormulaIsSafety( Ctlsp_Formula_t *formula) { assert(formula != NIL(Ctlsp_Formula_t)); if (Ctlsp_isPropositionalFormula(formula)){ return TRUE; } if (Ctlsp_LtlFormulaIsW(formula)){ return Ctlsp_LtlFormulaIsSafety(Ctlsp_FormulaReadLeftChild(formula)) && Ctlsp_LtlFormulaIsSafety(Ctlsp_FormulaReadRightChild(formula)); } swtich (Ctlsp_FormulaReadType(formula)){ case Ctlsp_AND_c: case Ctlsp_OR_c: return Ctlsp_LtlFormulaIsSafety(Ctlsp_FormulaReadLeftChild(formula)) && Ctlsp_LtlFormulaIsSafety(Ctlsp_FormulaReadRightChild(formula)); case Ctlsp_X_c: return Ctlsp_LtlFormulaIsSafety(Ctlsp_FormulaReadLeftChild(formula)); case Ctlsp_NOT_c: case Ctlsp_U_c: case Ctlsp_R_c: return FALSE; default: fail("unexpected node type in abbreviation-free formula\n"); return FALSE; /* not reached */ } /* == Ctlsp_F_c) && Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadLeftChild(formula))){ return TRUE; } */ if (Ctlsp_FormulaReadType(formula) == Ctlsp_U_c) { if (Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(formula) == Ctlsp_TRUE_c) && Ctlsp_isPropositionalFormula(Ctlsp_FormulaReadRightChild(formula))) { return TRUE; } } return FALSE; } /* Ctlsp_LtlFormulaIsSafety */ #endif /**Function******************************************************************** Synopsis [Add fairness constraints to an array of LTL formulae.] Description [This function modifies an array of LTL formulae by adding to each of them a fairness constraint. This fairness constraint is the conjunction of all fairness constraints in constraintArray. For consistency with what done throughout VIS, each line in the file is interpreted as a condition that must hold infinitely often. The function assumes that the incoming array only contains LTL formulae. The returned formulae are not normalized and not converted to DAGs.] SideEffects [formulaArray is modified] SeeAlso [] ******************************************************************************/ void Ctlsp_FormulaArrayAddLtlFairnessConstraints( array_t *formulaArray /* array of LTL formulae */, array_t *constraintArray /* array of fairness constraints */) { Ctlsp_Formula_t *formula; /* a generic LTL formula */ Ctlsp_Formula_t *fairness; /* a generic fairness constraint */ int i; /* iteration variable */ assert(formulaArray != NIL(array_t)); assert(constraintArray != NIL(array_t)); /* * Create the overall fairness constraints. If the given constraints * are C_1, C_2, ..., C_k, build the formula /\_i GF C_i. */ fairness = NIL(Ctlsp_Formula_t); arrayForEachItem(Ctlsp_Formula_t *, constraintArray, i, formula) { Ctlsp_Formula_t *finally; Ctlsp_Formula_t *globally; finally = Ctlsp_FormulaCreate(Ctlsp_F_c, formula, NIL(Ctlsp_Formula_t)); globally = Ctlsp_FormulaCreate(Ctlsp_G_c, finally, NIL(Ctlsp_Formula_t)); if (i == 0) { fairness = globally; } else { fairness = Ctlsp_FormulaCreate(Ctlsp_AND_c, fairness, globally); } } /* Empty fairness constraint files are forbidden. */ assert(fairness != NIL(Ctlsp_Formula_t)); /* * Add fairness to each given formula: Replace f_i by (fairness -> f_i). */ arrayForEachItem(Ctlsp_Formula_t *, formulaArray, i, formula) { Ctlsp_Formula_t *modified; modified = Ctlsp_FormulaCreate(Ctlsp_THEN_c, Ctlsp_FormulaDup(fairness), formula); array_insert(Ctlsp_Formula_t *, formulaArray, i, modified); } Ctlsp_FormulaFree(fairness); } /* Ctlsp_FormulaArrayAddLtlFairnessConstraints */ /**Function******************************************************************** Synopsis [Translate a CTL formula into a CTL* formula.] Description [Translate a CTL formula into a CTL* formula.] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_CtlFormulaToCtlsp(Ctlp_Formula_t *F) { Ctlsp_Formula_t *Fsp; Ctlp_FormulaType Ftype; Ctlsp_FormulaType Fsptype; if (F == NIL(Ctlp_Formula_t)) return NIL(Ctlsp_Formula_t); Ftype = Ctlp_FormulaReadType(F); Fsptype = (Ctlsp_FormulaType) Ftype; if (Ftype == Ctlp_TRUE_c) { Fsp = Ctlsp_FormulaCreate(Ctlsp_TRUE_c, NIL(Ctlsp_Formula_t), NIL(Ctlsp_Formula_t)); }else if (Ftype == Ctlp_FALSE_c) { Fsp = Ctlsp_FormulaCreate(Ctlsp_FALSE_c, NIL(Ctlsp_Formula_t), NIL(Ctlsp_Formula_t)); }else if (Ftype == Ctlp_ID_c) { char *nameString = Ctlp_FormulaReadVariableName(F); char *valueString = Ctlp_FormulaReadValueName(F); Fsp = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav(nameString), util_strsav(valueString)); }else { Ctlp_Formula_t *Fleft = Ctlp_FormulaReadLeftChild(F); Ctlp_Formula_t *Fright = Ctlp_FormulaReadRightChild(F); Ctlsp_Formula_t *Fspleft, *Fspright; Fspleft = Ctlsp_CtlFormulaToCtlsp(Fleft); Fspright = Ctlsp_CtlFormulaToCtlsp(Fright); switch(Ftype) { case Ctlp_NOT_c: Fsptype = Ctlsp_NOT_c; break; case Ctlp_AND_c: Fsptype = Ctlsp_AND_c; break; case Ctlp_OR_c: Fsptype = Ctlsp_OR_c; break; case Ctlp_THEN_c: Fsptype = Ctlsp_THEN_c; break; case Ctlp_EQ_c: Fsptype = Ctlsp_EQ_c; break; case Ctlp_XOR_c: Fsptype = Ctlsp_XOR_c; break; default: assert(0); } if (Fspleft) CtlspFormulaIncrementRefCount(Fspleft); if (Fspright) CtlspFormulaIncrementRefCount(Fspright); Fsp = Ctlsp_FormulaCreate(Fsptype, Fspleft, Fspright); } return Fsp; } /**Function******************************************************************** Synopsis [Return a LTL formula with the abbreviations expanded.] Description [The input must be a legal LTL formula. The result shares nothing with the input, not even a string; The result itself does not share sub-formulae. The translation rule is: Ctlsp_THEN_c a->b : !a + b Ctlsp_EQ_c a<->b : a*b +!a*!b Ctlsp_XOR_c a^b : a*!b + !a*b Ctlsp_F_c Fa : true U a Ctlsp_G_c Ga : false R a Ctlsp_A_c Aa : a ] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_LtlFormulaExpandAbbreviation( Ctlsp_Formula_t *formula) { Ctlsp_Formula_t *new_; if (formula == NIL(Ctlsp_Formula_t)) return formula; switch (formula->type) { case Ctlsp_THEN_c: /* a -> b :: !a + b */ new_ = FormulaCreateWithType(Ctlsp_OR_c); new_->left = FormulaCreateWithType(Ctlsp_NOT_c); new_->left->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left); new_->right = Ctlsp_LtlFormulaExpandAbbreviation(formula->right); break; case Ctlsp_EQ_c: /* a <-> b :: a*b + !a*!b */ new_ = FormulaCreateWithType(Ctlsp_OR_c); new_->left = FormulaCreateWithType(Ctlsp_AND_c); new_->right= FormulaCreateWithType(Ctlsp_AND_c); new_->left->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left); new_->left->right= Ctlsp_LtlFormulaExpandAbbreviation(formula->right); new_->right->left = FormulaCreateWithType(Ctlsp_NOT_c); new_->right->left->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left); new_->right->right= FormulaCreateWithType(Ctlsp_NOT_c); new_->right->right->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->right); break; case Ctlsp_XOR_c: /* a ^ b :: a*!b + !a*b */ new_ = FormulaCreateWithType(Ctlsp_OR_c); new_->left = FormulaCreateWithType(Ctlsp_AND_c); new_->left->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left); new_->left->right= FormulaCreateWithType(Ctlsp_NOT_c); new_->left->right->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->right); new_->right = FormulaCreateWithType(Ctlsp_AND_c); new_->right->left= FormulaCreateWithType(Ctlsp_NOT_c); new_->right->left->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left); new_->right->right = Ctlsp_LtlFormulaExpandAbbreviation(formula->right); break; case Ctlsp_F_c: /* F a :: true U a */ new_ = FormulaCreateWithType(Ctlsp_U_c); new_->left = FormulaCreateWithType(Ctlsp_TRUE_c); new_->right= Ctlsp_LtlFormulaExpandAbbreviation(formula->left); break; case Ctlsp_G_c: /* G a :: false R a */ new_ = FormulaCreateWithType(Ctlsp_R_c); new_->left = FormulaCreateWithType(Ctlsp_FALSE_c); new_->right= Ctlsp_LtlFormulaExpandAbbreviation(formula->left); break; case Ctlsp_W_c: /* a W b :: b R (a+b) */ new_ = FormulaCreateWithType(Ctlsp_R_c); new_->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->right); new_->right = FormulaCreateWithType(Ctlsp_OR_c); new_->right->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->right); new_->right->right = Ctlsp_LtlFormulaExpandAbbreviation(formula->left); break; case Ctlsp_ID_c: /* Make a copy of the name, and create a new formula. */ new_ = FormulaCreateWithType(Ctlsp_ID_c); new_->left = (Ctlsp_Formula_t *) util_strsav((char *)(formula->left)); new_->right= (Ctlsp_Formula_t *) util_strsav((char *)(formula->right)); break; case Ctlsp_A_c: /* Ignore A */ new_ = Ctlsp_LtlFormulaExpandAbbreviation(formula->left); break; default: /* These are already in the correct form. Just convert subformulas. */ new_ = FormulaCreateWithType(formula->type); new_->left = Ctlsp_LtlFormulaExpandAbbreviation(formula->left); new_->right= Ctlsp_LtlFormulaExpandAbbreviation(formula->right); } return new_; } /**Function******************************************************************** Synopsis [Return the Negation Normal Form (NNF) of a LTL formula.] Description [The negation is pushed to the bottom (only ahead fo atomic formulae). The result shares nothing with the input, not even a string; subformulae in the result are not shared either. Assume the formula is abbreviation-free, and there are only the following types of formulae before translation: TRUE/ FALSE/ ID/ AND/ OR/ U/ R/ X/ ! .] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_LtlFormulaNegationNormalForm( Ctlsp_Formula_t *formula) { Ctlsp_Formula_t *new_, *left, *right; #if 0 Ctlsp_Formula_t *negRight, *negLeft; #endif Ctlsp_FormulaType dual; if (formula == NIL(Ctlsp_Formula_t)) return formula; if (formula->type == Ctlsp_TRUE_c || formula->type == Ctlsp_FALSE_c) { new_ = FormulaCreateWithType(formula->type); return new_; } if (formula->type == Ctlsp_ID_c) { new_ = FormulaCreateWithType(formula->type); new_->left =(Ctlsp_Formula_t *)util_strsav((char *)(formula->left)); new_->right=(Ctlsp_Formula_t *)util_strsav((char *)(formula->right)); return new_; } if (formula->type != Ctlsp_NOT_c) { new_ = FormulaCreateWithType(formula->type); new_->left = Ctlsp_LtlFormulaNegationNormalForm(formula->left); new_->right= Ctlsp_LtlFormulaNegationNormalForm(formula->right); return new_; } /* In the following, formula->type == Ctlsp_NOT_c */ if (formula->left->type == Ctlsp_NOT_c) return Ctlsp_LtlFormulaNegationNormalForm(formula->left->left); if (formula->left->type == Ctlsp_ID_c) { new_ = FormulaCreateWithType(formula->type); new_->left = Ctlsp_LtlFormulaNegationNormalForm(formula->left); return new_; } #if 0 if (formula->left->type == Ctlsp_THEN_c ) { left = Ctlsp_LtlFormulaNegationNormalForm(formula->left->left); right = Ctlsp_FormulaCreate(Ctlsp_NOT_c, formula->left->right, NIL(Ctlsp_Formula_t)); right = Ctlsp_LtlFormulaNegationNormalForm(right); new_ = Ctlsp_FormulaCreate(Ctlsp_AND_c, left, right); return new_; } if (formula->left->type == Ctlsp_EQ_c ) { left = Ctlsp_LtlFormulaNegationNormalForm(formula->left->left); right = Ctlsp_LtlFormulaNegationNormalForm(formula->left->right); negRight = Ctlsp_FormulaCreate(Ctlsp_NOT_c, right, NIL(Ctlsp_Formula_t)); negLeft = Ctlsp_FormulaCreate(Ctlsp_NOT_c, left, NIL(Ctlsp_Formula_t)); left = right= Ctlsp_FormulaCreate(Ctlsp_AND_c, left, negRight); right = right= Ctlsp_FormulaCreate(Ctlsp_AND_c, negLeft, right); new_ = Ctlsp_FormulaCreate(Ctlsp_OR_c, left, right); return Ctlsp_LtlFormulaNegationNormalForm(new_); } #endif /* for TRUE/ FALSE/ AND/ OR/ U/ R/ X/ F/ G */ switch (formula->left->type) { case Ctlsp_TRUE_c: dual = Ctlsp_FALSE_c; break; case Ctlsp_FALSE_c: dual = Ctlsp_TRUE_c; break; case Ctlsp_AND_c: dual = Ctlsp_OR_c; break; case Ctlsp_OR_c: dual = Ctlsp_AND_c; break; case Ctlsp_U_c: dual = Ctlsp_R_c; break; case Ctlsp_R_c: dual = Ctlsp_U_c; break; case Ctlsp_X_c: dual = Ctlsp_X_c; break; case Ctlsp_F_c: dual = Ctlsp_G_c; break; case Ctlsp_G_c: dual = Ctlsp_F_c; break; default: fail("Unexpected type"); } /* alloc temporary formulae (! left) and (! right) */ left = Ctlsp_FormulaCreate(Ctlsp_NOT_c, formula->left->left, NIL(Ctlsp_Formula_t)); right= Ctlsp_FormulaCreate(Ctlsp_NOT_c, formula->left->right, NIL(Ctlsp_Formula_t)); /* create the new formula */ new_ = FormulaCreateWithType(dual); if ((dual == Ctlsp_X_c) || (dual == Ctlsp_F_c) || (dual == Ctlsp_G_c) ){ new_->left = Ctlsp_LtlFormulaNegationNormalForm(left); }else if (dual != Ctlsp_TRUE_c && dual != Ctlsp_FALSE_c) { new_->left = Ctlsp_LtlFormulaNegationNormalForm(left); new_->right= Ctlsp_LtlFormulaNegationNormalForm(right); } FREE(left); FREE(right); return new_; } /**Function******************************************************************** Synopsis [Hash the LTL formula and its sub-formulae into uniquetable.] Description [It is possible that 'F' is freed, in which case a new 'F' is returned.] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_LtlFormulaHashIntoUniqueTable( Ctlsp_Formula_t *F, st_table *uniqueTable) { Ctlsp_Formula_t *uniqueFormula; uniqueFormula = FormulaHashIntoUniqueTable(F, uniqueTable); /* If there is a copy 'uniqueFormula' in the uniqueTable, free F and increment the refCount of 'uniqueFormula' */ if(uniqueFormula != F) { CtlspFormulaDecrementRefCount(F); CtlspFormulaIncrementRefCount(uniqueFormula); } return uniqueFormula; } /**Function******************************************************************** Synopsis [Clear the '.marked' field of the LTL formula.] Description [Recursively clear the .marked field for all its sub-formulae.] SideEffects [] SeeAlso [] ******************************************************************************/ void Ctlsp_LtlFormulaClearMarks( Ctlsp_Formula_t *F) { if(F) { F->marked = 0; if (F->type != Ctlsp_ID_c) { Ctlsp_LtlFormulaClearMarks(F->left); Ctlsp_LtlFormulaClearMarks(F->right); } } } /**Function******************************************************************** Synopsis [Clear the '.marked' field of the LTL formula.] Description [Recursively clear the .marked field for all its sub-formulae.] SideEffects [] SeeAlso [] ******************************************************************************/ int Ctlsp_LtlFormulaCountNumber( Ctlsp_Formula_t *F) { int result = 1; if (!F) return 0; if (F->marked) return 0; F->marked = 1; if (F->type == Ctlsp_TRUE_c || F->type == Ctlsp_FALSE_c || F->type == Ctlsp_ID_c) return 1; result += Ctlsp_LtlFormulaCountNumber(F->left); result += Ctlsp_LtlFormulaCountNumber(F->right); return result; } /**Function******************************************************************** Synopsis [Alloc a unqiue table for formulae.] Description [Use FormulaHash and formulaCompare.] SideEffects [] SeeAlso [] ******************************************************************************/ st_table * Ctlsp_LtlFormulaCreateUniqueTable( void ) { return st_init_table(FormulaCompare, FormulaHash); } /**Function******************************************************************** Synopsis [Return True iff formula is an "elementary formula".] Description [Return True iff formula is an elementary formula. This is the original definition used in "Wring": it's a TRUE/FALSE/literal/X-formula.] SideEffects [] SeeAlso [] ******************************************************************************/ int Ctlsp_LtlFormulaIsElementary2( Ctlsp_Formula_t *F) { assert(F != 0); return (F->type == Ctlsp_X_c || Ctlsp_LtlFormulaIsAtomicPropositional(F) ); } /**Function******************************************************************** Synopsis [Return True iff formula is an "elementary formula".] Description [Return True iff the formula is an elementary formula. The definition of 'elementary formula' is slightly different from the one in "Wring": it's a TRUE/FALSE/Atomic Propositions/X-formula.] SideEffects [] SeeAlso [] ******************************************************************************/ int Ctlsp_LtlFormulaIsElementary( Ctlsp_Formula_t *F) { assert(F != NIL(Ctlsp_Formula_t)); return (F->type == Ctlsp_X_c || Ctlsp_LtlFormulaIsPropositional(F) ); } /**Function******************************************************************** Synopsis [Return TRUE iff abbreviation-free LTL formula is bounded.] Description [A bounded LTL formula is one that contains only atomic propositions, Boolean connectives, and the next-time (X) operator. The depth of a bounded formula is the maximum number of Xs along a path of its parse tree. This function can only be applied to abbreviation-free LTL formulae.] SideEffects [The depth is returned as a side effect. (Only if the function returns TRUE.)] SeeAlso [Ctlsp_LtlFormulaExpandAbbreviation, Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe] ******************************************************************************/ boolean Ctlsp_LtlFormulaTestIsBounded( Ctlsp_Formula_t *formula, int *depth) { Ctlsp_Formula_t *leftChild; Ctlsp_Formula_t *rightChild; int leftDepth, rightDepth; assert(formula != NIL(Ctlsp_Formula_t)); switch (Ctlsp_FormulaReadType(formula)) { case Ctlsp_TRUE_c: case Ctlsp_FALSE_c: case Ctlsp_ID_c: *depth = 0; return TRUE; case Ctlsp_AND_c: case Ctlsp_OR_c: leftChild = Ctlsp_FormulaReadLeftChild(formula); if (Ctlsp_LtlFormulaTestIsBounded(leftChild, &leftDepth)) { rightChild = Ctlsp_FormulaReadRightChild(formula); if (Ctlsp_LtlFormulaTestIsBounded(rightChild, &rightDepth)) { *depth = leftDepth > rightDepth ? leftDepth : rightDepth; return TRUE; } else { return FALSE; } } else { return FALSE; } case Ctlsp_NOT_c: case Ctlsp_X_c: leftChild = Ctlsp_FormulaReadLeftChild(formula); if (Ctlsp_LtlFormulaTestIsBounded(leftChild, &leftDepth)) { if (Ctlsp_FormulaReadType(formula) == Ctlsp_X_c) leftDepth++; *depth = leftDepth; return TRUE; } else { return FALSE; } case Ctlsp_U_c: case Ctlsp_R_c: return FALSE; default: fail("unexpected node type in abbreviation-free formula\n"); return FALSE; /* not reached */ } } /* Ctlsp_LtlFormulaTestIsBounded */ /**Function******************************************************************** Synopsis [Return the depth of abbreviation-free LTL formula.] Description [The depth of the LTL formula f is the maximum level of nesting of temporal operators in f. This function can only be applied to abbreviation-free LTL formulae.] SideEffects [] SeeAlso [Ctlsp_LtlFormulaExpandAbbreviation] ******************************************************************************/ int Ctlsp_LtlFormulaDepth( Ctlsp_Formula_t *formula) { int leftDepth, rightDepth; assert(formula != NIL(Ctlsp_Formula_t)); switch (Ctlsp_FormulaReadType(formula)) { case Ctlsp_TRUE_c: case Ctlsp_FALSE_c: case Ctlsp_ID_c: return 0; case Ctlsp_AND_c: case Ctlsp_OR_c: leftDepth = Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadLeftChild(formula)); rightDepth = Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadRightChild(formula)); return leftDepth > rightDepth ? leftDepth : rightDepth; case Ctlsp_NOT_c: return Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadLeftChild(formula)); case Ctlsp_X_c: return 1+Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadLeftChild(formula)); case Ctlsp_U_c: case Ctlsp_R_c: leftDepth = Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadLeftChild(formula)); rightDepth = Ctlsp_LtlFormulaDepth(Ctlsp_FormulaReadRightChild(formula)); return 1+(leftDepth > rightDepth ? leftDepth : rightDepth); default: fail("unexpected node type in abbreviation-free formula\n"); return 0; /* not reached */ } } /* Ctlsp_LtlFormulaDepth */ /**Function******************************************************************** Synopsis [Return TRUE iff LTL formula in negation normal form is syntactically co-safe.] Description [A syntactically co-safe LTL formula is a formula in negation normal form that contains no release (R) operators. This function can only be applied to abbreviation-free LTL formulae in negation normal form. We test co-safety because this function is meant to be called on the negation of the given formula.] SideEffects [none] SeeAlso [Ctlsp_LtlFormulaNegationNormalForm, Ctlsp_LtlFormulaTestIsBounded] ******************************************************************************/ boolean Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(Ctlsp_Formula_t *formula) { Ctlsp_Formula_t *leftChild; Ctlsp_Formula_t *rightChild; assert(formula != NIL(Ctlsp_Formula_t)); /* Check for unless temporal operator. a W b = (a U b) OR (FALSE R a) its negation = (!a R !b) AND (TRUE U !a) */ if(Ctlsp_FormulaReadType(formula) == Ctlsp_AND_c){ leftChild = Ctlsp_FormulaReadLeftChild(formula); rightChild = Ctlsp_FormulaReadRightChild(formula); if((Ctlsp_FormulaReadType(leftChild) == Ctlsp_R_c) && (Ctlsp_FormulaReadType(rightChild) == Ctlsp_U_c)){ if(Ctlsp_FormulaReadLeftChild(leftChild) == Ctlsp_FormulaReadRightChild(rightChild)){ if(Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(rightChild)) == Ctlsp_TRUE_c){ return Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe( Ctlsp_FormulaReadLeftChild(leftChild)) && Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe( Ctlsp_FormulaReadRightChild(leftChild)); } } } /* a W b = (FALSE R a) OR (a U b) its negation = (TRUE U !a) AND (!a R !b) */ if((Ctlsp_FormulaReadType(rightChild) == Ctlsp_R_c) && (Ctlsp_FormulaReadType(leftChild) == Ctlsp_U_c)){ if(Ctlsp_FormulaReadLeftChild(rightChild) == Ctlsp_FormulaReadRightChild(leftChild)){ if(Ctlsp_FormulaReadType(Ctlsp_FormulaReadLeftChild(leftChild)) == Ctlsp_TRUE_c){ return Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe( Ctlsp_FormulaReadLeftChild(rightChild)) && Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe( Ctlsp_FormulaReadRightChild(rightChild)); } } } } switch (Ctlsp_FormulaReadType(formula)) { case Ctlsp_TRUE_c: case Ctlsp_FALSE_c: case Ctlsp_ID_c: return TRUE; case Ctlsp_AND_c: case Ctlsp_OR_c: case Ctlsp_U_c: leftChild = Ctlsp_FormulaReadLeftChild(formula); if (Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(leftChild)) { rightChild = Ctlsp_FormulaReadRightChild(formula); return Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(rightChild); } else { return FALSE; } case Ctlsp_NOT_c: leftChild = Ctlsp_FormulaReadLeftChild(formula); /* The formula is in negation normal form. */ assert(Ctlsp_FormulaReadType(leftChild) == Ctlsp_ID_c); return TRUE; case Ctlsp_X_c: leftChild = Ctlsp_FormulaReadLeftChild(formula); return Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(leftChild); case Ctlsp_R_c: return FALSE; default: fail("unexpected node type in abbreviation-free formula\n"); return FALSE; /* not reached */ } } /* Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe */ /**Function******************************************************************** Synopsis [Tests if each formula in an array of LTL formulae is propositional] Description [This function tests each LTL formula in negation normal form to see if it is a propositional formula. Return TRUE if all formulae are propositional formulae.] SideEffects [none] SeeAlso [Ctlsp_LtlFormulaIsPropositional] ******************************************************************************/ int Ctlsp_LtlFormulaArrayIsPropositional( array_t * formulaArray) { int i; Ctlsp_Formula_t *formula; for (i = 0; i < array_n(formulaArray); i++) { formula = array_fetch(Ctlsp_Formula_t *, formulaArray, i); if(!Ctlsp_isPropositionalFormula(formula)){ /*if(Ctlsp_LtlFormulaIsPropositional(formula) == 0){*/ return 0; } } return 1; } /* Ctlsp_LtlFormulaArrayIsPropositional */ /**Function******************************************************************** Synopsis [Return T iff formula is a "propositional formula".] Description [This function tests an LTL formula in negation normal form to see if it is a propositional formula. A propositional formula contains only Boolean connectives, TRUE, FALSE, and literals. A literal is an atomic proposition or the negation of an atomic popposition.] SideEffects [none] SeeAlso [Ctlsp_LtlFormulaIsAtomicPropositional] ******************************************************************************/ int Ctlsp_LtlFormulaIsPropositional( Ctlsp_Formula_t *F) { int result; assert(F != NIL(Ctlsp_Formula_t)); switch (F->type) { case Ctlsp_TRUE_c: case Ctlsp_FALSE_c: case Ctlsp_ID_c: result = 1; break; case Ctlsp_NOT_c: /* negation only appears ahead of AP */ if (F->left->type == Ctlsp_ID_c) result = 1; else result = 0; break; case Ctlsp_AND_c: case Ctlsp_OR_c: result = (Ctlsp_LtlFormulaIsPropositional(F->left) && Ctlsp_LtlFormulaIsPropositional(F->right)); break; default: result = 0; } return result; } /* Ctlsp_LtlFormulaIsPropositional() */ /**Function******************************************************************** Synopsis [Return T iff formula is an "atomic propositional formula".] Description [TRUE/FALSE/literal. literal: an atomic proposition or the negation of an atomic popposition.] SideEffects [none] SeeAlso [Ctlsp_LtlFormulaIsPropositional] ******************************************************************************/ int Ctlsp_LtlFormulaIsAtomicPropositional( Ctlsp_Formula_t *F) { int result; assert(F != 0); switch (F->type) { case Ctlsp_TRUE_c: case Ctlsp_FALSE_c: case Ctlsp_ID_c: result = 1; break; case Ctlsp_NOT_c: /* negation only appears ahead of AP */ if (F->left->type == Ctlsp_ID_c) result = 1; else result = 0; break; default: result = 0; } return result; } /**Function******************************************************************** Synopsis [Return T iff formula is a "FG formula".] Description [TRUE U (FALSE R p).] SideEffects [] SeeAlso [Ctlsp_LtlFormulaIsGF, Ctlsp_LtlFormulaIsFGorGF] ******************************************************************************/ int Ctlsp_LtlFormulaIsFG( Ctlsp_Formula_t *F) { int result = 0; if (F->type == Ctlsp_U_c) { if (F->left->type == Ctlsp_TRUE_c && F->right->type == Ctlsp_R_c) { result = (F->right->left->type == Ctlsp_FALSE_c); } } return result; } /**Function******************************************************************** Synopsis [Return T iff formula is a "GF formula".] Description [FALSE R (TRUE U p).] SideEffects [] SeeAlso [Ctlsp_LtlFormulaIsFG, Ctlsp_LtlFormulaIsFGorGF] ******************************************************************************/ int Ctlsp_LtlFormulaIsGF( Ctlsp_Formula_t *F) { int result = 0; if (F->type == Ctlsp_R_c) { if (F->left->type == Ctlsp_FALSE_c && F->right->type == Ctlsp_U_c) { result = (F->right->left->type == Ctlsp_TRUE_c); } } return result; } /**Function******************************************************************** Synopsis [Return T iff formula is a "FG or GF formula".] Description [TRUE U (FALSE R p).] SideEffects [] SeeAlso [Ctlsp_LtlFormulaIsGF, Ctlsp_LtlFormulaIsFG] ******************************************************************************/ int Ctlsp_LtlFormulaIsFGorGF( Ctlsp_Formula_t *F) { return (Ctlsp_LtlFormulaIsFG(F) || Ctlsp_LtlFormulaIsGF(F)); } /**Function******************************************************************** Synopsis [Return T iff (form -> to).] Description [Since determine '->' is hard, we only consider easy case which can be determined syntatically. Notice that, before calling this function, 'from' and 'to' are hashed into the same UniqueTable (This helps in identifying "from==to").] SideEffects [] SeeAlso [] ******************************************************************************/ int Ctlsp_LtlFormulaSimplyImply( Ctlsp_Formula_t *from, Ctlsp_Formula_t *to) { #if 0 fprintf(vis_stdout, "\n------------------------\n"); Ctlsp_FormulaPrint(vis_stdout, from); fprintf(vis_stdout, "\n ==>\n"); Ctlsp_FormulaPrint(vis_stdout, to); fprintf(vis_stdout, "\n------------------------\n"); #endif /* from -> from : 1 */ if (from == to) return 1; /* from -> TRUE : 1 */ if (to->type == Ctlsp_TRUE_c) return 1; /* FALSE -> to : 1 */ if (from->type == Ctlsp_FALSE_c) return 1; if (to->type == Ctlsp_U_c) { /* from -> tL U tR: (from->tR)? */ if (Ctlsp_LtlFormulaSimplyImply(from, to->right)) return 1; /* (fL U fR) -> (tl U tR) : (fL->tL)? && (fR->tR)? */ if (from->type == Ctlsp_U_c) return (Ctlsp_LtlFormulaSimplyImply(from->left, to->left) && Ctlsp_LtlFormulaSimplyImply(from->right, to->right)); } if (to->type == Ctlsp_R_c) { /* from -> tL R tR: (from->tL)? && (from->tR)? */ if (Ctlsp_LtlFormulaSimplyImply(from, to->left) && Ctlsp_LtlFormulaSimplyImply(from, to->right)) return 1; /* (fL R fR) -> (tL R tR) : (fL->tL)? && (fR->tR)? */ if (from->type == Ctlsp_R_c) return (Ctlsp_LtlFormulaSimplyImply(from->left, to->left) && Ctlsp_LtlFormulaSimplyImply(from->right, to->right)); } /* (fL U fR) -> to :: (fL->to)? && (fR->to)? */ if (from->type == Ctlsp_U_c) { if (Ctlsp_LtlFormulaSimplyImply(from->left, to) && Ctlsp_LtlFormulaSimplyImply(from->right,to) ) return 1; } /* (fL R fR) -> to :: (fR->to)? */ if (from->type == Ctlsp_R_c) { if (Ctlsp_LtlFormulaSimplyImply(from->right,to)) return 1; } /************************************************************************* * (1) If we unwinding every propositional formula, sometimes it will * become really hard. This is due to the feature of the CTL* parser. * For example, "state[1024]=0" would be parsed into 1024 subformulae * * (2) Without unwinding, some possible simplification cases can not be * detected. For example, "p + !p", "p * !p" (while p and the left * subformula in !p are syntatically different. ************************************************************************/ if (!Ctlsp_LtlFormulaIsPropositional(to)) { /* form -> tL*tR : (from->tL)? && (from->rR)? */ if (to->type == Ctlsp_AND_c) return (Ctlsp_LtlFormulaSimplyImply(from, to->left) && Ctlsp_LtlFormulaSimplyImply(from, to->right)); /* from -> tL+tR : (from->tL)? || (from->rR)? */ if (to->type == Ctlsp_OR_c) return (Ctlsp_LtlFormulaSimplyImply(from, to->left) || Ctlsp_LtlFormulaSimplyImply(from, to->right) ); } if (!Ctlsp_LtlFormulaIsPropositional(from)) { /* (fL * fR) -> to :: (fL->to)? || (fR->to)? */ if (from->type == Ctlsp_AND_c) return (Ctlsp_LtlFormulaSimplyImply(from->left, to) || Ctlsp_LtlFormulaSimplyImply(from->right,to) ); /* (fL + fR) -> to :: (fL->to)? && (fR->to)? */ if (from->type == Ctlsp_OR_c) return (Ctlsp_LtlFormulaSimplyImply(from->left, to) && Ctlsp_LtlFormulaSimplyImply(from->right,to) ); } return 0; } /**Function******************************************************************** Synopsis [Translate LTL formula into Separated Normal Form (SNF)] Description [Translate LTL formula into Separated Normal Form (SNF). Each LTL formula is translated into a set of rules in the form (p --> f(q)), where p and q are propositional and f(q) contains at most one temporal operator which is either X or F.] SideEffects [] SeeAlso [Ctlsp_LtlTranslateIntoSNFRecursive] ******************************************************************************/ array_t * Ctlsp_LtlTranslateIntoSNF( Ctlsp_Formula_t *formula) { Ctlsp_Formula_t *leftNode; int index, i; array_t *formulaArray = array_alloc(Ctlsp_Formula_t *, 0); /* rule#1: an LTL formula must hold at an initial state. */ leftNode = Ctlsp_FormulaCreate(Ctlsp_ID_c, (void *)util_strsav(" SNFstart"), (void *)util_strsav("1")); /* rightNode = Ctlsp_FormulaCreate(Ctlsp_ID_c, (void *)util_strsav("SNFx_0"), (void *)util_strsav("1")); newNode = Ctlsp_FormulaCreate(Ctlsp_THEN_c, leftNode, rightNode); */ index = 0; Ctlsp_LtlTranslateIntoSNFRecursive(leftNode, formula, formulaArray, &index); fprintf(vis_stdout, "The SNF rules are:\n"); for (i = 0; i < array_n(formulaArray); i++) { Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *, formulaArray, i); Ctlsp_FormulaPrint(vis_stdout, ltlFormula); fprintf(vis_stdout, "\n"); } return formulaArray; } /**Function******************************************************************** Synopsis [Trnalate LTL formula into Separated Normal Form (SNF)] Description [Recursively trnaslate LTL formula into SNF Assume the formula is abbreviation-free NNF, and there are only the following types of formulae before translation: TRUE FALSE ID AND OR U R X ! .] SideEffects [] SeeAlso [] ******************************************************************************/ void Ctlsp_LtlTranslateIntoSNFRecursive( Ctlsp_Formula_t *propNode, Ctlsp_Formula_t *formula, array_t *formulaArray, int *index) { Ctlsp_Formula_t *leftNode, *rightNode, *newNode, *result; if(formula == NIL(Ctlsp_Formula_t)){ return; } if(Ctlsp_LtlFormulaIsPropositional(formula)){ newNode = CtlspFunctionThen(propNode, formula); CtlspFormulaIncrementRefCount(newNode); array_insert_last(Ctlsp_Formula_t *, formulaArray, newNode); return; } switch (Ctlsp_FormulaReadType(formula)) { case Ctlsp_AND_c: leftNode = Ctlsp_FormulaReadLeftChild(formula); rightNode = Ctlsp_FormulaReadRightChild(formula); Ctlsp_LtlTranslateIntoSNFRecursive(propNode, leftNode, formulaArray, index); Ctlsp_LtlTranslateIntoSNFRecursive(propNode, rightNode, formulaArray, index); break; case Ctlsp_OR_c: leftNode = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index); rightNode = createSNFnode(Ctlsp_FormulaReadRightChild(formula), formulaArray, index); newNode = CtlspFunctionOr(leftNode, rightNode); Ctlsp_LtlTranslateIntoSNFRecursive(propNode, newNode, formulaArray, index); break; case Ctlsp_THEN_c: leftNode = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index); rightNode = createSNFnode(Ctlsp_FormulaReadRightChild(formula), formulaArray, index); newNode = CtlspFunctionOr( Ctlsp_FormulaCreate(Ctlsp_NOT_c, leftNode, NIL(Ctlsp_Formula_t)) , rightNode); Ctlsp_LtlTranslateIntoSNFRecursive(propNode, newNode, formulaArray, index); break; case Ctlsp_NOT_c: if (!Ctlsp_isPropositionalFormula(formula)){ fprintf(vis_stderr,"SNF error: the LTL formula is not in NNF\n"); } break; case Ctlsp_X_c: /* propNode -> X leftNode */ leftNode = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index); newNode = Ctlsp_FormulaCreate(Ctlsp_X_c, leftNode, NIL(Ctlsp_Formula_t)); newNode = CtlspFunctionThen(propNode, newNode); CtlspFormulaIncrementRefCount(newNode); array_insert_last(Ctlsp_Formula_t *, formulaArray, newNode); break; case Ctlsp_F_c: /* propNode -> F leftNode */ leftNode = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index); newNode = Ctlsp_FormulaCreate(Ctlsp_F_c, leftNode, NIL(Ctlsp_Formula_t)); newNode = CtlspFunctionThen(propNode, newNode); CtlspFormulaIncrementRefCount(newNode); array_insert_last(Ctlsp_Formula_t *, formulaArray, newNode); break; case Ctlsp_G_c: /* propNode -> G leftNode */ leftNode = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index); newNode = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strcat3(" SNFx","_", util_inttostr((*index)++)), (void *)util_strsav("1")); result = CtlspFunctionAnd(leftNode, newNode); Ctlsp_LtlTranslateIntoSNFRecursive(propNode, result, formulaArray, index); result = Ctlsp_FormulaCreate(Ctlsp_X_c, result, NIL(Ctlsp_Formula_t)); Ctlsp_LtlTranslateIntoSNFRecursive(newNode, result, formulaArray, index); break; case Ctlsp_U_c: /* x --> a U b = x --> b + a*y y --> X(b + a*y) x --> F(b) */ newNode = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strcat3(" SNFx","_", util_inttostr((*index)++)), (void *)util_strsav("1")); leftNode = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index); rightNode = createSNFnode(Ctlsp_FormulaReadRightChild(formula), formulaArray, index); result = CtlspFunctionAnd(leftNode, newNode); result = CtlspFunctionOr(rightNode, result); Ctlsp_LtlTranslateIntoSNFRecursive(propNode, result, formulaArray, index); result = Ctlsp_FormulaCreate(Ctlsp_X_c, result, NIL(Ctlsp_Formula_t)); Ctlsp_LtlTranslateIntoSNFRecursive(newNode, result, formulaArray, index); result = Ctlsp_FormulaCreate(Ctlsp_F_c, rightNode, NIL(Ctlsp_Formula_t)); Ctlsp_LtlTranslateIntoSNFRecursive(propNode, result, formulaArray, index); break; case Ctlsp_W_c: /* x --> a W b = x --> b + a*y y --> X(b + a*y) */ newNode = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strcat3(" SNFx","_", util_inttostr((*index)++)), (void *)util_strsav("1")); leftNode = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index); rightNode = createSNFnode(Ctlsp_FormulaReadRightChild(formula), formulaArray, index); result = CtlspFunctionAnd(leftNode, newNode); result = CtlspFunctionOr(rightNode, result); Ctlsp_LtlTranslateIntoSNFRecursive(propNode, result, formulaArray, index); result = Ctlsp_FormulaCreate(Ctlsp_X_c, result, NIL(Ctlsp_Formula_t)); Ctlsp_LtlTranslateIntoSNFRecursive(newNode, result, formulaArray, index); break; case Ctlsp_R_c: /* x --> left R right = x --> left*right + right*y y --> X(left*rigt* + right*y) */ newNode = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strcat3(" SNFx","_", util_inttostr((*index)++)), (void *)util_strsav("1")); leftNode = createSNFnode(Ctlsp_FormulaReadLeftChild(formula), formulaArray, index); rightNode = createSNFnode(Ctlsp_FormulaReadRightChild(formula), formulaArray, index); leftNode = CtlspFunctionAnd(leftNode, rightNode); result = CtlspFunctionAnd(rightNode, newNode); result = CtlspFunctionOr(leftNode, result); Ctlsp_LtlTranslateIntoSNFRecursive(propNode, result, formulaArray, index); result = Ctlsp_FormulaCreate(Ctlsp_X_c, result, NIL(Ctlsp_Formula_t)); Ctlsp_LtlTranslateIntoSNFRecursive(newNode, result, formulaArray, index); break; default: fail("unexpected node type in abbreviation-free formula\n"); return; /* not reached */ } } /**Function******************************************************************** Synopsis [Perform simple rewriting of a formula.] Description [We return a formula which shares nothing with the input formula] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * Ctlsp_LtlFormulaSimpleRewriting( Ctlsp_Formula_t *formula) { Ctlsp_Formula_t *F, *newF; st_table *Utable = st_init_table(FormulaCompare, FormulaHash); st_generator *stGen; char *key; /* copy the input formula (so that they share nothing) */ F = Ctlsp_LtlFormulaNegationNormalForm(formula); /* hash into the 'Utable' */ F = Ctlsp_LtlFormulaHashIntoUniqueTable(F, Utable); /* simple rewriting */ F = CtlspLtlFormulaSimpleRewriting_Aux(F, Utable); /* copy F into 'newF' (they shares nothing) */ newF = Ctlsp_LtlFormulaNegationNormalForm(F); /* free formulae in st_table */ st_foreach_item(Utable, stGen, &key, &F) { if (F->type == Ctlsp_ID_c) { FREE(F->left); FREE(F->right); } FREE(F); } st_free_table(Utable); return (newF); } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Rewriting the LTL formula recursively.] Description [Recursive call, used in Ctlsp_LtlFormulaSimpleRewriting() only.] SideEffects [The given formula F might be freed (hence unrecoverable)] SeeAlso [Ctlsp_LtlFormulaSimpleRewriting] ******************************************************************************/ Ctlsp_Formula_t * CtlspLtlFormulaSimpleRewriting_Aux( Ctlsp_Formula_t *F, st_table *Utable) { Ctlsp_Formula_t *left, *right; Ctlsp_Formula_t *tmpf1, *tmpf2; Ctlsp_Formula_t *True, *False; if (F == NIL(Ctlsp_Formula_t)) return F; if (F->type == Ctlsp_ID_c || F->type == Ctlsp_TRUE_c || F->type == Ctlsp_FALSE_c) { F = Ctlsp_LtlFormulaHashIntoUniqueTable(F, Utable); return F; } #if 0 fprintf(vis_stdout, "\nRewriting ...\n"); Ctlsp_FormulaPrint(vis_stdout, F); fprintf(vis_stdout, "\n"); #endif /* First of all, rewrite F->left, F->right */ left = CtlspLtlFormulaSimpleRewriting_Aux(F->left, Utable); #if 0 fprintf(vis_stdout, "\n... Rewriting(left)\n"); Ctlsp_FormulaPrint(vis_stdout, left); fprintf(vis_stdout, "\n"); #endif right = CtlspLtlFormulaSimpleRewriting_Aux(F->right, Utable); #if 0 fprintf(vis_stdout, "\n... Rewriting(right)\n"); Ctlsp_FormulaPrint(vis_stdout, right); fprintf(vis_stdout, "\n"); #endif /* in case we want to use TRUE/FALSE */ True = Ctlsp_LtlFormulaHashIntoUniqueTable(FormulaCreateWithType(Ctlsp_TRUE_c), Utable); False = Ctlsp_LtlFormulaHashIntoUniqueTable(FormulaCreateWithType(Ctlsp_FALSE_c), Utable); switch (F->type) { case Ctlsp_AND_c: /* r -> l : l*r == r */ if (Ctlsp_LtlFormulaSimplyImply(right, left)) return right; /* l -> r, l*r == l */ if (Ctlsp_LtlFormulaSimplyImply(left, right)) return left; /* r -> !l, l*r == FALSE*/ tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c); tmpf1->left = left; tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1); FREE(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); if (Ctlsp_LtlFormulaSimplyImply(right, tmpf2)) return False; /* l -> !r, l*r == FALSE*/ tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c); tmpf1->left = right; tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1); FREE(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); if (Ctlsp_LtlFormulaSimplyImply(left, tmpf2)) return False; /* (ll R lr) * (ll R rr) == (ll) R (lr*rr) */ if (left->type == Ctlsp_R_c && right->type == Ctlsp_R_c) { if (left->left == right->left) { tmpf1 = FormulaCreateWithType(Ctlsp_AND_c); tmpf1->left = left->right; tmpf1->right = right->right; CtlspFormulaIncrementRefCount(left->right); CtlspFormulaIncrementRefCount(right->right); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_R_c); tmpf2->left = left->left; tmpf2->right = tmpf1; CtlspFormulaIncrementRefCount(left->left); CtlspFormulaIncrementRefCount(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } } /* (ll U lr) * (rl U lr) == (ll * rl) U (lr) */ if (left->type == Ctlsp_U_c && right->type == Ctlsp_U_c) { if (left->right == right->right) { tmpf1 = FormulaCreateWithType(Ctlsp_AND_c); tmpf1->left = left->left; tmpf1->right = right->left; CtlspFormulaIncrementRefCount(left->left); CtlspFormulaIncrementRefCount(right->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_U_c); tmpf2->left = tmpf1; tmpf2->right = left->right; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(left->right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } } /* (X ll)*(X rl) == X (ll*rl) */ if (left->type == Ctlsp_X_c && right->type == Ctlsp_X_c) { tmpf1 = FormulaCreateWithType(Ctlsp_AND_c); tmpf1->left = left->left; tmpf1->right = right->left; CtlspFormulaIncrementRefCount(left->left); CtlspFormulaIncrementRefCount(right->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_X_c); tmpf2->left = tmpf1; CtlspFormulaIncrementRefCount(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } /* (ll R lr) * (rl U ll) == ( (X lr * rl) U ll) * lr */ if (left->type == Ctlsp_R_c && right->type == Ctlsp_U_c) { if (left->left == right->right) { tmpf1 = FormulaCreateWithType(Ctlsp_X_c); tmpf1->left = left->right; CtlspFormulaIncrementRefCount(left->right); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); if (right->left->type != Ctlsp_TRUE_c) { tmpf2 = FormulaCreateWithType(Ctlsp_AND_c); tmpf2->left = tmpf1; tmpf2->right = right->left; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(right->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); } tmpf2 = FormulaCreateWithType(Ctlsp_U_c); tmpf2->left = tmpf1; tmpf2->right = left->left; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(left->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_AND_c); tmpf2->left = tmpf1; tmpf2->right = left->right; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(left->right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } } /* (ll U lr) * (lr R rr) == ( (X rr * ll) U rl) * rr */ if (left->type == Ctlsp_U_c && right->type == Ctlsp_R_c) { if (left->right == right->left) { tmpf1 = FormulaCreateWithType(Ctlsp_X_c); tmpf1->left = right->right; CtlspFormulaIncrementRefCount(right->right); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); if (left->left->type != Ctlsp_TRUE_c) { tmpf2 = FormulaCreateWithType(Ctlsp_AND_c); tmpf2->left = tmpf1; tmpf2->right = left->left; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(left->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); } tmpf2 = FormulaCreateWithType(Ctlsp_U_c); tmpf2->left = tmpf1; tmpf2->right = right->left; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(right->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_AND_c); tmpf2->left = tmpf1; tmpf2->right = right->right; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(right->right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } } /* (ll R lr) * r, r=>ll == lr *r */ if (left->type == Ctlsp_R_c && Ctlsp_LtlFormulaSimplyImply(right, left->left)) { tmpf1 = FormulaCreateWithType(Ctlsp_AND_c); tmpf1->left = left->right; tmpf1->right = right; CtlspFormulaIncrementRefCount(left->right); CtlspFormulaIncrementRefCount(right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; } /* l *(rl R rr), l=>rl == l * rr */ if (right->type == Ctlsp_R_c && Ctlsp_LtlFormulaSimplyImply(left, right->left)) { tmpf1 = FormulaCreateWithType(Ctlsp_AND_c); tmpf1->left = left; tmpf1->right = right->right; CtlspFormulaIncrementRefCount(left); CtlspFormulaIncrementRefCount(right->right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; } /* (ll U lr) * r, r=>!ll == lr * r */ if (left->type == Ctlsp_U_c) { tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c); tmpf1->left = left->left; tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1); FREE(tmpf1); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); if (Ctlsp_LtlFormulaSimplyImply(right, tmpf1)) { tmpf1 = FormulaCreateWithType(Ctlsp_AND_c); tmpf1->left = left->right; tmpf1->right = right; CtlspFormulaIncrementRefCount(left->right); CtlspFormulaIncrementRefCount(right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; } } /* l * (rl U rr), l=>!rl == l * rr */ if (right->type == Ctlsp_U_c) { tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c); tmpf1->left = right->left; tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1); FREE(tmpf1); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); if (Ctlsp_LtlFormulaSimplyImply(left, tmpf1)) { tmpf1 = FormulaCreateWithType(Ctlsp_AND_c); tmpf1->left = left; tmpf1->right = right->right; CtlspFormulaIncrementRefCount(left); CtlspFormulaIncrementRefCount(right->right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; } } /* FG lrr * FG rrr = FG (lrr * rrr) */ if (Ctlsp_LtlFormulaIsFG(left) && Ctlsp_LtlFormulaIsFG(right)) { tmpf1 = FormulaCreateWithType(Ctlsp_AND_c); tmpf1->left = left->right->right; tmpf1->right = right->right->right; CtlspFormulaIncrementRefCount(left->right->right); CtlspFormulaIncrementRefCount(right->right->right); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_R_c); tmpf2->left = False; tmpf2->right = tmpf1; CtlspFormulaIncrementRefCount(False); CtlspFormulaIncrementRefCount(tmpf1); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_U_c); tmpf2->left = True; tmpf2->right = tmpf1; CtlspFormulaIncrementRefCount(True); CtlspFormulaIncrementRefCount(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } /* return (l * r) */ tmpf1 = FormulaCreateWithType(Ctlsp_AND_c); tmpf1->left = left; tmpf1->right = right; CtlspFormulaIncrementRefCount(left); CtlspFormulaIncrementRefCount(right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; case Ctlsp_OR_c: /* r -> l, l+r == l */ if (Ctlsp_LtlFormulaSimplyImply(right, left)) return left; /* l -> r, l+r == r */ if (Ctlsp_LtlFormulaSimplyImply(left, right)) return right; /* !r -> l, l+r == TRUE*/ tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c); tmpf1->left = right; tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1); FREE(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); if (Ctlsp_LtlFormulaSimplyImply(tmpf2, left)) return True; /* !l -> r, l+r == TRUE*/ tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c); tmpf1->left = left; tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1); FREE(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); if (Ctlsp_LtlFormulaSimplyImply(tmpf2, right)) return True; /* (ll U lr) + (ll U rr) == (ll) U (lr+rr) */ if (left->type == Ctlsp_U_c && right->type == Ctlsp_U_c) { if (left->left == right->left) { tmpf1 = FormulaCreateWithType(Ctlsp_OR_c); tmpf1->left = left->right; tmpf1->right = right->right; CtlspFormulaIncrementRefCount(left->right); CtlspFormulaIncrementRefCount(right->right); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_U_c); tmpf2->left = left->left; tmpf2->right = tmpf1; CtlspFormulaIncrementRefCount(left->left); CtlspFormulaIncrementRefCount(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } } /* (ll R lr) + (rl R lr) == (ll+rl) R (lr) */ if (left->type == Ctlsp_R_c && right->type == Ctlsp_R_c) { if (left->right == right->right) { tmpf1 = FormulaCreateWithType(Ctlsp_OR_c); tmpf1->left = left->left; tmpf1->right = right->left; CtlspFormulaIncrementRefCount(left->left); CtlspFormulaIncrementRefCount(right->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_R_c); tmpf2->left = tmpf1; tmpf2->right = left->right; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(left->right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } } /* (X ll) + (X rl) == X (ll+rl) */ if (left->type == Ctlsp_X_c && right->type == Ctlsp_X_c) { tmpf1 = FormulaCreateWithType(Ctlsp_OR_c); tmpf1->left = left->left; tmpf1->right = right->left; CtlspFormulaIncrementRefCount(left->left); CtlspFormulaIncrementRefCount(right->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_X_c); tmpf2->left = tmpf1; CtlspFormulaIncrementRefCount(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } /* ll U lr + rl R ll == ((Xlr + rl) R ll) +lr */ if (left->type == Ctlsp_U_c && right->type == Ctlsp_R_c) { if (left->left == right->right) { tmpf1 = FormulaCreateWithType(Ctlsp_X_c); tmpf1->left = left->right; CtlspFormulaIncrementRefCount(left->right); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); if (right->left->type != Ctlsp_FALSE_c) { tmpf2 = FormulaCreateWithType(Ctlsp_OR_c); tmpf2->left = tmpf1; tmpf2->right = right->left; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(right->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); } tmpf2 = FormulaCreateWithType(Ctlsp_R_c); tmpf2->left = tmpf1; tmpf2->right = left->left; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(left->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_OR_c); tmpf2->left = tmpf1; tmpf2->right = left->right; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(left->right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } } /* ll R lr + lr U rr == ((Xrr + ll) R lr) + rr */ if (left->type == Ctlsp_R_c && right->type == Ctlsp_U_c) { if (left->right == right->left) { tmpf1 = FormulaCreateWithType(Ctlsp_X_c); tmpf1->left = right->right; CtlspFormulaIncrementRefCount(right->right); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); if (left->left->type != Ctlsp_FALSE_c) { tmpf2 = FormulaCreateWithType(Ctlsp_OR_c); tmpf2->left = tmpf1; tmpf2->right = left->left; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(left->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); } tmpf2 = FormulaCreateWithType(Ctlsp_R_c); tmpf2->left = tmpf1; tmpf2->right = left->right; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(left->right); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_OR_c); tmpf2->left = tmpf1; tmpf2->right = right->right; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(right->right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } } /* ll U lr + r , ll =>r == lr + r ??? */ if (left->type == Ctlsp_U_c) { if (Ctlsp_LtlFormulaSimplyImply(left->left, right)) { tmpf1 = FormulaCreateWithType(Ctlsp_OR_c); tmpf1->left = left->right; tmpf1->right = right; CtlspFormulaIncrementRefCount(left->right); CtlspFormulaIncrementRefCount(right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; } } /* l + rl U rr , rl => l == rr + l */ if (right->type == Ctlsp_U_c) { if (Ctlsp_LtlFormulaSimplyImply(right->left, left)) { tmpf1 = FormulaCreateWithType(Ctlsp_OR_c); tmpf1->left = left; tmpf1->right = right->right; CtlspFormulaIncrementRefCount(left); CtlspFormulaIncrementRefCount(right->right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; } } /* ll R lr + r , !ll => r == lr + r */ if (left->type == Ctlsp_R_c) { tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c); tmpf1->left = left->left; tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1); FREE(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); if (Ctlsp_LtlFormulaSimplyImply(tmpf2, right)) { tmpf1 = FormulaCreateWithType(Ctlsp_OR_c); tmpf1->left = left->right; tmpf1->right = right; CtlspFormulaIncrementRefCount(left->right); CtlspFormulaIncrementRefCount(right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; } } /* l + rl R rr , !rl => l == rr + l */ if (right->type == Ctlsp_R_c) { tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c); tmpf1->left = right->left; tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1); FREE(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); if (Ctlsp_LtlFormulaSimplyImply(tmpf2, left)) { tmpf1 = FormulaCreateWithType(Ctlsp_OR_c); tmpf1->left = left; tmpf1->right = right->right; CtlspFormulaIncrementRefCount(left); CtlspFormulaIncrementRefCount(right->right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; } } /* GF lrr + GF rrr = GF (lrr + rrr) */ if (Ctlsp_LtlFormulaIsGF(left) && Ctlsp_LtlFormulaIsGF(right)) { tmpf1 = FormulaCreateWithType(Ctlsp_OR_c); tmpf1->left = left->right->right; tmpf1->right = right->right->right; CtlspFormulaIncrementRefCount(left->right->right); CtlspFormulaIncrementRefCount(right->right->right); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_U_c); tmpf2->left = True; tmpf2->right = tmpf1; CtlspFormulaIncrementRefCount(True); CtlspFormulaIncrementRefCount(tmpf1); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_R_c); tmpf2->left = False; tmpf2->right = tmpf1; CtlspFormulaIncrementRefCount(False); CtlspFormulaIncrementRefCount(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } /* return (l + r) */ tmpf1 = FormulaCreateWithType(Ctlsp_OR_c); tmpf1->left = left; tmpf1->right = right; CtlspFormulaIncrementRefCount(left); CtlspFormulaIncrementRefCount(right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; case Ctlsp_U_c: /* l -> r : l U r == r */ if (Ctlsp_LtlFormulaSimplyImply(left, right)) return right; /* l U FALSE = FALSE */ if (right->type == Ctlsp_FALSE_c) return False; /* (X ll) U (X rl) == X (ll U rl) */ if (left->type == Ctlsp_X_c && right->type == Ctlsp_X_c) { tmpf1 = FormulaCreateWithType(Ctlsp_U_c); tmpf1->left = left->left; tmpf1->right = right->left; CtlspFormulaIncrementRefCount(left->left); CtlspFormulaIncrementRefCount(right->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_X_c); tmpf2->left = tmpf1; CtlspFormulaIncrementRefCount(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } /* TRUE U (X rl) == X( TRUE U rl ) */ if (left->type == Ctlsp_TRUE_c && right->type == Ctlsp_X_c) { tmpf1 = FormulaCreateWithType(Ctlsp_U_c); tmpf1->left = True; tmpf1->right = right->left; CtlspFormulaIncrementRefCount(True); CtlspFormulaIncrementRefCount(right->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_X_c); tmpf2->left = tmpf1; CtlspFormulaIncrementRefCount(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } /* l->rl : l U (rl U rr) == rl U rr */ if (right->type == Ctlsp_U_c) { if (Ctlsp_LtlFormulaSimplyImply(left, right->left)) { return right; } } /* (TRUE or anything) U (FG rrr) == FG rrr */ /* (TRUE or anything) U (GF rrr) == GF rrr */ if (/*left->type == Ctlsp_TRUE_c &&*/ Ctlsp_LtlFormulaIsFGorGF(right)) return right; /* TRUE U (rl * FG rrrr) = F(rl) * FG(rrrr) */ /* TRUE U (rl * GF rrrr) = F(rl) * GF(rrrr) */ if (left->type == Ctlsp_TRUE_c && right->type == Ctlsp_AND_c) { if (Ctlsp_LtlFormulaIsFGorGF(right->right)) { tmpf1 = FormulaCreateWithType(Ctlsp_U_c); tmpf1->left = True; tmpf1->right = right->left; CtlspFormulaIncrementRefCount(True); CtlspFormulaIncrementRefCount(right->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_AND_c); tmpf2->left = tmpf1; tmpf2->right = right->right; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(right->right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } } /* TRUE U (FG rlrr * rr) == (FG rlrr) * F(rr) */ /* TRUE U (GF rlrr * rr) == (GF rlrr) * F(rr) */ if (left->type == Ctlsp_TRUE_c && right->type == Ctlsp_AND_c) { if (Ctlsp_LtlFormulaIsFGorGF(right->left)) { tmpf1 = FormulaCreateWithType(Ctlsp_U_c); tmpf1->left = True; tmpf1->right = right->right; CtlspFormulaIncrementRefCount(True); CtlspFormulaIncrementRefCount(right->right); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_AND_c); tmpf2->left = right->left; tmpf2->right = tmpf1; CtlspFormulaIncrementRefCount(right->left); CtlspFormulaIncrementRefCount(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } } /* !r -> l : (l U r) == TRUE U r */ tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c); tmpf1->left = right; tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1); FREE(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); if (Ctlsp_LtlFormulaSimplyImply(tmpf2, left)) { tmpf1 = FormulaCreateWithType(Ctlsp_U_c); tmpf1->left = True; tmpf1->right = right; CtlspFormulaIncrementRefCount(True); CtlspFormulaIncrementRefCount(right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; } /* (ll + lr) U r, ll => r == (lr U r) */ if (left->type == Ctlsp_OR_c) { if (Ctlsp_LtlFormulaSimplyImply(left->left, right)) { tmpf1 = FormulaCreateWithType(Ctlsp_U_c); tmpf1->left = left->right; tmpf1->right = right; CtlspFormulaIncrementRefCount(left->right); CtlspFormulaIncrementRefCount(right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; } } /* (ll + lr) U r, lr => r == (ll U r) */ if (left->type == Ctlsp_OR_c) { if (Ctlsp_LtlFormulaSimplyImply(left->right, right)) { tmpf1 = FormulaCreateWithType(Ctlsp_U_c); tmpf1->left = left->left; tmpf1->right = right; CtlspFormulaIncrementRefCount(left->left); CtlspFormulaIncrementRefCount(right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; } } /* return (left U right) */ tmpf1 = FormulaCreateWithType(Ctlsp_U_c); tmpf1->left = left; tmpf1->right = right; CtlspFormulaIncrementRefCount(left); CtlspFormulaIncrementRefCount(right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; case Ctlsp_R_c: /* r -> l : l R r == r */ if (Ctlsp_LtlFormulaSimplyImply(right,left)) return right; /* l R TRUE == TRUE */ if (right->type == Ctlsp_TRUE_c) return True; /* (X ll) R (X rl) == X (ll R rl) */ if (left->type == Ctlsp_X_c && right->type == Ctlsp_X_c) { tmpf1 = FormulaCreateWithType(Ctlsp_R_c); tmpf1->left = left->left; tmpf1->right = right->left; CtlspFormulaIncrementRefCount(left->left); CtlspFormulaIncrementRefCount(right->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_X_c); tmpf2->left = tmpf1; CtlspFormulaIncrementRefCount(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } /* FALSE R (X rl) == X( FALSE R rl) */ if (left->type == Ctlsp_TRUE_c && right->type == Ctlsp_X_c) { tmpf1 = FormulaCreateWithType(Ctlsp_R_c); tmpf1->left = False; tmpf1->right = right->left; CtlspFormulaIncrementRefCount(False); CtlspFormulaIncrementRefCount(right->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_X_c); tmpf2->left = tmpf1; CtlspFormulaIncrementRefCount(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } /* rl->l : l R (rl R rr) == (rl R rr) */ if (right->type == Ctlsp_R_c) if (Ctlsp_LtlFormulaSimplyImply(right->left, left)) return right; /* (FALSE or anything) R (FG rrr) == FG rrr */ /* (FALSE or anything) R (GF rrr) == GF rrr */ if (/*left->type == Ctlsp_FALSE_c &&*/ Ctlsp_LtlFormulaIsFGorGF(right)) return right; /* FALSE R (rl + FG rrrr) = G(rl) + FG(rrrr) */ /* FALSE R (rl + GF rrrr) = G(rl) + GF(rrrr) */ if (left->type == Ctlsp_FALSE_c && right->type == Ctlsp_OR_c) { if (Ctlsp_LtlFormulaIsFGorGF(right->right)) { tmpf1 = FormulaCreateWithType(Ctlsp_R_c); tmpf1->left = False; tmpf1->right = right->left; CtlspFormulaIncrementRefCount(False); CtlspFormulaIncrementRefCount(right->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_OR_c); tmpf2->left = tmpf1; tmpf2->right = right->right; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(right->right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } } /* FALSE R (FG rlrr + rr) = FG(rlrr) + G(rr) */ /* FALSE R (GF rlrr + rr) = GF(rlrr) + G(rr) */ if (left->type == Ctlsp_FALSE_c && right->type == Ctlsp_OR_c) { if (Ctlsp_LtlFormulaIsFGorGF(right->left)) { tmpf1 = FormulaCreateWithType(Ctlsp_R_c); tmpf1->left = False; tmpf1->right = right->right; CtlspFormulaIncrementRefCount(False); CtlspFormulaIncrementRefCount(right->right); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(Ctlsp_OR_c); tmpf2->left = tmpf1; tmpf2->right = right->left; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(right->left); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } } /* r -> !l : (l R r) == FALSE R r */ tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c); tmpf1->left = left; tmpf2 = Ctlsp_LtlFormulaNegationNormalForm(tmpf1); FREE(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); if (Ctlsp_LtlFormulaSimplyImply(right, tmpf2)) { tmpf1 = FormulaCreateWithType(Ctlsp_R_c); tmpf1->left = False; tmpf1->right = right; CtlspFormulaIncrementRefCount(False); CtlspFormulaIncrementRefCount(right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; } /* r=>ll : (ll * lr) R r == lr R r */ if (left->type == Ctlsp_AND_c) { if (Ctlsp_LtlFormulaSimplyImply(right, left->left)) { tmpf1 = FormulaCreateWithType(Ctlsp_R_c); tmpf1->left = left->right; tmpf1->right = right; CtlspFormulaIncrementRefCount(left->right); CtlspFormulaIncrementRefCount(right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; } } /* r=>lr : (ll * lr) R r == ll R r */ if (left->type == Ctlsp_AND_c) { if (Ctlsp_LtlFormulaSimplyImply(right, left->right)) { tmpf1 = FormulaCreateWithType(Ctlsp_R_c); tmpf1->left = left->left; tmpf1->right = right; CtlspFormulaIncrementRefCount(left->left); CtlspFormulaIncrementRefCount(right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; } } /* return (left R right) */ tmpf1 = FormulaCreateWithType(Ctlsp_R_c); tmpf1->left = left; tmpf1->right = right; CtlspFormulaIncrementRefCount(left); CtlspFormulaIncrementRefCount(right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; case Ctlsp_X_c: /* X(TRUE) == TRUE */ /* X(FALSE) == FALSE */ if (left->type == Ctlsp_TRUE_c || left->type == Ctlsp_FALSE_c) return left; /* X(FGorGF) == FGorGF */ if (Ctlsp_LtlFormulaIsFGorGF(left)) return left; /* X(ll + FGorGF lrrr) == X(ll) + FGorGF lrrr */ /* X(ll * FGorGF lrrr) == X(ll) * FGorGF lrrr */ if (left->type == Ctlsp_AND_c || left->type == Ctlsp_OR_c) { if (Ctlsp_LtlFormulaIsFGorGF(left->right)) { tmpf1 = FormulaCreateWithType(Ctlsp_X_c); tmpf1->left = left->left; CtlspFormulaIncrementRefCount(left->left); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(left->type); tmpf2->left = tmpf1; tmpf2->right = left->right; CtlspFormulaIncrementRefCount(tmpf1); CtlspFormulaIncrementRefCount(left->right); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } } /* X(FGorGF llrr + lr) == FGorGF llrr + X(lr) */ /* X(FGorGF llrr * lr) == FGorGF llrr * X(lr) */ if (left->type == Ctlsp_AND_c || left->type == Ctlsp_OR_c) { if (Ctlsp_LtlFormulaIsFGorGF(left->left)) { tmpf1 = FormulaCreateWithType(Ctlsp_X_c); tmpf1->left = left->right; CtlspFormulaIncrementRefCount(left->right); tmpf1 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); tmpf2 = FormulaCreateWithType(left->type); tmpf2->left = left->left; tmpf2->right = tmpf1; CtlspFormulaIncrementRefCount(left->left); CtlspFormulaIncrementRefCount(tmpf1); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf2, Utable); return tmpf2; } } /* return X(left) */ tmpf1 = FormulaCreateWithType(Ctlsp_X_c); tmpf1->left = left; CtlspFormulaIncrementRefCount(left); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; case Ctlsp_NOT_c: /* return !(left) */ tmpf1 = FormulaCreateWithType(Ctlsp_NOT_c); tmpf1->left = left; CtlspFormulaIncrementRefCount(left); tmpf2 = Ctlsp_LtlFormulaHashIntoUniqueTable(tmpf1, Utable); return tmpf2; default: assert(0); } return NIL(Ctlsp_Formula_t); } /**Function******************************************************************** Synopsis [Increments the reference count of a formula.] Description [The function increments the reference count of a formula. If the formula is NULL, the function does nothing.] SideEffects [] SeeAlso [] ******************************************************************************/ void CtlspFormulaIncrementRefCount( Ctlsp_Formula_t *formula) { if(formula!=NIL(Ctlsp_Formula_t)) { ++(formula->refCount); } } /**Function******************************************************************** Synopsis [Decrements the reference count of a formula.] Description [The function decrements the reference count of formula and if the reference count reaches 0, the formula is freed. If the formula is NULL, the function does nothing. It is an error to decrement the reference count below 0.] SideEffects [] SeeAlso [] ******************************************************************************/ void CtlspFormulaDecrementRefCount( Ctlsp_Formula_t *formula) { if(formula!=NIL(Ctlsp_Formula_t)) { assert(formula->refCount>0); if(--(formula->refCount) == 0) CtlspFormulaFree(formula); } } /**Function******************************************************************** Synopsis [Adds formula to the end of globalFormulaArray.] SideEffects [Manipulates the global variable globalFormulaArray.] SeeAlso [CtlspYyparse] ******************************************************************************/ void CtlspFormulaAddToGlobalArray( Ctlsp_Formula_t * formula) { array_insert_last(Ctlsp_Formula_t *, globalFormulaArray, formula); } /**Function******************************************************************** Synopsis [Frees a CTL* formula.] Description [The function frees all memory associated with the formula, including all MDDs and all character strings (however, does not free dbgInfo.originalFormula). It also decrements the reference counts of its two chidren. The function does nothing if formula is NULL.] SideEffects [] SeeAlso [Ctlsp_FormulaArrayFree] ******************************************************************************/ void CtlspFormulaFree( Ctlsp_Formula_t * formula) { if (formula != NIL(Ctlsp_Formula_t)) { /* * Free any fields that are not NULL. */ if (formula->type == Ctlsp_ID_c){ FREE(formula->left); FREE(formula->right); } else { if (formula->left != NIL(Ctlsp_Formula_t)) { CtlspFormulaDecrementRefCount(formula->left); } if (formula->right != NIL(Ctlsp_Formula_t)) { CtlspFormulaDecrementRefCount(formula->right); } } if (formula->states != NIL(mdd_t)) mdd_free(formula->states); if (formula->underapprox != NIL(mdd_t)) mdd_free(formula->underapprox); if (formula->overapprox != NIL(mdd_t)) mdd_free(formula->overapprox); if (formula->dbgInfo.data != NIL(void)){ (*formula->dbgInfo.freeFn)(formula); } FREE(formula); } } /**Function******************************************************************** Synopsis [Create a binary string of given value with size of interval.] Description [The value is a binary string starting with 'b', a hexadecimal string starting with 'x', or an integer string. If value does not fit the interval, or the binary string is not of the correct length, 0 is return. Otherwise 1 is returned. The result string is saved at given pointer.] SideEffects [] SeeAlso [] ******************************************************************************/ int CtlspStringChangeValueStrToBinString( char *value, char *binValueStr, int interval) { int i; long int num, mask; double maxNum; char *ptr; mask = 1; maxNum = pow(2.0,(double)interval); errno = 0; if(value[0] == 'b'){ if ((int)strlen(value)-1 == interval){ for(i=1;i<=interval;i++){ if (value[i] == '0' || value[i] == '1'){ binValueStr[i-1] = value[i]; }else{ return 0; } } binValueStr[interval] = '\0'; }else{ return 0; } }else if (value[0] == 'x'){ for(i=1; i < (int)strlen(value); i++){ if (!isxdigit((int)value[i])){ return 0; } } num = strtol(++value,&ptr,16); if (errno) return 0; if (num >= maxNum) return 0; for(i=0;i= maxNum) return 0; mask = 1; for(i=0;i] Description [] SideEffects [The input string contains ...[num] and this function changes it to ....] SeeAlso [] ******************************************************************************/ void CtlspChangeBracket( char *inStr) { int i, j; char *str; j = 0; for (i=0;i<(int)strlen(inStr)+1;i++){ if (inStr[i] != ' '){ inStr[i-j] = inStr[i]; }else{ j++; } } if (changeBracket == 0) return; str = strchr(inStr,'['); if (str == NULL) return; *str = '<'; str = strchr(inStr,']'); *str = '>'; } /**Function******************************************************************** Synopsis [Parse a given vector string.] Description [Parse given vector string of the form of var and string var is returned. Other information such as i, j, interval between i and j, and increment or decrement from i to j are saved.] SideEffects [] SeeAlso [] ******************************************************************************/ char * CtlspGetVectorInfoFromStr( char *str, int *start, int *end, int *interval, int *inc) { char *str1, *str2, *str3; char *startStr, *endStr; char *name, *ptr; str1 = strchr(str,'['); str2 = strchr(str,':'); str3 = strchr(str,']'); startStr = ALLOC(char, str2-str1); endStr = ALLOC(char, str3-str2); name = ALLOC(char, str1-str+1); (void) strncpy(name, str, str1-str); (void) strncpy(startStr, str1+1, str2-str1-1); (void) strncpy(endStr, str2+1, str3-str2-1); startStr[str2-str1-1] = '\0'; endStr[str3-str2-1] = '\0'; name[str1-str] = '\0'; *start = strtol(startStr,&ptr,0); *end = strtol(endStr,&ptr,0); if(*start > *end){ *inc = -1; *interval = *start - *end + 1; } else { *inc = 1; *interval = *end - *start + 1; } FREE(startStr); FREE(endStr); return name; } /**Function******************************************************************** Synopsis [Insert macro formula into symbol table.] Description [If the name is already in table return 0, otherwise insert the formula into the table and return 1] SideEffects [] SeeAlso [] ******************************************************************************/ int CtlspFormulaAddToTable( char *name, Ctlsp_Formula_t *formula, st_table *macroTable) { if(macroTable == NIL(st_table)){ macroTable = st_init_table(strcmp, st_strhash); } if(st_is_member(macroTable, name)){ return 0; } st_insert(macroTable, name, (char *)formula); return 1; } /**Function******************************************************************** Synopsis [Get macro formula from symbol table] Description [If macro string is not found in table, NULL pointer is returned] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * CtlspFormulaFindInTable( char *name, st_table *macroTable) { Ctlsp_Formula_t *formula; if (st_lookup(macroTable, name, &formula)){ return (Ctlsp_FormulaDup(formula)); }else{ return NIL(Ctlsp_Formula_t); } } /**Function******************************************************************** Synopsis [] Description [] SideEffects [] SeeAlso [FormulaTestIsForallQuantifier] ******************************************************************************/ Ctlsp_FormulaClass CtlspCheckClassOfExistentialFormulaRecur( Ctlsp_Formula_t *formula, boolean parity) { Ctlsp_FormulaClass result; Ctlsp_FormulaType formulaType = Ctlsp_FormulaReadType(formula); Ctlsp_Formula_t *rightFormula, *leftFormula; Ctlsp_FormulaClass resultLeft, resultRight, tempResult, currentClass; /* Depending on the formula type, create result or recur */ switch (formulaType) { case Ctlsp_E_c: leftFormula = Ctlsp_FormulaReadLeftChild(formula); resultLeft = CtlspCheckClassOfExistentialFormulaRecur(leftFormula, parity); resultRight = Ctlsp_QuantifierFree_c; tempResult = CtlspResolveClass(resultLeft, resultRight); if (!parity){ currentClass = Ctlsp_ECTL_c; }else{ currentClass = Ctlsp_ACTL_c; } result = CtlspResolveClass(currentClass, tempResult); break; case Ctlsp_A_c: /* The formula is supposed to be only existential */ error_append("Inconsistency detected in function "); error_append("FormulaTestIsForallQuantifier\n"); result = Ctlsp_invalid_c; break; case Ctlsp_OR_c: case Ctlsp_AND_c: rightFormula = Ctlsp_FormulaReadRightChild(formula); leftFormula = Ctlsp_FormulaReadLeftChild(formula); resultLeft = CtlspCheckClassOfExistentialFormulaRecur(leftFormula, parity); resultRight = CtlspCheckClassOfExistentialFormulaRecur(rightFormula, parity); result = CtlspResolveClass(resultLeft, resultRight); break; case Ctlsp_NOT_c: parity = !parity; leftFormula = Ctlsp_FormulaReadLeftChild(formula); result = CtlspCheckClassOfExistentialFormulaRecur(leftFormula, parity); break; case Ctlsp_ID_c: case Ctlsp_TRUE_c: case Ctlsp_FALSE_c: result = Ctlsp_QuantifierFree_c; break; case Ctlsp_Cmp_c: result = Ctlsp_Mixed_c; break; default: error_append("Unexpected operator detected."); result = Ctlsp_invalid_c; break; } return result; } /* End of FormulaTestIsForallQuantifier */ /**Function******************************************************************** Synopsis [] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_FormulaClass CtlspResolveClass( Ctlsp_FormulaClass class1, Ctlsp_FormulaClass class2) { Ctlsp_FormulaClass result; if ((class1 == Ctlsp_Mixed_c) || (class2 == Ctlsp_Mixed_c)){ result = Ctlsp_Mixed_c; }else if (class1 == Ctlsp_QuantifierFree_c){ result = class2; }else if (class2 == Ctlsp_QuantifierFree_c){ result = class1; }else if (class1 == class2){ result = class1; }else{ result = Ctlsp_Mixed_c; } return result; } /**Function******************************************************************** Synopsis [Performs a recursive step of Ctlsp_FormulaConvertToCTL() ] Description [] SideEffects [] Remarks [] SeeAlso [] ******************************************************************************/ Ctlp_Formula_t * CtlspFormulaConvertToCTL( Ctlsp_Formula_t *formula) { Ctlp_Formula_t *newNode, *leftNode, *rightNode; Ctlsp_Formula_t *childNode; char *variableNameCopy, *valueNameCopy; if (formula == NIL(Ctlsp_Formula_t)) { return NIL(Ctlp_Formula_t); } /* * Recursively convert each subformula. */ switch(formula->type) { case Ctlsp_E_c: childNode = formula->left; switch(childNode->type) { case Ctlsp_X_c: newNode = Ctlp_FormulaCreate(Ctlp_EX_c, CtlspFormulaConvertToCTL(childNode->left), NIL(Ctlsp_Formula_t)); break; case Ctlsp_F_c: newNode = Ctlp_FormulaCreate(Ctlp_EF_c, CtlspFormulaConvertToCTL(childNode->left), NIL(Ctlsp_Formula_t)); break; case Ctlsp_U_c: newNode = Ctlp_FormulaCreate(Ctlp_EU_c, CtlspFormulaConvertToCTL(childNode->left), CtlspFormulaConvertToCTL(childNode->right)); break; case Ctlsp_R_c: /* E(f R g) => !A( !f U !g) */ leftNode = Ctlp_FormulaCreate(Ctlp_NOT_c, CtlspFormulaConvertToCTL(childNode->left), NIL(Ctlsp_Formula_t)); rightNode = Ctlp_FormulaCreate(Ctlp_NOT_c, CtlspFormulaConvertToCTL(childNode->right), NIL(Ctlsp_Formula_t)); newNode = Ctlp_FormulaCreate(Ctlp_AU_c, leftNode, rightNode); newNode = Ctlp_FormulaCreate(Ctlp_NOT_c, newNode, NIL(Ctlsp_Formula_t)); break; case Ctlsp_W_c: /* E(f W g) => !A(!g U !(f + g)) */ leftNode = Ctlp_FormulaCreate(Ctlp_NOT_c, CtlspFormulaConvertToCTL(childNode->right), NIL(Ctlsp_Formula_t)); rightNode = Ctlp_FormulaCreate(Ctlp_OR_c, CtlspFormulaConvertToCTL(childNode->left), CtlspFormulaConvertToCTL(childNode->right)); rightNode = Ctlp_FormulaCreate(Ctlp_NOT_c, rightNode, NIL(Ctlsp_Formula_t)); newNode = Ctlp_FormulaCreate(Ctlp_AU_c, leftNode, rightNode); newNode = Ctlp_FormulaCreate(Ctlp_NOT_c, newNode, NIL(Ctlsp_Formula_t)); break; case Ctlsp_G_c: newNode = Ctlp_FormulaCreate(Ctlp_EG_c, CtlspFormulaConvertToCTL(childNode->left), NIL(Ctlsp_Formula_t)); break; default: fail("Unexpected type"); } /* switch: childNode->type */ break; case Ctlsp_A_c: childNode = formula->left; switch(childNode->type) { case Ctlsp_X_c: newNode = Ctlp_FormulaCreate(Ctlp_AX_c, CtlspFormulaConvertToCTL(childNode->left), NIL(Ctlsp_Formula_t)); break; case Ctlsp_F_c: newNode = Ctlp_FormulaCreate(Ctlp_AF_c, CtlspFormulaConvertToCTL(childNode->left), NIL(Ctlsp_Formula_t)); break; case Ctlsp_U_c: newNode = Ctlp_FormulaCreate(Ctlp_AU_c, CtlspFormulaConvertToCTL(childNode->left), CtlspFormulaConvertToCTL(childNode->right)); break; case Ctlsp_R_c: /* A(f R g) => !E( !f U !g) */ leftNode = Ctlp_FormulaCreate(Ctlp_NOT_c, CtlspFormulaConvertToCTL(childNode->left), NIL(Ctlsp_Formula_t)); rightNode = Ctlp_FormulaCreate(Ctlp_NOT_c, CtlspFormulaConvertToCTL(childNode->right), NIL(Ctlsp_Formula_t)); newNode = Ctlp_FormulaCreate(Ctlp_EU_c, leftNode, rightNode); newNode = Ctlp_FormulaCreate(Ctlp_NOT_c, newNode, NIL(Ctlsp_Formula_t)); break; case Ctlsp_W_c: /* A(f W g) => !E(!g U !(f + g)) */ leftNode = Ctlp_FormulaCreate(Ctlp_NOT_c, CtlspFormulaConvertToCTL(childNode->right), NIL(Ctlsp_Formula_t)); rightNode = Ctlp_FormulaCreate(Ctlp_OR_c, CtlspFormulaConvertToCTL(childNode->left), CtlspFormulaConvertToCTL(childNode->right)); rightNode = Ctlp_FormulaCreate(Ctlp_NOT_c, rightNode, NIL(Ctlsp_Formula_t)); newNode = Ctlp_FormulaCreate(Ctlp_EU_c, leftNode, rightNode); newNode = Ctlp_FormulaCreate(Ctlp_NOT_c, newNode, NIL(Ctlsp_Formula_t)); break; case Ctlsp_G_c: newNode = Ctlp_FormulaCreate(Ctlp_AG_c, CtlspFormulaConvertToCTL(childNode->left), NIL(Ctlsp_Formula_t)); break; default: fail("Unexpected type"); } /* switch: childNode->type */ break; case Ctlsp_ID_c: /* Make a copy of the name, and create a new formula. */ variableNameCopy = util_strsav((char *)(formula->left)); valueNameCopy = util_strsav((char *)(formula->right)); newNode = Ctlp_FormulaCreate(Ctlp_ID_c, variableNameCopy, valueNameCopy); break; case Ctlsp_THEN_c: newNode = Ctlp_FormulaCreate(Ctlp_THEN_c, CtlspFormulaConvertToCTL(formula->left) , CtlspFormulaConvertToCTL(formula->right) ); break; case Ctlsp_OR_c: newNode = Ctlp_FormulaCreate(Ctlp_OR_c, CtlspFormulaConvertToCTL(formula->left) , CtlspFormulaConvertToCTL(formula->right) ); break; case Ctlsp_AND_c: newNode = Ctlp_FormulaCreate(Ctlp_AND_c, CtlspFormulaConvertToCTL(formula->left) , CtlspFormulaConvertToCTL(formula->right) ); break; case Ctlsp_NOT_c: newNode = Ctlp_FormulaCreate(Ctlp_NOT_c, CtlspFormulaConvertToCTL(formula->left) , CtlspFormulaConvertToCTL(formula->right) ); break; case Ctlsp_XOR_c: newNode = Ctlp_FormulaCreate(Ctlp_XOR_c, CtlspFormulaConvertToCTL(formula->left) , CtlspFormulaConvertToCTL(formula->right) ); break; case Ctlsp_EQ_c: newNode = Ctlp_FormulaCreate(Ctlp_EQ_c, CtlspFormulaConvertToCTL(formula->left) , CtlspFormulaConvertToCTL(formula->right) ); break; case Ctlsp_TRUE_c: newNode = Ctlp_FormulaCreate(Ctlp_TRUE_c, CtlspFormulaConvertToCTL(formula->left) , CtlspFormulaConvertToCTL(formula->right) ); break; case Ctlsp_FALSE_c: newNode = Ctlp_FormulaCreate(Ctlp_FALSE_c, CtlspFormulaConvertToCTL(formula->left) , CtlspFormulaConvertToCTL(formula->right) ); break; default: fail("Unexpected type"); } return newNode; } /* CtlspFormulaConvertToCTL() */ /**Function******************************************************************** Synopsis [Performs OR function] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * CtlspFunctionOr( Ctlsp_Formula_t *left, Ctlsp_Formula_t *right) { Ctlsp_Formula_t *result; if((Ctlsp_FormulaReadType(left) == Ctlsp_TRUE_c) || (Ctlsp_FormulaReadType(right) == Ctlsp_TRUE_c)){ result = Ctlsp_FormulaCreate(Ctlsp_TRUE_c, NIL(Ctlsp_Formula_t), NIL(Ctlsp_Formula_t));; } else if(Ctlsp_FormulaReadType(left) == Ctlsp_FALSE_c){ result = right; } else if(Ctlsp_FormulaReadType(right) == Ctlsp_FALSE_c){ result = left; } else result = Ctlsp_FormulaCreate(Ctlsp_OR_c, left, right); return result; } /**Function******************************************************************** Synopsis [Performs And function] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * CtlspFunctionAnd( Ctlsp_Formula_t *left, Ctlsp_Formula_t *right) { Ctlsp_Formula_t *result; if((Ctlsp_FormulaReadType(left) == Ctlsp_FALSE_c) || (Ctlsp_FormulaReadType(right) == Ctlsp_FALSE_c)){ result = Ctlsp_FormulaCreate(Ctlsp_FALSE_c, NIL(Ctlsp_Formula_t), NIL(Ctlsp_Formula_t));; } else if(Ctlsp_FormulaReadType(left) == Ctlsp_TRUE_c){ result = right; } else if(Ctlsp_FormulaReadType(right) == Ctlsp_TRUE_c){ result = left; } else result = Ctlsp_FormulaCreate(Ctlsp_AND_c, left, right); return result; } /**Function******************************************************************** Synopsis [Performs Then(Imply) function] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ Ctlsp_Formula_t * CtlspFunctionThen( Ctlsp_Formula_t *left, Ctlsp_Formula_t *right) { Ctlsp_Formula_t *result; if((Ctlsp_FormulaReadType(left) == Ctlsp_TRUE_c) && (Ctlsp_FormulaReadType(right) == Ctlsp_FALSE_c)){ result = Ctlsp_FormulaCreate(Ctlsp_FALSE_c, NIL(Ctlsp_Formula_t), NIL(Ctlsp_Formula_t)); } else if(Ctlsp_FormulaReadType(left) == Ctlsp_FALSE_c){ result = Ctlsp_FormulaCreate(Ctlsp_TRUE_c, NIL(Ctlsp_Formula_t), NIL(Ctlsp_Formula_t)); } else if((Ctlsp_FormulaReadType(left) == Ctlsp_TRUE_c) && (Ctlsp_FormulaReadType(right) == Ctlsp_TRUE_c)){ result = Ctlsp_FormulaCreate(Ctlsp_TRUE_c, NIL(Ctlsp_Formula_t), NIL(Ctlsp_Formula_t)); } else result = Ctlsp_FormulaCreate(Ctlsp_THEN_c, left, right); return result; } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Creates a CTL* formula with just the type set.] Description [Calls Ctlsp_FormulaCreate with type, and all other fields NULL.] SideEffects [] SeeAlso [Ctlsp_FormulaCreate] ******************************************************************************/ static Ctlsp_Formula_t * FormulaCreateWithType( Ctlsp_FormulaType type) { return (Ctlsp_FormulaCreate(type, NIL(Ctlsp_Formula_t), NIL(Ctlsp_Formula_t))); } /**Function******************************************************************** Synopsis [The comparison function for the formula unique table.] Description [The function takes as parameters two CTL* formulae. It compares the formula type, the left child and the right child, and returns 0 if they match. Otherwise, it returns -1.] SideEffects [] SeeAlso [FormulaHash] ******************************************************************************/ static int FormulaCompare( const char *key1, const char *key2) { Ctlsp_Formula_t *formula1 = (Ctlsp_Formula_t *) key1; Ctlsp_Formula_t *formula2 = (Ctlsp_Formula_t *) key2; assert(key1 != NIL(char)); assert(key2 != NIL(char)); if(formula1->type != formula2->type) { return -1; } if(formula1->type == Ctlsp_ID_c) { if(strcmp((char *) (formula1->left), (char *) (formula2->left)) || strcmp((char *) (formula1->right), (char *) (formula2->right))) { return -1; } else return 0; } else { if(formula1->left != formula2->left) return -1; if(formula1->right != formula2->right) return -1; if (formula1->type == Ctlsp_Cmp_c && formula1->compareValue != formula2->compareValue) { return -1; } return 0; } } /**Function******************************************************************** Synopsis [The hash function for the formula unique table.] Description [The function takes as parameter a CTL* formula. If the formula type is Ctlsp_ID_c, st_strhash is used with a concatenation of left and right children as the key string. Otherwise, something very similar to st_ptrhash is done.] SideEffects [] SeeAlso [FormulaCompare] ******************************************************************************/ static int FormulaHash( char *key, int modulus) { char *hashString; int hashValue; Ctlsp_Formula_t *formula = (Ctlsp_Formula_t *) key; if(formula->type==Ctlsp_ID_c) { hashString = util_strcat3((char *) (formula->left), (char *) (formula->right), ""); hashValue = st_strhash(hashString, modulus); FREE(hashString); return hashValue; } return (int) ((((unsigned long) formula->left >>2) + ((unsigned long) formula->right >>2)) % modulus); } /**Function******************************************************************** Synopsis [Hashes the formula into the unique table.] Description [The function takes a formula and hashes it and all its subformulae into a unique table. It returns the unique formula identical to the formula being hashed. The formula returned will have maximum sharing with the formulae that are already present in uniqueTable. It returns NIL(Ctlsp_Formula_t) if the formula is NIL(Ctlsp_Formula_t).] SideEffects [If a copy of some subformula of formula is present in uniqueTable then the copy is substituted for it and the reference count of the subformula is decremented.] SeeAlso [FormulaCompare] ******************************************************************************/ static Ctlsp_Formula_t * FormulaHashIntoUniqueTable( Ctlsp_Formula_t *formula, st_table *uniqueTable) { Ctlsp_Formula_t *uniqueFormula, *uniqueLeft, *uniqueRight; if(formula == NIL(Ctlsp_Formula_t)) return NIL(Ctlsp_Formula_t); if(st_lookup(uniqueTable, formula, &uniqueFormula)) { return uniqueFormula; } else { if(formula->type == Ctlsp_ID_c) { st_insert(uniqueTable, (char *) formula, (char *) formula); return formula; } else { uniqueLeft = FormulaHashIntoUniqueTable(formula->left, uniqueTable); if(uniqueLeft != NIL(Ctlsp_Formula_t)) if(uniqueLeft != formula->left) { CtlspFormulaDecrementRefCount(formula->left); formula->left = uniqueLeft; CtlspFormulaIncrementRefCount(formula->left); } uniqueRight = FormulaHashIntoUniqueTable(formula->right, uniqueTable); if(uniqueRight != NIL(Ctlsp_Formula_t)) if(uniqueRight != formula->right) { CtlspFormulaDecrementRefCount(formula->right); formula->right = uniqueRight; CtlspFormulaIncrementRefCount(formula->right); } if(st_lookup(uniqueTable, formula, &uniqueFormula)) { return uniqueFormula; } else { st_insert(uniqueTable, (char *) formula, (char *) formula); return formula; } } } } /**Function******************************************************************** Synopsis [Create SNF propositional variable if the passed formula is not propositional] Description [If formula is not propositional, generate SNF for the formula first and returned the renamed variable] SideEffects [Add the new generated SNF rule to formulaArray] SeeAlso [Ctlsp_LtlTranslateIntoSNFRecursive] ******************************************************************************/ static Ctlsp_Formula_t * createSNFnode( Ctlsp_Formula_t *formula, array_t *formulaArray, int *index) { Ctlsp_Formula_t *newNode; if(!Ctlsp_LtlFormulaIsPropositional(formula)){ newNode = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strcat3(" SNFx","_", util_inttostr((*index)++)), (void *)util_strsav("1")); Ctlsp_LtlTranslateIntoSNFRecursive(newNode, formula, formulaArray, index); return newNode; } else { return Ctlsp_FormulaDup(formula); } }