/**CHeaderFile***************************************************************** FileName [ctlsp.h] PackageName [ctlsp] Synopsis [Routines for parsing, writing and accessing CTL* formulas.] Description [This package implements a parser for CTL* formulas. CTL* is a language used to describe properties of systems.] SeeAlso [] Author [Mohammad Awedh] 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.] Revision [$Id: ctlsp.h,v 1.28 2009/04/11 01:32:36 fabio Exp $] ******************************************************************************/ #ifndef _CTLSP #define _CTLSP #include "vm.h" #include "ctlp.h" /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /**Enum************************************************************************ Synopsis [Types of operators allowed in CTL* formulas.] Description [The types of nodes in a CTL* formula parse tree. ID, TRUE, and FALSE are leaves, and all others are internal nodes.] SeeAlso [Ctlsp_FormulaReadType] ******************************************************************************/ typedef enum { Ctlsp_E_c, /* there exists */ Ctlsp_A_c, /* for all paths*/ Ctlsp_X_c, /* Next */ Ctlsp_G_c, /* globally */ Ctlsp_F_c, /* finally */ Ctlsp_U_c, /* until (not symmetric in args) */ Ctlsp_R_c, /* release (not symmetric in args) */ Ctlsp_W_c, /* weak until (not symmetric in args) */ Ctlsp_OR_c, /* Boolean disjunction */ Ctlsp_AND_c, /* Boolean conjunction */ Ctlsp_NOT_c, /* Boolean negation*/ Ctlsp_THEN_c, /* Boolean implies (not symmetric) */ Ctlsp_XOR_c, /* Boolean XOR */ Ctlsp_EQ_c, /* Boolean equal */ Ctlsp_ID_c, /* an atomic proposition */ Ctlsp_TRUE_c, /* tautology (used only for translation to exist. form) */ Ctlsp_FALSE_c, /* empty (used only for translation to exist. form) */ Ctlsp_Fwd_c, /* forward */ Ctlsp_Y_c, /* previous state */ Ctlsp_H_c, /* past */ Ctlsp_Init_c, /* initial states */ Ctlsp_Cmp_c /* compare two leaves in forward CTL* */ } Ctlsp_FormulaType; /**Enum************************************************************************ Synopsis [Types of operators allowed in CTL formulas.] Description [The types of nodes in a CTL formula parse tree. ID, TRUE, and FALSE are leaves, and all others are internal nodes.] SeeAlso [Ctlsp_FormulaReadType] ******************************************************************************/ typedef enum { Ctlsp_ECTL_c, Ctlsp_ACTL_c, Ctlsp_Mixed_c, Ctlsp_QuantifierFree_c, Ctlsp_LTL_c, Ctlsp_stateFormuls_c, Ctlsp_invalid_c } Ctlsp_FormulaClass; /**Enum************************************************************************ Synopsis [Types of approximations that are possible] Description [We can have overapproximations, underapproximations, exact approximations, or incomparable sets. Question: is ctlsp the right place for this? It is used in ctlsp, mc, rch. (RB)] SeeAlso [] ******************************************************************************/ typedef enum { Ctlsp_Incomparable_c, Ctlsp_Underapprox_c, Ctlsp_Overapprox_c, Ctlsp_Exact_c } Ctlsp_Approx_t; /**Enum************************************************************************ Synopsis [ Class of CTL* formulas.] Description [The classes of nodes in CTL* formula.] Note: [We explicity assign values to the enumerated values becuase we are going to use the numerical values in determining the class of a CTL* formula. These values are used in table1, table2, and table3 macros.] SeeAlso [ctlspInt.h] ******************************************************************************/ typedef enum { Ctlsp_propformula_c = 0, Ctlsp_LTLformula_c = 1, Ctlsp_stateformula_c = 2, Ctlsp_pathformula_c = 3 } Ctlsp_ClassOfFormula; /**Enum************************************************************************ Synopsis [ Class of CTL formulas.] Description [The classes of CTL formula. This help to find out whether a formula is CTL or not. During the parsing of a CTL* formula the parser determines whether the subformula is a CTL formula, (Ctlsp_CTL_c) can be CTL formula (Ctlsp_PathCTL_c), or not CTL formula (Ctlsp_NotCTL_c).] SeeAlso [ctlsp.y] ******************************************************************************/ typedef enum { Ctlsp_NotCTL_c, Ctlsp_PathCTL_c, Ctlsp_CTL_c } Ctlsp_ClassOfCTLFormula; /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ typedef struct CtlspFormulaStruct Ctlsp_Formula_t; typedef void (*Ctlsp_DbgInfoFreeFn) (Ctlsp_Formula_t *); /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Function prototypes */ /*---------------------------------------------------------------------------*/ EXTERN void Ctlsp_Init(void); EXTERN void Ctlsp_End(void); EXTERN array_t * Ctlsp_FileParseFormulaArray(FILE * fp); EXTERN array_t * Ctlsp_FileParseCTLFormulaArray(FILE * fp); EXTERN char * Ctlsp_FormulaConvertToString(Ctlsp_Formula_t * formula); EXTERN void Ctlsp_FormulaPrint(FILE * fp, Ctlsp_Formula_t * formula); EXTERN Ctlsp_FormulaType Ctlsp_FormulaReadType(Ctlsp_Formula_t * formula); EXTERN int Ctlsp_FormulaReadCompareValue(Ctlsp_Formula_t * formula); EXTERN char * Ctlsp_FormulaReadVariableName(Ctlsp_Formula_t * formula); EXTERN char * Ctlsp_FormulaReadValueName(Ctlsp_Formula_t * formula); EXTERN Ctlsp_Formula_t * Ctlsp_FormulaReadLeftChild(Ctlsp_Formula_t * formula); EXTERN Ctlsp_Formula_t * Ctlsp_FormulaReadRightChild(Ctlsp_Formula_t * formula); EXTERN mdd_t * Ctlsp_FormulaObtainStates(Ctlsp_Formula_t * formula); EXTERN mdd_t * Ctlsp_FormulaObtainApproxStates(Ctlsp_Formula_t *formula, Ctlsp_Approx_t approx); EXTERN void Ctlsp_FormulaSetStates(Ctlsp_Formula_t * formula, mdd_t * states); EXTERN void Ctlsp_FormulaSetApproxStates(Ctlsp_Formula_t * formula, mdd_t * states, Ctlsp_Approx_t approx); EXTERN void Ctlsp_FormulaSetDbgInfo(Ctlsp_Formula_t * formula, void *data, Ctlsp_DbgInfoFreeFn freeFn); EXTERN void * Ctlsp_FormulaReadDebugData(Ctlsp_Formula_t * formula); EXTERN boolean Ctlsp_FormulaTestIsConverted(Ctlsp_Formula_t * formula); EXTERN boolean Ctlsp_FormulaTestIsQuantifierFree(Ctlsp_Formula_t *formula); EXTERN Ctlsp_Formula_t * Ctlsp_FormulaReadOriginalFormula(Ctlsp_Formula_t * formula); EXTERN int Ctlsp_FormulaReadABIndex(Ctlsp_Formula_t * formula); EXTERN void Ctlsp_FormulaSetABIndex(Ctlsp_Formula_t * formula, int ab_idx); EXTERN int Ctlsp_FormulaReadLabelIndex(Ctlsp_Formula_t * formula); EXTERN void Ctlsp_FormulaSetLabelIndex(Ctlsp_Formula_t * formula, int label_idx); EXTERN char Ctlsp_FormulaReadRhs(Ctlsp_Formula_t * formula); EXTERN void Ctlsp_FormulaSetRhs(Ctlsp_Formula_t * formula); EXTERN void Ctlsp_FormulaResetRhs(Ctlsp_Formula_t * formula); EXTERN char Ctlsp_FormulaReadMarked(Ctlsp_Formula_t * formula); EXTERN void Ctlsp_FormulaSetMarked(Ctlsp_Formula_t * formula); EXTERN void Ctlsp_FormulaResetMarked(Ctlsp_Formula_t * formula); EXTERN void Ctlsp_FormulaFree(Ctlsp_Formula_t *formula); EXTERN void Ctlsp_FlushStates(Ctlsp_Formula_t * formula); EXTERN Ctlsp_Formula_t * Ctlsp_FormulaDup(Ctlsp_Formula_t * formula); EXTERN void Ctlsp_FormulaArrayFree(array_t * formulaArray); EXTERN array_t * Ctlsp_FormulaArrayConvertToDAG(array_t *formulaArray); EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreate(Ctlsp_FormulaType type, void * left_, void * right_); EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreateOr(char *name, char *valueStr); EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreateVectorAnd(char *nameVector, char *value); EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreateVectorOr(char *nameVector, char *valueStr); EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreateEquiv(char *left, char *right); EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreateVectorEquiv(char *left, char *right); EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreateXMult(char *string, Ctlsp_Formula_t *formula); EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreateEXMult(char *string, Ctlsp_Formula_t *formula); EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreateAXMult(char *string, Ctlsp_Formula_t *formula); EXTERN char * Ctlsp_FormulaGetTypeString(Ctlsp_Formula_t *formula); EXTERN Ctlsp_FormulaClass Ctlsp_CheckClassOfExistentialFormula(Ctlsp_Formula_t *formula); EXTERN Ctlsp_FormulaClass Ctlsp_CheckClassOfExistentialFormulaArray(array_t *formulaArray); EXTERN Ctlsp_ClassOfFormula Ctlsp_FormulaReadClass(Ctlsp_Formula_t *formula); EXTERN void Ctlsp_FormulaSetClass(Ctlsp_Formula_t *formula, Ctlsp_ClassOfFormula newClass); EXTERN Ctlsp_ClassOfCTLFormula Ctlsp_FormulaReadClassOfCTL(Ctlsp_Formula_t *formula); EXTERN void Ctlsp_FormulaSetClassOfCTL(Ctlsp_Formula_t *formula, Ctlsp_ClassOfCTLFormula newCTLclass); EXTERN array_t * Ctlsp_FormulaArrayConvertToLTL(array_t *formulaArray); EXTERN array_t * Ctlsp_FormulaArrayConvertToCTL(array_t *formulaArray); EXTERN Ctlp_Formula_t * Ctlsp_FormulaConvertToCTL(Ctlsp_Formula_t *formula); EXTERN Ctlp_Formula_t * Ctlsp_PropositionalFormulaToCTL(Ctlsp_Formula_t *formula); EXTERN int Ctlsp_isPropositionalFormula(Ctlsp_Formula_t *formula); EXTERN int Ctlsp_isCtlFormula(Ctlsp_Formula_t *formula); EXTERN int Ctlsp_isLtlFormula(Ctlsp_Formula_t *formula); EXTERN Ctlsp_Formula_t * Ctlsp_LtllFormulaNegate(Ctlsp_Formula_t *ltlFormula); EXTERN void Ctlsp_LtlSetClass(Ctlsp_Formula_t *formula); EXTERN int Ctlsp_LtlFormulaIsGFp(Ctlsp_Formula_t *formula); EXTERN boolean Ctlsp_LtlFormulaIsGp(Ctlsp_Formula_t *formula); EXTERN boolean Ctlsp_LtlFormulaIsFp(Ctlsp_Formula_t *formula); EXTERN boolean Ctlsp_LtlFormulaIsSafety(Ctlsp_Formula_t *formula); EXTERN void Ctlsp_FormulaArrayAddLtlFairnessConstraints(array_t *formulaArray, array_t *constraintArray); EXTERN Ctlsp_Formula_t * Ctlsp_CtlFormulaToCtlsp(Ctlp_Formula_t *F); EXTERN Ctlsp_Formula_t * Ctlsp_LtlFormulaExpandAbbreviation(Ctlsp_Formula_t *formula); EXTERN Ctlsp_Formula_t * Ctlsp_LtlFormulaNegationNormalForm(Ctlsp_Formula_t *formula); EXTERN Ctlsp_Formula_t * Ctlsp_LtlFormulaHashIntoUniqueTable(Ctlsp_Formula_t *F, st_table *uniqueTable); EXTERN void Ctlsp_LtlFormulaClearMarks(Ctlsp_Formula_t *F); EXTERN int Ctlsp_LtlFormulaCountNumber(Ctlsp_Formula_t *F); EXTERN st_table * Ctlsp_LtlFormulaCreateUniqueTable(void); EXTERN int Ctlsp_LtlFormulaIsElementary2(Ctlsp_Formula_t *F); EXTERN int Ctlsp_LtlFormulaIsElementary(Ctlsp_Formula_t *F); EXTERN boolean Ctlsp_LtlFormulaTestIsBounded(Ctlsp_Formula_t *formula, int *depth); EXTERN int Ctlsp_LtlFormulaDepth(Ctlsp_Formula_t *formula); EXTERN boolean Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(Ctlsp_Formula_t *formula); EXTERN int Ctlsp_LtlFormulaArrayIsPropositional(array_t * formulaArray); EXTERN int Ctlsp_LtlFormulaIsPropositional(Ctlsp_Formula_t *F); EXTERN int Ctlsp_LtlFormulaIsAtomicPropositional(Ctlsp_Formula_t *F); EXTERN int Ctlsp_LtlFormulaIsFG(Ctlsp_Formula_t *F); EXTERN int Ctlsp_LtlFormulaIsGF(Ctlsp_Formula_t *F); EXTERN int Ctlsp_LtlFormulaIsFGorGF(Ctlsp_Formula_t *F); EXTERN int Ctlsp_LtlFormulaSimplyImply(Ctlsp_Formula_t *from, Ctlsp_Formula_t *to); EXTERN array_t * Ctlsp_LtlTranslateIntoSNF(Ctlsp_Formula_t *formula); EXTERN void Ctlsp_LtlTranslateIntoSNFRecursive(Ctlsp_Formula_t *propNode, Ctlsp_Formula_t *formula, array_t *formulaArray, int *index); EXTERN Ctlsp_Formula_t * Ctlsp_LtlFormulaSimpleRewriting(Ctlsp_Formula_t *formula); /**AutomaticEnd***************************************************************/ #endif /* _CTLSP */