imgHybrid.c: Routines for hybrid image computation.
imgIwls95.c: Routines for image computation using component transition relation approach described in the proceedings of IWLS'95, (henceforth referred to Iwls95 technique).
imgLinear.c: Routines for image computation using Linear Arrangement published in TACAS02.
imgMlp.c: Routines for image computation using MLP(Minimal Lifetime Permutation) published in FMCAD00.
imgMonolithic.c: Routines for image computation using a monolithic transition relation.
imgTfm.c: Routines for image and preimage computations using transition function method.
imgTfmBwd.c: Routines for preimage computation using transition function method.
imgTfmCache.c: Routines for image cache in transition function method.
imgTfmFwd.c: Routines for image computation using transition function method.
imgTfmUtil.c: Routines for image computation using transition function method.
imgUtil.c: High-level routines to perform image computations.

imgHybrid.c

Routines for hybrid image computation.

By: In-Ho Moon

The hybrid image computation method combines transition function and relation methods, in other words, combines splitting and conjunction methods.

Img_PrintHybridOptions(): Prints the options for hybrid image computation.
ImgDecideSplitOrConjoin(): Decides whether to split or to conjoin.
ImgImageByHybrid(): Computes an image by transition relation.
ImgImageByHybridWithStaticSplit(): Computes an image by transition relation.
ImgPreImageByHybrid(): Computes a preimage by transition relation.
ImgPreImageByHybridWithStaticSplit(): Computes a preimage by transition relation.
ImgCheckEquivalence(): Checks whether a vector is equivalent to a relation array.
ImgCheckMatching(): Checks whether a vector corresponds to its relation array.
ComputeSupportLambda(): Computes variable lifetime lambda.

imgIwls95.c

Routines for image computation using component transition relation approach described in the proceedings of IWLS'95, (henceforth referred to Iwls95 technique).

By: Rajeev K. Ranjan, In-Ho Moon, Kavita Ravi

The initialization process performs following steps:

Create the relation of the roots at the bit level in terms of the quantify and domain variables.
Order the bit level relations.
Group the relations of bits together, making a cluster whenever the BDD size reaches a threshold.
For each cluster, quantify out the quantify variables which are local to that particular cluster.
Order the clusters using the algorithm given in "Efficient BDD Algorithms for FSM Synthesis and Verification", by R. K. Ranjan et. al. in the proceedings of IWLS'95{1}.
The orders of the clusters for forward and backward image are calculated and stored. Also stored is the schedule of variables for early quantification.

For forward and backward image computation the corresponding routines are called with appropriate ordering of clusters and early quantification schedule.

Note that, a cubic implementation of the above algorithm is straightforward. However, to obtain quadratic complexity requires significant amount of book-keeping. This is the reason for the complexity of the code in this file.

