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

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

Vis main file for expermeriments
File size: 21.7 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    // For robustness computation
184  struct {
185    mdd_t * originalreachableStates;
186    mdd_t * Safe; FILE* fSafe;
187    mdd_t * Forb; FILE* fForb;
188    mdd_t * Req;  FILE* fReq;
189  } RobSets;
190
191};
192
193/**Struct**********************************************************************
194
195  Synopsis [Specifies options for ARDC computation.]
196
197  Description [Specifies options for ARDC computation.]
198
199  SideEffects []
200 
201  SeeAlso []
202
203******************************************************************************/
204struct FsmArdcOptionsStruct {
205    Fsm_Ardc_TraversalType_t traversalMethod; /* one of MBM, RFBF, TFBF, TMBM,
206                                                 LMBM, SIMPLE */
207    int groupSize; /* number of latches per group in state space
208                      decomposition */
209    float affinityFactor; /* controls weight between dependency and
210                             correlation in state space decomposition */
211    Img_MinimizeType constrainMethod;
212                /* which operator is going to be used for image constraining
213                ** operation among restrict, constrain, compact, and squeeze */
214    Fsm_Ardc_ConstrainTargetType_t constrainTarget;
215                /* where to apply image constraining between
216                ** transition relation and initial states */
217    int maxIteration; /* maximum iteration number in approximate traversal */
218    Fsm_Ardc_AbstPpiType_t abstractPseudoInput;
219                /* when to abstract pseudo input variables
220                ** from transition relation or reachable states */
221    boolean decomposeFlag;
222                /* whether to use single conjuncted approximate reachable
223                ** states or decomposed approximate reachable states */
224    boolean projectedInitialFlag; /* whether to use original initial states or
225                                     projected initial states */
226    boolean constrainReorderFlag; /* if set, allow variable reorderings
227                                     during image constraining operation */
228    Img_MethodType ardcImageMethod;
229    boolean useHighDensity; /* if set, use high density */
230    boolean reorderPtrFlag;
231    int faninConstrainMode;
232    char *readGroupFile;
233    char *writeGroupFile;
234    int lmbmInitialStatesMode;
235    boolean mbmReuseTrFlag;
236    int createPseudoVarMode;
237    int verbosity; /* print more information */
238};
239
240/**Struct**********************************************************************
241  Synopsis [Approximate Traversal option structure.]
242
243  Description [Approximate Traversal option structure. Set by set commands. See help in CommandPrintHdOptions.]
244
245  SideEffects []
246 
247  SeeAlso []
248 
249******************************************************************************/
250struct FsmHdTravOptions {
251  int nvars; /* number of bdd state variables */
252  bdd_approx_type_t frontierApproxMethod; /* type of approximation to use to extract subset of from */
253  int frontierApproxThreshold; /* threshold for approximation */
254  Fsm_HdDeadEndType_t deadEnd; /* kind of dead-end method to use */
255  bdd_approx_type_t deadEndSubsetMethod;  /* which approximation method to use in dead-ends */
256  double quality; /* quality factor for bdd_apprxo_remap_ua method */
257  double qualityBias; /* quality factor for bdd_approx_remap_ua method */
258  boolean scrapStates; /* option to not add scrap states */
259  boolean newOnly; /* option to pick frontier from the new states only */
260  boolean onlyPartialImage; /* option to only use partial image computation */
261};
262
263
264/**Struct**********************************************************************
265  Synopsis [Stats structure to store size and minterm count]
266
267  Description [Stats structure to store size and minterm count]
268
269  SideEffects []
270 
271  SeeAlso []
272   
273******************************************************************************/
274struct FsmHdMintSizeStats {
275  int sizeTo;  /* size of image */
276  double mintermTo; /* minterms of image */
277  int sizeFrom; /* size of from (frontier) */
278  double mintermFrom; /* minterms of from (frontier) */
279  int sizeFromSubset; /* size of subset of frontier */
280  double mintermFromSubset; /* minterms of subset of frontier */
281  int sizeReached; /* size of reached set */
282  double mintermReached; /* minterms of reached set */
283}; 
284
285
286/**Struct**********************************************************************
287  Synopsis [Structure to store HD related information.]
288
289  Description [Structure to store HD related information.]
290
291  SideEffects []
292 
293  SeeAlso []
294   
295******************************************************************************/
296struct FsmHdStruct {
297  int numDeadEnds; /* number of dead computations performed. */
298  boolean firstSubset; /* indicates that first subset has been computed*/
299  int lastIter;    /* indicates the last iteration in which a slow growth
300                    * of reached was recorded. */
301  boolean partialImage;/* iff partial image computation was performed */
302  int residueCount;/* number of times the residue has been used in a dead end*/
303  mdd_t *interiorStates; /* states which cannot produce any new states */
304  mdd_t *interiorStateCandidate; /* states which could potentially belong to
305                                  * interior states. */
306  mdd_t *deadEndResidue; /*  states which do not lie in dense subset
307                          * of "from" after dead-end computation */
308  struct FsmHdTravOptions *options;     /* options for HD traversal */
309  struct FsmHdMintSizeStats *stats; /* structure storing minterms and sizes of the
310                                * various BDDs of traversal.
311                                */
312  boolean imageOfReachedComputed;  /* iff image of reached set was computed.*/
313  boolean onlyPartialImage;    /* flag indicating that only partial image
314                                * should be used during traversal. */
315  int slowGrowth;  /* number of successive iterations of slow growth of
316                    * reached */
317
318  boolean deadEndWithOriginalTR; /* this flag allows computing a dead end at
319                                          * the end if all the frontier under the original
320                                          * TR is generated at some point. */
321  boolean deadEndComputation;
322};
323
324
325
326/*---------------------------------------------------------------------------*/
327/* Type declarations                                                         */
328/*---------------------------------------------------------------------------*/
329typedef struct FsmHdMintSizeStats FsmHdMintSizeStats_t;
330typedef struct FsmHdStruct FsmHdStruct_t;
331
332/**Struct**********************************************************************
333  Synopsis [Enumerated type to specify various quantities in HD]
334******************************************************************************/
335typedef enum {
336    Fsm_Hd_From,
337    Fsm_Hd_To,
338    Fsm_Hd_FromSubset,
339    Fsm_Hd_Reached
340} Fsm_Hd_Quant_t;
341
342/*---------------------------------------------------------------------------*/
343/* Macro declarations                                                        */
344/*---------------------------------------------------------------------------*/
345
346/**Struct**********************************************************************
347  Synopsis [Read Minterms of Reached from stats structure]
348
349******************************************************************************/
350#define FsmHdStatsReadMintermReached(stats) (stats->mintermReached)
351
352/**Struct**********************************************************************
353  Synopsis [Read Minterms of To from stats structure]
354
355******************************************************************************/
356#define FsmHdStatsReadMintermTo(stats) (stats->mintermTo)
357
358/**Struct**********************************************************************
359  Synopsis [Read Minterms of From from stats structure]
360
361******************************************************************************/
362#define FsmHdStatsReadMintermFrom(stats) (stats->mintermFrom)
363
364/**Struct**********************************************************************
365  Synopsis [Read Minterms of FromSubset from stats structure]
366
367******************************************************************************/
368#define FsmHdStatsReadMintermFromSubset(stats) (stats->mintermFromSubset)
369
370/**Struct**********************************************************************
371  Synopsis [Read Size of Reached from stats structure]
372
373******************************************************************************/
374#define FsmHdStatsReadSizeReached(stats) (stats->sizeReached)
375
376/**Struct**********************************************************************
377  Synopsis [Read Size of To from stats structure]
378
379******************************************************************************/
380#define FsmHdStatsReadSizeTo(stats) (stats->sizeTo)
381
382/**Struct**********************************************************************
383  Synopsis [Read Size of From from stats structure]
384
385******************************************************************************/
386#define FsmHdStatsReadSizeFrom(stats) (stats->sizeFrom)
387
388/**Struct**********************************************************************
389  Synopsis [Read Size of FromSubset from stats structure]
390
391******************************************************************************/
392#define FsmHdStatsReadSizeFromSubset(stats) (stats->sizeFromSubset)
393
394/**Struct**********************************************************************
395  Synopsis [Read Density of From from stats structure]
396
397******************************************************************************/
398#define FsmHdStatsReadDensityFrom(stats) \
399              (FsmHdStatsReadMintermFrom(stats)/FsmHdStatsReadSizeFrom(stats))
400
401/**Struct**********************************************************************
402  Synopsis [Read Density of FromSubset from stats structure]
403
404******************************************************************************/
405#define FsmHdStatsReadDensityFromSubset(stats) \
406  (FsmHdStatsReadMintermFromSubset(stats)/FsmHdStatsReadSizeFromSubset(stats))
407
408/**Struct**********************************************************************
409  Synopsis [Read Density of Reached from stats structure]
410
411******************************************************************************/
412#define FsmHdStatsReadDensityReached(stats) \
413        (FsmHdStatsReadMintermReached(stats)/FsmHdStatsReadSizeReached(stats))
414
415/**Struct**********************************************************************
416  Synopsis [Set Size of From from stats structure]
417
418******************************************************************************/
419#define FsmHdStatsSetSizeFrom(stats, value) (stats->sizeFrom = value)
420
421/**Struct**********************************************************************
422  Synopsis [Set Minterm of From from stats structure]
423
424******************************************************************************/
425#define FsmHdStatsSetMintermFrom(stats, value) (stats->mintermFrom = value)
426
427/**Struct**********************************************************************
428  Synopsis [Set Size of FromSubset from stats structure]
429
430******************************************************************************/
431#define FsmHdStatsSetSizeFromSubset(stats, value) \
432                                   (stats->sizeFromSubset = value)
433
434/**Struct**********************************************************************
435  Synopsis [Set Minterm of FromSubset from stats structure]
436
437******************************************************************************/
438#define FsmHdStatsSetMintermFromSubset(stats, value) \
439                                      (stats->mintermFromSubset = value)
440
441/**Struct**********************************************************************
442  Synopsis [Set Size of Reached from stats structure]
443
444******************************************************************************/
445#define FsmHdStatsSetSizeReached(stats, value) (stats->sizeReached = value)
446
447
448/**AutomaticStart*************************************************************/
449
450/*---------------------------------------------------------------------------*/
451/* Function prototypes                                                       */
452/*---------------------------------------------------------------------------*/
453
454EXTERN int FsmArdcCheckInvariant(Fsm_Fsm_t *fsm, array_t *invarStates);
455EXTERN void FsmArdcPrintOptions(void);
456EXTERN void FsmArdcPrintOverApproximateReachableStates(Fsm_Fsm_t *fsm);
457EXTERN void FsmArdcPrintExactReachableStates(Fsm_Fsm_t *fsm);
458EXTERN void FsmArdcPrintBddOfNode(Fsm_Fsm_t *fsm, mdd_t *node);
459EXTERN void FsmArdcPrintArrayOfArrayInt(array_t *arrayOfArray);
460EXTERN boolean FsmGetArdcSetBooleanValue(char *string, boolean defaultValue);
461EXTERN Fsm_Fairness_t * FsmFsmCreateDefaultFairnessConstraint(Fsm_Fsm_t *fsm);
462EXTERN boolean FsmFairnessConstraintIsDefault(Fsm_Fairness_t *fairness);
463EXTERN void FsmFairnessFree(Fsm_Fairness_t *fairness);
464EXTERN Fsm_Fairness_t * FsmFairnessAlloc(Fsm_Fsm_t *fsm);
465EXTERN void FsmFairnessAddConjunct(Fsm_Fairness_t *fairness, Ctlp_Formula_t *finallyInf, Ctlp_Formula_t *globallyInf, int i, int j);
466EXTERN void FsmFsmFairnessInfoUpdate(Fsm_Fsm_t *fsm, mdd_t *states, Fsm_Fairness_t *constraint, array_t *dbgArray);
467EXTERN void FsmSetReachabilityOnionRings(Fsm_Fsm_t *fsm, array_t *onionRings);
468EXTERN void FsmSetReachabilityOnionRingsMode(Fsm_Fsm_t *fsm, Fsm_RchType_t value);
469EXTERN void FsmSetReachabilityOnionRingsUpToDateFlag(Fsm_Fsm_t *fsm, boolean value);
470EXTERN void FsmSetReachabilityApproxComputationStatus(Fsm_Fsm_t *fsm, Fsm_RchStatus_t value);
471EXTERN void FsmSetReachabilityOverApproxComputationStatus(Fsm_Fsm_t *fsm, Fsm_Ardc_StatusType_t status);
472EXTERN Fsm_Ardc_StatusType_t FsmReadReachabilityOverApproxComputationStatus(Fsm_Fsm_t *fsm);
473EXTERN void FsmSetReachabilityComputationMode(Fsm_Fsm_t *fsm, Fsm_RchType_t value);
474EXTERN Fsm_RchType_t FsmReadReachabilityComputationMode(Fsm_Fsm_t *fsm);
475EXTERN void FsmResetReachabilityFields(Fsm_Fsm_t *fsm, Fsm_RchType_t approxFlag);
476EXTERN FsmHdStruct_t * FsmHdStructAlloc(int nvars);
477EXTERN void FsmHdStructFree(FsmHdStruct_t *hdInfo);
478EXTERN void FsmGuidedSearchPrintOptions(void);
479EXTERN FsmHdMintSizeStats_t * FsmHdStatsStructAlloc(void);
480EXTERN void FsmHdStatsStructFree(FsmHdMintSizeStats_t *stats);
481EXTERN void FsmHdStatsComputeSizeAndMinterms(mdd_manager *mddManager, mdd_t *f, array_t *varArray, int nvars, Fsm_Hd_Quant_t field, FsmHdMintSizeStats_t *stats);
482EXTERN void FsmHdStatsReset(FsmHdMintSizeStats_t *stats, Fsm_Hd_Quant_t field);
483EXTERN void FsmHdPrintOptions(void);
484EXTERN mdd_t * FsmHdDeadEnd(mdd_manager *mddManager, Img_ImageInfo_t *imageInfo, mdd_t *reachableStates, FsmHdStruct_t *hdInfo, array_t *varArray, int greedy, int verbosity);
485EXTERN 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);
486
487/**AutomaticEnd***************************************************************/
488
489#endif /* _FSMINT */
Note: See TracBrowser for help on using the repository browser.