source: vis_dev/vis-2.3/src/amc/amcInt.h

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

vis2.3
File size: 7.3 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [amcInt.h]
4
5  PackageName [amc]
6
7  Synopsis    [Internal data type definitions and macros to handle the
8  structures of the amc package.]
9
10  Author      [Woohyuk Lee <woohyuk@duke.colorado.edu>]
11
12  Copyright [This file was created at the University of Colorado at Boulder.
13  The University of Colorado at Boulder makes no warranty about the suitability
14  of this software for any purpose.  It is presented on an AS IS basis.]
15
16  Revision    [$Id: amcInt.h,v 1.23 2002/09/08 02:10:46 fabio Exp $]
17
18******************************************************************************/
19
20#ifndef _AMCINT
21#define _AMCINT
22
23/*---------------------------------------------------------------------------*/
24/* Nested includes                                                           */
25/*---------------------------------------------------------------------------*/
26/* #include <unistd.h> */
27#include "amc.h"
28#include <string.h>
29
30
31/*---------------------------------------------------------------------------*/
32/* Constant declarations                                                     */
33/*---------------------------------------------------------------------------*/
34
35/*---------------------------------------------------------------------------*/
36/* Type declarations                                                         */
37/*---------------------------------------------------------------------------*/
38typedef int (*AmcCallBackProc)  ARGS((Amc_Info_t *, Ctlp_Formula_t *, int));
39typedef void (*AmcFreeProc) ARGS((Amc_Info_t *));
40
41
42/*---------------------------------------------------------------------------*/
43/* Structure declarations                                                    */
44/*---------------------------------------------------------------------------*/
45/**Struct**********************************************************************
46
47  Synopsis    [Information regarding a subsystem.]
48
49  Description [Each field represents information associated with a subsystem.]
50
51  SeeAlso     [AmcInfoStruct]
52
53******************************************************************************/
54struct AmcSubsystemInfo{
55  Fsm_Fsm_t     *fsm;                  /* Sub-Fsm of this subsystem */
56  array_t       *relationArray;        /* Array of MDD representation of the
57                                          transition relation */
58  mdd_t         *nextStateVarSmoothen; /* Transition relation of subsystems
59                                          with next state variables existentially
60                                          quantified */
61  mdd_t         *satisfyStates;        /* Sub(Super)-set of states satisfying
62                                          given formula */
63  st_table      *vertexTable;          /* Vertices in the subsystem */
64  st_table      *fanInTable;           /* */
65  st_table      *fanOutTable;          /* */
66  int           takenIntoOptimal;      /* If 1, the subsystem is part of the system */
67  char          *methodSpecificData;   /* May be used to store method specific data */
68};
69
70
71/**Struct**********************************************************************
72
73  Synopsis    [Information regarding the amc package.]
74
75  Description [This is a higher level of information related to the amc package.]
76
77  SeeAlso     [AmcSubsystemInfo]
78
79******************************************************************************/
80struct AmcInfoStruct{
81  Ntk_Network_t         *network;        /* Corresponding network */
82  Amc_MethodType        methodType;      /* Approximation method type */
83  void                  *methodData;     /* Method-dependent data structure */
84
85  array_t               *subSystemArray; /* Array of AmcSubsystemInfo *  */
86  Amc_SubsystemInfo_t   *optimalSystem;  /* */
87  mdd_t                 *initialStates;  /* */
88  AmcCallBackProc       amcBoundProc;    /* Function using upper bound approximation */ 
89  AmcFreeProc           amcFreeProc;     /* Function to free method-specific data structure */
90  int                   isVerified;      /* isVerified=1  whenever formula is verified */
91  Amc_Verified_Answer   amcAnswer;       /* {Unknown, True, False} */
92  int                   isMBM;           /* isMBM=1 when Machine by Machine method is applied */
93  int                   groupingMethod;  /* */
94  boolean               lowerBound;      /* lowerBound=1 when lower bound approximation is used */
95  int                   currentLevel;    /* Current lattice approximation level */ 
96};
97
98
99/*---------------------------------------------------------------------------*/
100/* Variable declarations                                                     */
101/*---------------------------------------------------------------------------*/
102
103
104/*---------------------------------------------------------------------------*/
105/* Macro declarations                                                        */
106/*---------------------------------------------------------------------------*/
107
108#define AmcSubsystemReadFsm(system) \
109  (system)->fsm
110
111#define AmcSubsystemSetFsm(system, data) \
112  (system)->fsm = (data)
113
114
115#define AmcSubsystemReadRelationArray(system) \
116  (system)->relationArray
117
118#define AmcSubsystemSetRelationArray(system, data) \
119  (system)->relationArray = (data)
120
121
122#define AmcSubsystemReadNextStateVarSmoothen(system) \
123  (system)->nextStateVarSmoothen
124
125#define AmcSubsystemSetNextStateVarSmoothen(system, data) \
126  (system)->nextStateVarSmoothen = (data)
127
128
129#define AmcSubsystemReadSatisfy(system) \
130  (system)->satisfyStates
131
132#define AmcSubsystemSetSatisfy(system, data) \
133  (system)->satisfyStates = (data)
134
135
136#define AmcSubsystemReadVertexTable(system) \
137  (system)->vertexTable
138
139#define AmcSubsystemSetVertexTable(system, data) \
140  (system)->vertexTable = (data)
141
142
143#define AmcSubsystemReadFanInTable(system) \
144  (system)->fanInTable
145
146#define AmcSubsystemSetFanInTable(system, data) \
147  (system)->fanInTable = (data)
148
149
150#define AmcSubsystemReadFanOutTable(system) \
151  (system)->fanOutTable
152
153#define AmcSubsystemSetFanOutTable(system, data) \
154  (system)->fanOutTable = (data)
155
156
157#define AmcSubsystemReadMethodSpecificData(system) \
158  (system)->methodSpecificData
159
160#define AmcSubsystemSetMethodSpecificData(system, data) \
161  (system)->methodSpecificData = (char *) (data)
162
163
164#define AmcReadInitialStates(system) \
165  (system)->initialStates
166
167#define AmcSetInitialStates(system, data) \
168  (system)->initialStates = (data)
169
170
171#define AmcReadOptimalSystem(system) \
172  (system)->optimalSystem
173
174#define AmcSetOptimalSystem(system, data) \
175  (system)->optimalSystem = (data)
176
177
178#define AmcReadMethodData(system) \
179  (system)->methodData
180
181#define AmcSetMethodData(system, data) \
182  (system)->methodData = (data)
183
184
185
186
187/**AutomaticStart*************************************************************/
188
189/*---------------------------------------------------------------------------*/
190/* Function prototypes                                                       */
191/*---------------------------------------------------------------------------*/
192
193EXTERN array_t  * AmcCreateSubsystemArray(Ntk_Network_t *network, Ctlp_Formula_t *formulA);
194EXTERN void AmcPrintOptimalSystem(FILE *fp, Amc_Info_t *amcInfo);
195EXTERN void AmcCheckSupportAndOutputFunctions(array_t *subSystemArray);
196EXTERN st_table * AmcCreateFunctionSupportTable(Mvf_Function_t *mvf);
197EXTERN mdd_t * AmcModelCheckAtomicFormula(Fsm_Fsm_t *modelFsm, Ctlp_Formula_t *ctlFormula);
198EXTERN int AmcBlockTearingProc(Amc_Info_t *amcInfo, Ctlp_Formula_t *formula, int verbosity);
199EXTERN void AmcFreeBlock(Amc_Info_t *amcInfo);
200EXTERN boolean FormulaTestIsForallQuantifier(Ctlp_Formula_t *formula);
201
202/**AutomaticEnd***************************************************************/
203
204#endif /* _AMCINT */
205
206
207
208
209
210
211
212
213
214
215
216
Note: See TracBrowser for help on using the repository browser.