void 
Img_AbstractTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  array_t * abstractVars, 
  mdd_t * abstractCube, 
  Img_DirectionType  directionType 
)
Abstracts out given variables from transition relation. abstractVars should be an array of bdd variables. 


mdd_t * 
Img_AddDontCareToImage(
  mdd_t * image, 
  mdd_t * constraint, 
  Img_MinimizeType  method 
)
Adds a dont care set to the given image. 


mdd_t * 
Img_ApproximateImage(
  mdd_manager * mgr, 
  mdd_t * image, 
  bdd_approx_dir_t  approxDir, 
  bdd_approx_type_t  approxMethod, 
  int  approxThreshold, 
  double  approxQuality, 
  double  approxQualityBias, 
  mdd_t * bias 
)
Approximate image. 


int 
Img_ApproximateTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  bdd_approx_dir_t  approxDir, 
  bdd_approx_type_t  approxMethod, 
  int  approxThreshold, 
  double  approxQuality, 
  double  approxQualityBias, 
  Img_DirectionType  directionType, 
  mdd_t * bias 
)
Approximate transition relation. 


void 
Img_ClusterRelationArray(
  mdd_manager * mddManager, 
  Img_MethodType  method, 
  Img_DirectionType  direction, 
  array_t * relationArray, 
  array_t * domainVarMddIdArray, 
  array_t * rangeVarMddIdArray, 
  array_t * quantifyVarMddIdArray, 
  array_t ** clusteredRelationArray, 
  array_t ** arraySmoothVarBddArray, 
  array_t ** smoothVarCubeArray, 
  boolean  freeRelationArray 
)
Clusters relation array and returns quantification schedule. 


mdd_t * 
Img_ComposeIntermediateNodes(
  graph_t * partition, 
  mdd_t * node, 
  array_t * psVars, 
  array_t * nsVars, 
  array_t * inputVars 
)
Replace partitioned transition relation. 


void 
Img_DupTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Duplicates the transition relation for backup. Copies transition relation as well as quantification schedule for temporary use. 


void 
Img_End(
    
)
End the image package.

See Also Img_Init 

void 
Img_ForwardImageInfoConjoinWithWinningStrategy(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * winningStrategy 
)
Create restricted transition relations by conjoining with winning strategy. 


void 
Img_ForwardImageInfoRecoverFromWinningStrategy(
  Img_ImageInfo_t * imageInfo 
)
Restore original transition relations from restricted transition relations by conjoining with winning strategy 


int 
Img_GetNumberOfImageComputation(
  Img_DirectionType  imgDir 
)
Returns number of image/preimage computation. 


array_t * 
Img_GetPartitionedTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Returns current partitioned transition relation. 


Img_MinimizeType 
Img_GuidedSearchReadOverApproxMinimizeMethod(
    
)
Returns the guided search minimize method of overapproximating the transition relation. Default is OrNot. 


Img_MinimizeType 
Img_GuidedSearchReadUnderApproxMinimizeMethod(
    
)
Returns the guided search minimize method of underapproximating the transition relation. Default is And. 


void 
Img_ImageAllowPartialImage(
  Img_ImageInfo_t * info, 
  boolean  value 
)
Sets the flag to allow the next image computation to return a subset of the actual image. Default is to not allow partial image computations. This flag is reset at the end of every image/preimage computation i.e., has to be specified before every image/preimage computation if partial image is desired.

Side Effects Flag is reset at the end of every image/preimage computation.

See Also Img_ImageWasPartialImage 

