source: vis_dev/vis-2.3/src/fsm/fsm.h @ 21

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

un delete de trop
File size: 18.5 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [fsm.h]
4
5  PackageName [fsm]
6
7  Synopsis    [Finite state machine abstraction of a network.]
8
9  Description [A finite state machine contains a pointer to a network, so it
10  inherits all the information that is contained in the network, such as node
11  names and MDD ids.  An FSM has a partition associated with it; the output
12  and next state functions are derived from the partition.  This partition
13  does not necessarily have to be the default partition associated with the
14  network.<p>
15
16  The FSM maintains information relating to state reachability
17  (initial states, reachable states, underapprox or not, and the
18  partition of reachable states into "onion rings"), and fairness
19  information (fair states, fairness constraints, and generic
20  debugging information).  Also, the FSM stores the MDD ids of present
21  state, next state, and input variables, in a convenient format.]
22
23  Author [Shaker Sarwary, Tom Shiple, Rajeev Ranjan, Kavita Ravi, In-Ho Moon]
24
25  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
26  All rights reserved.
27
28  Permission is hereby granted, without written agreement and without license
29  or royalty fees, to use, copy, modify, and distribute this software and its
30  documentation for any purpose, provided that the above copyright notice and
31  the following two paragraphs appear in all copies of this software.
32
33  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
34  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
35  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
36  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
37
38  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
39  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
40  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
41  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
42  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
43
44  Revision    [$Id: fsm.h,v 1.76 2005/05/13 08:30:30 hhhan Exp $]
45
46******************************************************************************/
47
48#ifndef _FSM
49#define _FSM
50
51/*---------------------------------------------------------------------------*/
52/* Nested includes                                                           */
53/*---------------------------------------------------------------------------*/
54#include "img.h"
55#include "ctlp.h"
56
57/*---------------------------------------------------------------------------*/
58/* Constant declarations                                                     */
59/*---------------------------------------------------------------------------*/
60#define FSM_NETWORK_APPL_KEY "Fsm_NetworkApplKey"
61#define Fsm_Rch_Default_c Fsm_Rch_Bfs_c
62
63/*---------------------------------------------------------------------------*/
64/* Type declarations                                                         */
65/*---------------------------------------------------------------------------*/
66typedef struct FsmFsmStruct Fsm_Fsm_t;
67typedef struct FsmFairnessStruct Fsm_Fairness_t;
68typedef struct FsmArdcOptionsStruct Fsm_ArdcOptions_t;
69typedef struct FsmHdTravOptions FsmHdTravOptions_t;
70typedef array_t Fsm_HintsArray_t;
71
72/**Function********************************************************************
73
74  Synopsis [Specifies type of reachability computation.]
75
76  Description [Specifies type of reachability
77  computation. Fsm_Rch_Bfs_c specifies normal BFS. Fsm_Rch_Hd_c
78  specifies HD computation (Ravi & Somenzi ICCAD95). Fsm_Rch_Oa_c
79  specified Approximate reachability analysis first published by Cho
80  in EDAC'93. Fsm_Rch_PureSat_c is first published by Bing Li in BMC'03 ]
81
82  SideEffects []
83
84  SeeAlso []
85 
86******************************************************************************/
87typedef enum {
88    Fsm_Rch_Bfs_c,
89    Fsm_Rch_Gs_c,
90    Fsm_Rch_Hd_c,
91    Fsm_Rch_Oa_c,
92    Fsm_Rch_Grab_c,
93    Fsm_Rch_PureSat_c
94} Fsm_RchType_t;
95
96/**Function********************************************************************
97
98  Synopsis [Specifies the status of reachable states.]
99
100  Description [Specifies the status of reachable states.]
101
102  SideEffects []
103
104  SeeAlso []
105 
106******************************************************************************/
107typedef enum {
108    Fsm_Rch_Exact_c,
109    Fsm_Rch_Under_c,
110    Fsm_Rch_Over_c
111} Fsm_RchStatus_t;
112
113/**Function********************************************************************
114
115  Synopsis [Specifies type of dead-end computation.]
116
117  Description [Specifies type of dead-end computation. Fsm_Hd_DE_BF_c
118  implies computation of the entire Reached set. Fsm_Hd_DE_Con_c
119  specifies dead-end computation by decomposing Reached in terms of
120  disjunctive factors.  Fsm_Hd_DE_Hyb_c first tries to extract a
121  subset of Reached to compute its image. If no new states are found,
122  it computes the image of Reached by decomposing it into disjunctive
123  parts.]
124
125
126  SideEffects []
127
128  SeeAlso []
129 
130******************************************************************************/
131typedef enum {
132  Fsm_Hd_DE_BF_c,
133  Fsm_Hd_DE_Con_c,
134  Fsm_Hd_DE_Hyb_c
135} Fsm_HdDeadEndType_t;
136
137/**Enum************************************************************************
138
139  Synopsis [Specifies type of approximate FSM traversal.]
140
141  Description [Specifies type of approximate FSM traversal.]
142
143  SideEffects []
144
145  SeeAlso []
146 
147******************************************************************************/
148typedef enum {
149  Fsm_Ardc_Traversal_Mbm_c,
150  Fsm_Ardc_Traversal_Rfbf_c,
151  Fsm_Ardc_Traversal_Tfbf_c,
152  Fsm_Ardc_Traversal_Tmbm_c,
153  Fsm_Ardc_Traversal_Lmbm_c,
154  Fsm_Ardc_Traversal_Tlmbm_c,
155  Fsm_Ardc_Traversal_Simple_c
156} Fsm_Ardc_TraversalType_t;
157
158/**Enum************************************************************************
159
160  Synopsis [Specifies type of what-to-constrain.]
161
162  Description [Specifies type of what-to-constrain.]
163
164  SideEffects []
165
166  SeeAlso []
167 
168******************************************************************************/
169typedef enum {
170  Fsm_Ardc_Constrain_Tr_c, /* Tr : transition relation */
171  Fsm_Ardc_Constrain_Initial_c,
172  Fsm_Ardc_Constrain_Both_c
173} Fsm_Ardc_ConstrainTargetType_t;
174
175/**Enum************************************************************************
176
177  Synopsis [Specifies type of when to abstract pseudo PIs.]
178
179  Description [Specifies type of when to abstract pseudo PIs.]
180
181  SideEffects []
182
183  SeeAlso []
184 
185******************************************************************************/
186typedef enum {
187  Fsm_Ardc_Abst_Ppi_No_c,
188  Fsm_Ardc_Abst_Ppi_Before_Image_c,
189  Fsm_Ardc_Abst_Ppi_After_Image_c,
190  Fsm_Ardc_Abst_Ppi_At_End_c
191} Fsm_Ardc_AbstPpiType_t;
192
193#include "mc.h"
194
195/**AutomaticStart*************************************************************/
196
197/*---------------------------------------------------------------------------*/
198/* Function prototypes                                                       */
199/*---------------------------------------------------------------------------*/
200
201EXTERN void Fsm_ArdcMinimizeTransitionRelation(Fsm_Fsm_t *fsm, Img_DirectionType fwdbwd);
202EXTERN mdd_t * Fsm_ArdcComputeImage(Fsm_Fsm_t *fsm, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray);
203EXTERN array_t * Fsm_FsmComputeOverApproximateReachableStates(Fsm_Fsm_t *fsm, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, int recompute);
204EXTERN array_t * Fsm_ArdcComputeOverApproximateReachableStates(Fsm_Fsm_t *fsm, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, int recompute, Fsm_ArdcOptions_t *options);
205EXTERN array_t * Fsm_ArdcDecomposeStateSpace(Ntk_Network_t *network, array_t *presentStateVars, array_t *nextStateFunctions, Fsm_ArdcOptions_t *options);
206EXTERN Fsm_ArdcOptions_t * Fsm_ArdcAllocOptionsStruct(void);
207EXTERN void Fsm_ArdcGetDefaultOptions(Fsm_ArdcOptions_t *options);
208EXTERN Fsm_Ardc_TraversalType_t Fsm_ArdcOptionsReadTraversalMethod(Fsm_ArdcOptions_t *options);
209EXTERN int Fsm_ArdcOptionsReadGroupSize(Fsm_ArdcOptions_t *options);
210EXTERN float Fsm_ArdcOptionsReadAffinityFactor(Fsm_ArdcOptions_t *options);
211EXTERN Img_MinimizeType Fsm_ArdcOptionsReadConstrainMethod(Fsm_ArdcOptions_t *options);
212EXTERN Fsm_Ardc_ConstrainTargetType_t Fsm_ArdcOptionsReadConstrainTarget(Fsm_ArdcOptions_t *options);
213EXTERN int Fsm_ArdcOptionsReadMaxIteration(Fsm_ArdcOptions_t *options);
214EXTERN Fsm_Ardc_AbstPpiType_t Fsm_ArdcOptionsReadAbstractPseudoInput(Fsm_ArdcOptions_t *options);
215EXTERN boolean Fsm_ArdcOptionsReadDecomposeFlag(Fsm_ArdcOptions_t *options);
216EXTERN boolean Fsm_ArdcOptionsReadProjectedInitialFlag(Fsm_ArdcOptions_t *options);
217EXTERN boolean Fsm_ArdcOptionsReadConstrainReorderFlag(Fsm_ArdcOptions_t *options);
218EXTERN Img_MethodType Fsm_ArdcOptionsReadImageMethod(Fsm_ArdcOptions_t *options);
219EXTERN boolean Fsm_ArdcOptionsReadUseHighDensity(Fsm_ArdcOptions_t *options);
220EXTERN int Fsm_ArdcOptionsReadVerbosity(Fsm_ArdcOptions_t *options);
221EXTERN void Fsm_ArdcOptionsSetTraversalMethod(Fsm_ArdcOptions_t *options, Fsm_Ardc_TraversalType_t traversalMethod);
222EXTERN void Fsm_ArdcOptionsSetGroupSize(Fsm_ArdcOptions_t *options, int groupSize);
223EXTERN void Fsm_ArdcOptionsSetAffinityFactor(Fsm_ArdcOptions_t *options, float affinityFactor);
224EXTERN void Fsm_ArdcOptionsSetConstrainMethod(Fsm_ArdcOptions_t *options, Img_MinimizeType constrainMethod);
225EXTERN void Fsm_ArdcOptionsSetConstrainTarget(Fsm_ArdcOptions_t *options, Fsm_Ardc_ConstrainTargetType_t constrainTarget);
226EXTERN void Fsm_ArdcOptionsSetMaxIteration(Fsm_ArdcOptions_t *options, int maxIteration);
227EXTERN void Fsm_ArdcOptionsSetAbstractPseudoInput(Fsm_ArdcOptions_t *options, Fsm_Ardc_AbstPpiType_t abstractPseudoInput);
228EXTERN void Fsm_ArdcOptionsSetDecomposeFlag(Fsm_ArdcOptions_t *options, boolean decomposeFlag);
229EXTERN void Fsm_ArdcOptionsSetProjectedInitialFlag(Fsm_ArdcOptions_t *options, boolean projectedInitialFlag);
230EXTERN void Fsm_ArdcOptionsSetConstrainReorderFlag(Fsm_ArdcOptions_t *options, int constrainReorderFlag);
231EXTERN void Fsm_ArdcOptionsSetImageMethod(Fsm_ArdcOptions_t *options, Img_MethodType ardcImageMethod);
232EXTERN void Fsm_ArdcOptionsSetUseHighDensity(Fsm_ArdcOptions_t *options, boolean useHighDensity);
233EXTERN void Fsm_ArdcOptionsSetVerbosity(Fsm_ArdcOptions_t *options, int verbosity);
234EXTERN double Fsm_ArdcCountOnsetOfOverApproximateReachableStates(Fsm_Fsm_t *fsm);
235EXTERN int Fsm_ArdcBddSizeOfOverApproximateReachableStates(Fsm_Fsm_t *fsm);
236EXTERN mdd_t * Fsm_ArdcGetMddOfOverApproximateReachableStates(Fsm_Fsm_t *fsm);
237EXTERN void Fsm_ArdcPrintReachabilityResults(Fsm_Fsm_t *fsm, long elapseTime);
238EXTERN int Fsm_ArdcReadVerbosity(void);
239EXTERN void Fsm_Init(void);
240EXTERN void Fsm_End(void);
241EXTERN Fsm_Fairness_t * Fsm_FsmReadFairnessConstraint(Fsm_Fsm_t *fsm);
242EXTERN mdd_t * Fsm_FsmComputeFairStates(Fsm_Fsm_t *fsm, array_t *careSetArray, int verbosity, int dcLevel, Mc_GSHScheduleType schedule, Mc_FwdBwdAnalysis direction, boolean useEarlyTermination);
243EXTERN Ctlp_Formula_t * Fsm_FairnessReadFinallyInfFormula(Fsm_Fairness_t *fairness, int i, int j);
244EXTERN Ctlp_Formula_t * Fsm_FairnessReadGloballyInfFormula(Fsm_Fairness_t *fairness, int i, int j);
245EXTERN mdd_t * Fsm_FairnessObtainFinallyInfMdd(Fsm_Fairness_t *fairness, int i, int j, array_t *careSetArray, Mc_DcLevel dcLevel);
246EXTERN mdd_t * Fsm_FairnessObtainGloballyInfMdd(Fsm_Fairness_t *fairness, int i, int j, array_t *careSetArray, Mc_DcLevel dcLevel);
247EXTERN boolean Fsm_FairnessTestIsStreett(Fsm_Fairness_t *fairness);
248EXTERN boolean Fsm_FairnessTestIsBuchi(Fsm_Fairness_t *fairness);
249EXTERN int Fsm_FairnessReadNumDisjuncts(Fsm_Fairness_t *fairness);
250EXTERN int Fsm_FairnessReadNumConjunctsOfDisjunct(Fsm_Fairness_t *fairness, int i);
251EXTERN array_t * Fsm_FsmReadDebugArray(Fsm_Fsm_t *fsm);
252EXTERN Fsm_Fsm_t * Fsm_FsmCreateFromNetworkWithPartition(Ntk_Network_t *network, graph_t *partition);
253EXTERN Fsm_Fsm_t * Fsm_FsmCreateReducedFsm(Ntk_Network_t *network, graph_t *partition, array_t *latches, array_t *inputs, array_t *fairArray);
254EXTERN Fsm_Fsm_t * Fsm_FsmCreateAbstractFsm(Ntk_Network_t *network, graph_t *partition, array_t *latches, array_t *invisibleLatches, array_t *inputs, array_t *fairArray, boolean independentFlag);
255EXTERN void Fsm_FsmFree(Fsm_Fsm_t * fsm);
256EXTERN void Fsm_FsmSubsystemFree(Fsm_Fsm_t * fsm);
257EXTERN void Fsm_FsmFreeCallback(void * data);
258EXTERN Ntk_Network_t * Fsm_FsmReadNetwork(Fsm_Fsm_t * fsm);
259EXTERN mdd_manager * Fsm_FsmReadMddManager(Fsm_Fsm_t * fsm);
260EXTERN Fsm_Fsm_t * Fsm_NetworkReadOrCreateFsm(Ntk_Network_t * network);
261EXTERN Fsm_Fsm_t * Fsm_NetworkReadFsm(Ntk_Network_t * network);
262EXTERN Img_ImageInfo_t * Fsm_FsmReadImageInfo(Fsm_Fsm_t *fsm);
263EXTERN void Fsm_FsmFreeImageInfo(Fsm_Fsm_t *fsm);
264EXTERN graph_t * Fsm_FsmReadPartition(Fsm_Fsm_t *fsm);
265EXTERN boolean Fsm_FsmTestIsReachabilityDone(Fsm_Fsm_t *fsm);
266EXTERN boolean Fsm_FsmTestIsOverApproximateReachabilityDone(Fsm_Fsm_t *fsm);
267EXTERN mdd_t * Fsm_FsmReadReachableStates(Fsm_Fsm_t *fsm);
268EXTERN mdd_t * Fsm_FsmReadCurrentReachableStates(Fsm_Fsm_t *fsm);
269EXTERN array_t * Fsm_FsmReadOverApproximateReachableStates(Fsm_Fsm_t *fsm);
270EXTERN array_t * Fsm_FsmReadCurrentOverApproximateReachableStates(Fsm_Fsm_t *fsm);
271EXTERN array_t * Fsm_FsmReadReachabilityOnionRings(Fsm_Fsm_t *fsm);
272EXTERN boolean Fsm_FsmReachabilityOnionRingsStates(Fsm_Fsm_t *fsm, mdd_t ** result);
273EXTERN boolean Fsm_FsmTestReachabilityOnionRingsUpToDate(Fsm_Fsm_t *fsm);
274EXTERN Fsm_RchType_t Fsm_FsmReadReachabilityOnionRingsMode(Fsm_Fsm_t *fsm);
275EXTERN Img_ImageInfo_t * Fsm_FsmReadOrCreateImageInfo(Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag);
276EXTERN Img_ImageInfo_t * Fsm_FsmReadOrCreateImageInfoFAFW(Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag);
277EXTERN Img_ImageInfo_t * Fsm_FsmReadOrCreateImageInfoForComputingRange(Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag);
278EXTERN mdd_t * Fsm_FsmComputeInitialStates(Fsm_Fsm_t *fsm);
279EXTERN array_t * Fsm_FsmReadPresentStateVars(Fsm_Fsm_t *fsm);
280EXTERN array_t * Fsm_FsmReadNextStateVars(Fsm_Fsm_t *fsm);
281EXTERN array_t * Fsm_FsmReadNextStateFunctionNames(Fsm_Fsm_t *fsm);
282EXTERN array_t * Fsm_FsmReadInputVars(Fsm_Fsm_t *fsm);
283EXTERN array_t * Fsm_FsmReadPrimaryInputVars(Fsm_Fsm_t *fsm);
284EXTERN array_t * Fsm_FsmReadPseudoInputVars(Fsm_Fsm_t *fsm);
285EXTERN mdd_t * Fsm_FsmReadFairnessStates(Fsm_Fsm_t *fsm);
286EXTERN void Fsm_FsmSetInputVars(Fsm_Fsm_t *fsm, array_t *inputVars);
287EXTERN void Fsm_FsmSetInitialStates(Fsm_Fsm_t *fsm, mdd_t *initStates);
288EXTERN Fsm_Fsm_t * Fsm_HrcManagerReadCurrentFsm(Hrc_Manager_t *hmgr);
289EXTERN Fsm_Fsm_t * Fsm_FsmCreateSubsystemFromNetwork(Ntk_Network_t *network, graph_t *partition, st_table *vertexTable, boolean independentFlag, int createPseudoVarMode);
290EXTERN void Fsm_InstantiateHint(Fsm_Fsm_t *fsm, mdd_t *hint, int fwdFlag, int bwdFlag, Ctlp_Approx_t type, int printStatus);
291EXTERN void Fsm_CleanUpHints(Fsm_Fsm_t *fsm, int fwdFlag, int bwdFlag, int printStatus);
292EXTERN void Fsm_FsmFreeReachableStates(Fsm_Fsm_t *fsm);
293EXTERN void Fsm_FsmFreeOverApproximateReachableStates(Fsm_Fsm_t *fsm);
294EXTERN int Fsm_FsmGetReachableDepth(Fsm_Fsm_t *fsm);
295EXTERN boolean Fsm_FsmCheckSameSubFsmInTotalFsm(Fsm_Fsm_t *fsm, Fsm_Fsm_t *subFsm1, Fsm_Fsm_t *subFsm2);
296EXTERN Fsm_RchStatus_t Fsm_FsmReadReachabilityApproxComputationStatus(Fsm_Fsm_t *fsm);
297EXTERN void Fsm_MinimizeTransitionRelationWithReachabilityInfo(Fsm_Fsm_t *fsm, Img_DirectionType fwdbwd, boolean verbosity);
298EXTERN FsmHdTravOptions_t * Fsm_FsmHdGetTravOptions(int nvars);
299EXTERN void Fsm_FsmHdFreeTravOptions(FsmHdTravOptions_t *options);
300EXTERN int Fsm_FsmHdOptionReadNumVars(FsmHdTravOptions_t *options);
301EXTERN int Fsm_FsmHdOptionReadFrontierApproxThreshold(FsmHdTravOptions_t *options);
302EXTERN boolean Fsm_FsmHdOptionReadOnlyPartialImage(FsmHdTravOptions_t *options);
303EXTERN boolean Fsm_FsmHdOptionReadScrapStates(FsmHdTravOptions_t *options);
304EXTERN double Fsm_FsmHdOptionReadQuality(FsmHdTravOptions_t *options);
305EXTERN bdd_approx_type_t Fsm_FsmHdOptionReadFrontierApproxMethod(FsmHdTravOptions_t *options);
306EXTERN Fsm_HdDeadEndType_t Fsm_FsmHdOptionReadDeadEnd(FsmHdTravOptions_t *options);
307EXTERN boolean Fsm_FsmHdOptionReadNewOnly(FsmHdTravOptions_t *options);
308EXTERN bdd_approx_type_t Fsm_FsmHdOptionReadDeadEndSubsetMethod(FsmHdTravOptions_t *options);
309EXTERN int Fsm_FsmHdOptionSetFrontierApproxThreshold(FsmHdTravOptions_t *options, int threshold);
310EXTERN void Fsm_FsmHdOptionSetOnlyPartialImage(FsmHdTravOptions_t *options, boolean onlyPartial);
311EXTERN void Fsm_FsmHdOptionSetScrapStates(FsmHdTravOptions_t *options, boolean scrapStates);
312EXTERN void Fsm_FsmHdOptionSetQuality(FsmHdTravOptions_t *options, double quality);
313EXTERN void Fsm_FsmHdOptionSetFrontierApproxMethod(FsmHdTravOptions_t *options, bdd_approx_type_t approxMethod);
314EXTERN void Fsm_FsmHdOptionSetDeadEnd(FsmHdTravOptions_t *options, Fsm_HdDeadEndType_t deadEnd);
315EXTERN void Fsm_FsmHdOptionSetNewOnly(FsmHdTravOptions_t *options, boolean newOnly);
316EXTERN void Fsm_FsmHdOptionSetDeadEndSubsetMethod(FsmHdTravOptions_t *options, bdd_approx_type_t approxMethod);
317EXTERN mdd_t * Fsm_FsmComputeReachableStates(Fsm_Fsm_t *fsm, int incrementalFlag, int verbosityLevel, int printStep, int depthValue, int shellFlag, int reorderFlag, int reorderThreshold, Fsm_RchType_t approxFlag, int ardc, int recompute, array_t *invarStates, boolean printWarning, array_t *guideArray);
318EXTERN mdd_t * Fsm_MddMultiwayAndSmooth(mdd_manager *mddManager, array_t *mddArray, array_t *smoothingVars);
319EXTERN void Fsm_FsmReachabilityPrintResults(Fsm_Fsm_t *fsm, long elapseTime, int approxFlag);
320EXTERN void Fsm_FsmFairnessUpdate(Fsm_Fsm_t *fsm, array_t *formulaArray);
321EXTERN mdd_t *Fsm_FsmReadUniQuantifyInputCube(Fsm_Fsm_t *fsm);
322EXTERN mdd_t *Fsm_FsmReadExtQuantifyInputCube(Fsm_Fsm_t *fsm);
323EXTERN Img_ImageInfo_t * Fsm_FsmReadOrCreateImageInfoPrunedFAFW(Fsm_Fsm_t *fsm, mdd_t *Winning, int bwdImgFlag, int fwdImgFlag);
324EXTERN boolean Fsm_FsmReadUseUnquantifiedFlag( Fsm_Fsm_t * fsm);
325EXTERN void Fsm_FsmSetImageInfo( Fsm_Fsm_t *fsm, Img_ImageInfo_t *imageInfo);
326EXTERN void Fsm_FsmSetUseUnquantifiedFlag(Fsm_Fsm_t *fsm, boolean value);
327EXTERN int Fsm_FsmReadFAFWFlag(Fsm_Fsm_t *fsm);
328EXTERN void Fsm_FsmSetFAFWFlag(Fsm_Fsm_t *fsm, boolean FAFWFlag);
329EXTERN void Fsm_FsmSetSystemVariableFAFW(Fsm_Fsm_t *fsm, st_table *bddIdTable);
330EXTERN void Fsm_ImageInfoConjoinWithWinningStrategy( Fsm_Fsm_t *modelFsm, Img_DirectionType directionType, mdd_t *winningStrategy);
331EXTERN void Fsm_ImageInfoRecoverFromWinningStrategy( Fsm_Fsm_t *modelFsm, Img_DirectionType directionType);
332int ComputeNumberOfBinaryStateVariables(mdd_manager *mddManager, array_t *mddIdArray);
333
334/**AutomaticEnd***************************************************************/
335
336#endif /* _FSM */
Note: See TracBrowser for help on using the repository browser.