/**CHeaderFile***************************************************************** FileName [ctlspInt.h] PackageName [ctlsp] Synopsis [Declarations for internal use.] Author [Mohammad Awedh] Copyright [Copyright (c) 2000-2001 The Regents of the Univ. of Colorado at Boulder. All rights reserved. Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software. IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] Revision [$Id: ctlspInt.h,v 1.8 2004/09/15 20:06:29 awedh Exp $] ******************************************************************************/ #ifndef _CTLSPINT #define _CTLSPINT #define MAX_LENGTH_OF_VAR_NAME 512 #include #include "ctlsp.h" #include "hrc.h" #include "cmd.h" /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /**Struct********************************************************************** Synopsis [Tree representing a CTL formula.] Description [Data structure for a CTL formula. A formula is a tree or a one-rooted DAG. An internal vertex has one or two children, depending on the operator type: if the operator takes just one argument, then the left child holds the subformula, and the right child is NULL; if the operator takes two arguments, then both children are non-NULL.

A leaf is either a pair of a variable name in the network and a value, TRUE or FALSE. The left and right fields are used in leaf vertices only in the first case above. (The left child holds a variable name while the right child holds a value. Note that these two fields are used differently in internal vertices and leaves.) DbgInfo is an uninterpreted pointer used by the CTL debugger to store information needed to debug a formula. States holds the exact satisfying set of a formula in some fsm (that is not stored along with the set). Under- and overapprox are approximations of states, and either states is NIL, or both underapprox and overapprox are. ] ******************************************************************************/ struct CtlspFormulaStruct { Ctlsp_FormulaType type; Ctlsp_Formula_t *left; /* left child in formula */ Ctlsp_Formula_t *right; /* right child, or null if not used */ int refCount; /* number of formulas referring to this formula as a left or right child */ mdd_t *states; /* set of states satifying formula */ mdd_t *underapprox; /* Underapproximation of states (for hints) */ mdd_t *overapprox; /* overapprox for hints */ struct { void *data; /* used to store information used by debugger */ Ctlsp_DbgInfoFreeFn freeFn; /* free function for data */ boolean convertedFlag; /* was converted to existential form by non-trivial transformation */ Ctlsp_Formula_t *originalFormula; /* pointer to formula from which this was converted */ } dbgInfo; /* ** The following fields are added for forward model checking. */ short top; /* 0 : , 1 : forward */ short compareValue; /* 0 : = false, 1 : != false */ /* ** The following field is added to specify the Class of the Node */ Ctlsp_ClassOfFormula class_; /* ** The following field is added to specify weather the sub-formula is CTL or not. */ Ctlsp_ClassOfCTLFormula CTLclass; /* The following fields are for LTL->AUT */ int ab_idx; int label_idx; char rhs; char marked; }; /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /**Variable******************************************************************** Synopsis [Global flag for parsing CTL file.] Description [This flag is set to 0 before parsing a CTL file commences. If an error is found while parsing the file, this flag is set to 1. After the parser returns, if this flag is set, then the global CTL formula array is freed.] ******************************************************************************/ extern int CtlspGlobalError; /**Variable******************************************************************** Synopsis [Global pointer to the CTL formulas being created.] Description [This pointer is always set to the current formula so that the parser can free a partially constructed CTL formula when an error is detected. Every time the parser starts reasing a new formula, this variable is set to NIL(Ctlsp_Fromula_t).] ******************************************************************************/ extern Ctlsp_Formula_t *CtlspGlobalFormula; /**Variable******************************************************************** Synopsis [Global pointer to the macro table of formulae] Description [This pointer is always set to the macro table so that the parser can substitute macro string with defined formula] ******************************************************************************/ extern st_table *CtlspMacroTable; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**Macro*********************************************************************** Synopsis [Determine the class of a binary operator CTL* node given the class of its children (x, y)] Description [This macro determine the class of a binary operator CTL* node given the class of its children (x, y). prop LTL state path ------------------------------- prop | prop LTL state path LTL | LTL path path state | state path path | path ] SideEffects [] SeeAlso [] ******************************************************************************/ #define table1(\ x,\ y\ )\ ((Ctlsp_ClassOfFormula) ((x) | (y)) ) /**Macro*********************************************************************** Synopsis [Determine the class of a uniry operator CTL* node given the class of its childn (x)] Description [This macro determine the class of a uniry operator CTL* node given the class of its child (x). prop LTL state path ---------------------- LTL LTL path path ] SideEffects [] SeeAlso [] ******************************************************************************/ #define table2( \ x \ ) \ ((Ctlsp_ClassOfFormula) ((x) | Ctlsp_LTLformula_c) ) /**Macro*********************************************************************** Synopsis [Determine the class of a binary Temporal operator CTL* node given the class of its children (x, y)] Description [This macro determine the class of a Binary Temporal operator CTL* node given the class of its children (x, y). prop LTL state path ------------------------------- prop | LTL LTL path path LTL | LTL path path state | path path path | path ] SideEffects [] SeeAlso [] ******************************************************************************/ #define table3(\ x,\ y\ )\ ((Ctlsp_ClassOfFormula) ((x) | (y) | Ctlsp_LTLformula_c) ) /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Function prototypes */ /*---------------------------------------------------------------------------*/ EXTERN void CtlspFormulaSetStatesToNULL(Ctlsp_Formula_t *formula); EXTERN Ctlsp_Formula_t * CtlspLtlFormulaSimpleRewriting_Aux(Ctlsp_Formula_t *F, st_table *Utable); EXTERN void CtlspFormulaIncrementRefCount(Ctlsp_Formula_t *formula); EXTERN void CtlspFormulaDecrementRefCount(Ctlsp_Formula_t *formula); EXTERN void CtlspFormulaAddToGlobalArray(Ctlsp_Formula_t * formula); EXTERN void CtlspFormulaFree(Ctlsp_Formula_t * formula); EXTERN int CtlspStringChangeValueStrToBinString(char *value, char *binValueStr, int interval); EXTERN void CtlspChangeBracket(char *inStr); EXTERN char * CtlspGetVectorInfoFromStr(char *str, int *start, int *end, int *interval, int *inc); EXTERN int CtlspFormulaAddToTable(char *name, Ctlsp_Formula_t *formula, st_table *macroTable); EXTERN Ctlsp_Formula_t * CtlspFormulaFindInTable(char *name, st_table *macroTable); EXTERN Ctlsp_FormulaClass CtlspCheckClassOfExistentialFormulaRecur(Ctlsp_Formula_t *formula, boolean parity); EXTERN Ctlsp_FormulaClass CtlspResolveClass(Ctlsp_FormulaClass class1, Ctlsp_FormulaClass class2); EXTERN Ctlp_Formula_t * CtlspFormulaConvertToCTL(Ctlsp_Formula_t *formula); EXTERN Ctlsp_Formula_t * CtlspFunctionOr(Ctlsp_Formula_t *left, Ctlsp_Formula_t *right); EXTERN Ctlsp_Formula_t * CtlspFunctionAnd(Ctlsp_Formula_t *left, Ctlsp_Formula_t *right); EXTERN Ctlsp_Formula_t * CtlspFunctionThen(Ctlsp_Formula_t *left, Ctlsp_Formula_t *right); /**AutomaticEnd***************************************************************/ EXTERN void CtlspFileSetup(FILE *fp); /* lives in a .l file, so not automatically generated */ EXTERN int CtlspYyparse(void); #endif /* _CTLSPINT */