source: vis_dev/vis-2.3/src/ctlp/ctlpInt.h @ 57

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

vis2.3
File size: 8.0 KB
RevLine 
[14]1/**CHeaderFile*****************************************************************
2
3  FileName    [ctlpInt.h]
4
5  PackageName [ctlp]
6
7  Synopsis    [Declarations for internal use.]
8
9  Author      [Gary York, Ramin Hojati, Tom Shiple, Adnan Aziz, Yuji Kukimoto,
10               Jae-Young Jang, In-Ho Moon]
11
12  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
13  All rights reserved.
14
15  Permission is hereby granted, without written agreement and without license
16  or royalty fees, to use, copy, modify, and distribute this software and its
17  documentation for any purpose, provided that the above copyright notice and
18  the following two paragraphs appear in all copies of this software.
19
20  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
21  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
22  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
23  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
24
25  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
26  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
27  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
28  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
29  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
30
31  Revision    [$Id: ctlpInt.h,v 1.26 2005/05/13 05:51:05 fabio Exp $]
32
33******************************************************************************/
34
35#ifndef _CTLPINT
36#define _CTLPINT
37
38#define MAX_LENGTH_OF_VAR_NAME 512
39
40#include <string.h>
41#include "ctlp.h"
42#include "hrc.h"
43#include "cmd.h"
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  <p>DbgInfo is an uninterpreted pointer used by the CTL debugger to store
68  information needed to debug a formula.
69
70  <p>States holds the exact satisfying set of a formula in some fsm (the fsm is
71  not stored along with the set).  The Underapprox and overapprox fields are
72  approximations of the states field. Either states is NIL (no exact result is
73  known), or both underapprox and overapprox are NIL (the exact result is
74  known, or nothing is known at all).
75
76  Note that the convertedFlag being NIL does not imply that originalFormula is
77  NIL: a conversion could have been done that was trivial for the particular
78  node.]
79
80******************************************************************************/
81struct CtlpFormulaStruct {
82  Ctlp_FormulaType type;
83  Ctlp_Formula_t *left;   /* left child in formula */
84  Ctlp_Formula_t *right;  /* right child, or null if not used */
85  int refCount;           /* number of formulas referring to this
86                             formula as a left or right child */
87  mdd_t *states;          /* set of states satifying formula */
88  mdd_t *underapprox;     /* Underapproximation of states (for hints) */
89  mdd_t *overapprox;      /* overapprox for hints */
90  array_t *Bottomstates;
91  array_t *Topstates;
92  array_t *leaves;
93  array_t *matchfound_top;    /*array of booleans*/
94  array_t *matchelement_top;  /* array of match numbers*/
95  array_t *matchfound_bot;    /*array of booleans*/
96  array_t *matchelement_bot;  /* array of match numbers*/
97  Ctlp_Parity_t negation_parity; /* negation parity */
98  int share;
99  struct {
100    void *data;           /* used  to store information used by debugger */
101    Ctlp_DbgInfoFreeFn freeFn;         /* free function for data */
102    boolean convertedFlag;  /* was converted to existential form
103                                           by non-trivial transformation */
104    Ctlp_Formula_t *originalFormula; /* pointer to formula from which this
105                                           was converted */
106  } dbgInfo;
107  /*
108  ** The following fields are added for forward model checking.
109  */
110  short top; /* 0 : , 1 : forward */
111  short compareValue; /* 0 : = false, 1 : != false */
112  Ctlp_Approx_t latest;   /* which of the three results is most recent */
113  array_t *BotOnionRings;
114  array_t *TopOnionRings;
115};
116
117
118/*---------------------------------------------------------------------------*/
119/* Variable declarations                                                     */
120/*---------------------------------------------------------------------------*/
121
122/**Variable********************************************************************
123
124  Synopsis    [Global flag for parsing CTL file.]
125
126  Description [This flag is set to 0 before parsing a CTL file commences.  If
127  an error is found while parsing the file, this flag is set to 1.  After the
128  parser returns, if this flag is set, then the global CTL formula array is
129  freed.]
130
131******************************************************************************/
132extern int CtlpGlobalError;
133
134/**Variable********************************************************************
135
136  Synopsis    [Global pointer to the CTL formulas being created.]
137
138  Description [This pointer is always set to the current formula
139  so that the parser can free a partially constructed CTL formula
140  when an error is detected. Every time the parser starts reasing
141  a new formula, this variable is set to NIL(Ctlp_Fromula_t).]
142
143******************************************************************************/
144extern Ctlp_Formula_t *CtlpGlobalFormula;
145
146/**Variable********************************************************************
147
148  Synopsis    [Global pointer to the macro table of formulae]
149
150  Description [This pointer is always set to the macro table so that
151  the parser can substitute macro string with defined formula]
152
153******************************************************************************/
154extern st_table *CtlpMacroTable;
155
156/**AutomaticStart*************************************************************/
157
158/*---------------------------------------------------------------------------*/
159/* Function prototypes                                                       */
160/*---------------------------------------------------------------------------*/
161
162EXTERN void CtlpFormulaSetStatesToNULL(Ctlp_Formula_t *formula);
163EXTERN void CtlpFormulaIncrementRefCount(Ctlp_Formula_t *formula);
164EXTERN void CtlpFormulaDecrementRefCount(Ctlp_Formula_t *formula);
165EXTERN void CtlpFormulaAddToGlobalArray(Ctlp_Formula_t * formula);
166EXTERN void CtlpFormulaFree(Ctlp_Formula_t * formula);
167EXTERN int CtlpStringChangeValueStrToBinString(char *value, char *binValueStr, int interval);
168EXTERN void CtlpChangeBracket(char *inStr);
169EXTERN char * CtlpGetVectorInfoFromStr(char *str, int *start, int *end, int *interval, int *inc);
170EXTERN int CtlpFormulaAddToTable(char *name, Ctlp_Formula_t *formula, st_table *macroTable);
171EXTERN Ctlp_Formula_t * CtlpFormulaFindInTable(char *name, st_table *macroTable);
172EXTERN Ctlp_FormulaClass CtlpResolveClass(Ctlp_FormulaClass class1, Ctlp_FormulaClass class2);
173EXTERN Ctlp_FormulaClass CtlpNegateFormulaClass(Ctlp_FormulaClass class_);
174
175/**AutomaticEnd***************************************************************/
176
177EXTERN void CtlpFileSetup(FILE *fp);  /* lives in a .l file, so not
178                                                automatically generated */
179EXTERN int CtlpYyparse(void);
180#endif /* _CTLPINT */
Note: See TracBrowser for help on using the repository browser.