/**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.] ******************************************************************************/ #include "imgInt.h" static char rcsid[] UNUSED = "$Id: imgMonolithic.c,v 1.23 2002/08/27 08:43:12 fabio Exp $"; /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static mdd_t * ImageComputeMonolithic(mdd_t *methodData, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray, array_t *smoothVars, mdd_t *smoothCube); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**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] ******************************************************************************/ void * ImgImageInfoInitializeMono(void *methodData, ImgFunctionData_t * functionData, Img_DirectionType directionType) { 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; irangeVars, 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; } } /**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] ******************************************************************************/ mdd_t * ImgImageInfoComputeFwdMono( ImgFunctionData_t * functionData, Img_ImageInfo_t * imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t * toCareSetArray) { return ImageComputeMonolithic((mdd_t *) imageInfo->methodData, fromLowerBound, fromUpperBound, toCareSetArray, functionData->domainBddVars, functionData->domainCube); } /**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] ******************************************************************************/ mdd_t * ImgImageInfoComputeFwdWithDomainVarsMono( ImgFunctionData_t *functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) { 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; } /**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] ******************************************************************************/ mdd_t * ImgImageInfoComputeBwdMono( ImgFunctionData_t * functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) { return ImageComputeMonolithic((mdd_t*)imageInfo->methodData, fromLowerBound, fromUpperBound, toCareSetArray, functionData->rangeBddVars, functionData->rangeCube); } /**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] ******************************************************************************/ mdd_t * ImgImageInfoComputeBwdWithDomainVarsMono( ImgFunctionData_t * functionData, Img_ImageInfo_t *imageInfo, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray) { 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; } /**Function******************************************************************** Synopsis [Frees the method data associated with the monolithic method.] SideEffects [] ******************************************************************************/ void ImgImageInfoFreeMono(void * methodData) { mdd_free((mdd_t *)methodData); } /**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 [] ******************************************************************************/ void ImgImageInfoPrintMethodParamsMono(void *methodData, FILE *fp) { 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)); } /**Function******************************************************************** Synopsis [Restores original transition relation from saved.] Description [Restores original transition relation from saved.] SideEffects [] ******************************************************************************/ void ImgRestoreTransitionRelationMono(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType) { mdd_free((mdd_t *) imageInfo->methodData); imageInfo->methodData = (mdd_t *)imageInfo->savedRelation; imageInfo->savedRelation = NIL(void); return; } /**Function******************************************************************** Synopsis [Duplicates transition relation.] Description [Duplicates transition relation. Assumes that the Transition Relation is a MDD.] SideEffects [] ******************************************************************************/ void ImgDuplicateTransitionRelationMono(Img_ImageInfo_t *imageInfo) { imageInfo->savedRelation = (void *)mdd_dup((mdd_t *) imageInfo->methodData); return; } /**Function******************************************************************** Synopsis [Minimizes transition relation with given constraint.] Description [Minimizes transition relation with given constraint.] SideEffects [] ******************************************************************************/ void ImgMinimizeTransitionRelationMono(Img_ImageInfo_t *imageInfo, array_t *constrainArray, Img_MinimizeType minimizeMethod, int printStatus) { 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)); } } /**Function******************************************************************** Synopsis [Add dont care to transition relation.] Description [Add dont care to transition relation. The constrain array contains care sets.] SideEffects [] ******************************************************************************/ void ImgAddDontCareToTransitionRelationMono(Img_ImageInfo_t *imageInfo, array_t *constrainArray, Img_MinimizeType minimizeMethod, int printStatus) { 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)); } } /**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 [] ******************************************************************************/ void ImgAbstractTransitionRelationMono(Img_ImageInfo_t *imageInfo, array_t *abstractVars, mdd_t *abstractCube, int printStatus) { 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; } /**Function******************************************************************** Synopsis [Approximates transition relation.] Description [Approximates transition relation.] SideEffects [] ******************************************************************************/ 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) { 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); } /**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 ] ******************************************************************************/ void ImgImageConstrainAndClusterTransitionRelationMono(Img_ImageInfo_t *imageInfo, mdd_t *constrain, Img_MinimizeType minimizeMethod, boolean underApprox, boolean cleanUp, boolean forceReorder, int printStatus) { 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; irangeVars, 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); } } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**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 [] ******************************************************************************/ static mdd_t * ImageComputeMonolithic(mdd_t *methodData, mdd_t *fromLowerBound, mdd_t *fromUpperBound, array_t *toCareSetArray, array_t *smoothVars, mdd_t *smoothCube) { 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; }