Img_MultiwayLinearAndSmooth(): Returns the result after existentially quantifying a set of variables after taking the product of the array of relations.
Img_PrintPartitionedTransitionRelation(): Prints info of the partitioned transition relation.
Img_ReorderPartitionedTransitionRelation(): Reorder partitioned transition relation.
Img_UpdateQuantificationSchedule(): Updates quantification schedule.
Img_ClusterRelationArray(): Clusters relation array and returns quantification schedule.
ImgMultiwayLinearAndSmooth(): Returns the result after existentially quantifying a set of variables after taking the product of the array of relations.
ImgMultiwayLinearAndSmoothWithFrom(): Returns the result after existentially quantifying a set of variables after taking the product of the array of relations.
ImgBddLinearAndSmooth(): Returns a BDD after taking the product of fromSet with the BDDs in the relationArray and quantifying out the variables using the schedule given in the arraySmoothVarBddArray.
ImgClusterRelationArray(): Clusters relation array and makes quantification schedule.
ImgGetQuantificationSchedule(): Returns quantification schedule for a given relation array.
ImgGetTrmOptions(): Allocates an option structure for transition relation method.
ImgFreeTrmOptions(): Frees the option structure for transition relation method.
ImgResetMethodDataLinearComputeRange(): Turn off option to apply linear based image computation by comsidering range of state variables
ImgSetMethodDataLinearComputeRange(): Turn on option to apply linear based image computation by comsidering range of state variables
Img_ImageGetUnreachableStates(): Get unreachable states
ImgImageInfoInitializeIwls95(): Initializes an image data structure for image computation using the Iwls95 technique.
ImgImageInfoComputeFwdIwls95(): Computes the forward image of a set of states.
ImgImageInfoComputeFwdWithDomainVarsIwls95(): Computes the forward image of a set of states in terms of domain variables.
ImgImageInfoComputeBwdIwls95(): Computes the backward image of domainSubset.
ImgImageInfoComputeBwdWithDomainVarsIwls95(): Computes the backward image of a set of states.
ImgImageInfoFreeIwls95(): Frees the memory associated with imageInfo.
ImgImageInfoPrintMethodParamsIwls95(): Prints information about the IWLS95 method.
ImgBddGetSupportIdTable(): Returns the st_table containing the bdd id of the support variables of the function.
ImgImageWasPartialIwls95(): Checks if the last image/preimage was partial.
ImgImageAllowPartialImageIwls95(): Sets the flag to allow partial images.
ImgRestoreTransitionRelationIwls95(): Restores original transition relation from saved.
ImgDuplicateTransitionRelationIwls95(): Duplicates transition relation.
ImgMinimizeTransitionRelationIwls95(): Minimizes transition relation with given set of constraints.
ImgAbstractTransitionRelationIwls95(): Abstracts out given variables from transition relation.
ImgApproximateTransitionRelationIwls95(): Approximate transition relation.
ImgGetTransitionRelationIwls95(): Returns current transition relation.
ImgUpdateTransitionRelationIwls95(): Overwrites transition relation with given.
ImgReplaceIthPartitionedTransitionRelationIwls95(): Replace ith partitioned transition relation.
ImgImageFreeClusteredTransitionRelationIwls95(): Frees current transition relation and associated quantification schedule for the given direction.
ImgImageConstrainAndClusterTransitionRelationIwls95OrMlp(): Constrains/Adds dont-cares to the bit relation and creates a new transition relation.
ImgPrintIntegerArray(): Prints integers from an array.
ImgPrintPartition(): Prints the given parition.
ImgPrintPartitionedTransitionRelation(): Prints info of the partitioned transition relation.
ImgTrmEliminateDependVars(): Eliminates dependent variables from transition relation.
ResetClusteredCofactoredRelationArray(): Reset the clusteredcofactoredrelationarray to the clusteredrelationarray.
FreeClusteredCofactoredRelationArray(): Frees the clusteredcofactoredrelationarray
TrmGetOptions(): Gets the necessary options for computing the image and returns in the option structure.
CreateBitRelationArray(): Creates the bit relations and the mdd id array for the quantifiable variables and stores it in the ImgIwls95 structure.
FreeBitRelationArray(): Frees bit relation array and the quantification variables.
OrderClusterOrder(): Takes an array of relations and does order, cluster, order on it according to the IWLS95 method. This forms a heuristically optimized clustered transition relation, plus a quantification schedule that goes with it.
CreateClusters(): Forms the clusters of relations based on BDD size heuristic.
OrderRelationArray(): Returns an array of ordered relations and an array of BDD cubes (array of BDDs).
RelationArraySmoothLocalVars(): This function takes an array of relations and quantifies out the quantify variables which are local to a particular relation.
OrderRelationArrayAux(): An auxiliary routine for orderRelationArray to order the clusters.
UpdateInfoArrays(): This function computes the set of variables which can be smoothed out once a particular cluster is chosen to be multiplied in the product.
CalculateBenefit(): Gets the necessary options for computing the image and returns in the option structure.
PrintOption(): Prints the option values used in IWLS95 techinique for image computation.
Iwls95InfoStructAlloc(): Allocates and initializes the info structure for IWLS95 technique.
CtrInfoStructAlloc(): Allocates and initializes memory for ctrInfoStruct.
CtrInfoStructFree(): Frees the memory associated with ctrInfoStruct.
VarInfoStructAlloc(): Allocates and initializes memory for varInfoStruct.
VarInfoStructFree(): Frees the memory associated with varInfoStruct.
CtrItemStructFree(): Frees the memory associated with CtrItemStruct
VarItemStructFree(): Frees the memory associated with VarItemStruct
CtrInfoMaxIndexCompare(): Compare function used to sort the ctrInfoStruct based on the maxSmoothVarIndex field.
PrintCtrInfoStruct(): Prints the CtrInfo_t data structure.
PrintVarInfoStruct(): Prints the VarInfo_t structure.
CheckQuantificationSchedule(): Given an array of BDD's representing the relations and another array of BDD cubes (in the form of array of bdd_t of variable) representing the quantification schedule, this function checks if the schedule is correct.
CheckCtrInfoArray(): Checks the validity of an array of CtrInfoStructs.
CheckCtrInfo(): Checks the validity of a CtrInfoStruct.
CheckVarInfoArray(): Checks the validity of an array of VarInfoStruct.
BddArrayDup(): Duplicates an array of BDDs.
BddLinearAndSmooth(): Returns a BDD after taking the product of fromSet with the BDDs in the relationArray and quantifying out the variables using the schedule given in the arraySmoothVarBddArray.
HashIdToBddTable(): Hashes bdd id to bdd in the table.
PrintSmoothIntroducedCount(): Prints information about the schedule of clusters and the the corresponding smooth cubes.
PrintBddIdFromBddArray(): Prints Ids of an array of BDDs.
PrintBddIdTable(): Prints the integers from a symbol table.
PartitionTraverseRecursively(): Traverses the partition recursively, creating the relations for the intermediate vertices.
PrintPartitionRecursively(): Prints the partition recursively.
RecomputeImageIfNecessary(): Recompute partial image by relaxing the parameters.
ComputeSubsetOfIntermediateProduct(): Approximate intermediate product according to method.
ComputeClippedAndAbstract(): Clipping and-abstract
CopyArrayBddArray(): Copy an array of bdd array.
PrintPartitionedTransitionRelation(): Prints info of the partitioned transition relation.
ReorderPartitionedTransitionRelation(): Reorder partitioned transition relation.
UpdateQuantificationSchedule(): Updates quantification schedule.
MakeSmoothVarCubeArray(): Returns array of cubes of smoothing variables.
TrmEliminateDependVars(): Eliminates dependent variables from transition relation.
TrmSignatureCompare(): Comparison function used by qsort.
SetupLazySifting(): Setups lazy sifting.
Img_IsTransitionRelationOptimized(): Check whether the given transition relation is optimized.
MddSizeCompare(): Compare the size of two MDDs.
Img_ForwardImageInfoRecoverFromWinningStrategy(): Restore original transition relations from restricted transition relations by conjoining with winning strategy
Img_ForwardImageInfoConjoinWithWinningStrategy(): Create restricted transition relations by conjoining with winning strategy