void 
Img_ImageConstrainAndClusterTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  direction, 
  mdd_t * constrain, 
  Img_MinimizeType  minimizeMethod, 
  boolean  underApprox, 
  boolean  cleanUp, 
  boolean  forceReorder, 
  int  printStatus 
)
Constrains/adds dont-cares to the bit relations with the given constraint and creates a new transition relation in the direction indicated. This procedure will incur the cost of creating the bit relations if they dont already exist. An over/under approximation of the transition relation may be created according to the underApprox flag. The flag is TRUE for underapproximations and FALSE for over approximation. An underapproximation of the transition relation will be in the interval [T.C, T

Side Effects Current transition relation and quantification schedule are freed. Bit relations are freed if indicated by the cleanUp flag.

See Also Img_GuidedSearchReadUnderApproxMinimizeMethod Img_GuidedSearchReadOverApproxMinimizeMethod 

mdd_t * 
Img_ImageGetUnreachableStates(
  Img_ImageInfo_t * imageInfo 
)
Return unreachable states 


mdd_t * 
Img_ImageInfoComputeBwdWithDomainVars(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  mdd_t * toCareSet 
)
Computes the backward image of a set expressed in terms of domain variables. FromLowerBound, fromUpperBound, and toCareSet are expressed in terms of domain variables. See Img_ImageInfoComputeBwd for more information. This function takes a care set, as opposed to ComputeBwd, which takes a care-set array.

See Also Img_ImageInfoComputeBwd 

mdd_t * 
Img_ImageInfoComputeBwd(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Computes the backward image of a set, under the function vector in imageInfo, using the image computation method specified in imageInfo. The set for which the backward image is computed is some set containing fromLowerBound and contained in fromUpperBound. The exact set used is chosen to simplify the computation. ToCareSet specifies those backward image points of interest; any points not in this set may or may not belong to the returned set. The MDDs fromLowerBound and fromUpperBound are defined over the range variables. The MDD toCareSet and the returned MDD are defined over the domain variables. If fromLowerBound is zero, then zero will be returned.

See Also Img_ImageInfoInitialize Img_ImageInfoComputeFwd Img_ImageInfoFree Img_ImageInfoComputeBwdWithDomainVars 

mdd_t * 
Img_ImageInfoComputeEXWithDomainVars(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Computes the backward image of a set expressed in terms of domain variables. FromLowerBound, fromUpperBound, and toCareSetArray are expressed in terms of domain variables. See Img_ImageInfoComputeBwd for more information. This function takes a care-set array, as opposed to Img_ImageInfoComputeBwdWithDomainVars, which takes a care set.

See Also Img_ImageInfoComputeBwd 

mdd_t * 
Img_ImageInfoComputeFwdWithDomainVars(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  mdd_t * toCareSet 
)
Computes the forward image of a set and expresses it in terms of domain variables. FromLowerBound, fromUpperBound, and toCareSet are expressed in terms of domain variables. See Img_ImageInfoComputeFwd for more information. (Takes care states as a set.)

See Also Img_ImageInfoComputeFwd 

mdd_t * 
Img_ImageInfoComputeFwd(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Computes the forward image of a set, under the function vector in imageInfo, using the image computation method specified in imageInfo. The set for which the forward image is computed is some set containing fromLowerBound and contained in fromUpperBound. The exact set used is chosen to simplify the computation. ToCareSet specifies those forward image points of interest; any points not in this set may or may not belong to the returned set. The MDDs fromLowerBound and fromUpperBound are defined over the domain variables. The MDD toCareSet and the returned MDD are defined over the range variables. If fromLowerBound is zero, then zero will be returned. (Takes care states as an array.)

See Also Img_ImageInfoInitialize Img_ImageInfoComputeBwd Img_ImageInfoFree Img_ImageInfoComputeFwdWithDomainVars 

mdd_t * 
Img_ImageInfoComputeImageWithDomainVars(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Computes the forward image of a set and expresses it in terms of domain variables. FromLowerBound, fromUpperBound, and toCareSet are expressed in terms of domain variables. See Img_ImageInfoComputeFwd for more information. (Takes care set as an array.)

See Also Img_ImageInfoComputeFwd 

mdd_t * 
Img_ImageInfoComputePreImageWithDomainVars(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * fromLowerBound, 
  mdd_t * fromUpperBound, 
  array_t * toCareSetArray 
)
Computes the backward image of a set expressed in terms of domain variables. FromLowerBound, fromUpperBound, and toCareSetArray are expressed in terms of domain variables. See Img_ImageInfoComputeBwd for more information. This function takes a care-set array, as opposed to Img_ImageInfoComputeBwdWithDomainVars, which takes a care set.

See Also Img_ImageInfoComputeBwd 

void 
Img_ImageInfoFreeFAFW(
  Img_ImageInfo_t * imageInfo 
)
Frees the memory associated with imageInfo.

See Also Img_ImageInfoInitialize Img_ImageInfoComputeFwd Img_ImageInfoComputeBwd 

void 
Img_ImageInfoFree(
  Img_ImageInfo_t * imageInfo 
)
Frees the memory associated with imageInfo.

See Also Img_ImageInfoInitialize Img_ImageInfoComputeFwd Img_ImageInfoComputeBwd 

Img_ImageInfo_t * 
Img_ImageInfoInitialize(
  Img_ImageInfo_t * imageInfo, 
  graph_t * mddNetwork, 
  array_t * roots, 
  array_t * domainVars, 
  array_t * rangeVars, 
  array_t * quantifyVars, 
  mdd_t * domainCube, 
  mdd_t * rangeCube, 
  mdd_t * quantifyCube, 
  Ntk_Network_t * network, 
  Img_MethodType  methodType, 
  Img_DirectionType  directionType, 
  int  FAFWFlag, 
  mdd_t * Winning 
)
Initializes an imageInfo structure. MethodType specifies which image computation method to use. If methodType is Img_Default_c, then if the user-settable flag "image_method" has been set, then this method is used, otherwise some default is used. DirectionType specifies which types of image computations will be performed (forward, backward, or both). Method-specific initialization takes into account the value of relevant parameters in the global flag table.

MddNetwork is a graph representing the functions to be used. Each vertex of the graph contains a multi-valued function (MVF) and an MDD id. The MVF gives the function of the vertex in terms of the MDD ids of the immediate fanins of the vertex.

Roots is an array of char* specifying the vertices of the graph which represent those functions for which we want to compute the image (it must not be empty); for example, for an FSM, roots represent the next state functions. DomainVars is an array of mddIds; for an FSM, these are the present state variables. Subsets of the domain are defined over these variables. RangeVars is an array of mddIds over which the range is expressed; for an FSM, these are the next state variables. This array must be in one-to-one correspondence with the array of roots. QuantifyVars is an array of mddIds, representing variables to be quantified from results of backward images; for an FSM, these are the input variables. This array may be empty. No copies are made of any of the input parameters, and thus it is the application's responsibility to free this data *after* the returned Img_ImageInfo_t is freed.

See Also Img_ImageInfoComputeFwd Img_ImageInfoComputeBwd Img_ImageInfoFree 

char * 
Img_ImageInfoObtainMethodTypeAsString(
  Img_ImageInfo_t * imageInfo 
)
Returns a string giving the method type of an imageInfo. It is the user's responsibility to free this string.

See Also Img_ImageInfoInitialize 

Img_MethodType 
Img_ImageInfoObtainMethodType(
  Img_ImageInfo_t * imageInfo 
)
Returns the method type of an imageInfo.

See Also Img_ImageInfoInitialize 

Img_OptimizeType 
Img_ImageInfoObtainOptimizeType(
  Img_ImageInfo_t * imageInfo 
)
Returns the method type of an imageInfo.

See Also Img_ImageInfoInitialize 

void 
Img_ImageInfoPrintMethodParams(
  Img_ImageInfo_t * imageInfo, 
  FILE * fp 
)
Prints information about the image technique currently used.

Side Effects None. 


void 
Img_ImageInfoResetLinearComputeRange(
  Img_ImageInfo_t * imageInfo 
)
Reset linear compute range flag.

See Also Img_ImageInfoInitialize 

void 
Img_ImageInfoResetUseOptimizedRelationFlag(
  Img_ImageInfo_t * imageInfo 
)
reset optimization relation flag .

See Also Img_ImageInfoInitialize 

void 
Img_ImageInfoSetLinearComputeRange(
  Img_ImageInfo_t * imageInfo 
)
Set linear compute range flag.

See Also Img_ImageInfoInitialize 

void 
Img_ImageInfoSetUseOptimizedRelationFlag(
  Img_ImageInfo_t * imageInfo 
)
set optimization relation flag .

See Also Img_ImageInfoInitialize 

void 
Img_ImageInfoUpdateVariables(
  Img_ImageInfo_t * imageInfo, 
  graph_t * mddNetwork, 
  array_t * domainVars, 
  array_t * quantifyVars, 
  mdd_t * domainCube, 
  mdd_t * quantifyCube 
)
Updates present state and primary input variables. This function is called after calling ImageInfoInitialize for a subFsm.

See Also Img_ImageInfoInitialize 

void 
Img_ImagePrintPartialImageOptions(
    
)
Prints partial image options. 


boolean 
Img_ImageWasPartial(
  Img_ImageInfo_t * info 
)
Queries whether the last image computation was partial. Reset before every image/preimage computation i.e., this information is valid for only the previous image/preimage computation.

Side Effects Reset before every image/preimage computation.

See Also Img_ImageAllowPartialImage 

void 
Img_Init(
    
)
Initialize the image package.

See Also Img_End 

int 
Img_IsPartitionedTransitionRelation(
  Img_ImageInfo_t * imageInfo 
)
Returns 1 if partitioned transition relation is used. 


int 
Img_IsQuantifyArraySame(
  Img_ImageInfo_t * imageInfo, 
  array_t * quantifyArray 
)
This function is for remove memory leakage.

See Also Img_ImageInfoInitialize 

int 
Img_IsQuantifyCubeSame(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * quantifyCube 
)
This function is for remove memory leakage.

See Also Img_ImageInfoInitialize 

int 
Img_IsTransitionRelationOptimized(
  Img_ImageInfo_t * imageInfo 
)
Check whether the given transition relation is optimized. 


mdd_t * 
Img_MinimizeImageArray(
  mdd_t * image, 
  array_t * constraintArray, 
  Img_MinimizeType  method, 
  boolean  underapprox 
)
Minimizes a bdd with given set of constraints. Underapproximates if underapprox is true, otherwise overapproximated (in which case method has to be ornot or squeeze).

Side Effects Img_MinimizeImage 


mdd_t * 
Img_MinimizeImage(
  mdd_t * image, 
  mdd_t * constraint, 
  Img_MinimizeType  method, 
  boolean  underapprox 
)
Minimizes an image with given constraint. This function can be used to minimize any BDDs.

If underapprox is 1, the the bdds are underapproximated. If it is 0, they are overapproximated, and the minimizeMethod has to be either ornot or squeeze. 


void 
Img_MinimizeTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  array_t * constrainArray, 
  Img_MinimizeType  minimizeMethod, 
  Img_DirectionType  directionType, 
  boolean  reorderIwls95Clusters 
)
Minimizes transition relation with given constraint if it hasn't been minimized already (does nothing otherwise). The constraint is expressed as an array of conjuncts of BDDs, The transition relation is minimized with each one of the conjuncts.

The boolean reorderIwls95Clusters is only relevant to the iwls95 image method. It causes the clusters to be ordered again after minimization.

The conjuncts have to be in terms of present-state variables or inputs. Next-state variables are not allowed.

For the hybrid and tfm methods, for image, we can only minimize wrt a set that includes any possible argument. For preimage, the result is only correct for as far as it lies within the set that the TR is minimized with. That means that reachability info can be usefully applied here.

For the other methods, we can also minimize wrt different sets. The edges in the TR that are outgoing from states not in this set may then get removed. 


mdd_t* 
Img_MultiwayLinearAndSmooth(
  mdd_manager * mddManager, 
  array_t * relationArray, 
  array_t * smoothVarMddIdArray, 
  array_t * introducedVarMddIdArray, 
  Img_MethodType  method, 
  Img_DirectionType  direction 
)
"relationArray" is an array of mdd's which need to be multiplied and the variables in the "smoothVarMddIdArray" need to be quantified out from the product. "introducedVarMddIdArray" is the array of mddIds of the variables (other than the variables to be quantified out) in the support of the relations. This array is used to compute the product order such that the number of new variables introduced in the product is minimized. However passing an empty array or an array of mddIds of partial support will not result in any error (some optimality will be lost though). The computation consists of 2 phases. In phase 1, an ordering of the relations and a schedule of quantifying variables is found (based on IWLS95) heuristic. In phase 2, the relations are multiplied in order and the quantifying variables are quantified according to the schedule.

Side Effects None 


void 
Img_PrintHybridOptions(
    
)
Prints the options for hybrid image computation. 


void 
Img_PrintMlpOptions(
    
)
Prints the options for MLP image computation. 


void 
Img_PrintPartitionedTransitionRelation(
  mdd_manager * mddManager, 
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Prints info of the partitioned transition relation. 


void 
Img_PrintTfmOptions(
    
)
Prints the options for image computation using transition function method. 


Img_MinimizeType 
Img_ReadMinimizeMethod(
    
)
Returns current method of minimizing transition relation. Default is restrict. 


int 
Img_ReadPrintMinimizeStatus(
  Img_ImageInfo_t * imageInfo 
)
Reads the flag whether to print the status of minimizing transition relation. 


void 
Img_ReorderPartitionedTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Reorder partitioned transition relation. 


void 
Img_ReplaceIthPartitionedTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  int  i, 
  mdd_t * relation, 
  Img_DirectionType  directionType 
)
Replace ith partitioned transition relation. 


void 
Img_ReplacePartitionedTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  array_t * relationArray, 
  Img_DirectionType  directionType 
)
Replace partitioned transition relation. 


void 
Img_ResetNumberOfImageComputation(
  Img_DirectionType  imgDir 
)
Resets number of image/preimage computation. 


void 
Img_ResetTrMinimizedFlag(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Resets the flag that transition relation is minimized. 


void 
Img_RestoreTransitionRelation(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Restores original transition relation from saved. 


void 
Img_SetPrintMinimizeStatus(
  Img_ImageInfo_t * imageInfo, 
  int  status 
)
Sets the flag whether to print the status of minimizing transition relation. 


mdd_t * 
Img_Substitute(
  Img_ImageInfo_t * imageInfo, 
  mdd_t * f, 
  Img_SubstituteDir  dir 
)
Substitutes variables between domain and range. 


int 
Img_TfmCheckGlobalCache(
  int  preFlag 
)
Checks whether a global cache is used for transition function method. If it is, returns 1, otherwise returns 0. A global cache can be used when all image-info structs store the results into one image cache. A local cache is used for each image-info struct stores its results into its own image cache. 


void 
Img_TfmFlushCache(
  Img_ImageInfo_t * imageInfo, 
  int  preFlag 
)
Frees all cache contents of image computation using transition function method. This function is to free the cache contents only when requested and when tfm_auto_flush_cache is off. 


int 
Img_TfmGetCacheStatistics(
  Img_ImageInfo_t * imageInfo, 
  int  preFlag, 
  double * inserts, 
  double * lookups, 
  double * hits, 
  double * entries, 
  int * nSlots, 
  int * maxChainLength 
)
Gets the statistics of image cache of transition function method 


int 
Img_TfmGetRecursionStatistics(
  Img_ImageInfo_t * imageInfo, 
  int  preFlag, 
  int * nRecurs, 
  int * nLeaves, 
  int * nTurns, 
  float * averageDepth, 
  int * maxDepth, 
  int * nDecomps, 
  int * topDecomp, 
  int * maxDecomp, 
  float * averageDecomp 
)
Gets the statistics of recursions of transition function method. 


void 
Img_TfmPrintCacheStatistics(
  Img_ImageInfo_t * imageInfo, 
  int  preFlag 
)
Prints the statistics of image cache of transition function method. 


void 
Img_TfmPrintRecursionStatistics(
  Img_ImageInfo_t * imageInfo, 
  int  preFlag 
)
Prints the statistics of recursions for transition function method. 


void 
Img_TfmPrintStatistics(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  dir 
)
Prints the statistics of image cache and recursions in in transition function method. 


void 
Img_UpdateQuantificationSchedule(
  Img_ImageInfo_t * imageInfo, 
  Img_DirectionType  directionType 
)
Updates quantification schedule. 


Img_MethodType 
Img_UserSpecifiedMethod(
    
)
Returns the method selected by Img_ImageInfoInitialize if Img_Default_c is passed in. Note that this may change if the user changes the definition of the image_method set flag.

See Also Img_ImageInfoIninitialize
Last updated on 20050519 00h50