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

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

vis2.3
File size: 10.6 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [ctlspInt.h]
4
5  PackageName [ctlsp]
6
7  Synopsis    [Declarations for internal use.]
8
9  Author      [Mohammad Awedh]
10
11  Copyright   [Copyright (c) 2000-2001 The Regents of the Univ. of Colorado
12  at Boulder. All rights reserved.
13
14  Permission is hereby granted, without written agreement and without license
15  or royalty fees, to use, copy, modify, and distribute this software and its
16  documentation for any purpose, provided that the above copyright notice and
17  the following two paragraphs appear in all copies of this software.
18
19  IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR
20  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
21  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
22  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
23
24  THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES,
25  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
26  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
27  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
28  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
29
30  Revision    [$Id: ctlspInt.h,v 1.8 2004/09/15 20:06:29 awedh Exp $]
31
32******************************************************************************/
33
34#ifndef _CTLSPINT
35#define _CTLSPINT
36
37#define MAX_LENGTH_OF_VAR_NAME 512
38
39#include <string.h>
40#include "ctlsp.h"
41#include "hrc.h"
42#include "cmd.h"
43
44
45
46/*---------------------------------------------------------------------------*/
47/* Structure declarations                                                    */
48/*---------------------------------------------------------------------------*/
49
50/**Struct**********************************************************************
51
52  Synopsis    [Tree representing a CTL formula.]
53
54  Description [Data structure for a CTL formula.  A formula is a tree
55  or a one-rooted DAG.  An internal vertex has one or two children,
56  depending on the operator type: if the operator takes just one
57  argument, then the left child holds the subformula, and the right
58  child is NULL; if the operator takes two arguments, then both
59  children are non-NULL.
60 
61  <p>A leaf is either a pair of a variable name in the network and a
62  value, TRUE or FALSE.  The left and right fields are used in leaf
63  vertices only in the first case above. (The left child holds a
64  variable name while the right child holds a value. Note that these
65  two fields are used differently in internal vertices and leaves.)
66
67  DbgInfo is an uninterpreted pointer used by the CTL debugger
68  to store information needed to debug a formula.
69
70  States holds the exact satisfying set of a formula in some fsm (that
71  is not stored along with the set).  Under- and overapprox are
72  approximations of states, and either states is NIL, or both
73  underapprox and overapprox are.  ]
74
75******************************************************************************/
76struct CtlspFormulaStruct {
77  Ctlsp_FormulaType type;
78  Ctlsp_Formula_t *left;   /* left child in formula */
79  Ctlsp_Formula_t *right;  /* right child, or null if not used */
80  int refCount;           /* number of formulas referring to this
81                             formula as a left or right child */
82  mdd_t *states;          /* set of states satifying formula */
83  mdd_t *underapprox;     /* Underapproximation of states (for hints) */
84  mdd_t *overapprox;      /* overapprox for hints */
85 
86  struct {
87    void *data;           /* used  to store information used by debugger */
88    Ctlsp_DbgInfoFreeFn freeFn;         /* free function for data */
89    boolean convertedFlag;  /* was converted to existential form
90                                           by non-trivial transformation */
91    Ctlsp_Formula_t *originalFormula; /* pointer to formula from which this
92                                           was converted */
93  } dbgInfo;
94  /*
95  ** The following fields are added for forward model checking.
96  */
97  short top; /* 0 : , 1 : forward */
98  short compareValue; /* 0 : = false, 1 : != false */
99  /*
100  ** The following field is added to specify the Class of the Node
101   */
102  Ctlsp_ClassOfFormula class_;
103  /*
104  ** The following field is added to specify weather the sub-formula is CTL or not.
105   */
106  Ctlsp_ClassOfCTLFormula CTLclass;
107
108    /* The following fields are for LTL->AUT */
109    int  ab_idx;
110    int  label_idx;
111    char rhs;
112    char marked;
113};
114
115
116/*---------------------------------------------------------------------------*/
117/* Variable declarations                                                     */
118/*---------------------------------------------------------------------------*/
119
120/**Variable********************************************************************
121
122  Synopsis    [Global flag for parsing CTL file.]
123
124  Description [This flag is set to 0 before parsing a CTL file commences.  If
125  an error is found while parsing the file, this flag is set to 1.  After the
126  parser returns, if this flag is set, then the global CTL formula array is
127  freed.]
128
129******************************************************************************/
130extern int CtlspGlobalError;
131
132/**Variable********************************************************************
133
134  Synopsis    [Global pointer to the CTL formulas being created.]
135
136  Description [This pointer is always set to the current formula
137  so that the parser can free a partially constructed CTL formula
138  when an error is detected. Every time the parser starts reasing
139  a new formula, this variable is set to NIL(Ctlsp_Fromula_t).]
140
141******************************************************************************/
142extern Ctlsp_Formula_t *CtlspGlobalFormula;
143
144/**Variable********************************************************************
145
146  Synopsis    [Global pointer to the macro table of formulae]
147
148  Description [This pointer is always set to the macro table so that
149  the parser can substitute macro string with defined formula]
150
151******************************************************************************/
152extern st_table *CtlspMacroTable;
153
154/*---------------------------------------------------------------------------*/
155/* Macro declarations                                                        */
156/*---------------------------------------------------------------------------*/
157
158/**Macro***********************************************************************
159
160  Synopsis     [Determine the class of a binary operator CTL* node given the
161               class of its children (x, y)]
162
163  Description  [This macro determine the class of a binary operator CTL* node
164               given the class of its children (x, y).
165
166                       prop  LTL  state  path
167               -------------------------------
168               prop  | prop  LTL  state  path
169               LTL   |       LTL  path   path
170               state |            state  path
171               path  |                   path
172
173
174               ]
175
176  SideEffects  []
177
178  SeeAlso      []
179
180******************************************************************************/
181#define table1(\
182  x,\
183  y\
184)\
185  ((Ctlsp_ClassOfFormula)  ((x) | (y)) )
186
187/**Macro***********************************************************************
188
189  Synopsis     [Determine the class of a uniry operator CTL* node given the
190               class of its childn (x)]
191
192  Description  [This macro determine the class of a uniry operator CTL* node
193               given the class of its child (x).
194
195               prop  LTL  state  path
196               ----------------------
197               LTL   LTL  path   path
198
199               ]
200
201  SideEffects  []
202
203  SeeAlso      []
204
205******************************************************************************/
206#define table2(     \
207  x                 \
208)                   \
209  ((Ctlsp_ClassOfFormula)  ((x) |  Ctlsp_LTLformula_c) )
210
211/**Macro***********************************************************************
212
213  Synopsis     [Determine the class of a binary Temporal operator CTL* node
214               given the class of its children (x, y)]
215
216  Description  [This macro determine the class of a Binary Temporal  operator CTL* node
217               given the class of its children (x, y).
218
219                       prop  LTL  state  path
220               -------------------------------
221               prop  | LTL   LTL  path  path
222               LTL   |       LTL  path  path
223               state |            path  path
224               path  |                  path
225
226
227               ]
228
229  SideEffects  []
230
231  SeeAlso      []
232
233******************************************************************************/
234#define table3(\
235  x,\
236  y\
237)\
238  ((Ctlsp_ClassOfFormula)  ((x) | (y) |  Ctlsp_LTLformula_c) )
239
240
241/**AutomaticStart*************************************************************/
242
243/*---------------------------------------------------------------------------*/
244/* Function prototypes                                                       */
245/*---------------------------------------------------------------------------*/
246
247EXTERN void CtlspFormulaSetStatesToNULL(Ctlsp_Formula_t *formula);
248EXTERN Ctlsp_Formula_t * CtlspLtlFormulaSimpleRewriting_Aux(Ctlsp_Formula_t *F, st_table *Utable);
249EXTERN void CtlspFormulaIncrementRefCount(Ctlsp_Formula_t *formula);
250EXTERN void CtlspFormulaDecrementRefCount(Ctlsp_Formula_t *formula);
251EXTERN void CtlspFormulaAddToGlobalArray(Ctlsp_Formula_t * formula);
252EXTERN void CtlspFormulaFree(Ctlsp_Formula_t * formula);
253EXTERN int CtlspStringChangeValueStrToBinString(char *value, char *binValueStr, int interval);
254EXTERN void CtlspChangeBracket(char *inStr);
255EXTERN char * CtlspGetVectorInfoFromStr(char *str, int *start, int *end, int *interval, int *inc);
256EXTERN int CtlspFormulaAddToTable(char *name, Ctlsp_Formula_t *formula, st_table *macroTable);
257EXTERN Ctlsp_Formula_t * CtlspFormulaFindInTable(char *name, st_table *macroTable);
258EXTERN Ctlsp_FormulaClass CtlspCheckClassOfExistentialFormulaRecur(Ctlsp_Formula_t *formula, boolean parity);
259EXTERN Ctlsp_FormulaClass CtlspResolveClass(Ctlsp_FormulaClass class1, Ctlsp_FormulaClass class2);
260EXTERN Ctlp_Formula_t * CtlspFormulaConvertToCTL(Ctlsp_Formula_t *formula);
261EXTERN Ctlsp_Formula_t * CtlspFunctionOr(Ctlsp_Formula_t *left, Ctlsp_Formula_t *right);
262EXTERN Ctlsp_Formula_t * CtlspFunctionAnd(Ctlsp_Formula_t *left, Ctlsp_Formula_t *right);
263EXTERN Ctlsp_Formula_t * CtlspFunctionThen(Ctlsp_Formula_t *left, Ctlsp_Formula_t *right);
264
265/**AutomaticEnd***************************************************************/
266
267EXTERN void CtlspFileSetup(FILE *fp);  /* lives in a .l file, so not
268                                                automatically generated */
269EXTERN int CtlspYyparse(void);
270#endif /* _CTLSPINT */
271
272
273
274
275
276
277
Note: See TracBrowser for help on using the repository browser.