Ctlsp_FormulaClass 
Ctlsp_CheckClassOfExistentialFormulaArray(
  array_t * formulaArray 
)
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.

See Also Ctlsp_CheckClassOfExistentialFormula 

Ctlsp_FormulaClass 
Ctlsp_CheckClassOfExistentialFormula(
  Ctlsp_Formula_t * formula 
)
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. 


Ctlsp_Formula_t * 
Ctlsp_CtlFormulaToCtlsp(
  Ctlp_Formula_t * F 
)
Translate a CTL formula into a CTL* formula. 


void 
Ctlsp_End(
    
)
Ends the CTL* parser package.

See Also Ctlsp_Init 

array_t * 
Ctlsp_FileParseFormulaArray(
  FILE * fp 
)
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.

Side Effects Manipulates the global variables globalFormulaArray, CtlspGlobalError and CtlspGlobalFormula.

See Also Ctlsp_FormulaArrayFree Ctlsp_FormulaPrint 

void 
Ctlsp_FlushStates(
  Ctlsp_Formula_t * formula 
)
Recursively frees states, underapprox and overapprox fields of Ctlsp_Formula_t, and the debug data

See Also Ctlsp_FormulaFree 

void 
Ctlsp_FormulaArrayAddLtlFairnessConstraints(
  array_t * formulaArray, array of LTL formulae
  array_t * constraintArray array of fairness constraints
)
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.

Side Effects formulaArray is modified 


array_t * 
Ctlsp_FormulaArrayConvertToCTL(
  array_t * formulaArray 
)
This function take an array of CTL* formulas and return an array of CTL formulas if applicable. Function returns NIL if any CTL * formula can't be converted to CTL formul. The return CTL formulae share absolutely nothing with the original CTL* formulae (not even a string).

See Also Ctlsp_FormulaConvertToCTL 

array_t * 
Ctlsp_FormulaArrayConvertToDAG(
  array_t * formulaArray 
)
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.

Side Effects 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. 


array_t * 
Ctlsp_FormulaArrayConvertToLTL(
  array_t * formulaArray 
)
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). 


void 
Ctlsp_FormulaArrayFree(
  array_t * formulaArray of Ctlsp_Formula_t
)
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.

See Also Ctlsp_FormulaFree 

Ctlp_Formula_t * 
Ctlsp_FormulaConvertToCTL(
  Ctlsp_Formula_t * formula 
)
This function take a formula in CTL* and return the 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

See Also Ctlsp_FormulaArrayConvertToCTL 

char * 
Ctlsp_FormulaConvertToString(
  Ctlsp_Formula_t * formula 
)
Returns formula as a character string. All subformulas are delimited by parenthesis. Does nothing if passed a NULL formula. 


Ctlsp_Formula_t * 
Ctlsp_FormulaCreateAXMult(
  char * string, 
  Ctlsp_Formula_t * formula 
)
This function returns a formula, which is the multiple times of AX. The given string includes the number of depth 


Ctlsp_Formula_t * 
Ctlsp_FormulaCreateEXMult(
  char * string, 
  Ctlsp_Formula_t * formula 
)
This function returns a formula, which is the multiple times of EX. The given string includes the number of depth 


Ctlsp_Formula_t * 
Ctlsp_FormulaCreateEquiv(
  char * left, 
  char * right 
)
This function assumes that each child is defined in binary domain. Enumerate type is not supported 


Ctlsp_Formula_t * 
Ctlsp_FormulaCreateOr(
  char * name, 
  char * valueStr 
)
This function returns Ctlsp_Formula_t for name = {v1,v2,...}. In case of failure, a NULL pointer is returned. 


