source: vis_dev/vis-2.3/src/ctlsp/ctlsp.h @ 82

Last change on this file since 82 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 11.9 KB
RevLine 
[14]1/**CHeaderFile*****************************************************************
2
3  FileName    [ctlsp.h]
4
5  PackageName [ctlsp]
6
7  Synopsis    [Routines for parsing, writing and accessing CTL* formulas.]
8
9  Description [This package implements a parser for CTL* formulas.  CTL* is
10  a language used to describe properties of systems.]
11
12  SeeAlso     []
13
14  Author      [Mohammad Awedh]
15
16  Copyright   [This file was created at the University of Colorado at Boulder.
17  The University of Colorado at Boulder makes no warranty about the suitability
18  of this software for any purpose.  It is presented on an AS IS basis.]
19
20  Revision    [$Id: ctlsp.h,v 1.28 2009/04/11 01:32:36 fabio Exp $]
21
22******************************************************************************/
23
24#ifndef _CTLSP
25#define _CTLSP
26
27#include "vm.h"
28#include "ctlp.h"
29
30/*---------------------------------------------------------------------------*/
31/* Structure declarations                                                    */
32/*---------------------------------------------------------------------------*/
33
34/**Enum************************************************************************
35
36  Synopsis    [Types of operators allowed in CTL* formulas.]
37
38  Description [The types of nodes in a CTL* formula parse tree. ID, TRUE, and
39  FALSE are leaves, and all others are internal nodes.]
40
41  SeeAlso     [Ctlsp_FormulaReadType]
42
43******************************************************************************/
44typedef enum {
45  Ctlsp_E_c,      /* there exists */
46  Ctlsp_A_c,      /* for all paths*/
47  Ctlsp_X_c,      /* Next */
48  Ctlsp_G_c,      /* globally */
49  Ctlsp_F_c,      /* finally */
50  Ctlsp_U_c,      /* until (not symmetric in args) */
51  Ctlsp_R_c,      /* release (not symmetric in args) */
52  Ctlsp_W_c,      /* weak until (not symmetric in args) */
53  Ctlsp_OR_c,     /* Boolean disjunction */
54  Ctlsp_AND_c,    /* Boolean conjunction */
55  Ctlsp_NOT_c,    /* Boolean negation*/
56  Ctlsp_THEN_c,   /* Boolean implies (not symmetric) */
57  Ctlsp_XOR_c,    /* Boolean XOR */
58  Ctlsp_EQ_c,     /* Boolean equal */
59  Ctlsp_ID_c,     /* an atomic proposition */
60  Ctlsp_TRUE_c,   /* tautology (used only for translation to exist. form) */
61  Ctlsp_FALSE_c,  /* empty (used only for translation to exist. form) */
62  Ctlsp_Fwd_c,    /* forward */
63  Ctlsp_Y_c,     /* previous state */
64  Ctlsp_H_c,     /* past */
65  Ctlsp_Init_c,  /* initial states */
66  Ctlsp_Cmp_c    /* compare two leaves in forward CTL* */
67} Ctlsp_FormulaType;
68
69
70/**Enum************************************************************************
71
72  Synopsis    [Types of operators allowed in CTL formulas.]
73
74  Description [The types of nodes in a CTL formula parse tree. ID, TRUE, and
75  FALSE are leaves, and all others are internal nodes.]
76
77  SeeAlso     [Ctlsp_FormulaReadType]
78
79******************************************************************************/
80typedef enum {
81  Ctlsp_ECTL_c,
82  Ctlsp_ACTL_c,
83  Ctlsp_Mixed_c,
84  Ctlsp_QuantifierFree_c,
85  Ctlsp_LTL_c,
86  Ctlsp_stateFormuls_c,
87  Ctlsp_invalid_c
88} Ctlsp_FormulaClass;
89
90
91/**Enum************************************************************************
92
93  Synopsis    [Types of approximations that are possible]
94
95  Description [We can have overapproximations, underapproximations, exact
96  approximations, or incomparable sets.  Question: is ctlsp the right place for
97  this?  It is used in ctlsp, mc, rch. (RB)]
98
99  SeeAlso     []
100
101******************************************************************************/
102typedef enum {
103  Ctlsp_Incomparable_c,
104  Ctlsp_Underapprox_c,
105  Ctlsp_Overapprox_c,
106  Ctlsp_Exact_c
107} Ctlsp_Approx_t;
108
109/**Enum************************************************************************
110
111  Synopsis    [ Class of CTL* formulas.]
112
113  Description [The classes of nodes in CTL* formula.]
114
115  Note: [We explicity assign values to the enumerated values becuase we
116         are going to use the numerical values in determining the class of
117         a CTL* formula. These values are used in table1, table2, and
118         table3 macros.]
119
120  SeeAlso [ctlspInt.h]
121
122******************************************************************************/
123typedef enum {
124  Ctlsp_propformula_c  = 0,
125  Ctlsp_LTLformula_c   = 1,
126  Ctlsp_stateformula_c = 2,
127  Ctlsp_pathformula_c  = 3
128} Ctlsp_ClassOfFormula;
129
130
131/**Enum************************************************************************
132
133  Synopsis    [ Class of CTL formulas.]
134
135  Description [The classes of CTL formula. This help to find out whether a
136              formula is CTL or not.  During the parsing of a CTL* formula
137              the parser determines whether the subformula is a CTL formula,
138              (Ctlsp_CTL_c) can be CTL formula (Ctlsp_PathCTL_c), or not
139              CTL formula (Ctlsp_NotCTL_c).]
140
141  SeeAlso     [ctlsp.y]
142
143******************************************************************************/
144typedef enum {
145  Ctlsp_NotCTL_c,
146  Ctlsp_PathCTL_c,
147  Ctlsp_CTL_c
148} Ctlsp_ClassOfCTLFormula;
149
150
151/*---------------------------------------------------------------------------*/
152/* Type declarations                                                         */
153/*---------------------------------------------------------------------------*/
154typedef struct CtlspFormulaStruct Ctlsp_Formula_t;
155typedef void   (*Ctlsp_DbgInfoFreeFn) (Ctlsp_Formula_t *);
156
157
158/**AutomaticStart*************************************************************/
159
160/*---------------------------------------------------------------------------*/
161/* Function prototypes                                                       */
162/*---------------------------------------------------------------------------*/
163
164EXTERN void Ctlsp_Init(void);
165EXTERN void Ctlsp_End(void);
166EXTERN array_t * Ctlsp_FileParseFormulaArray(FILE * fp);
167EXTERN array_t * Ctlsp_FileParseCTLFormulaArray(FILE * fp);
168EXTERN char * Ctlsp_FormulaConvertToString(Ctlsp_Formula_t * formula);
169EXTERN void Ctlsp_FormulaPrint(FILE * fp, Ctlsp_Formula_t * formula);
170EXTERN Ctlsp_FormulaType Ctlsp_FormulaReadType(Ctlsp_Formula_t * formula);
171EXTERN int Ctlsp_FormulaReadCompareValue(Ctlsp_Formula_t * formula);
172EXTERN char * Ctlsp_FormulaReadVariableName(Ctlsp_Formula_t * formula);
173EXTERN char * Ctlsp_FormulaReadValueName(Ctlsp_Formula_t * formula);
174EXTERN Ctlsp_Formula_t * Ctlsp_FormulaReadLeftChild(Ctlsp_Formula_t * formula);
175EXTERN Ctlsp_Formula_t * Ctlsp_FormulaReadRightChild(Ctlsp_Formula_t * formula);
176EXTERN mdd_t * Ctlsp_FormulaObtainStates(Ctlsp_Formula_t * formula);
177EXTERN mdd_t * Ctlsp_FormulaObtainApproxStates(Ctlsp_Formula_t *formula, Ctlsp_Approx_t approx);
178EXTERN void Ctlsp_FormulaSetStates(Ctlsp_Formula_t * formula, mdd_t * states);
179EXTERN void Ctlsp_FormulaSetApproxStates(Ctlsp_Formula_t * formula, mdd_t * states, Ctlsp_Approx_t approx);
180EXTERN void Ctlsp_FormulaSetDbgInfo(Ctlsp_Formula_t * formula, void *data, Ctlsp_DbgInfoFreeFn freeFn);
181EXTERN void * Ctlsp_FormulaReadDebugData(Ctlsp_Formula_t * formula);
182EXTERN boolean Ctlsp_FormulaTestIsConverted(Ctlsp_Formula_t * formula);
183EXTERN boolean Ctlsp_FormulaTestIsQuantifierFree(Ctlsp_Formula_t *formula);
184EXTERN Ctlsp_Formula_t * Ctlsp_FormulaReadOriginalFormula(Ctlsp_Formula_t * formula);
185EXTERN int Ctlsp_FormulaReadABIndex(Ctlsp_Formula_t * formula);
186EXTERN void Ctlsp_FormulaSetABIndex(Ctlsp_Formula_t * formula, int ab_idx);
187EXTERN int Ctlsp_FormulaReadLabelIndex(Ctlsp_Formula_t * formula);
188EXTERN void Ctlsp_FormulaSetLabelIndex(Ctlsp_Formula_t * formula, int label_idx);
189EXTERN char Ctlsp_FormulaReadRhs(Ctlsp_Formula_t * formula);
190EXTERN void Ctlsp_FormulaSetRhs(Ctlsp_Formula_t * formula);
191EXTERN void Ctlsp_FormulaResetRhs(Ctlsp_Formula_t * formula);
192EXTERN char Ctlsp_FormulaReadMarked(Ctlsp_Formula_t * formula);
193EXTERN void Ctlsp_FormulaSetMarked(Ctlsp_Formula_t * formula);
194EXTERN void Ctlsp_FormulaResetMarked(Ctlsp_Formula_t * formula);
195EXTERN void Ctlsp_FormulaFree(Ctlsp_Formula_t *formula);
196EXTERN void Ctlsp_FlushStates(Ctlsp_Formula_t * formula);
197EXTERN Ctlsp_Formula_t * Ctlsp_FormulaDup(Ctlsp_Formula_t * formula);
198EXTERN void Ctlsp_FormulaArrayFree(array_t * formulaArray);
199EXTERN array_t * Ctlsp_FormulaArrayConvertToDAG(array_t *formulaArray);
200EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreate(Ctlsp_FormulaType type, void * left_, void * right_);
201EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreateOr(char *name, char *valueStr);
202EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreateVectorAnd(char *nameVector, char *value);
203EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreateVectorOr(char *nameVector, char *valueStr);
204EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreateEquiv(char *left, char *right);
205EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreateVectorEquiv(char *left, char *right);
206EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreateXMult(char *string, Ctlsp_Formula_t *formula);
207EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreateEXMult(char *string, Ctlsp_Formula_t *formula);
208EXTERN Ctlsp_Formula_t * Ctlsp_FormulaCreateAXMult(char *string, Ctlsp_Formula_t *formula);
209EXTERN char * Ctlsp_FormulaGetTypeString(Ctlsp_Formula_t *formula);
210EXTERN Ctlsp_FormulaClass Ctlsp_CheckClassOfExistentialFormula(Ctlsp_Formula_t *formula);
211EXTERN Ctlsp_FormulaClass Ctlsp_CheckClassOfExistentialFormulaArray(array_t *formulaArray);
212EXTERN Ctlsp_ClassOfFormula Ctlsp_FormulaReadClass(Ctlsp_Formula_t *formula);
213EXTERN void Ctlsp_FormulaSetClass(Ctlsp_Formula_t *formula, Ctlsp_ClassOfFormula newClass);
214EXTERN Ctlsp_ClassOfCTLFormula Ctlsp_FormulaReadClassOfCTL(Ctlsp_Formula_t *formula);
215EXTERN void Ctlsp_FormulaSetClassOfCTL(Ctlsp_Formula_t *formula, Ctlsp_ClassOfCTLFormula newCTLclass);
216EXTERN array_t * Ctlsp_FormulaArrayConvertToLTL(array_t *formulaArray);
217EXTERN array_t * Ctlsp_FormulaArrayConvertToCTL(array_t *formulaArray);
218EXTERN Ctlp_Formula_t * Ctlsp_FormulaConvertToCTL(Ctlsp_Formula_t *formula);
219EXTERN Ctlp_Formula_t * Ctlsp_PropositionalFormulaToCTL(Ctlsp_Formula_t *formula);
220EXTERN int Ctlsp_isPropositionalFormula(Ctlsp_Formula_t *formula);
221EXTERN int Ctlsp_isCtlFormula(Ctlsp_Formula_t *formula);
222EXTERN int Ctlsp_isLtlFormula(Ctlsp_Formula_t *formula);
223EXTERN Ctlsp_Formula_t * Ctlsp_LtllFormulaNegate(Ctlsp_Formula_t *ltlFormula);
224EXTERN void Ctlsp_LtlSetClass(Ctlsp_Formula_t *formula);
225EXTERN int Ctlsp_LtlFormulaIsGFp(Ctlsp_Formula_t *formula);
226EXTERN boolean Ctlsp_LtlFormulaIsGp(Ctlsp_Formula_t *formula);
227EXTERN boolean Ctlsp_LtlFormulaIsFp(Ctlsp_Formula_t *formula);
228EXTERN boolean Ctlsp_LtlFormulaIsSafety(Ctlsp_Formula_t *formula);
229EXTERN void Ctlsp_FormulaArrayAddLtlFairnessConstraints(array_t *formulaArray, array_t *constraintArray);
230EXTERN Ctlsp_Formula_t * Ctlsp_CtlFormulaToCtlsp(Ctlp_Formula_t *F);
231EXTERN Ctlsp_Formula_t * Ctlsp_LtlFormulaExpandAbbreviation(Ctlsp_Formula_t *formula);
232EXTERN Ctlsp_Formula_t * Ctlsp_LtlFormulaNegationNormalForm(Ctlsp_Formula_t *formula);
233EXTERN Ctlsp_Formula_t * Ctlsp_LtlFormulaHashIntoUniqueTable(Ctlsp_Formula_t *F, st_table *uniqueTable);
234EXTERN void Ctlsp_LtlFormulaClearMarks(Ctlsp_Formula_t *F);
235EXTERN int Ctlsp_LtlFormulaCountNumber(Ctlsp_Formula_t *F);
236EXTERN st_table * Ctlsp_LtlFormulaCreateUniqueTable(void);
237EXTERN int Ctlsp_LtlFormulaIsElementary2(Ctlsp_Formula_t *F);
238EXTERN int Ctlsp_LtlFormulaIsElementary(Ctlsp_Formula_t *F);
239EXTERN boolean Ctlsp_LtlFormulaTestIsBounded(Ctlsp_Formula_t *formula, int *depth);
240EXTERN int Ctlsp_LtlFormulaDepth(Ctlsp_Formula_t *formula);
241EXTERN boolean Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(Ctlsp_Formula_t *formula);
242EXTERN int Ctlsp_LtlFormulaArrayIsPropositional(array_t * formulaArray);
243EXTERN int Ctlsp_LtlFormulaIsPropositional(Ctlsp_Formula_t *F);
244EXTERN int Ctlsp_LtlFormulaIsAtomicPropositional(Ctlsp_Formula_t *F);
245EXTERN int Ctlsp_LtlFormulaIsFG(Ctlsp_Formula_t *F);
246EXTERN int Ctlsp_LtlFormulaIsGF(Ctlsp_Formula_t *F);
247EXTERN int Ctlsp_LtlFormulaIsFGorGF(Ctlsp_Formula_t *F);
248EXTERN int Ctlsp_LtlFormulaSimplyImply(Ctlsp_Formula_t *from, Ctlsp_Formula_t *to);
249EXTERN array_t * Ctlsp_LtlTranslateIntoSNF(Ctlsp_Formula_t *formula);
250EXTERN void  Ctlsp_LtlTranslateIntoSNFRecursive(Ctlsp_Formula_t *propNode, Ctlsp_Formula_t *formula, array_t *formulaArray, int *index);
251EXTERN Ctlsp_Formula_t * Ctlsp_LtlFormulaSimpleRewriting(Ctlsp_Formula_t *formula);
252
253/**AutomaticEnd***************************************************************/
254
255#endif /* _CTLSP */
Note: See TracBrowser for help on using the repository browser.