1 /** 2 @file 3 4 @ingroup nanotrav 5 6 @brief Simple-minded package to do traversal. 7 8 @author Fabio Somenzi 9 10 @copyright@parblock 11 Copyright (c) 1995-2015, Regents of the University of Colorado 12 13 All rights reserved. 14 15 Redistribution and use in source and binary forms, with or without 16 modification, are permitted provided that the following conditions 17 are met: 18 19 Redistributions of source code must retain the above copyright 20 notice, this list of conditions and the following disclaimer. 21 22 Redistributions in binary form must reproduce the above copyright 23 notice, this list of conditions and the following disclaimer in the 24 documentation and/or other materials provided with the distribution. 25 26 Neither the name of the University of Colorado nor the names of its 27 contributors may be used to endorse or promote products derived from 28 this software without specific prior written permission. 29 30 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 31 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 32 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 33 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE 34 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, 35 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, 36 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; 37 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER 38 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT 39 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN 40 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 41 POSSIBILITY OF SUCH DAMAGE. 42 @endparblock 43 44 */ 45 46 #ifndef _NTR 47 #define _NTR 48 49 /*---------------------------------------------------------------------------*/ 50 /* Nested includes */ 51 /*---------------------------------------------------------------------------*/ 52 53 #include "dddmp.h" 54 #include "bnet.h" 55 56 #ifdef __cplusplus 57 extern "C" { 58 #endif 59 60 /*---------------------------------------------------------------------------*/ 61 /* Constant declarations */ 62 /*---------------------------------------------------------------------------*/ 63 64 #define PI_PS_FROM_FILE 0 65 #define PI_PS_DFS 1 66 #define PI_PS_GIVEN 2 67 68 #define NTR_IMAGE_MONO 0 69 #define NTR_IMAGE_PART 1 70 #define NTR_IMAGE_CLIP 2 71 #define NTR_IMAGE_DEPEND 3 72 73 #define NTR_UNDER_APPROX 0 74 #define NTR_OVER_APPROX 1 75 76 #define NTR_FROM_NEW 0 77 #define NTR_FROM_REACHED 1 78 #define NTR_FROM_RESTRICT 2 79 #define NTR_FROM_COMPACT 3 80 #define NTR_FROM_SQUEEZE 4 81 #define NTR_FROM_UNDERAPPROX 5 82 #define NTR_FROM_OVERAPPROX 6 83 84 #define NTR_GROUP_NONE 0 85 #define NTR_GROUP_DEFAULT 1 86 #define NTR_GROUP_FIXED 2 87 88 #define NTR_SHORT_NONE 0 89 #define NTR_SHORT_BELLMAN 1 90 #define NTR_SHORT_FLOYD 2 91 #define NTR_SHORT_SQUARE 3 92 93 /*---------------------------------------------------------------------------*/ 94 /* Stucture declarations */ 95 /*---------------------------------------------------------------------------*/ 96 97 /*---------------------------------------------------------------------------*/ 98 /* Type declarations */ 99 /*---------------------------------------------------------------------------*/ 100 101 /** 102 @brief Options for nanotrav. 103 */ 104 typedef struct NtrOptions { 105 long initialTime; /**< this is here for convenience */ 106 int verify; /**< read two networks and compare them */ 107 char *file1; /**< first network file name */ 108 char *file2; /**< second network file name */ 109 int second; /**< a second network is given */ 110 int traverse; /**< do reachability analysis */ 111 int depend; /**< do latch dependence analysis */ 112 int image; /**< monolithic, partitioned, or clip */ 113 double imageClip; /**< clipping depth in image computation */ 114 int approx; /**< under or over approximation */ 115 int threshold; /**< approximation threshold */ 116 int from; /**< method to compute from states */ 117 int groupnsps; /**< group present state and next state vars */ 118 int closure; /**< use transitive closure */ 119 double closureClip; /**< clipping depth in closure computation */ 120 int envelope; /**< compute outer envelope */ 121 int scc; /**< compute strongly connected components */ 122 int zddtest; /**< do zdd test */ 123 int printcover; /**< print ISOP covers when testing ZDDs */ 124 int maxflow; /**< compute maximum flow in network */ 125 int shortPath; /**< compute shortest paths in network */ 126 int selectiveTrace; /**< use selective trace in shortest paths */ 127 char *sinkfile; /**< file for externally provided sink node */ 128 int partition; /**< test McMillan conjunctive partitioning */ 129 int char2vect; /**< test char-to-vect decomposition */ 130 int density; /**< test density-related functions */ 131 double quality; /**< quality parameter for density functions */ 132 int decomp; /**< test decomposition functions */ 133 int cofest; /**< test cofactor estimation */ 134 double clip; /**< test clipping functions */ 135 int dontcares; /**< test equivalence and containment with DCs */ 136 int closestCube; /**< test Cudd_bddClosestCube */ 137 int clauses; /**< test extraction of two-literal clauses */ 138 int noBuild; /**< do not build BDDs; just echo order */ 139 int stateOnly; /**< ignore primary outputs */ 140 char *node; /**< only node for which to build %BDD */ 141 int locGlob; /**< build global or local BDDs */ 142 int progress; /**< report output names while building BDDs */ 143 int cacheSize; /**< computed table initial size */ 144 size_t maxMemory; /**< target maximum memory */ 145 size_t maxMemHard; /**< maximum allowed memory */ 146 unsigned int maxLive; /**< maximum number of nodes */ 147 int slots; /**< unique subtable initial slots */ 148 int ordering; /**< FANIN DFS ... */ 149 char *orderPiPs; /**< file for externally provided order */ 150 Cudd_ReorderingType reordering; /**< NONE RANDOM PIVOT SIFTING ... */ 151 int autoDyn; /**< ON OFF */ 152 Cudd_ReorderingType autoMethod; /**< RANDOM PIVOT SIFTING CONVERGE ... */ 153 char *treefile; /**< file name for variable tree */ 154 int firstReorder; /**< when to do first reordering */ 155 int countDead; /**< count dead nodes toward triggering 156 reordering */ 157 int maxGrowth; /**< maximum growth during reordering (%) */ 158 Cudd_AggregationType groupcheck; /**< grouping function */ 159 int arcviolation; /**< percent violation of arcs in 160 extended symmetry check */ 161 int symmviolation; /**< percent symm violation in 162 extended symmetry check */ 163 int recomb; /**< recombination parameter for grouping */ 164 int nodrop; /**< don't drop intermediate BDDs ASAP */ 165 int signatures; /**< computation of signatures */ 166 int gaOnOff; /**< whether to run GA at the end */ 167 int populationSize; /**< population size for GA */ 168 int numberXovers; /**< number of crossovers for GA */ 169 int bdddump; /**< ON OFF */ 170 int dumpFmt; /**< 0 -> dot 1 -> blif 2 ->daVinci 3 -> DDcal 171 ** 4 -> factored form */ 172 char *dumpfile; /**< filename for dump */ 173 int store; /**< iteration at which to store Reached */ 174 char *storefile; /**< filename for storing Reached */ 175 int load; /**< load initial states from file */ 176 char *loadfile; /**< filename for loading states */ 177 int verb; /**< level of verbosity */ 178 int32_t seed; /**< seed for random number generator */ 179 } NtrOptions; 180 181 /** 182 @brief Type of entry of NtrHeap. 183 */ 184 typedef struct NtrHeapSlot NtrHeapSlot; 185 186 /** 187 @brief Type of heap-based priority queue. 188 */ 189 typedef struct NtrHeap NtrHeap; 190 191 /** 192 @brief Data structure for partitioned transition relation. 193 */ 194 typedef struct NtrPartTR { 195 int nparts; /**< number of parts */ 196 DdNode **part; /**< array of parts */ 197 DdNode **icube; /**< quantification cubes for image */ 198 DdNode **pcube; /**< quantification cubes for preimage */ 199 DdNode **nscube; /**< next state variables in each part */ 200 DdNode *preiabs; /**< present state vars and inputs in no part */ 201 DdNode *prepabs; /**< inputs in no part */ 202 DdNode *xw; /**< cube of all present states and PIs */ 203 NtrHeap *factors; /**< factors extracted from the image */ 204 int nlatches; /**< number of latches */ 205 DdNode **x; /**< array of present state variables */ 206 DdNode **y; /**< array of next state variables */ 207 } NtrPartTR; 208 209 /*---------------------------------------------------------------------------*/ 210 /* Variable declarations */ 211 /*---------------------------------------------------------------------------*/ 212 213 /*---------------------------------------------------------------------------*/ 214 /* Macro declarations */ 215 /*---------------------------------------------------------------------------*/ 216 217 #ifndef TRUE 218 # define TRUE 1 219 #endif 220 #ifndef FALSE 221 # define FALSE 0 222 #endif 223 224 /** 225 @brief Returns 1 if the two arguments are identical strings. 226 227 @sideeffect none 228 229 */ 230 #define STRING_EQUAL(s1,s2) (strcmp((s1),(s2)) == 0) 231 232 233 /** \cond */ 234 235 /*---------------------------------------------------------------------------*/ 236 /* Function prototypes */ 237 /*---------------------------------------------------------------------------*/ 238 239 extern int Ntr_buildDDs (BnetNetwork *net, DdManager *dd, NtrOptions *option, BnetNetwork *net2); 240 extern NtrPartTR * Ntr_buildTR (DdManager *dd, BnetNetwork *net, NtrOptions *option, int image); 241 extern DdNode * Ntr_TransitiveClosure (DdManager *dd, NtrPartTR *TR, NtrOptions *option); 242 extern int Ntr_Trav (DdManager *dd, BnetNetwork *net, NtrOptions *option); 243 extern int Ntr_SCC (DdManager *dd, BnetNetwork *net, NtrOptions *option); 244 extern int Ntr_ClosureTrav (DdManager *dd, BnetNetwork *net, NtrOptions *option); 245 extern void Ntr_freeTR (DdManager *dd, NtrPartTR *TR); 246 extern NtrPartTR * Ntr_cloneTR (NtrPartTR *TR); 247 extern DdNode * Ntr_initState (DdManager *dd, BnetNetwork *net, NtrOptions *option); 248 extern DdNode * Ntr_getStateCube (DdManager *dd, BnetNetwork *net, char *filename, int pr); 249 extern int Ntr_Envelope (DdManager *dd, NtrPartTR *TR, FILE *dfp, NtrOptions *option); 250 extern int Ntr_TestMinimization (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option); 251 extern int Ntr_TestDensity (DdManager *dd, BnetNetwork *net1, NtrOptions *option); 252 extern int Ntr_TestDecomp (DdManager *dd, BnetNetwork *net1, NtrOptions *option); 253 extern int Ntr_VerifyEquivalence (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option); 254 extern int Ntr_TestCofactorEstimate (DdManager * dd, BnetNetwork * net, NtrOptions * option); 255 extern int Ntr_TestClipping (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option); 256 extern int Ntr_TestEquivAndContain (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option); 257 extern int Ntr_TestClosestCube (DdManager * dd, BnetNetwork * net, NtrOptions * option); 258 extern int Ntr_TestTwoLiteralClauses (DdManager * dd, BnetNetwork * net1, NtrOptions * option); 259 extern int Ntr_TestCharToVect(DdManager * dd, BnetNetwork * net1, NtrOptions * option); 260 extern int Ntr_maxflow (DdManager *dd, BnetNetwork *net, NtrOptions *option); 261 extern double Ntr_maximum01Flow (DdManager *bdd, DdNode *sx, DdNode *ty, DdNode *E, DdNode **F, DdNode **cut, DdNode **x, DdNode **y, DdNode **z, int n, int pr); 262 extern int Ntr_testZDD (DdManager *dd, BnetNetwork *net, NtrOptions *option); 263 extern int Ntr_testISOP (DdManager *dd, BnetNetwork *net, NtrOptions *option); 264 extern NtrHeap * Ntr_InitHeap (int size); 265 extern void Ntr_FreeHeap (NtrHeap *heap); 266 extern int Ntr_HeapInsert (NtrHeap *heap, void *item, int key); 267 extern int Ntr_HeapExtractMin (NtrHeap *heap, void *item, int *key); 268 extern int Ntr_HeapCount (NtrHeap *heap); 269 extern NtrHeap * Ntr_HeapClone (NtrHeap *source); 270 extern void Ntr_HeapForeach (NtrHeap *heap, void (*f)(void *e, void *arg), void *arg); 271 extern int Ntr_TestHeap (NtrHeap *heap, int i); 272 extern int Ntr_ShortestPaths (DdManager *dd, BnetNetwork *net, NtrOptions *option); 273 274 /** \endcond */ 275 276 277 #ifdef __cplusplus 278 } 279 #endif 280 281 #endif /* _NTR */ 282