Ctlsp_Formula_t * 
Ctlsp_FormulaCreateVectorAnd(
  char * nameVector, 
  char * value 
)
This function returns Ctlsp_Formula_t for nameVector = value, nameVector is a form of var[i:j 


Ctlsp_Formula_t * 
Ctlsp_FormulaCreateVectorEquiv(
  char * left, 
  char * right 
)
This function returns a formula, which is the AND of a bitwise equivalence 


Ctlsp_Formula_t * 
Ctlsp_FormulaCreateVectorOr(
  char * nameVector, 
  char * valueStr 
)
This function returns Ctlsp_Formula_t for nameVector = valueStr, nameVector is a form of var[i:j 


Ctlsp_Formula_t * 
Ctlsp_FormulaCreateXMult(
  char * string, 
  Ctlsp_Formula_t * formula 
)
This function returns a formula, which is the multiple times of AX. The given string includes the number of depth 


Ctlsp_Formula_t * 
Ctlsp_FormulaCreate(
  Ctlsp_FormulaType  type, 
  void * left_, 
  void * right_ 
)
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.

See Also CtlspFormulaDecrementRefCount 

Ctlsp_Formula_t * 
Ctlsp_FormulaDup(
  Ctlsp_Formula_t * formula 
)
Recursively duplicate a formula. Does nothing if the formula is NIL. Does not copy mdd for states, underapprox, overapprox, dbgInfo. 


void 
Ctlsp_FormulaFree(
  Ctlsp_Formula_t * formula 
)
The function decrements the refCount of the formula. As a consequence, if the refCount becomes 0, the formula is freed.

See Also CtlspFormulaFree CtlspDecrementRefCount 

char * 
Ctlsp_FormulaGetTypeString(
  Ctlsp_Formula_t * formula 
)
Returns a string for each formula type. 


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

See Also Ctlsp_FormulaSetStates 

mdd_t * 
Ctlsp_FormulaObtainStates(
  Ctlsp_Formula_t * formula 
)
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.

See Also Ctlsp_FormulaSetStates 

void 
Ctlsp_FormulaPrint(
  FILE * fp, 
  Ctlsp_Formula_t * formula 
)
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. 


int 
Ctlsp_FormulaReadABIndex(
  Ctlsp_Formula_t * formula 
)
Returns the Alpha-Beta Index. used for LTL->AUT 


Ctlsp_ClassOfCTLFormula 
Ctlsp_FormulaReadClassOfCTL(
  Ctlsp_Formula_t * formula 
)
Get the type of a CTL formula 


Ctlsp_ClassOfFormula 
Ctlsp_FormulaReadClass(
  Ctlsp_Formula_t * formula 
)
Get the current class of a CTL* sub-formula 


int 
Ctlsp_FormulaReadCompareValue(
  Ctlsp_Formula_t * formula 
)
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.

See Also ctlsp.h 

void * 
Ctlsp_FormulaReadDebugData(
  Ctlsp_Formula_t * formula 
)
Returns the debug data associated with a formula. This data is uninterpreted by the ctlsp package.

See Also Ctlsp_FormulaSetDbgInfo 

int 
Ctlsp_FormulaReadLabelIndex(
  Ctlsp_Formula_t * formula 
)
Returns the Label Index. used for LTL->AUT 


Ctlsp_Formula_t * 
Ctlsp_FormulaReadLeftChild(
  Ctlsp_Formula_t * formula 
)
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.

See Also Ctlsp_FormulaReadRightChild 

char 
Ctlsp_FormulaReadMarked(
  Ctlsp_Formula_t * formula 
)
Returns the marked. used for LTL->AUT 


Ctlsp_Formula_t * 
Ctlsp_FormulaReadOriginalFormula(
  Ctlsp_Formula_t * formula 
)
Returns original formula corresponding to converted formula. 


char 
Ctlsp_FormulaReadRhs(
  Ctlsp_Formula_t * formula 
)
Returns the RHS. used for LTL->AUT 


Ctlsp_Formula_t * 
Ctlsp_FormulaReadRightChild(
  Ctlsp_Formula_t * formula 
)
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.

See Also Ctlsp_FormulaReadLeftChild 

Ctlsp_FormulaType 
Ctlsp_FormulaReadType(
  Ctlsp_Formula_t * formula 
)
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.

See Also ctlsp.h 

char * 
Ctlsp_FormulaReadValueName(
  Ctlsp_Formula_t * formula 
)
Reads the value name of a leaf formula. It is an error to call this function on a non-leaf formula. 


char * 
Ctlsp_FormulaReadVariableName(
  Ctlsp_Formula_t * formula 
)
Reads the variable name of a leaf formula. It is an error to call this function on a non-leaf formula. 


void 
Ctlsp_FormulaResetMarked(
  Ctlsp_Formula_t * formula 
)
Reset the Alpha-Beta Index. used for LTL->AUT 


void 
Ctlsp_FormulaResetRhs(
  Ctlsp_Formula_t * formula 
)
Reset the RHS. used for LTL->AUT 


void 
Ctlsp_FormulaSetABIndex(
  Ctlsp_Formula_t * formula, 
  int  ab_idx 
)
Set the Alpha-Beta Index. used for LTL->AUT 


void 
Ctlsp_FormulaSetApproxStates(
  Ctlsp_Formula_t * formula, 
  mdd_t * states, 
  Ctlsp_Approx_t  approx 
)
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.

See Also Ctlsp_FormulaObtainStates 

void 
Ctlsp_FormulaSetClassOfCTL(
  Ctlsp_Formula_t * formula, 
  Ctlsp_ClassOfCTLFormula  newCTLclass 
)
Set the class of CTL 


void 
Ctlsp_FormulaSetClass(
  Ctlsp_Formula_t * formula, 
  Ctlsp_ClassOfFormula  newClass 
)
Set the class of a formula 


void 
Ctlsp_FormulaSetDbgInfo(
  Ctlsp_Formula_t * formula, 
  void * data, 
  Ctlsp_DbgInfoFreeFn  freeFn 
)
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.

See Also Ctlsp_FormulaReadDebugData 

void 
Ctlsp_FormulaSetLabelIndex(
  Ctlsp_Formula_t * formula, 
  int  label_idx 
)
Set the Label Index. used for LTL->AUT 


void 
Ctlsp_FormulaSetMarked(
  Ctlsp_Formula_t * formula 
)
Set the Alpha-Beta Index. used for LTL->AUT 


void 
Ctlsp_FormulaSetRhs(
  Ctlsp_Formula_t * formula 
)
Set the RHS. used for LTL->AUT 


void 
Ctlsp_FormulaSetStates(
  Ctlsp_Formula_t * formula, 
  mdd_t * states 
)
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.

See Also Ctlsp_FormulaObtainStates 

boolean 
Ctlsp_FormulaTestIsConverted(
  Ctlsp_Formula_t * formula 
)
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. 


boolean 
Ctlsp_FormulaTestIsQuantifierFree(
  Ctlsp_Formula_t * formula 
)
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. 


void 
Ctlsp_Init(
    
)
Initializes the CTL* parser package.

See Also Ctlsp_End 

int 
Ctlsp_LtlFormulaArrayIsPropositional(
  array_t * formulaArray 
)
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.

Side Effects none

See Also Ctlsp_LtlFormulaIsPropositional 

void 
Ctlsp_LtlFormulaClearMarks(
  Ctlsp_Formula_t * F 
)
Recursively clear the .marked field for all its sub-formulae. 


int 
Ctlsp_LtlFormulaCountNumber(
  Ctlsp_Formula_t * F 
)
Recursively clear the .marked field for all its sub-formulae. 


st_table * 
Ctlsp_LtlFormulaCreateUniqueTable(
    
)
Use FormulaHash and formulaCompare. 


int 
Ctlsp_LtlFormulaDepth(
  Ctlsp_Formula_t * formula 
)
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.

See Also Ctlsp_LtlFormulaExpandAbbreviation 

Ctlsp_Formula_t * 
Ctlsp_LtlFormulaExpandAbbreviation(
  Ctlsp_Formula_t * formula 
)
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 


Ctlsp_Formula_t * 
Ctlsp_LtlFormulaHashIntoUniqueTable(
  Ctlsp_Formula_t * F, 
  st_table * uniqueTable 
)
It is possible that 'F' is freed, in which case a new 'F' is returned. 


int 
Ctlsp_LtlFormulaIsAtomicPropositional(
  Ctlsp_Formula_t * F 
)
TRUE/FALSE/literal. literal: an atomic proposition or the negation of an atomic popposition.

Side Effects none

See Also Ctlsp_LtlFormulaIsPropositional 

int 
Ctlsp_LtlFormulaIsElementary2(
  Ctlsp_Formula_t * F 
)
Return True iff formula is an elementary formula. This is the original definition used in "Wring": it's a TRUE/FALSE/literal/X-formula. 


int 
Ctlsp_LtlFormulaIsElementary(
  Ctlsp_Formula_t * F 
)
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. 


int 
Ctlsp_LtlFormulaIsFGorGF(
  Ctlsp_Formula_t * F 
)
TRUE U (FALSE R p).

See Also Ctlsp_LtlFormulaIsGF Ctlsp_LtlFormulaIsFG 

int 
Ctlsp_LtlFormulaIsFG(
  Ctlsp_Formula_t * F 
)
TRUE U (FALSE R p).

See Also Ctlsp_LtlFormulaIsGF Ctlsp_LtlFormulaIsFGorGF 

boolean 
Ctlsp_LtlFormulaIsFp(
  Ctlsp_Formula_t * formula 
)
F(p) = TRUE U p in abbreviation-free LTL formulae.

See Also Ctlsp_isPropositionalFormula 

int 
Ctlsp_LtlFormulaIsGFp(
  Ctlsp_Formula_t * formula 
)
GFp = FALSE R (TRUE U p) in abbreviation-free LTL formulae. 


int 
Ctlsp_LtlFormulaIsGF(
  Ctlsp_Formula_t * F 
)
FALSE R (TRUE U p).

See Also Ctlsp_LtlFormulaIsFG Ctlsp_LtlFormulaIsFGorGF 

boolean 
Ctlsp_LtlFormulaIsGp(
  Ctlsp_Formula_t * formula 
)
G(p) = FALSE R p in abbreviation-free LTL formulae.

See Also Ctlsp_isPropositionalFormula 

int 
Ctlsp_LtlFormulaIsPropositional(
  Ctlsp_Formula_t * F 
)
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.

Side Effects none

See Also Ctlsp_LtlFormulaIsAtomicPropositional 

boolean 
Ctlsp_LtlFormulaIsSafety(
  Ctlsp_Formula_t * formula 
)
The characterization of LTL formula as a sfety formula is taken from the papaer 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. 


Ctlsp_Formula_t * 
Ctlsp_LtlFormulaNegationNormalForm(
  Ctlsp_Formula_t * formula 
)
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/ ! . 


Ctlsp_Formula_t * 
Ctlsp_LtlFormulaSimpleRewriting(
  Ctlsp_Formula_t * formula 
)
We return a formula which shares nothing with the input formula 


int 
Ctlsp_LtlFormulaSimplyImply(
  Ctlsp_Formula_t * from, 
  Ctlsp_Formula_t * to 
)
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"). 


boolean 
Ctlsp_LtlFormulaTestIsBounded(
  Ctlsp_Formula_t * formula, 
  int * depth 
)
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.

Side Effects The depth is returned as a side effect. (Only if the function returns TRUE.)

See Also Ctlsp_LtlFormulaExpandAbbreviation Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe 

boolean 
Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(
  Ctlsp_Formula_t * formula 
)
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.

Side Effects none

See Also Ctlsp_LtlFormulaNegationNormalForm Ctlsp_LtlFormulaTestIsBounded 

void 
Ctlsp_LtlSetClass(
  Ctlsp_Formula_t * formula 
)
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.

See Also ctlspInt.h Ctlsp_FormulaCreate 

void 
Ctlsp_LtlTranslateIntoSNFRecursive(
  Ctlsp_Formula_t * propNode, 
  Ctlsp_Formula_t * formula, 
  array_t * formulaArray, 
  int * index 
)
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 ! . 


array_t * 
Ctlsp_LtlTranslateIntoSNF(
  Ctlsp_Formula_t * formula 
)
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.

See Also Ctlsp_LtlTranslateIntoSNFRecursive 

Ctlsp_Formula_t * 
Ctlsp_LtllFormulaNegate(
  Ctlsp_Formula_t * ltlFormula 
)
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. 


Ctlp_Formula_t * 
Ctlsp_PropositionalFormulaToCTL(
  Ctlsp_Formula_t * formula 
)
A wrapper to CtlspFormulaConvertToCTL

See Also Ctlsp_FormulaArrayConvertToCTL 

int 
Ctlsp_isCtlFormula(
  Ctlsp_Formula_t * formula 
)
Return true if CTL* formula is an CTL formula.

See Also Ctlsp_FormulaReadClassOfCTL() 

int 
Ctlsp_isLtlFormula(
  Ctlsp_Formula_t * formula 
)
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)

See Also Ctlsp_FormulaReadClass() 

int 
Ctlsp_isPropositionalFormula(
  Ctlsp_Formula_t * formula 
)
Return true if CTL* formula is a propositional formula.

See Also Ctlsp_FormulaReadClass()
Last updated on 20050519 00h50