|
|
/**
@file
@ingroup nanotrav
@brief Simple-minded package to do traversal.
@author Fabio Somenzi
@copyright@parblock Copyright (c) 1995-2015, Regents of the University of Colorado
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. @endparblock
*/
#ifndef _NTR
#define _NTR
/*---------------------------------------------------------------------------*//* Nested includes *//*---------------------------------------------------------------------------*/
#include "dddmp.h"
#include "bnet.h"
#ifdef __cplusplus
extern "C" {#endif
/*---------------------------------------------------------------------------*//* Constant declarations *//*---------------------------------------------------------------------------*/
#define PI_PS_FROM_FILE 0
#define PI_PS_DFS 1
#define PI_PS_GIVEN 2
#define NTR_IMAGE_MONO 0
#define NTR_IMAGE_PART 1
#define NTR_IMAGE_CLIP 2
#define NTR_IMAGE_DEPEND 3
#define NTR_UNDER_APPROX 0
#define NTR_OVER_APPROX 1
#define NTR_FROM_NEW 0
#define NTR_FROM_REACHED 1
#define NTR_FROM_RESTRICT 2
#define NTR_FROM_COMPACT 3
#define NTR_FROM_SQUEEZE 4
#define NTR_FROM_UNDERAPPROX 5
#define NTR_FROM_OVERAPPROX 6
#define NTR_GROUP_NONE 0
#define NTR_GROUP_DEFAULT 1
#define NTR_GROUP_FIXED 2
#define NTR_SHORT_NONE 0
#define NTR_SHORT_BELLMAN 1
#define NTR_SHORT_FLOYD 2
#define NTR_SHORT_SQUARE 3
/*---------------------------------------------------------------------------*//* Stucture declarations *//*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*//* Type declarations *//*---------------------------------------------------------------------------*/
/**
@brief Options for nanotrav.*/typedef struct NtrOptions { long initialTime; /**< this is here for convenience */ int verify; /**< read two networks and compare them */ char *file1; /**< first network file name */ char *file2; /**< second network file name */ int second; /**< a second network is given */ int traverse; /**< do reachability analysis */ int depend; /**< do latch dependence analysis */ int image; /**< monolithic, partitioned, or clip */ double imageClip; /**< clipping depth in image computation */ int approx; /**< under or over approximation */ int threshold; /**< approximation threshold */ int from; /**< method to compute from states */ int groupnsps; /**< group present state and next state vars */ int closure; /**< use transitive closure */ double closureClip; /**< clipping depth in closure computation */ int envelope; /**< compute outer envelope */ int scc; /**< compute strongly connected components */ int zddtest; /**< do zdd test */ int printcover; /**< print ISOP covers when testing ZDDs */ int maxflow; /**< compute maximum flow in network */ int shortPath; /**< compute shortest paths in network */ int selectiveTrace; /**< use selective trace in shortest paths */ char *sinkfile; /**< file for externally provided sink node */ int partition; /**< test McMillan conjunctive partitioning */ int char2vect; /**< test char-to-vect decomposition */ int density; /**< test density-related functions */ double quality; /**< quality parameter for density functions */ int decomp; /**< test decomposition functions */ int cofest; /**< test cofactor estimation */ double clip; /**< test clipping functions */ int dontcares; /**< test equivalence and containment with DCs */ int closestCube; /**< test Cudd_bddClosestCube */ int clauses; /**< test extraction of two-literal clauses */ int noBuild; /**< do not build BDDs; just echo order */ int stateOnly; /**< ignore primary outputs */ char *node; /**< only node for which to build %BDD */ int locGlob; /**< build global or local BDDs */ int progress; /**< report output names while building BDDs */ int cacheSize; /**< computed table initial size */ size_t maxMemory; /**< target maximum memory */ size_t maxMemHard; /**< maximum allowed memory */ unsigned int maxLive; /**< maximum number of nodes */ int slots; /**< unique subtable initial slots */ int ordering; /**< FANIN DFS ... */ char *orderPiPs; /**< file for externally provided order */ Cudd_ReorderingType reordering; /**< NONE RANDOM PIVOT SIFTING ... */ int autoDyn; /**< ON OFF */ Cudd_ReorderingType autoMethod; /**< RANDOM PIVOT SIFTING CONVERGE ... */ char *treefile; /**< file name for variable tree */ int firstReorder; /**< when to do first reordering */ int countDead; /**< count dead nodes toward triggering
reordering */ int maxGrowth; /**< maximum growth during reordering (%) */ Cudd_AggregationType groupcheck; /**< grouping function */ int arcviolation; /**< percent violation of arcs in
extended symmetry check */ int symmviolation; /**< percent symm violation in
extended symmetry check */ int recomb; /**< recombination parameter for grouping */ int nodrop; /**< don't drop intermediate BDDs ASAP */ int signatures; /**< computation of signatures */ int gaOnOff; /**< whether to run GA at the end */ int populationSize; /**< population size for GA */ int numberXovers; /**< number of crossovers for GA */ int bdddump; /**< ON OFF */ int dumpFmt; /**< 0 -> dot 1 -> blif 2 ->daVinci 3 -> DDcal
** 4 -> factored form */ char *dumpfile; /**< filename for dump */ int store; /**< iteration at which to store Reached */ char *storefile; /**< filename for storing Reached */ int load; /**< load initial states from file */ char *loadfile; /**< filename for loading states */ int verb; /**< level of verbosity */ int32_t seed; /**< seed for random number generator */} NtrOptions;
/**
@brief Type of entry of NtrHeap.*/typedef struct NtrHeapSlot NtrHeapSlot;
/**
@brief Type of heap-based priority queue.*/typedef struct NtrHeap NtrHeap;
/**
@brief Data structure for partitioned transition relation.*/typedef struct NtrPartTR { int nparts; /**< number of parts */ DdNode **part; /**< array of parts */ DdNode **icube; /**< quantification cubes for image */ DdNode **pcube; /**< quantification cubes for preimage */ DdNode **nscube; /**< next state variables in each part */ DdNode *preiabs; /**< present state vars and inputs in no part */ DdNode *prepabs; /**< inputs in no part */ DdNode *xw; /**< cube of all present states and PIs */ NtrHeap *factors; /**< factors extracted from the image */ int nlatches; /**< number of latches */ DdNode **x; /**< array of present state variables */ DdNode **y; /**< array of next state variables */} NtrPartTR;
/*---------------------------------------------------------------------------*//* Variable declarations *//*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*//* Macro declarations *//*---------------------------------------------------------------------------*/
#ifndef TRUE
# define TRUE 1
#endif
#ifndef FALSE
# define FALSE 0
#endif
/**
@brief Returns 1 if the two arguments are identical strings.
@sideeffect none
*/#define STRING_EQUAL(s1,s2) (strcmp((s1),(s2)) == 0)
/** \cond */
/*---------------------------------------------------------------------------*//* Function prototypes *//*---------------------------------------------------------------------------*/
extern int Ntr_buildDDs (BnetNetwork *net, DdManager *dd, NtrOptions *option, BnetNetwork *net2);extern NtrPartTR * Ntr_buildTR (DdManager *dd, BnetNetwork *net, NtrOptions *option, int image);extern DdNode * Ntr_TransitiveClosure (DdManager *dd, NtrPartTR *TR, NtrOptions *option);extern int Ntr_Trav (DdManager *dd, BnetNetwork *net, NtrOptions *option);extern int Ntr_SCC (DdManager *dd, BnetNetwork *net, NtrOptions *option);extern int Ntr_ClosureTrav (DdManager *dd, BnetNetwork *net, NtrOptions *option);extern void Ntr_freeTR (DdManager *dd, NtrPartTR *TR);extern NtrPartTR * Ntr_cloneTR (NtrPartTR *TR);extern DdNode * Ntr_initState (DdManager *dd, BnetNetwork *net, NtrOptions *option);extern DdNode * Ntr_getStateCube (DdManager *dd, BnetNetwork *net, char *filename, int pr);extern int Ntr_Envelope (DdManager *dd, NtrPartTR *TR, FILE *dfp, NtrOptions *option);extern int Ntr_TestMinimization (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);extern int Ntr_TestDensity (DdManager *dd, BnetNetwork *net1, NtrOptions *option);extern int Ntr_TestDecomp (DdManager *dd, BnetNetwork *net1, NtrOptions *option);extern int Ntr_VerifyEquivalence (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);extern int Ntr_TestCofactorEstimate (DdManager * dd, BnetNetwork * net, NtrOptions * option);extern int Ntr_TestClipping (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);extern int Ntr_TestEquivAndContain (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);extern int Ntr_TestClosestCube (DdManager * dd, BnetNetwork * net, NtrOptions * option);extern int Ntr_TestTwoLiteralClauses (DdManager * dd, BnetNetwork * net1, NtrOptions * option);extern int Ntr_TestCharToVect(DdManager * dd, BnetNetwork * net1, NtrOptions * option);extern int Ntr_maxflow (DdManager *dd, BnetNetwork *net, NtrOptions *option);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);extern int Ntr_testZDD (DdManager *dd, BnetNetwork *net, NtrOptions *option);extern int Ntr_testISOP (DdManager *dd, BnetNetwork *net, NtrOptions *option);extern NtrHeap * Ntr_InitHeap (int size);extern void Ntr_FreeHeap (NtrHeap *heap);extern int Ntr_HeapInsert (NtrHeap *heap, void *item, int key);extern int Ntr_HeapExtractMin (NtrHeap *heap, void *item, int *key);extern int Ntr_HeapCount (NtrHeap *heap);extern NtrHeap * Ntr_HeapClone (NtrHeap *source);extern void Ntr_HeapForeach (NtrHeap *heap, void (*f)(void *e, void *arg), void *arg);extern int Ntr_TestHeap (NtrHeap *heap, int i);extern int Ntr_ShortestPaths (DdManager *dd, BnetNetwork *net, NtrOptions *option);
/** \endcond */
#ifdef __cplusplus
}#endif
#endif /* _NTR */
|
