ntr.h Source File

00001 
00024 #ifndef _NTR
00025 #define _NTR
00026 
00027 /*---------------------------------------------------------------------------*/
00028 /* Nested includes                                                           */
00029 /*---------------------------------------------------------------------------*/
00030 
00031 #include "dddmp.h"
00032 #include "bnet.h"
00033 
00034 /*---------------------------------------------------------------------------*/
00035 /* Constant declarations                                                     */
00036 /*---------------------------------------------------------------------------*/
00037 
00038 #define PI_PS_FROM_FILE 0
00039 #define PI_PS_DFS 1
00040 #define PI_PS_GIVEN 2
00041 
00042 #define NTR_IMAGE_MONO 0
00043 #define NTR_IMAGE_PART 1
00044 #define NTR_IMAGE_CLIP 2
00045 #define NTR_IMAGE_DEPEND 3
00046 
00047 #define NTR_UNDER_APPROX 0
00048 #define NTR_OVER_APPROX 1
00049 
00050 #define NTR_FROM_NEW 0
00051 #define NTR_FROM_REACHED 1
00052 #define NTR_FROM_RESTRICT 2
00053 #define NTR_FROM_COMPACT 3
00054 #define NTR_FROM_SQUEEZE 4
00055 #define NTR_FROM_UNDERAPPROX 5
00056 #define NTR_FROM_OVERAPPROX 6
00057 
00058 #define NTR_GROUP_NONE 0
00059 #define NTR_GROUP_DEFAULT 1
00060 #define NTR_GROUP_FIXED 2
00061 
00062 /*---------------------------------------------------------------------------*/
00063 /* Stucture declarations                                                     */
00064 /*---------------------------------------------------------------------------*/
00065 
00066 /*---------------------------------------------------------------------------*/
00067 /* Type declarations                                                         */
00068 /*---------------------------------------------------------------------------*/
00069 
00070 typedef struct  NtrOptions {
00071     long  initialTime;  /* this is here for convenience */
00072     int   verify;   /* read two networks and compare them */
00073     char  *file1;   /* first network file name */
00074     char  *file2;   /* second network file name */
00075     int   second;   /* a second network is given */
00076     int   traverse; /* do reachability analysis */
00077     int   depend;   /* do latch dependence analysis */
00078     int   image;    /* monolithic, partitioned, or clip */
00079     double  imageClip;  /* clipping depth in image computation */
00080     int   approx;   /* under or over approximation */
00081     int   threshold;  /* approximation threshold */
00082     int   from;   /* method to compute from states */
00083     int   groupnsps;  /* group present state and next state vars */
00084     int   closure;  /* use transitive closure */
00085     double  closureClip;  /* clipping depth in closure computation */
00086     int   envelope; /* compute outer envelope */
00087     int   scc;    /* compute strongly connected components */
00088     int   zddtest;  /* do zdd test */
00089     int   maxflow;  /* compute maximum flow in network */
00090     char  *sinkfile;  /* file for externally provided sink node */
00091     int   partition;  /* test McMillan conjunctive partitioning */
00092     int   char2vect;  /* test char-to-vect decomposition */
00093     int   density;  /* test density-related functions */
00094     double  quality;  /* quality parameter for density functions */
00095     int   decomp;   /* test decomposition functions */
00096     int   cofest;   /* test cofactor estimation */
00097     double  clip;   /* test clipping functions */
00098     int   noBuild;  /* do not build BDDs; just echo order */
00099     int   stateOnly;  /* ignore primary outputs */
00100     char  *node;    /* only node for which to build BDD */
00101     int   locGlob;  /* build global or local BDDs */
00102     int   progress; /* report output names while building BDDs */
00103     int   cacheSize;  /* computed table initial size */
00104     unsigned long maxMemory;  /* computed table maximum size */
00105     int   slots;    /* unique subtable initial slots */
00106     int   ordering; /* FANIN DFS ... */
00107     char  *orderPiPs; /* file for externally provided order */
00108     Cudd_ReorderingType reordering; /* NONE RANDOM PIVOT SIFTING ... */
00109     int   autoDyn;  /* ON OFF */
00110     Cudd_ReorderingType autoMethod; /* RANDOM PIVOT SIFTING CONVERGE ... */
00111     char  *treefile;  /* file name for variable tree */
00112     int   firstReorder; /* when to do first reordering */
00113     int   countDead;  /* count dead nodes toward triggering
00114            reordering */
00115     int   maxGrowth;  /* maximum growth during reordering (%) */
00116     Cudd_AggregationType groupcheck; /* grouping function */
00117     int   arcviolation;   /* percent violation of arcs in
00118            extended symmetry check */
00119     int   symmviolation;  /* percent symm violation in
00120            extended symmetry check */
00121     int   recomb;   /* recombination parameter for grouping */
00122     int   nodrop;   /* don't drop intermediate BDDs ASAP */
00123     int   signatures; /* computation of signatures */
00124     int   gaOnOff;  /* whether to run GA at the end */
00125     int   populationSize; /* population size for GA */
00126     int   numberXovers; /* number of crossovers for GA */
00127     int   bdddump;  /* ON OFF */
00128     int   dumpFmt;  /* 0 -> dot 1 -> blif 2 ->daVinci 3 -> DDcal
00129         ** 4 -> factored form */
00130     char  *dumpfile;  /* filename for dump */
00131     int   store;    /* iteration at which to store Reached */
00132     char  *storefile; /* filename for storing Reached */
00133     int   load;   /* load initial states from file */
00134     char  *loadfile;  /* filename for loading states */
00135     int   verb;   /* level of verbosity */
00136 } NtrOptions;
00137 
00138 typedef struct NtrHeapSlot {
00139     void *item;
00140     int key;
00141 } NtrHeapSlot;
00142 
00143 typedef struct NtrHeap {
00144     int size;
00145     int nslots;
00146     NtrHeapSlot *slots;
00147 } NtrHeap;
00148 
00149 typedef struct NtrPartTR {
00150     int nparts;     /* number of parts */
00151     DdNode **part;    /* array of parts */
00152     DdNode **icube;   /* quantification cubes for image */
00153     DdNode **pcube;   /* quantification cubes for preimage */
00154     DdNode **nscube;    /* next state variables in each part */
00155     DdNode *preiabs;    /* present state vars and inputs in no part */
00156     DdNode *prepabs;    /* inputs in no part */
00157     DdNode *xw;     /* cube of all present states and PIs */
00158     NtrHeap *factors;   /* factors extracted from the image */
00159     int nlatches;   /* number of latches */
00160     DdNode **x;     /* array of present state variables */
00161     DdNode **y;     /* array of next state variables */
00162 } NtrPartTR;
00163 
00164 /*---------------------------------------------------------------------------*/
00165 /* Variable declarations                                                     */
00166 /*---------------------------------------------------------------------------*/
00167 
00168 /*---------------------------------------------------------------------------*/
00169 /* Macro declarations                                                        */
00170 /*---------------------------------------------------------------------------*/
00171 
00172 /* These are potential duplicates. */
00173 #ifndef EXTERN
00174 #   ifdef __cplusplus
00175 # define EXTERN extern "C"
00176 #   else
00177 # define EXTERN extern
00178 #   endif
00179 #endif
00180 #ifndef ARGS
00181 #   if defined(__STDC__) || defined(__cplusplus)
00182 # define ARGS(protos) protos    /* ANSI C */
00183 #   else /* !(__STDC__ || __cplusplus) */
00184 # define ARGS(protos) ()    /* K&R C */
00185 #   endif /* !(__STDC__ || __cplusplus) */
00186 #endif
00187 
00188 #ifndef TRUE
00189 #   define TRUE 1
00190 #endif
00191 #ifndef FALSE
00192 #   define FALSE 0
00193 #endif
00194 
00206 #define STRING_EQUAL(s1,s2) (strcmp((s1),(s2)) == 0)
00207 
00208 
00211 /*---------------------------------------------------------------------------*/
00212 /* Function prototypes                                                       */
00213 /*---------------------------------------------------------------------------*/
00214 
00215 EXTERN int Ntr_buildDDs ARGS((BnetNetwork *net, DdManager *dd, NtrOptions *option, BnetNetwork *net2));
00216 EXTERN NtrPartTR * Ntr_buildTR ARGS((DdManager *dd, BnetNetwork *net, NtrOptions *option, int image));
00217 EXTERN DdNode * Ntr_TransitiveClosure ARGS((DdManager *dd, NtrPartTR *TR, NtrOptions *option));
00218 EXTERN int Ntr_Trav ARGS((DdManager *dd, BnetNetwork *net, NtrOptions *option));
00219 EXTERN int Ntr_SCC ARGS((DdManager *dd, BnetNetwork *net, NtrOptions *option));
00220 EXTERN int Ntr_ClosureTrav ARGS((DdManager *dd, BnetNetwork *net, NtrOptions *option));
00221 EXTERN void Ntr_freeTR ARGS((DdManager *dd, NtrPartTR *TR));
00222 EXTERN NtrPartTR * Ntr_cloneTR ARGS((NtrPartTR *TR));
00223 EXTERN DdNode * Ntr_initState ARGS((DdManager *dd, BnetNetwork *net, NtrOptions *option));
00224 EXTERN DdNode * Ntr_getStateCube ARGS((DdManager *dd, BnetNetwork *net, char *filename, int pr));
00225 EXTERN int Ntr_Envelope ARGS((DdManager *dd, NtrPartTR *TR, FILE *dfp, NtrOptions *option));
00226 EXTERN int Ntr_TestMinimization ARGS((DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option));
00227 EXTERN int Ntr_TestDensity ARGS((DdManager *dd, BnetNetwork *net1, NtrOptions *option));
00228 EXTERN int Ntr_TestDecomp ARGS((DdManager *dd, BnetNetwork *net1, NtrOptions *option));
00229 EXTERN int Ntr_VerifyEquivalence ARGS((DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option));
00230 EXTERN int Ntr_TestCofactorEstimate ARGS((DdManager * dd, BnetNetwork * net, NtrOptions * option));
00231 EXTERN int Ntr_TestClipping ARGS((DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option));
00232 EXTERN int Ntr_maxflow ARGS((DdManager *dd, BnetNetwork *net, NtrOptions *option));
00233 EXTERN double Ntr_maximum01Flow ARGS((DdManager *bdd, DdNode *sx, DdNode *ty, DdNode *E, DdNode **F, DdNode **cut, DdNode **x, DdNode **y, DdNode **z, int n, int pr));
00234 EXTERN int Ntr_testZDD ARGS((DdManager *dd, BnetNetwork *net, NtrOptions *option));
00235 EXTERN int Ntr_testISOP ARGS((DdManager *dd, BnetNetwork *net, NtrOptions *option));
00236 EXTERN NtrHeap * Ntr_InitHeap ARGS((int size));
00237 EXTERN void Ntr_FreeHeap ARGS((NtrHeap *heap));
00238 EXTERN int Ntr_HeapInsert ARGS((NtrHeap *heap, void *item, int key));
00239 EXTERN int Ntr_HeapExtractMin ARGS((NtrHeap *heap, void **item, int *key));
00240 EXTERN int Ntr_HeapCount ARGS((NtrHeap *heap));
00241 EXTERN NtrHeap * Ntr_HeapClone ARGS((NtrHeap *source));
00242 EXTERN int Ntr_TestHeap ARGS((NtrHeap *heap, int i));
00243 
00246 #endif /* _NTR */