imgLinear.c

Routines for image computation using Linear Arrangement published in TACAS02.

By: HoonSang Jin

ImgLinearClusterRelationArray(): Cluster fine grain transition relation
ImgLinearRelationInit(): Initialize the data structure for linear arrangement and clustering.
ImgLinearGetSupportBddId(): Find support varaibles of bdd
ImgLinearExtractRelationArray(): Create relation array for image computation from Relation_t data structure
ImgLinearExtractRelationArrayT(): Create relation array for image computation from Relation_t data structure
ImgLinearOptimizeAll(): Function for optimizing state varaibles
ImgLinearPropagateConstant(): Propagate the constant to simply the transition relation
ImgLinearOptimizeStateVariables(): Remove corresponding current (next) state variables if the next (current state variables are eleminated aftetr clustering
ImgLinearOptimizeInternalVariables(): Remove intermediate variables after propagating constant.
ImgLinearRefineRelation(): Refine transition relation.
ImgLinearConjunctOrderMainCC(): Order the fine grain transition relation.
ImgLinearBuildConjunctArrayWithQuotientCC(): Order the each connected component
ImgLinearConnectedComponent(): Find the connected component from fine grain transition relation
ImgLinearFindConnectedComponent(): Find the connected component from fine grain transition relation
ImgLinearExtractSingletonCase(): Extract the relation contains only one next state varaible
ImgLinearAddConjunctIntoClusterArray(): Add Conjunct into Cluster Array
ImgLinearExtractNextStateCase(): Extract the relation that contains next state varaibles only
ImgLinearRelationQuit(): Free Relation_t data structure
ImgLinearClusteringIteratively(): Apply clustering iteratively
ImgLinearClusteringByConstraints(): Apply clustering with given priority function
ImgLinearInsertClusterCandidate(): Add candidates for clustering
ImgLinearClusteringSmooth(): Apply clustering while quantifying the variables that are isolated
ImgLinearClusterUsingHeap(): Apply clustering with priority queue
linearCheckRange(): compare function for checking range of cluster
ImgLinearClusteringPairSmooth(): Clustering pair of transition relation
ImgLinearBuildInitialCandidate(): Build data structure for clustering
ImgLinearInsertPairClusterCandidate(): Insert initial candidate set
ImgLinearPrintDebugInfo(): Print information of debug information
ImgLinearConjunctOrderMain(): Main function of linear arrangement
ImgLinearConjunctionOrder(): Generate linear arrangement with CAPO
ImgLinearCAPOInterfaceConjunctNodes(): Make interface files for CAPO
ImgLinearCAPOInterfaceConjunctNet(): Make interface files for CAPO
ImgLinearCAPOInterfaceConjunctScl(): Make interface files for CAPO
ImgLinearCAPOInterfaceConjunctPl(): Make interface files for CAPO
ImgLinearCAPOInterfaceAux(): Make interface files for CAPO
ImgLinearCAPORun(): Run batch job of CAPO
ImgLinearCAPOReadConjunctOrder(): Read result of CAPO
ImgLinearVariableOrder(): Make interface for variable ordering
ImgLinearCAPOInterfaceVariableNodes(): Make interface for CAPO
ImgLinearCAPOInterfaceVariableNet(): Make interface for CAPO
ImgLinearCAPOInterfaceVariableScl(): Make interface for CAPO
ImgLinearCAPOInterfaceVariablePl(): Make interface for CAPO
ImgLinearCAPOReadVariableOrder(): Read result of CAPO
ImgLinearPrintVariableProfile(): Print profile of variables
ImgLinearPrintMatrix(): Print matrix
ImgLinearPrintMatrixFull(): Print matrix
ImgLinearFreeSmoothArray(): Free smooth variable array
ImgLinearComputeLifeTime(): Compute life time of variables
ImgLinearPrintTransitionInfo(): Print transition relation info
ImgLinearMakeSmoothVarBdd(): Make the array of smooth variables
ImgLinearCompareVarEffFromSmall(): Priority function for clutering
ImgLinearCompareVarDummyLarge(): Priority function for clutering
ImgLinearCompareVarEffFromLarge(): Priority function for clutering
ImgLinearCompareVarId(): Priority function for clutering
ImgLinearCompareVarSize(): Priority function for clutering
ImgLinearCompareConjunctRangeMinusDomain(): Priority function for clutering
ImgLinearCompareConjunctDummy(): Priority function for clutering
ImgLinearCompareConjunctIndex(): Priority function for clutering
ImgLinearCompareConjunctSize(): Priority function for clutering
ImgLinearCompareVarIndex(): Priority function for clutering
ImgLinearCompareDeadAffinityLive(): Priority function for clutering
ImgLinearCompareDeadLiveAffinity(): Priority function for clutering
ImgLinearCompareAffinityDeadLive(): Priority function for clutering
ImgLinearCompareLiveAffinityDead(): Priority function for clutering
ImgLinearHeapCompareDeadAffinityLive(): Priority function for clutering
ImgLinearHeapCompareDeadLiveAffinity(): Priority function for clutering
ImgLinearHeapCompareAffinityDeadLive(): Priority function for clutering
ImgLinearHeapCompareLiveAffinityDead(): Priority function for clutering
ImgLinearVariableArrayInit(): Initialize variable array
ImgLinearUpdateVariableArrayWithId(): Update variable array with id of variable id
ImgLinearQuantifyVariablesFromConjunct(): Apply quantification with candidate variables
ImgLinearConjunctRefine(): Refine conjunction array to fill the empty slot.
ImgLinearConjunctArrayRefine(): Refine conjunction array to fill the empty slot.
ImgLinearSetEffectiveNumberOfStateVariable(): Get the number of state variables after applying optimization
ImgLinearAddSingletonCase(): Find the case that the relation contains only one next state varaible
ImgLinearExpandSameSupportSet(): Find transtion relations that have smae support set
ImgLinearClusterSameSupportSet(): Cluster the relation that has same support set
ImgLinearFindSameSupportConjuncts(): Find the conjuncts that have same support variables.
ImgLinearIsSameConjunct(): Check if given conjuncts have same support variables
ImgLinearAddConjunctIntoArray(): Add conjunct into array
ImgLinearConjunctQuit(): Free conjunct_t data structure
ImgLinearVariableArrayQuit(): Free variable array
ImgLinearVariableLifeQuit(): Free variable life array
ImgLinearClustering(): Main function of clustering
ImgCountOnsetDisjunctiveArray(): Count onset of relation array
ImgCheckRangeTestAndOverapproximate(): Check range of variables
ImgLinearAddNextStateCase(): Add singleton next state variable case into array

imgMlp.c

Routines for image computation using MLP(Minimal Lifetime Permutation) published in FMCAD00.

By: In-Ho Moon

Img_PrintMlpOptions(): Prints the options for MLP image computation.
ImgMlpMultiwayAndSmooth(): Performs multiway and_smooth using MLP.
ImgMlpClusterRelationArray(): Clusters relation array and makes quantification schedule.
ImgMlpOrderRelationArray(): Orders relation array and makes quantification schedule.
ImgMlpComputeLambda(): Compute variables lifetime using MLP.
ImgMlpGetQuantificationSchedule(): Makes a quantification schedule using MLP.
ImgMlpPrintDependenceMatrix(): Prints dependence matrix.
ImgMlpWriteClusterFile(): Writes cluster to a file.
ImgMlpReadClusterFile(): Reads cluster file.
SetupMlp(): Setups MLP.
MlpDecomposeScc(): Performs connected component decomposition.
SccSortListIncreasingWithVars(): Sorts connected components with the number of variables.
SccSortListDecreasingWithVars(): Sorts connected components with the number of variables.
SccSortListIncreasingWithArea(): Sorts connected components with area.
SccSortListDecreasingWithArea(): Sorts connected components with area.
SccSortListIncreasingWithRatio(): Sorts connected components with aspect ratio.
SccSortListDecreasingWithRatio(): Sorts connected components with aspect ratio.
SccSortRc(): Sorts rows or columns using connected component index.
FreeSccList(): Frees list of connected components.
NumOfSccs(): Returns the number of connected components in the list.
BlockLowerTriangle(): Makes dependence matrix block lower triangle.
MoveBestRows(): Finds and moves the best row iteratively.
MoveBestCols(): Finds and moves the best column iteratively.
MlpPostProcess(): Performs a postprocessing after MLP.
ComputeLambdaMlp(): Compute variable lifetime lambda.
FindAndMoveSingletonRows(): Finds and moves singleton rows.
MoveSingletonRow(): Moves a singleton row.
FindAndMoveSingletonCols(): Finds and moves singleton columns.
MoveSingletonCol(): Moves a singleton column.
MoveRowToTop(): Moves a row to the top of the active region.
MoveColToLeft(): Moves a column to the left of the active region.
MoveRowToBottom(): Moves a row to the bottom of the active region.
MoveColToRight(): Moves a column to the tight of the active region.
PrintMatrix(): Prints a maxtrix.
PrintMatrixWithCluster(): Prints a matrix with cluster information.
PrintClusterMatrix(): Prints cluster information.
CheckMatrix(): Checks a matrix for sanity.
CheckCluster(): Checks cluster for sanity.
WriteMatrix(): Writes a matrix to a file.
PrintRow(): Prints a row.
PrintCol(): Prints a column.
SortedListAlloc(): Allocates a list for sorting.
SortedListFree(): Frees a list used for sorting.
SortedListInsert(): Inserts a list to the sorting list.
SortedListDelete(): Deletes a list from the sorting list.
SortedListMove(): Moves a list in the sorting list.
CheckSortedList(): Checks the sorting list for sanity.
MlpCluster(): Clusters on the ordered bits.
MlpCountSupport(): Counts the number of supports of the list.
MlpSupportAffinity(): Computes the affinity of two lists.
RecursiveCluster(): Clusters recursively with affinity.
RemoveLocalVarsInCluster(): Removes local variables in a cluster.
MlpNumQuantifyVars(): Retuns the number of variables to be quantified in a list.
ClusterSortedListInsert(): Inserts a cluster in a sorting list.
CountClusterList(): Returns the number of lists in a cluster list.
CountClusterSortedList(): Returns the number of lists in a sorted cluster list.
CreateInitialCluster(): Creates an initial cluster using ARDC decomposition.
SortCol(): Updates matrix information properly.
UpdateDisapearingPsVars(): Finds disappearing present state variables in a row.
UpdateDisapearingPsVarsInCluster(): Finds disappearing present state variables in a cluster.
UpdateNonappearingNsVars(): Finds non-appearing next state variables.
WriteOrder(): Writes variable order in coulumn of the matrix.

imgMonolithic.c

Routines for image computation using a monolithic transition relation.

By: Rajeev K. Ranjan, Tom Shiple, Abelardo Pardo, In-Ho Moon

ImgImageInfoInitializeMono(): Initializes an image structure for image computation using a monolithic transition relation.
ImgImageInfoComputeFwdMono(): Computes the forward image of a set of states between fromLowerBound and fromUpperBound.
ImgImageInfoComputeFwdWithDomainVarsMono(): Computes the forward image on domain variables of a set of states between fromLowerBound and fromUpperBound.
ImgImageInfoComputeBwdMono(): Computes the backward image of a set of states between fromLowerBound and fromUpperBound.
ImgImageInfoComputeBwdWithDomainVarsMono(): Computes the backward image of a set of states between fromLowerBound and fromUpperBound.
ImgImageInfoFreeMono(): Frees the method data associated with the monolithic method.
ImgImageInfoPrintMethodParamsMono(): Prints information about the IWLS95 method.
ImgRestoreTransitionRelationMono(): Restores original transition relation from saved.
ImgDuplicateTransitionRelationMono(): Duplicates transition relation.
ImgMinimizeTransitionRelationMono(): Minimizes transition relation with given constraint.
ImgAddDontCareToTransitionRelationMono(): Add dont care to transition relation.
ImgAbstractTransitionRelationMono(): Abstracts out given variables from transition relation.
ImgApproximateTransitionRelationMono(): Approximates transition relation.
ImgImageConstrainAndClusterTransitionRelationMono(): Constrains/adds dont-cares to the bit relation and creates a new transition relation.
ImageComputeMonolithic(): A generic routine for computing the image.

imgTfm.c

Routines for image and preimage computations using transition function method.

By: In-Ho Moon

Transition function method is implemented as a part of the hybrid image computation (refer to "To Split or to Conjoin: The Question in Image Computation", In-Ho Moon et. al. in the proceedings of DAC00.) The hybrid method starts with transition function method based on splitting, then switches to transition relation method based on conjunctions. The decision is based on computing variable lifetimes from dependence matrix dynamically at every recursion. The transition function method itself also can be used as an image_method, however we do not recommend to use this method for general purpose. This method can be used for experimental purpose. However, this method performs quite well for most approximate reachability and some examples on exact reachability. There are two image computation methods in transition function method; input splitting (default) and output splitting. Also three preimage computation methods in transition function method are implemented; domain cofactoring (default), sequential substitution, and simultaneous substitution. The performance of transition function method is significantly depending on both the choice of splitting variable and the use of image cache. However, the hybrid method does not use image cache by default. Since the recursion depths are bounded (not so deep) in the hybrid method, the cache hit ratio is usually very low. The implementation of the transition function method and the hybrid method is very complicate since there are so many options. For details, try print_tfm_options and print_hybrid_options commands in vis, also more detailed descriptions for all options can be read by using help in vis for the two commands. The hybrid method can start with either only function vector or only transition relation, as well as with both function vector and transition relation. In case of starting with only the function vector, when we switch to conjoin, transition relation is built on demand. This method may consume less memory than the others, but it may take more time since it is a big overhead to build transition relation at every conjunction. To reduce this overhead, the hybrid method can start with both function vector and transition relation (default). In the presense of non-determinism, the hybrid mehtod also can start with only transition relation without the function vector.

Img_TfmGetRecursionStatistics(): Gets the statistics of recursions of transition function method.
Img_TfmPrintStatistics(): Prints the statistics of image cache and recursions in in transition function method.
Img_TfmPrintRecursionStatistics(): Prints the statistics of recursions for transition function method.
Img_PrintTfmOptions(): Prints the options for image computation using transition function method.
ImgImageInfoInitializeTfm(): Initializes an image data structure for image computation using transition function method.
ImgImageInfoComputeFwdTfm(): Computes the forward image of a set of states.
ImgImageInfoComputeFwdWithDomainVarsTfm(): Computes the forward image of a set of states in terms of domain variables.
ImgImageInfoComputeBwdTfm(): Computes the backward image of domainSubset.
ImgImageInfoComputeBwdWithDomainVarsTfm(): Computes the backward image of a set of states.
ImgImageInfoFreeTfm(): Frees the memory associated with imageInfo.
ImgImageInfoPrintMethodParamsTfm(): Prints information about the transition function method.
ImgRestoreTransitionFunction(): Restores original transition function from saved.
ImgDuplicateTransitionFunction(): Duplicates transition function.
ImgMinimizeTransitionFunction(): Minimizes transition function with given set of constraints.
ImgAddDontCareToTransitionFunction(): Adds a dont care set to the transition function and relation.
ImgAbstractTransitionFunction(): Abstracts out given variables from transition function.
ImgApproximateTransitionFunction(): Approximate transition function.
ImgGetTransitionFunction(): Returns current transition function.
ImgUpdateTransitionFunction(): Overwrites transition function with given.
ImgReplaceIthTransitionFunction(): Replace ith transition function.
ImgTfmGetOptions(): Gets the necessary options for computing the image and returns in the option structure.
ImgImageFreeClusteredTransitionRelationTfm(): Frees current transition function vector and relation for the given direction.
ImgImageConstrainAndClusterTransitionRelationTfm(): Constrains the bit function and relation and creates a new transition function vector and relation.
ImgIsPartitionedTransitionRelationTfm(): Check whether transition relation is built in hybrid.
TfmInfoStructAlloc(): Allocates and initializes the info structure for transition function method.
CompareIndex(): Compares two variable indices of components.
HookInfoFunction(): Flushes cache entries in a list.
ChoosePartialVars(): Chooses variables for static splitting.
PrintRecursionStatistics(): Prints statistics of recursions for transition function method.
PrintFoundVariableStatistics(): Prints statistics of finding essential and dependent variables.
GetRecursionStatistics(): Returns the statistics of recursions of transition function method.
ReadSetIntValue(): Reads a set integer value.
ReadSetBooleanValue(): Reads a set Boolean value.
FindIntermediateVarsRecursively(): Traverses the partition recursively, creating the functions for the intermediate vertices.
GetIntermediateRelationsRecursively(): Traverses the partition recursively, creating the relations for the intermediate vertices.
CheckNondeterminism(): Checks whether the network is nondeterministic.
TfmCreateBitVector(): Creates function vector.
TfmCreateBitRelationArray(): Creates the bit relations.
TfmSetupPartialTransitionRelation(): Builds partial vector and relation array.
TfmBuildRelationArray(): Builds relation array from function vector or bit relation.
RebuildTransitionRelation(): Rebuilds transition relation from function vector.
MinimizeTransitionFunction(): Minimizes function vector or relation with given constraint.
AddDontCareToTransitionFunction(): Adds dont cares to function vector or relation.

imgTfmBwd.c

Routines for preimage computation using transition function method.

By: In-Ho Moon

ImgTfmPreImage(): Computes a preimage with transition function method.
PreImageByDomainCofactoring(): Computes preimage with domain cofactoring method.
PreImageByStaticDomainCofactoring(): Computes a preimage by static input splitting.
PreImageByConstraintCofactoring(): Computes preimage with constraint cofactoring method.
PreImageBySubstitution(): Computes a preimage by Filkorn's substitution.
PreImageMakeVectorCanonical(): Makes a vector canonical for preimage.
PreImageMakeRelationCanonical(): Makes transition relation canonical for preimage.
PreImageDeleteOneComponent(): Deletes a component in a vector.
PreImageChooseSplitVar(): Chooses a splitting variable for preimage.
DomainCofactoring(): Performs domain cofactoring on a vector and from set with respect to a variable.
CheckPreImageVector(): Checks sanity of a vector for preimage.

imgTfmCache.c

Routines for image cache in transition function method.

By: In-Ho Moon

Img_TfmGetCacheStatistics(): Gets the statistics of image cache of transition function method.
Img_TfmCheckGlobalCache(): Checks whether a global cache is used for transition function method.
Img_TfmPrintCacheStatistics(): Prints the statistics of image cache of transition function method.
Img_TfmFlushCache(): Frees all cache contents of image computation using transition function method.
ImgCacheInitTable(): Initializes a cache table.
ImgCacheDestroyTable(): Destroys a cache table.
ImgCacheLookupTable(): Lookups cache table.
ImgCacheInsertTable(): Inserts an entry into cache table.
ImgFlushCache(): Flushes all cache entries.
ImgPrintCacheStatistics(): Prints cache statistics for transition function method.
CacheDestroyEntry(): Destroys a cache entry.
VectorHash(): Returns hash value of a vector.
VectorStHash(): Returns hash value of a vector for st_table.
KeyStHash(): Returns hash value of a key for st_table.
VectorCompare(): Compares two vectors.
VectorSortCompare(): Compares two vectors considering substitution.
VectorSortCompareWithConstraint(): Compares two vectors considering substitution.
ImageKeyCompare(): Compares two keys.
ImageKeySortCompare(): Compares two keys considering substitution.
PreImageKeyCompare(): Compares two keys for preimage.
SubstituteCacheResult(): Substitutes a cache result.
SubstituteCacheResultRecur(): Recursive procedure of SubstituteCacheResult.

imgTfmFwd.c

Routines for image computation using transition function method.

By: In-Ho Moon

ImgTfmImage(): Computes an image with transition function method.
ImgChooseTrSplitVar(): Chooses splitting variables for static splitting.
ImageByInputSplit(): Computes an image by input splitting.
ImageByStaticInputSplit(): Computes an image by static input splitting.
ImageByOutputSplit(): Computes an image by output splitting.
ImageDecomposeAndChooseSplitVar(): Try to decompose function vector and find a splitting variable for each decomposed block.
ImageFast2(): Fast image computation when function vector contains only two functions.
FindDecomposableVariable(): Finds a decomposable variable (articulation)
TfmCheckImageValidity(): Checks the support of image.
FindIntermediateSupport(): Finds all other fanin intermediate functions of a given intermediate function.
PrintVectorDecomposition(): Print the information of the decomposition.
CheckIfValidSplitOrGetNew(): Checks the splitting variable is valid and chooses new one if not valid.
ChooseInputSplittingVariable(): Finds a splitting variable for input splitting.
ChooseOutputSplittingVariable(): Finds a splitting variable for output splitting.

imgTfmUtil.c

Routines for image computation using transition function method.

By: In-Ho Moon

ImgVectorConstrain(): Constrains a function vector with respect to a constraint.
ImgVectorMinimize(): Minimizes a function vector and a from set with respect to an essential cube.
ImgVectorFree(): Frees a function vector.
ImgVectorFunctionSize(): Returns the number of functions in a vector.
ImgVectorBddSize(): Returns the shared BDD size of a vector.
ImgVectorCopy(): Copies a vector.
ImgComponentAlloc(): Allocates a component.
ImgComponentCopy(): Copies a component
ImgComponentFree(): Frees a component.
ImgComponentGetSupport(): Gets the supports of a component.
ImgSupportCopy(): Copies the supports of a component.
ImgSupportClear(): Clears a support array.
ImgSupportPrint(): Prints a support array.
ImgSupportCount(): Returns the number of support of a support array.
ImgGetConstrainedRelationArray(): Constrains a relation array with respect to a constraint.
ImgGetCofactoredRelationArray(): Cofactors a relation array with respect to a function.
ImgCofactorRelationArray(): Cofactors a relation array with respect to a function.
ImgGetAbstractedRelationArray(): Smoothes a relation array with respect to a cube.
ImgAbstractRelationArray(): Smoothes a relation array with respect to a cube.
ImgGetCofactoredAbstractedRelationArray(): Cofactors and smooths a relation array.
ImgGetAbstractedCofactoredRelationArray(): Smothes and cofactors a relation array.
ImgGetConstrainedVector(): Constrains a function vector with respect to a constraint.
ImgGetCofactoredVector(): Cofactors a function vector with respect to a function.
ImgCofactorVector(): Cofactors a function vector with respect to a function.
ImgTfmEliminateDependVars(): Eliminates dependent variables from transition function.
ImgExistConstIntermediateVar(): Checks whether there is a constant function of intermediate variables.
ImgGetComposedFunction(): Returns a function composed all intermediate variables.
ImgGetLatchComponent(): Returns the first latch component.
ImgComposeConstIntermediateVars(): Compose the constant intermediate variable functions.
ImgCountBddSupports(): Returns the number of BDD supports in a function.
ImgCheckConstConstrain(): Quick checking whether the results of constrain between two functions are constant.
ImgConstConstrain(): Checks whether the result of constrain is constant.
ImgPrintVectorDependency(): Prints vector dependencies with support.
ImgPercentVectorDependency(): Returns the percent of non-zero elements in dependency matrix.
ImgWriteSupportMatrix(): Writes a gnuplot file with support matrix.
SignatureCompare(): Comparison function used by qsort.
CompareBddPointer(): Compares two function BDD pointers of components.

imgUtil.c

High-level routines to perform image computations.

By: Rajeev Ranjan, Tom Shiple, Abelardo Pardo, In-Ho Moon, Kavita Ravi

This file provides the exported interface to the method-specific image computation routines.

Minimization of the transition relation can be done in three ways (for Iwls95, not so sure about monolithic and hybrid) (RB):

You can call MinimizeTR. This way, you'll loose the old TR, though it could potentially reconstruct it from the bit relations. This is a good option for (overapproximate) reachability info, since the TR will remain valid.
You can call the triplet Img_DupTransitionRelation to copy the TR, Img_MinimizeTransitionRelation to minimize the TR, and Img_RestoreTransitionRelation to discard the minimized TR and to restore the original.
Finally, if you just want to minimize the TR for a single step, you can pass the care set to the (pre)image computation routine. This does unfortunately (and queerly) not work for image, but only for preimage. If you pas a care set, the TR gets minimized, and the minimized relation is kept and reused until you pass a different care set. Hence, minimizaiton is not done at every preimage computation, but only if you change the care set.

Img_Init(): Initialize the image package.
Img_End(): End the image package.
Img_UserSpecifiedMethod(): Return the image method preferred by the user.
Img_ImageInfoInitialize(): Initializes an imageInfo structure for the given method and direction.
Img_IsQuantifyCubeSame(): Check the given address of mdd_t is same as the functionData.quantifyCube.
Img_IsQuantifyArraySame(): Check the given address of array+t is same as the functionData.quantifyArray.
Img_ImageInfoUpdateVariables(): Updates present state and primary input variables.
Img_ImageAllowPartialImage(): Sets the flag to allow the next image computation to return a subset of the actual image.
Img_ImagePrintPartialImageOptions(): Prints partial image options.
Img_ImageWasPartial(): Queries whether the last image computation was partial.
Img_ImageInfoComputeImageWithDomainVars(): Computes the forward image of a set and expresses it in terms of domain variables.
Img_ImageInfoComputeFwdWithDomainVars(): Computes the forward image of a set and expresses it in terms of domain variables.
Img_ImageInfoComputeFwd(): Computes the forward image of a set.
Img_ImageInfoComputePreImageWithDomainVars(): Computes the backward image of a set expressed in terms of domain variables.
Img_ImageInfoComputeEXWithDomainVars(): Computes the backward image of a set expressed in terms of domain variables.
Img_ImageInfoComputeBwdWithDomainVars(): Computes the backward image of a set expressed in terms of domain variables.
Img_ImageInfoComputeBwd(): Computes the backward image of a set.
Img_ImageInfoFree(): Frees the memory associated with imageInfo.
Img_ImageInfoFreeFAFW(): Frees the memory associated with imageInfo.
Img_ImageInfoObtainMethodTypeAsString(): Returns a string giving the method type of an imageInfo.
Img_ImageInfoObtainMethodType(): Returns the method type of an imageInfo.
Img_ImageInfoObtainOptimizeType(): Returns the method type of an imageInfo.
Img_ImageInfoSetUseOptimizedRelationFlag(): set optimization relation flag .
Img_ImageInfoResetUseOptimizedRelationFlag(): reset optimization relation flag .
Img_ImageInfoResetLinearComputeRange(): Reset linear compute range flag.
Img_ImageInfoSetLinearComputeRange(): Set linear compute range flag.
Img_ImageInfoPrintMethodParams(): Prints information about the image technique currently used.
Img_ResetTrMinimizedFlag(): Resets the flag that transition relation is minimized.
Img_ReadMinimizeMethod(): Returns current method of minimizing transition relation.
Img_MinimizeTransitionRelation(): Minimizes transition relation with given constraint if it hasn't been minimized already.
Img_MinimizeImage(): Minimizes an image with given constraint.
Img_AddDontCareToImage(): Adds a dont care set to the given image.
Img_MinimizeImageArray(): Minimizes a single bdd with a set of constraint.
Img_SetPrintMinimizeStatus(): Sets the flag whether to print the status of minimizing transition relation.
Img_ReadPrintMinimizeStatus(): Reads the flag whether to print the status of minimizing transition relation.
Img_AbstractTransitionRelation(): Abstracts out given variables from transition relation.
Img_DupTransitionRelation(): Duplicates the transition relation for backup.
Img_RestoreTransitionRelation(): Restores original transition relation from saved.
Img_ApproximateTransitionRelation(): Approximate transition relation.
Img_ApproximateImage(): Approximate image.
Img_IsPartitionedTransitionRelation(): Returns 1 if partitioned transition relation is used.
Img_ResetNumberOfImageComputation(): Resets number of image/preimage computation.
Img_GetNumberOfImageComputation(): Returns number of image/preimage computation.
Img_GetPartitionedTransitionRelation(): Returns current partitioned transition relation.
Img_ReplaceIthPartitionedTransitionRelation(): Replace ith partitioned transition relation.
Img_ReplacePartitionedTransitionRelation(): Replace partitioned transition relation.
Img_ComposeIntermediateNodes(): Replace partitioned transition relation.
Img_ImageConstrainAndClusterTransitionRelation(): Constrains/adds dont-cares to the bit relations with the given constraint and creates a new transtion relation.
Img_GuidedSearchReadUnderApproxMinimizeMethod(): Returns the guided search minimize method of underapproximating the transition relation.
Img_GuidedSearchReadOverApproxMinimizeMethod(): Returns the guided search minimize method of overapproximating the transition relation.
Img_Substitute(): Substitutes variables between domain and range.
ImgMinimizeImageArrayWithCareSetArray(): Minimize array of bdds wrt a set of constraints
ImgMinimizeImageArrayWithCareSetArrayInSitu(): Minimize array of bdds wrt a set of constraints
ImgSubstitute(): Substitutes variables between domain and range.
ImgSubstituteArray(): Substitutes variables between domain and range.
ImgPrintPartialImageOptions(): Prints Partial Image options.
ImgGetPartialImageOptions(): Get partial image options.
ImgArrayBddArrayCheckValidity(): This function checks the validity of an array of array of BDD nodes.
ImgBddArrayCheckValidity(): This function checks the validity of array of BDD nodes.
ImgBddCheckValidity(): This function checks the validity of a BDD.
ImgPrintVarIdTable(): Prints the content of a table containing integers.
ImgCheckToCareSetArrayChanged(): Checks whether toCareSetArray changed.
CheckImageValidity(): Checks the validity of image

Last updated on 20050519 00h50