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

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

vis2.3
File size: 21.5 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [fsmInt.h]
4
5  PackageName [fsm]
6
7  Synopsis    [Internal declarations for fsm package.]
8
9  Author [Shaker Sarwary, Tom Shiple, Rajeev Ranjan, Kavita Ravi, In-Ho Moon]
10
11  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
12  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 CALIFORNIA 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 CALIFORNIA 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: fsmInt.h,v 1.45 2003/01/22 18:44:20 jinh Exp $]
31
32******************************************************************************/
33
34#ifndef _FSMINT
35#define _FSMINT
36
37#include "fsm.h"
38#include "ord.h"
39#include "part.h"
40#include "mc.h"
41#include <string.h>
42
43/*---------------------------------------------------------------------------*/
44/* Structure declarations                                                    */
45/*---------------------------------------------------------------------------*/
46
47/**Struct**********************************************************************
48
49  Synopsis    [Canonical fairness constraint.]
50
51  Description [Canonical fairness constraint. This is an array of arrays, where
52  each entry is a pair of CTL formulas, S_ij and T_ij.  Each CTL formula
53  identifies a set of states of the FSM. The interpretation of this 2-D array
54  is: (OR_i (AND_j (F-inf S_ij + G-inf T_ij))). Hence, disjunctArray is an
55  array of array_t * of FairnessConjunct_t *.]
56
57  SeeAlso     [Fsm_FsmReadFairnessConstraint]
58
59******************************************************************************/
60struct FsmFairnessStruct {
61  Fsm_Fsm_t *fsm;         /* fsm to which the fairness constraint is associated */
62  array_t   *disjunctArray; /* canonical fairness constraint */
63};
64
65/**Enum************************************************************************
66
67  Synopsis [Specifies type of status of overapproximate reached states.]
68
69  Description [Specifies type of status of overapproximate reached states.]
70
71  SideEffects []
72
73  SeeAlso []
74 
75******************************************************************************/
76typedef enum {
77  Fsm_Ardc_NotConverged_c,
78  Fsm_Ardc_Valid_c,
79  Fsm_Ardc_Converged_c,
80  Fsm_Ardc_Exact_c
81} Fsm_Ardc_StatusType_t;
82
83
84/**Struct**********************************************************************
85
86  Synopsis    [A finite state machine.]
87
88  Description [A finite state machine.  See fsm.h for an overview of the
89  structure. Non-obvious fields are described here:
90
91  <p>the ith entry of the array reachabilityInfo.onionRings contains the set of
92  states reached in i steps from the initial states. The type of reachability
93  computation may have been approximate. Therefore the distance from the
94  initial state may not exactly be i. Further, these onion rings may not be
95  consistent with the reachable states. But their sum will always be smaller
96  than or equal to the reachableStates field.
97
98  <p>The onionRingsUpToDate field indicates whether the onion rings are
99  consistent with the reachable states.
100
101  <p>The onionRingsBFS field indicates whether onion rings were generated with
102  BFS.
103
104  <p>The depth pertains to the depth of computation with respect to the
105  reachableStates field. In case of approximate computation and reordering, the
106  depth and the exact onion rings may not be reproducible.
107
108  <p>The mode field indicates how the reachable states were generated. If they
109  were ever generated using HD, this is marked.
110
111  <p>FairnessInfo.states is the set of fair states (i.e. those states from
112  which there exists a fair path).  FairnessInfo.dbgArray is an array of
113  array_t* of mdd_t*, where the jth MDD of the ith array gives the set of
114  states that can reach the ith Buchi set in j or fewer steps.
115
116  <p>FsmData.nextStateFunctions is an array of strings, containing the names of
117  the nodes driving the data inputs of latches.
118
119  <p>presentStateVars, nextStateVars, and nextStateFunctions are all in
120  one-to-one correspondence.]
121
122******************************************************************************/
123struct FsmFsmStruct {
124  Ntk_Network_t   *network;   /* corresponding network */
125  graph_t         *partition; /* DAG of MVFs giving the next state fns */
126  Img_ImageInfo_t *imageInfo;
127  Img_ImageInfo_t *unquantifiedImageInfo;
128  bdd_t           *extQuantifyInputCube;
129  bdd_t           *uniQuantifyInputCube;
130  boolean useUnquantifiedFlag;
131  boolean FAFWFlag;
132
133  struct {
134    mdd_t *initialStates;
135    mdd_t *reachableStates; /* reachable states or an under-approximation */
136    int depth;   /* depth upto which the traversal was carried out. */
137    Fsm_RchType_t reachabilityMode;   /* indicates what mode(BFS/HD) was
138                                         applied to reachability. */
139    Fsm_RchStatus_t rchStatus;  /* specified whether the reachable states is
140                                   exact or an under approximation or
141                                   an over aproximation. */
142    Fsm_Ardc_StatusType_t overApprox;  /* status of current overapproximate
143                                          reached states. */
144    array_t *apprReachableStates; /* to store overapproximate reachable states*/
145    array_t *subPsVars; /* to store real present state variables of submachines
146                           in over-approximate  reachability computation */
147    array_t *onionRings;   /* array of mdd_t* */
148    Fsm_RchType_t onionRingsMode; /* indicates whether onion rings were
149                                generated with BFS or some approximate method */
150    boolean onionRingsUpToDate;  /* flag which indicates whether the sum of
151                                    onion rings is equal to reachable states */
152  } reachabilityInfo;
153
154  struct {
155    mdd_t *states;
156    Fsm_Fairness_t *constraint;
157    array_t *dbgArray;                /* array of array_t* of mdd_t* */
158  } fairnessInfo;
159
160  struct {
161    array_t *presentStateVars;        /* array of MDD id's */
162    array_t *nextStateVars;           /* array of MDD id's */
163    array_t *inputVars;               /* array of MDD id's */
164    array_t *nextStateFunctions;      /* array of char* */
165    /* The following 3 are just for subsystems.
166     * inputVars = primaryInputVars + pseudoInputVars
167     * globalPsVars = presentStateVars + pseudoInputVars
168     */
169    array_t *pseudoInputVars;         /* array of MDD id's */
170    array_t *primaryInputVars;        /* array of MDD id's */
171    array_t *globalPsVars;            /* array of MDD id's */
172    mdd_t   *presentStateCube;
173    mdd_t   *nextStateCube;
174    mdd_t   *inputCube;
175    mdd_t   *pseudoInputCube;
176    mdd_t   *primaryInputCube;
177    mdd_t   *globalPsCube;
178    array_t *presentStateBddVars;     /* array of bdd variables */
179    array_t *pseudoInputBddVars;      /* array of bdd variables */
180    boolean createVarCubesFlag;
181  } fsmData;
182};
183
184/**Struct**********************************************************************
185
186  Synopsis [Specifies options for ARDC computation.]
187
188  Description [Specifies options for ARDC computation.]
189
190  SideEffects []
191 
192  SeeAlso []
193
194******************************************************************************/
195struct FsmArdcOptionsStruct {
196    Fsm_Ardc_TraversalType_t traversalMethod; /* one of MBM, RFBF, TFBF, TMBM,
197                                                 LMBM, SIMPLE */
198    int groupSize; /* number of latches per group in state space
199                      decomposition */
200    float affinityFactor; /* controls weight between dependency and
201                             correlation in state space decomposition */
202    Img_MinimizeType constrainMethod;
203                /* which operator is going to be used for image constraining
204                ** operation among restrict, constrain, compact, and squeeze */
205    Fsm_Ardc_ConstrainTargetType_t constrainTarget;
206                /* where to apply image constraining between
207                ** transition relation and initial states */
208    int maxIteration; /* maximum iteration number in approximate traversal */
209    Fsm_Ardc_AbstPpiType_t abstractPseudoInput;
210                /* when to abstract pseudo input variables
211                ** from transition relation or reachable states */
212    boolean decomposeFlag;
213                /* whether to use single conjuncted approximate reachable
214                ** states or decomposed approximate reachable states */
215    boolean projectedInitialFlag; /* whether to use original initial states or
216                                     projected initial states */
217    boolean constrainReorderFlag; /* if set, allow variable reorderings
218                                     during image constraining operation */
219    Img_MethodType ardcImageMethod;
220    boolean useHighDensity; /* if set, use high density */
221    boolean reorderPtrFlag;
222    int faninConstrainMode;
223    char *readGroupFile;
224    char *writeGroupFile;
225    int lmbmInitialStatesMode;
226    boolean mbmReuseTrFlag;
227    int createPseudoVarMode;
228    int verbosity; /* print more information */
229};
230
231/**Struct**********************************************************************
232  Synopsis [Approximate Traversal option structure.]
233
234  Description [Approximate Traversal option structure. Set by set commands. See help in CommandPrintHdOptions.]
235
236  SideEffects []
237 
238  SeeAlso []
239 
240******************************************************************************/
241struct FsmHdTravOptions {
242  int nvars; /* number of bdd state variables */
243  bdd_approx_type_t frontierApproxMethod; /* type of approximation to use to extract subset of from */
244  int frontierApproxThreshold; /* threshold for approximation */
245  Fsm_HdDeadEndType_t deadEnd; /* kind of dead-end method to use */
246  bdd_approx_type_t deadEndSubsetMethod;  /* which approximation method to use in dead-ends */
247  double quality; /* quality factor for bdd_apprxo_remap_ua method */
248  double qualityBias; /* quality factor for bdd_approx_remap_ua method */
249  boolean scrapStates; /* option to not add scrap states */
250  boolean newOnly; /* option to pick frontier from the new states only */
251  boolean onlyPartialImage; /* option to only use partial image computation */
252};
253
254
255/**Struct**********************************************************************
256  Synopsis [Stats structure to store size and minterm count]
257
258  Description [Stats structure to store size and minterm count]
259
260  SideEffects []
261 
262  SeeAlso []
263   
264******************************************************************************/
265struct FsmHdMintSizeStats {
266  int sizeTo;  /* size of image */
267  double mintermTo; /* minterms of image */
268  int sizeFrom; /* size of from (frontier) */
269  double mintermFrom; /* minterms of from (frontier) */
270  int sizeFromSubset; /* size of subset of frontier */
271  double mintermFromSubset; /* minterms of subset of frontier */
272  int sizeReached; /* size of reached set */
273  double mintermReached; /* minterms of reached set */
274}; 
275
276
277/**Struct**********************************************************************
278  Synopsis [Structure to store HD related information.]
279
280  Description [Structure to store HD related information.]
281
282  SideEffects []
283 
284  SeeAlso []
285   
286******************************************************************************/
287struct FsmHdStruct {
288  int numDeadEnds; /* number of dead computations performed. */
289  boolean firstSubset; /* indicates that first subset has been computed*/
290  int lastIter;    /* indicates the last iteration in which a slow growth
291                    * of reached was recorded. */
292  boolean partialImage;/* iff partial image computation was performed */
293  int residueCount;/* number of times the residue has been used in a dead end*/
294  mdd_t *interiorStates; /* states which cannot produce any new states */
295  mdd_t *interiorStateCandidate; /* states which could potentially belong to
296                                  * interior states. */
297  mdd_t *deadEndResidue; /*  states which do not lie in dense subset
298                          * of "from" after dead-end computation */
299  struct FsmHdTravOptions *options;     /* options for HD traversal */
300  struct FsmHdMintSizeStats *stats; /* structure storing minterms and sizes of the
301                                * various BDDs of traversal.
302                                */
303  boolean imageOfReachedComputed;  /* iff image of reached set was computed.*/
304  boolean onlyPartialImage;    /* flag indicating that only partial image
305                                * should be used during traversal. */
306  int slowGrowth;  /* number of successive iterations of slow growth of
307                    * reached */
308
309  boolean deadEndWithOriginalTR; /* this flag allows computing a dead end at
310                                          * the end if all the frontier under the original
311                                          * TR is generated at some point. */
312  boolean deadEndComputation;
313};
314
315
316
317/*---------------------------------------------------------------------------*/
318/* Type declarations                                                         */
319/*---------------------------------------------------------------------------*/
320typedef struct FsmHdMintSizeStats FsmHdMintSizeStats_t;
321typedef struct FsmHdStruct FsmHdStruct_t;
322
323/**Struct**********************************************************************
324  Synopsis [Enumerated type to specify various quantities in HD]
325******************************************************************************/
326typedef enum {
327    Fsm_Hd_From,
328    Fsm_Hd_To,
329    Fsm_Hd_FromSubset,
330    Fsm_Hd_Reached
331} Fsm_Hd_Quant_t;
332
333/*---------------------------------------------------------------------------*/
334/* Macro declarations                                                        */
335/*---------------------------------------------------------------------------*/
336
337/**Struct**********************************************************************
338  Synopsis [Read Minterms of Reached from stats structure]
339
340******************************************************************************/
341#define FsmHdStatsReadMintermReached(stats) (stats->mintermReached)
342
343/**Struct**********************************************************************
344  Synopsis [Read Minterms of To from stats structure]
345
346******************************************************************************/
347#define FsmHdStatsReadMintermTo(stats) (stats->mintermTo)
348
349/**Struct**********************************************************************
350  Synopsis [Read Minterms of From from stats structure]
351
352******************************************************************************/
353#define FsmHdStatsReadMintermFrom(stats) (stats->mintermFrom)
354
355/**Struct**********************************************************************
356  Synopsis [Read Minterms of FromSubset from stats structure]
357
358******************************************************************************/
359#define FsmHdStatsReadMintermFromSubset(stats) (stats->mintermFromSubset)
360
361/**Struct**********************************************************************
362  Synopsis [Read Size of Reached from stats structure]
363
364******************************************************************************/
365#define FsmHdStatsReadSizeReached(stats) (stats->sizeReached)
366
367/**Struct**********************************************************************
368  Synopsis [Read Size of To from stats structure]
369
370******************************************************************************/
371#define FsmHdStatsReadSizeTo(stats) (stats->sizeTo)
372
373/**Struct**********************************************************************
374  Synopsis [Read Size of From from stats structure]
375
376******************************************************************************/
377#define FsmHdStatsReadSizeFrom(stats) (stats->sizeFrom)
378
379/**Struct**********************************************************************
380  Synopsis [Read Size of FromSubset from stats structure]
381
382******************************************************************************/
383#define FsmHdStatsReadSizeFromSubset(stats) (stats->sizeFromSubset)
384
385/**Struct**********************************************************************
386  Synopsis [Read Density of From from stats structure]
387
388******************************************************************************/
389#define FsmHdStatsReadDensityFrom(stats) \
390              (FsmHdStatsReadMintermFrom(stats)/FsmHdStatsReadSizeFrom(stats))
391
392/**Struct**********************************************************************
393  Synopsis [Read Density of FromSubset from stats structure]
394
395******************************************************************************/
396#define FsmHdStatsReadDensityFromSubset(stats) \
397  (FsmHdStatsReadMintermFromSubset(stats)/FsmHdStatsReadSizeFromSubset(stats))
398
399/**Struct**********************************************************************
400  Synopsis [Read Density of Reached from stats structure]
401
402******************************************************************************/
403#define FsmHdStatsReadDensityReached(stats) \
404        (FsmHdStatsReadMintermReached(stats)/FsmHdStatsReadSizeReached(stats))
405
406/**Struct**********************************************************************
407  Synopsis [Set Size of From from stats structure]
408
409******************************************************************************/
410#define FsmHdStatsSetSizeFrom(stats, value) (stats->sizeFrom = value)
411
412/**Struct**********************************************************************
413  Synopsis [Set Minterm of From from stats structure]
414
415******************************************************************************/
416#define FsmHdStatsSetMintermFrom(stats, value) (stats->mintermFrom = value)
417
418/**Struct**********************************************************************
419  Synopsis [Set Size of FromSubset from stats structure]
420
421******************************************************************************/
422#define FsmHdStatsSetSizeFromSubset(stats, value) \
423                                   (stats->sizeFromSubset = value)
424
425/**Struct**********************************************************************
426  Synopsis [Set Minterm of FromSubset from stats structure]
427
428******************************************************************************/
429#define FsmHdStatsSetMintermFromSubset(stats, value) \
430                                      (stats->mintermFromSubset = value)
431
432/**Struct**********************************************************************
433  Synopsis [Set Size of Reached from stats structure]
434
435******************************************************************************/
436#define FsmHdStatsSetSizeReached(stats, value) (stats->sizeReached = value)
437
438
439/**AutomaticStart*************************************************************/
440
441/*---------------------------------------------------------------------------*/
442/* Function prototypes                                                       */
443/*---------------------------------------------------------------------------*/
444
445EXTERN int FsmArdcCheckInvariant(Fsm_Fsm_t *fsm, array_t *invarStates);
446EXTERN void FsmArdcPrintOptions(void);
447EXTERN void FsmArdcPrintOverApproximateReachableStates(Fsm_Fsm_t *fsm);
448EXTERN void FsmArdcPrintExactReachableStates(Fsm_Fsm_t *fsm);
449EXTERN void FsmArdcPrintBddOfNode(Fsm_Fsm_t *fsm, mdd_t *node);
450EXTERN void FsmArdcPrintArrayOfArrayInt(array_t *arrayOfArray);
451EXTERN boolean FsmGetArdcSetBooleanValue(char *string, boolean defaultValue);
452EXTERN Fsm_Fairness_t * FsmFsmCreateDefaultFairnessConstraint(Fsm_Fsm_t *fsm);
453EXTERN boolean FsmFairnessConstraintIsDefault(Fsm_Fairness_t *fairness);
454EXTERN void FsmFairnessFree(Fsm_Fairness_t *fairness);
455EXTERN Fsm_Fairness_t * FsmFairnessAlloc(Fsm_Fsm_t *fsm);
456EXTERN void FsmFairnessAddConjunct(Fsm_Fairness_t *fairness, Ctlp_Formula_t *finallyInf, Ctlp_Formula_t *globallyInf, int i, int j);
457EXTERN void FsmFsmFairnessInfoUpdate(Fsm_Fsm_t *fsm, mdd_t *states, Fsm_Fairness_t *constraint, array_t *dbgArray);
458EXTERN void FsmSetReachabilityOnionRings(Fsm_Fsm_t *fsm, array_t *onionRings);
459EXTERN void FsmSetReachabilityOnionRingsMode(Fsm_Fsm_t *fsm, Fsm_RchType_t value);
460EXTERN void FsmSetReachabilityOnionRingsUpToDateFlag(Fsm_Fsm_t *fsm, boolean value);
461EXTERN void FsmSetReachabilityApproxComputationStatus(Fsm_Fsm_t *fsm, Fsm_RchStatus_t value);
462EXTERN void FsmSetReachabilityOverApproxComputationStatus(Fsm_Fsm_t *fsm, Fsm_Ardc_StatusType_t status);
463EXTERN Fsm_Ardc_StatusType_t FsmReadReachabilityOverApproxComputationStatus(Fsm_Fsm_t *fsm);
464EXTERN void FsmSetReachabilityComputationMode(Fsm_Fsm_t *fsm, Fsm_RchType_t value);
465EXTERN Fsm_RchType_t FsmReadReachabilityComputationMode(Fsm_Fsm_t *fsm);
466EXTERN void FsmResetReachabilityFields(Fsm_Fsm_t *fsm, Fsm_RchType_t approxFlag);
467EXTERN FsmHdStruct_t * FsmHdStructAlloc(int nvars);
468EXTERN void FsmHdStructFree(FsmHdStruct_t *hdInfo);
469EXTERN void FsmGuidedSearchPrintOptions(void);
470EXTERN FsmHdMintSizeStats_t * FsmHdStatsStructAlloc(void);
471EXTERN void FsmHdStatsStructFree(FsmHdMintSizeStats_t *stats);
472EXTERN void FsmHdStatsComputeSizeAndMinterms(mdd_manager *mddManager, mdd_t *f, array_t *varArray, int nvars, Fsm_Hd_Quant_t field, FsmHdMintSizeStats_t *stats);
473EXTERN void FsmHdStatsReset(FsmHdMintSizeStats_t *stats, Fsm_Hd_Quant_t field);
474EXTERN void FsmHdPrintOptions(void);
475EXTERN mdd_t * FsmHdDeadEnd(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, mdd_t *reachableStates, FsmHdStruct_t *hdInfo, array_t *varArray, int greedy, int verbosity);
476EXTERN void FsmHdFromComputeDenseSubset(mdd_manager *mddManager, mdd_t **fromLowerBound, mdd_t **fromUpperBound, mdd_t **reachableStates, mdd_t **image, mdd_t *initialStates, FsmHdStruct_t *hdInfo, int shellFlag, array_t *onionRings, int sizeOfOnionRings, array_t *varArray);
477
478/**AutomaticEnd***************************************************************/
479
480#endif /* _FSMINT */
Note: See TracBrowser for help on using the repository browser.