VIS
|
#include "imgInt.h"
Go to the source code of this file.
Functions | |
static mdd_t * | ImageComputeMonolithic (mdd_t *methodData, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray, array_t *smoothVars, mdd_t *smoothCube) |
void * | ImgImageInfoInitializeMono (void *methodData, ImgFunctionData_t *functionData, Img_DirectionType directionType) |
mdd_t * | ImgImageInfoComputeFwdMono (ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) |
mdd_t * | ImgImageInfoComputeFwdWithDomainVarsMono (ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) |
mdd_t * | ImgImageInfoComputeBwdMono (ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) |
mdd_t * | ImgImageInfoComputeBwdWithDomainVarsMono (ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) |
void | ImgImageInfoFreeMono (void *methodData) |
void | ImgImageInfoPrintMethodParamsMono (void *methodData, FILE *fp) |
void | ImgRestoreTransitionRelationMono (Img_ImageInfo_t *imageInfo, Img_DirectionType directionType) |
void | ImgDuplicateTransitionRelationMono (Img_ImageInfo_t *imageInfo) |
void | ImgMinimizeTransitionRelationMono (Img_ImageInfo_t *imageInfo, array_t *constrainArray, Img_MinimizeType minimizeMethod, int printStatus) |
void | ImgAddDontCareToTransitionRelationMono (Img_ImageInfo_t *imageInfo, array_t *constrainArray, Img_MinimizeType minimizeMethod, int printStatus) |
void | ImgAbstractTransitionRelationMono (Img_ImageInfo_t *imageInfo, array_t *abstractVars, mdd_t *abstractCube, int printStatus) |
int | ImgApproximateTransitionRelationMono (mdd_manager *mgr, Img_ImageInfo_t *imageInfo, bdd_approx_dir_t approxDir, bdd_approx_type_t approxMethod, int approxThreshold, double approxQuality, double approxQualityBias, mdd_t *bias) |
void | ImgImageConstrainAndClusterTransitionRelationMono (Img_ImageInfo_t *imageInfo, mdd_t *constrain, Img_MinimizeType minimizeMethod, boolean underApprox, boolean cleanUp, boolean forceReorder, int printStatus) |
Variables | |
static char rcsid[] | UNUSED = "$Id: imgMonolithic.c,v 1.23 2002/08/27 08:43:12 fabio Exp $" |
static mdd_t * ImageComputeMonolithic | ( | mdd_t * | methodData, |
mdd_t * | fromLowerBound, | ||
mdd_t * | fromUpperBound, | ||
array_t * | toCareSetArray, | ||
array_t * | smoothVars, | ||
mdd_t * | smoothCube | ||
) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [A generic routine for computing the image.]
Description [This is a routine for image computation which is called by both forward image and backward image computation. The frontier set (the set of states for which the image is computed) is obtained by finding a small size BDD between lower and upper bounds. The transition relation is simplified by cofactoring it with the domainSubset (frontier set) and with the toCareSet. The order in which this simplification is unimportant from functionality point of view, but the order might effect the BDD size of the optimizedRelation. smoothVars should be an array of bdd variables.]
SideEffects []
Definition at line 620 of file imgMonolithic.c.
{ mdd_t *domainSubset, *image; mdd_t *optimizedRelation, *subOptimizedRelation; mdd_t *monolithicT = (mdd_t *)methodData; assert(monolithicT != NIL(mdd_t)); /* * Optimization steps: * Choose the domainSubset optimally. * Reduce the transition relation wrt to care set and domainSubset. */ domainSubset = bdd_between(fromLowerBound,fromUpperBound); subOptimizedRelation = bdd_cofactor_array(monolithicT, toCareSetArray); optimizedRelation = bdd_cofactor(subOptimizedRelation, domainSubset); mdd_free(domainSubset); mdd_free(subOptimizedRelation); /*optimizedRelation = bdd_and(fromLowerBound, monolithicT, 1, 1);*/ if (smoothCube) image = bdd_smooth_with_cube(optimizedRelation, smoothCube); else { if (array_n(smoothVars) == 0) image = mdd_dup(optimizedRelation); else image = bdd_smooth(optimizedRelation, smoothVars); } mdd_free(optimizedRelation); return image; }
void ImgAbstractTransitionRelationMono | ( | Img_ImageInfo_t * | imageInfo, |
array_t * | abstractVars, | ||
mdd_t * | abstractCube, | ||
int | printStatus | ||
) |
Function********************************************************************
Synopsis [Abstracts out given variables from transition relation.]
Description [Abstracts out given variables from transition relation. abstractVars should be an array of bdd variables.]
SideEffects []
Definition at line 428 of file imgMonolithic.c.
{ mdd_t *relation, *abstractedRelation; relation = (mdd_t *)imageInfo->methodData; if (abstractCube) abstractedRelation = bdd_smooth_with_cube(relation, abstractCube); else abstractedRelation = bdd_smooth(relation, abstractVars); if (printStatus) { (void) fprintf(vis_stdout, "Info: abstracted relation %d => %d\n", bdd_size(relation), bdd_size(abstractedRelation)); } mdd_free(relation); imageInfo->methodData = (void *)abstractedRelation; }
void ImgAddDontCareToTransitionRelationMono | ( | Img_ImageInfo_t * | imageInfo, |
array_t * | constrainArray, | ||
Img_MinimizeType | minimizeMethod, | ||
int | printStatus | ||
) |
Function********************************************************************
Synopsis [Add dont care to transition relation.]
Description [Add dont care to transition relation. The constrain array contains care sets.]
SideEffects []
Definition at line 381 of file imgMonolithic.c.
{ mdd_t *relation, *simplifiedRelation; int i, size = 0; mdd_t *constrain; relation = (mdd_t *)imageInfo->methodData; if (printStatus) size = bdd_size(relation); for (i = 0; i < array_n(constrainArray); i++) { constrain = array_fetch(mdd_t *, constrainArray, i); simplifiedRelation = Img_AddDontCareToImage(relation, constrain, minimizeMethod); if (printStatus) { (void) fprintf(vis_stdout, "Info: minimized relation %d | %d => %d\n", bdd_size(relation), bdd_size(constrain), bdd_size(simplifiedRelation)); } mdd_free(relation); relation = simplifiedRelation; } imageInfo->methodData = (void *)relation; if (printStatus) { (void) fprintf(vis_stdout, "IMG Info: minimized relation [%d | %ld => %d]\n", size, bdd_size_multiple(constrainArray), bdd_size(relation)); } }
int ImgApproximateTransitionRelationMono | ( | mdd_manager * | mgr, |
Img_ImageInfo_t * | imageInfo, | ||
bdd_approx_dir_t | approxDir, | ||
bdd_approx_type_t | approxMethod, | ||
int | approxThreshold, | ||
double | approxQuality, | ||
double | approxQualityBias, | ||
mdd_t * | bias | ||
) |
Function********************************************************************
Synopsis [Approximates transition relation.]
Description [Approximates transition relation.]
SideEffects []
Definition at line 457 of file imgMonolithic.c.
{ mdd_t *relation, *approxRelation; int unchanged; relation = (mdd_t *)imageInfo->methodData; approxRelation = Img_ApproximateImage(mgr, relation, approxDir, approxMethod, approxThreshold, approxQuality, approxQualityBias, bias); if (bdd_is_tautology(approxRelation, 1)) { fprintf(vis_stdout, "** img warning : bdd_one from subsetting.\n"); mdd_free(approxRelation); unchanged = 1; } else if (bdd_is_tautology(approxRelation, 0)) { fprintf(vis_stdout, "** img warning : bdd_zero from subsetting.\n"); mdd_free(approxRelation); unchanged = 1; } else if (mdd_equal(approxRelation, relation)) { mdd_free(approxRelation); unchanged = 1; } else { mdd_free(relation); imageInfo->methodData = (void *)approxRelation; unchanged = 0; } return(unchanged); }
void ImgDuplicateTransitionRelationMono | ( | Img_ImageInfo_t * | imageInfo | ) |
Function********************************************************************
Synopsis [Duplicates transition relation.]
Description [Duplicates transition relation. Assumes that the Transition Relation is a MDD.]
SideEffects []
Definition at line 319 of file imgMonolithic.c.
{ imageInfo->savedRelation = (void *)mdd_dup((mdd_t *) imageInfo->methodData); return; }
void ImgImageConstrainAndClusterTransitionRelationMono | ( | Img_ImageInfo_t * | imageInfo, |
mdd_t * | constrain, | ||
Img_MinimizeType | minimizeMethod, | ||
boolean | underApprox, | ||
boolean | cleanUp, | ||
boolean | forceReorder, | ||
int | printStatus | ||
) |
Function********************************************************************
Synopsis [Constrains/adds dont-cares to the bit relation and creates a new transition relation.]
Description [Constrains/adds dont-cares to the bit relation and creates a new transition relation. First, the existing transition relation is freed. The bit relation is created and constrained by the given constraint (underapprox) or its complement is add to the bit relation (overapprox) depending on the underApprox flag. Then the modified bit relation is clustered. The code is similar to ImgImageInfoInitializeMono. An over or under approximation of the transition relation may be created. The underApprox flag should be TRUE for an underapproximation and FALSE for an overapproximation. Although Img_MinimizeImage is used the minimizeMethod flag for underapproximations has to be passed by Img_GuidedSearchReadUnderApproxMinimizeMethod. The cleanUp flag is currently useless but is maintained for uniformity with other Image computation methods incase methodData changes in the future to store bitRelations. The flag ]
SideEffects [Current transition relation and quantification schedule are freed. Bit relations are freed if indicated.]
SeeAlso [Img_MultiwayLinearAndSmooth ImgImageInfoInitializeMono Img_MinimizeImage Img_AddDontCareToImage ]
Definition at line 520 of file imgMonolithic.c.
{ ImgFunctionData_t *functionData = &(imageInfo->functionData); mdd_t *methodData = (mdd_t *)imageInfo->methodData; int i; mdd_t *monolithicT; array_t *rootRelations = array_alloc(mdd_t*, 0); graph_t *mddNetwork = functionData->mddNetwork; mdd_manager *mddManager = Part_PartitionReadMddManager(mddNetwork); array_t *roots = functionData->roots; array_t *leaves = array_join(functionData->domainVars, functionData->quantifyVars); array_t *rootFunctions; mdd_t *relation; /*free existing relation. */ if (!methodData) ImgImageInfoFreeMono(methodData); if (forceReorder) bdd_reorder(mddManager); rootFunctions = Part_PartitionBuildFunctions(mddNetwork, roots, leaves, NIL(mdd_t)); array_free(leaves); /* * Take the product of the transition relation of all the root nodes * and smooth out the quantify variables. */ /* * Iterate over the function of all the root nodes. */ for (i=0; i<array_n(rootFunctions); i++) { Mvf_Function_t *rootFunction = array_fetch(Mvf_Function_t*, rootFunctions, i); int rangeVarMddId = array_fetch(int, functionData->rangeVars, i); mdd_t *rootRelation = Mvf_FunctionBuildRelationWithVariable(rootFunction, rangeVarMddId); array_insert_last(mdd_t*, rootRelations, rootRelation); } Mvf_FunctionArrayFree(rootFunctions); /* Constrain the bit relaitons */ if (constrain) { arrayForEachItem(mdd_t *, rootRelations, i, relation) { mdd_t *simplifiedRelation; simplifiedRelation = Img_MinimizeImage(relation, constrain, minimizeMethod, underApprox); if (printStatus) { (void) fprintf(vis_stdout, "Info: minimized relation %d | %d => %d\n", bdd_size(relation), bdd_size(constrain), bdd_size(simplifiedRelation)); } mdd_free(relation); array_insert(mdd_t *, rootRelations, i, simplifiedRelation); } } /* build the monolithic transition relation. */ monolithicT = Img_MultiwayLinearAndSmooth(mddManager, rootRelations, functionData->quantifyVars, functionData->domainVars, Img_Iwls95_c, Img_Forward_c); mdd_array_free(rootRelations); imageInfo->methodData = (void *)monolithicT; if (printStatus) { ImgImageInfoPrintMethodParamsMono(monolithicT, vis_stdout); } }
mdd_t* ImgImageInfoComputeBwdMono | ( | ImgFunctionData_t * | functionData, |
Img_ImageInfo_t * | imageInfo, | ||
mdd_t * | fromLowerBound, | ||
mdd_t * | fromUpperBound, | ||
array_t * | toCareSetArray | ||
) |
Function********************************************************************
Synopsis [Computes the backward image of a set of states between fromLowerBound and fromUpperBound.]
Description [Computes the backward image of a set of states between fromLowerBound and fromUpperBound. First a set of states between fromLowerBound and fromUpperBound is computed. Then, the transition relation is simplified by cofactoring it wrt to the set of states found in the first step, and wrt the toCareSet.]
SideEffects []
SeeAlso [ImgImageInfoComputeFwdMono,ImgImageInfoComputeBwdWithDomainVarsMono]
Definition at line 206 of file imgMonolithic.c.
{ return ImageComputeMonolithic((mdd_t*)imageInfo->methodData, fromLowerBound, fromUpperBound, toCareSetArray, functionData->rangeBddVars, functionData->rangeCube); }
mdd_t* ImgImageInfoComputeBwdWithDomainVarsMono | ( | ImgFunctionData_t * | functionData, |
Img_ImageInfo_t * | imageInfo, | ||
mdd_t * | fromLowerBound, | ||
mdd_t * | fromUpperBound, | ||
array_t * | toCareSetArray | ||
) |
Function********************************************************************
Synopsis [Computes the backward image of a set of states between fromLowerBound and fromUpperBound.]
Description [Identical to ImgImageInfoComputeBwdMono except that fromLowerBound and fromUpperBound and given in terms of domain variables, hence we need to substitute the range variables first.]
SideEffects []
SeeAlso [ImgImageInfoComputeBwdMono]
Definition at line 234 of file imgMonolithic.c.
{ mdd_t *fromLowerBoundRV = ImgSubstitute(fromLowerBound, functionData, Img_D2R_c); mdd_t *fromUpperBoundRV = ImgSubstitute(fromUpperBound, functionData, Img_D2R_c); mdd_t *image = ImgImageInfoComputeBwdMono(functionData, imageInfo, fromLowerBoundRV, fromUpperBoundRV, toCareSetArray); mdd_free(fromLowerBoundRV); mdd_free(fromUpperBoundRV); return image; }
mdd_t* ImgImageInfoComputeFwdMono | ( | ImgFunctionData_t * | functionData, |
Img_ImageInfo_t * | imageInfo, | ||
mdd_t * | fromLowerBound, | ||
mdd_t * | fromUpperBound, | ||
array_t * | toCareSetArray | ||
) |
Function********************************************************************
Synopsis [Computes the forward image of a set of states between fromLowerBound and fromUpperBound.]
Description [Computes the forward image of a set of states between fromLowerBound and fromUpperBound. First a set of states between fromLowerBound and fromUpperBound is computed. Then, the transition relation is simplified by cofactoring it wrt to the set of states found in the first step, and wrt the toCareSet.]
SideEffects []
SeeAlso [ImgImageInfoComputeBwdMono, ImgImageInfoComputeFwdWithDomainVarsMono]
Definition at line 139 of file imgMonolithic.c.
{ return ImageComputeMonolithic((mdd_t *) imageInfo->methodData, fromLowerBound, fromUpperBound, toCareSetArray, functionData->domainBddVars, functionData->domainCube); }
mdd_t* ImgImageInfoComputeFwdWithDomainVarsMono | ( | ImgFunctionData_t * | functionData, |
Img_ImageInfo_t * | imageInfo, | ||
mdd_t * | fromLowerBound, | ||
mdd_t * | fromUpperBound, | ||
array_t * | toCareSetArray | ||
) |
Function********************************************************************
Synopsis [Computes the forward image on domain variables of a set of states between fromLowerBound and fromUpperBound.]
Description [Identical to ImgImageInfoComputeFwdMono except 1. toCareSet is in terms of domain vars and hence range vars are substituted first. 2. Before returning the image, range vars are substituted with domain vars.]
SideEffects []
SeeAlso [ImgImageInfoComputeFwdMono]
Definition at line 168 of file imgMonolithic.c.
{ array_t *toCareSetArrayRV = ImgSubstituteArray(toCareSetArray, functionData, Img_D2R_c); mdd_t *imageRV = ImgImageInfoComputeFwdMono(functionData, imageInfo, fromLowerBound, fromUpperBound, toCareSetArrayRV); mdd_t *imageDV = ImgSubstitute(imageRV, functionData, Img_R2D_c); mdd_array_free(toCareSetArrayRV); mdd_free(imageRV); return imageDV; }
void ImgImageInfoFreeMono | ( | void * | methodData | ) |
Function********************************************************************
Synopsis [Frees the method data associated with the monolithic method.]
SideEffects []
Definition at line 265 of file imgMonolithic.c.
{ mdd_free((mdd_t *)methodData); }
void* ImgImageInfoInitializeMono | ( | void * | methodData, |
ImgFunctionData_t * | functionData, | ||
Img_DirectionType | directionType | ||
) |
AutomaticEnd Function********************************************************************
Synopsis [Initializes an image structure for image computation using a monolithic transition relation.]
Description [This function computes the monolithic transition relation characterizing the behavior of the system from the individual functions.]
SideEffects []
SeeAlso [Img_MultiwayLinearAndSmooth]
Definition at line 72 of file imgMonolithic.c.
{ if (!methodData){ /* Need to compute */ int i; mdd_t *monolithicT; array_t *rootRelations = array_alloc(mdd_t*, 0); graph_t *mddNetwork = functionData->mddNetwork; mdd_manager *mddManager = Part_PartitionReadMddManager(mddNetwork); array_t *roots = functionData->roots; array_t *leaves = array_join(functionData->domainVars, functionData->quantifyVars); array_t *rootFunctions = Part_PartitionBuildFunctions(mddNetwork, roots, leaves, NIL(mdd_t)); array_free(leaves); /* * Take the product of the transition relation of all the root nodes * and smooth out the quantify variables. */ /* * Iterate over the function of all the root nodes. */ for (i=0; i<array_n(rootFunctions); i++) { Mvf_Function_t *rootFunction = array_fetch(Mvf_Function_t*, rootFunctions, i); int rangeVarMddId = array_fetch(int, functionData->rangeVars, i); mdd_t *rootRelation = Mvf_FunctionBuildRelationWithVariable(rootFunction, rangeVarMddId); array_insert_last(mdd_t*, rootRelations, rootRelation); } Mvf_FunctionArrayFree(rootFunctions); monolithicT = Img_MultiwayLinearAndSmooth(mddManager, rootRelations, functionData->quantifyVars, functionData->domainVars, Img_Iwls95_c, Img_Forward_c); mdd_array_free(rootRelations); return ((void *)monolithicT); } else { return methodData; } }
void ImgImageInfoPrintMethodParamsMono | ( | void * | methodData, |
FILE * | fp | ||
) |
Function********************************************************************
Synopsis [Prints information about the IWLS95 method.]
Description [This function is used to obtain the information about the parameters used to initialize the imageInfo.]
SideEffects []
Definition at line 281 of file imgMonolithic.c.
{ mdd_t *monolithicRelation = (mdd_t *)methodData; (void) fprintf(fp,"Printing information about image method: Monolithic\n"); (void) fprintf(fp,"\tSize of monolithic relation = %10ld\n", (long) bdd_size(monolithicRelation)); }
void ImgMinimizeTransitionRelationMono | ( | Img_ImageInfo_t * | imageInfo, |
array_t * | constrainArray, | ||
Img_MinimizeType | minimizeMethod, | ||
int | printStatus | ||
) |
Function********************************************************************
Synopsis [Minimizes transition relation with given constraint.]
Description [Minimizes transition relation with given constraint.]
SideEffects []
Definition at line 335 of file imgMonolithic.c.
{ mdd_t *relation, *simplifiedRelation; int i, size = 0; mdd_t *constrain; relation = (mdd_t *)imageInfo->methodData; if (printStatus) size = bdd_size(relation); for (i = 0; i < array_n(constrainArray); i++) { constrain = array_fetch(mdd_t *, constrainArray, i); simplifiedRelation = Img_MinimizeImage(relation, constrain, minimizeMethod, TRUE); if (printStatus) { (void) fprintf(vis_stdout, "Info: minimized relation %d | %d => %d\n", bdd_size(relation), bdd_size(constrain), bdd_size(simplifiedRelation)); } mdd_free(relation); relation = simplifiedRelation; } imageInfo->methodData = (void *)relation; if (printStatus) { (void) fprintf(vis_stdout, "IMG Info: minimized relation [%d | %ld => %d]\n", size, bdd_size_multiple(constrainArray), bdd_size(relation)); } }
void ImgRestoreTransitionRelationMono | ( | Img_ImageInfo_t * | imageInfo, |
Img_DirectionType | directionType | ||
) |
Function********************************************************************
Synopsis [Restores original transition relation from saved.]
Description [Restores original transition relation from saved.]
SideEffects []
Definition at line 299 of file imgMonolithic.c.
{ mdd_free((mdd_t *) imageInfo->methodData); imageInfo->methodData = (mdd_t *)imageInfo->savedRelation; imageInfo->savedRelation = NIL(void); return; }
char rcsid [] UNUSED = "$Id: imgMonolithic.c,v 1.23 2002/08/27 08:43:12 fabio Exp $" [static] |
CFile***********************************************************************
FileName [imgMonolithic.c]
PackageName [img]
Synopsis [Routines for image computation using a monolithic transition relation.]
Author [Rajeev K. Ranjan, Tom Shiple, Abelardo Pardo, In-Ho Moon]
Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.
IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
Definition at line 35 of file imgMonolithic.c.