/**CFile*********************************************************************** FileName [imgUtil.c] PackageName [img] Synopsis [High-level routines to perform image computations.] Description [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):

  1. 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.
  2. 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.
  3. 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.
] Author [Rajeev Ranjan, Tom Shiple, Abelardo Pardo, In-Ho Moon, Kavita Ravi] 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: imgUtil.c,v 1.74 2005/05/14 21:08:32 jinh Exp $"; /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ static int nImgComps = 0; /* number of image computations */ static int nPreComps = 0; /* number of pre-image computations */ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static int CheckImageValidity(mdd_manager *mddManager, mdd_t *image, array_t *domainVarMddIdArray, array_t *quantifyVarMddIdArray); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ Img_OptimizeType Img_ImageInfoObtainOptimizeType(Img_ImageInfo_t * imageInfo); void Img_ImageInfoSetUseOptimizedRelationFlag(Img_ImageInfo_t * imageInfo); void Img_ImageInfoResetUseOptimizedRelationFlag(Img_ImageInfo_t * imageInfo); void Img_ImageInfoResetLinearComputeRange(Img_ImageInfo_t * imageInfo); void Img_ImageInfoSetLinearComputeRange(Img_ImageInfo_t * imageInfo); /**Function******************************************************************** Synopsis [Initialize the image package.] SideEffects [] SeeAlso [Img_End] ******************************************************************************/ void Img_Init(void) { /* Set the default settings. */ } /**Function******************************************************************** Synopsis [End the image package.] SideEffects [] SeeAlso [Img_Init] ******************************************************************************/ void Img_End(void) { /* Do Nothing. */ } /**Function******************************************************************** Synopsis [Return the image method preferred by the user.] Description [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.] SideEffects [] SeeAlso [Img_ImageInfoIninitialize] ******************************************************************************/ Img_MethodType Img_UserSpecifiedMethod(void) { char *userSpecifiedMethod; userSpecifiedMethod = Cmd_FlagReadByName("image_method"); if (userSpecifiedMethod == NIL(char)) return IMGDEFAULT_METHOD; if (strcmp(userSpecifiedMethod, "monolithic") == 0) return Img_Monolithic_c; if (strcmp(userSpecifiedMethod, "tfm") == 0) return Img_Tfm_c; if (strcmp(userSpecifiedMethod, "hybrid") == 0) return Img_Hybrid_c; if (strcmp(userSpecifiedMethod, "iwls95") == 0) return Img_Iwls95_c; if (strcmp(userSpecifiedMethod, "mlp") == 0) return Img_Mlp_c; fprintf(vis_stderr, "** img error: Unrecognized image_method %s", userSpecifiedMethod); fprintf(vis_stderr, "using default method.\n"); return IMGDEFAULT_METHOD; } /**Function******************************************************************** Synopsis [Initializes an imageInfo structure for the given method and direction.] Description [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.] Comment [To add a new method, see the instructions at the top of imgInt.h.] SideEffects [] SeeAlso [Img_ImageInfoComputeFwd Img_ImageInfoComputeBwd Img_ImageInfoFree] ******************************************************************************/ 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) { char *flagValue; int verbosity; mdd_manager *mddManager = Part_PartitionReadMddManager(mddNetwork); int updateFlag = 0; assert(array_n(roots) != 0); /* If it does not exist, create a new one and initialize fields appropriately */ if (imageInfo == NIL(Img_ImageInfo_t)) { imageInfo = ALLOC(Img_ImageInfo_t, 1); memset(imageInfo, 0, sizeof(Img_ImageInfo_t)); imageInfo->directionType = directionType; if (Cmd_FlagReadByName("linear_optimize")) imageInfo->linearOptimize = Opt_NS; /* * Initialization of the function structure inside ImageInfo . * Since no duplication is needed, this process is not encapsulated * inside a static procedure. */ imageInfo->functionData.FAFWFlag = FAFWFlag; imageInfo->functionData.Winning = Winning; imageInfo->functionData.mddNetwork = mddNetwork; imageInfo->functionData.roots = roots; imageInfo->functionData.domainVars = domainVars; imageInfo->functionData.rangeVars = rangeVars; imageInfo->functionData.quantifyVars = quantifyVars; imageInfo->functionData.domainCube = domainCube; imageInfo->functionData.rangeCube = rangeCube; imageInfo->functionData.quantifyCube = quantifyCube; imageInfo->functionData.domainBddVars = mdd_id_array_to_bdd_array( mddManager, domainVars); imageInfo->functionData.rangeBddVars = mdd_id_array_to_bdd_array( mddManager, rangeVars); imageInfo->functionData.quantifyBddVars = mdd_id_array_to_bdd_array( mddManager, quantifyVars); if (bdd_get_package_name() == CUDD) { int i, nVars, idD, idR; mdd_t *varD, *varR; nVars = bdd_num_vars(mddManager); imageInfo->functionData.permutD2R = ALLOC(int, sizeof(int) * nVars); imageInfo->functionData.permutR2D = ALLOC(int, sizeof(int) * nVars); for (i = 0; i < nVars; i++) { imageInfo->functionData.permutD2R[i] = i; imageInfo->functionData.permutR2D[i] = i; } nVars = array_n(imageInfo->functionData.rangeBddVars); for (i = 0; i < nVars; i++) { varD = array_fetch(bdd_t *, imageInfo->functionData.domainBddVars, i); varR = array_fetch(bdd_t *, imageInfo->functionData.rangeBddVars, i); idD = (int)bdd_top_var_id(varD); idR = (int)bdd_top_var_id(varR); imageInfo->functionData.permutD2R[idD] = idR; imageInfo->functionData.permutR2D[idR] = idD; } } else { imageInfo->functionData.permutD2R = NIL(int); imageInfo->functionData.permutR2D = NIL(int); } if (domainCube) imageInfo->functionData.createVarCubesFlag = 1; imageInfo->functionData.network = network; imageInfo->methodData = NIL(void); updateFlag = 1; } /* * If methodType is default, use user-specified method if set. */ if (methodType == Img_Default_c) methodType = Img_UserSpecifiedMethod(); /* If image_method changes, we need to free existing method data and * to update proper function calls. */ if (imageInfo->methodData) { if (imageInfo->methodType != methodType) { (*imageInfo->imageFreeProc)(imageInfo->methodData); imageInfo->methodData = NIL(void); updateFlag = 1; } } if (updateFlag) { imageInfo->methodType = methodType; switch (methodType) { case Img_Monolithic_c: imageInfo->imageComputeFwdProc = ImgImageInfoComputeFwdMono; imageInfo->imageComputeBwdProc = ImgImageInfoComputeBwdMono; imageInfo->imageComputeFwdWithDomainVarsProc = ImgImageInfoComputeFwdWithDomainVarsMono; imageInfo->imageComputeBwdWithDomainVarsProc = ImgImageInfoComputeBwdWithDomainVarsMono; imageInfo->imageFreeProc = ImgImageInfoFreeMono; imageInfo->imagePrintMethodParamsProc = ImgImageInfoPrintMethodParamsMono; break; case Img_Tfm_c: case Img_Hybrid_c: imageInfo->imageComputeFwdProc = ImgImageInfoComputeFwdTfm; imageInfo->imageComputeBwdProc = ImgImageInfoComputeBwdTfm; imageInfo->imageComputeFwdWithDomainVarsProc = ImgImageInfoComputeFwdWithDomainVarsTfm; imageInfo->imageComputeBwdWithDomainVarsProc = ImgImageInfoComputeBwdWithDomainVarsTfm; imageInfo->imageFreeProc = ImgImageInfoFreeTfm; imageInfo->imagePrintMethodParamsProc = ImgImageInfoPrintMethodParamsTfm; break; case Img_Linear_Range_c: case Img_Iwls95_c: case Img_Mlp_c: case Img_Linear_c: imageInfo->imageComputeFwdProc = ImgImageInfoComputeFwdIwls95; imageInfo->imageComputeBwdProc = ImgImageInfoComputeBwdIwls95; imageInfo->imageComputeFwdWithDomainVarsProc = ImgImageInfoComputeFwdWithDomainVarsIwls95; imageInfo->imageComputeBwdWithDomainVarsProc = ImgImageInfoComputeBwdWithDomainVarsIwls95; imageInfo->imageFreeProc = ImgImageInfoFreeIwls95; imageInfo->imagePrintMethodParamsProc = ImgImageInfoPrintMethodParamsIwls95; break; default: fail("** img error: Unexpected type when updating image method"); } imageInfo->fwdTrMinimizedFlag = FALSE; imageInfo->bwdTrMinimizedFlag = FALSE; imageInfo->printMinimizeStatus = 0; imageInfo->savedRelation = NIL(void); flagValue = Cmd_FlagReadByName("image_verbosity"); if (flagValue != NIL(char)) { verbosity = atoi(flagValue); imageInfo->verbosity = verbosity; if (verbosity == 1) imageInfo->printMinimizeStatus = 1; else if (verbosity > 1) imageInfo->printMinimizeStatus = 2; } } /* * Perform method-specific initialization of methodData. */ switch (imageInfo->methodType) { case Img_Monolithic_c: imageInfo->methodData = ImgImageInfoInitializeMono(imageInfo->methodData, &(imageInfo->functionData), directionType); break; case Img_Tfm_c: case Img_Hybrid_c: imageInfo->methodData = ImgImageInfoInitializeTfm(imageInfo->methodData, &(imageInfo->functionData), directionType, imageInfo->methodType); break; case Img_Iwls95_c: case Img_Mlp_c: case Img_Linear_c: case Img_Linear_Range_c: imageInfo->methodData = ImgImageInfoInitializeIwls95(imageInfo->methodData, &(imageInfo->functionData), directionType, imageInfo->methodType); break; default: fail("IMG Error : Unexpected type when initalizing image method"); } return imageInfo; } /**Function******************************************************************** Synopsis [Check the given address of mdd_t is same as the functionData.quantifyCube.] Description [This function is for remove memory leakage.] SideEffects [] SeeAlso [Img_ImageInfoInitialize] ******************************************************************************/ int Img_IsQuantifyCubeSame( Img_ImageInfo_t *imageInfo, mdd_t *quantifyCube) { if(imageInfo->functionData.quantifyCube == quantifyCube) return (1); else return(0); } /**Function******************************************************************** Synopsis [Check the given address of array+t is same as the functionData.quantifyArray.] Description [This function is for remove memory leakage.] SideEffects [] SeeAlso [Img_ImageInfoInitialize] ******************************************************************************/ int Img_IsQuantifyArraySame( Img_ImageInfo_t *imageInfo, array_t *quantifyArray) { if(imageInfo->functionData.quantifyVars == quantifyArray) return (1); else return(0); } /**Function******************************************************************** Synopsis [Updates present state and primary input variables.] Description [Updates present state and primary input variables. This function is called after calling ImageInfoInitialize for a subFsm.] SideEffects [] SeeAlso [Img_ImageInfoInitialize] ******************************************************************************/ void Img_ImageInfoUpdateVariables( Img_ImageInfo_t *imageInfo, graph_t * mddNetwork, array_t * domainVars, array_t * quantifyVars, mdd_t * domainCube, mdd_t * quantifyCube) { mdd_manager *mddManager = Part_PartitionReadMddManager(mddNetwork); imageInfo->functionData.domainVars = domainVars; imageInfo->functionData.quantifyVars = quantifyVars; imageInfo->functionData.domainCube = domainCube; imageInfo->functionData.quantifyCube = quantifyCube; mdd_array_free(imageInfo->functionData.domainBddVars); imageInfo->functionData.domainBddVars = mdd_id_array_to_bdd_array( mddManager, domainVars); mdd_array_free(imageInfo->functionData.quantifyBddVars); imageInfo->functionData.quantifyBddVars = mdd_id_array_to_bdd_array( mddManager, quantifyVars); } /**Function******************************************************************** Synopsis [Sets the flag to allow the next image computation to return a subset of the actual image.] Description [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. ] SideEffects [Flag is reset at the end of every image/preimage computation.] SeeAlso [Img_ImageWasPartialImage] ******************************************************************************/ void Img_ImageAllowPartialImage(Img_ImageInfo_t *info, boolean value) { if (info->methodType == Img_Iwls95_c || info->methodType == Img_Mlp_c) { ImgImageAllowPartialImageIwls95(info->methodData, value); } return; } /**Function******************************************************************** Synopsis [Prints partial image options.] Description [Prints partial image options.] SideEffects [] ******************************************************************************/ void Img_ImagePrintPartialImageOptions(void) { ImgPrintPartialImageOptions(); return; } /**Function******************************************************************** Synopsis [Queries whether the last image computation was partial.] Description [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.] SideEffects [Reset before every image/preimage computation.] SeeAlso [Img_ImageAllowPartialImage] ******************************************************************************/ boolean Img_ImageWasPartial(Img_ImageInfo_t *info) { if (info->methodType == Img_Iwls95_c || info->methodType == Img_Mlp_c) return (ImgImageWasPartialIwls95(info->methodData)); else return FALSE; } /**Function******************************************************************** Synopsis [Computes the forward image of a set and expresses it in terms of domain variables.] Description [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.)] SideEffects [] SeeAlso [Img_ImageInfoComputeFwd] ******************************************************************************/ mdd_t * Img_ImageInfoComputeImageWithDomainVars( Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, array_t * toCareSetArray) { mdd_t *image; mdd_manager *mddManager; long peakMem; int peakLiveNode; if (mdd_is_tautology(fromLowerBound, 0)){ mddManager = Part_PartitionReadMddManager( imageInfo->functionData.mddNetwork); return (mdd_zero(mddManager)); } image = ((*imageInfo->imageComputeFwdWithDomainVarsProc) (&(imageInfo->functionData), imageInfo, fromLowerBound, fromUpperBound, toCareSetArray)); nImgComps++; if (imageInfo->verbosity >= 2 && bdd_get_package_name() == CUDD) { mddManager = Part_PartitionReadMddManager( imageInfo->functionData.mddNetwork); peakMem = bdd_read_peak_memory(mddManager); peakLiveNode = bdd_read_peak_live_node(mddManager); fprintf(vis_stdout, "** img info: current peak memory = %ld\n", peakMem); fprintf(vis_stdout, "** img info: current peak live nodes = %d\n", peakLiveNode); } #ifndef NDEBUG assert(CheckImageValidity( Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork), image, imageInfo->functionData.rangeVars, imageInfo->functionData.quantifyVars)); #endif return(image); } /**Function******************************************************************** Synopsis [Computes the forward image of a set and expresses it in terms of domain variables.] Description [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.)] SideEffects [] SeeAlso [Img_ImageInfoComputeFwd] ******************************************************************************/ mdd_t * Img_ImageInfoComputeFwdWithDomainVars( Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, mdd_t * toCareSet) { array_t *toCareSetArray; mdd_t *image; toCareSetArray = array_alloc(mdd_t *, 0); array_insert(mdd_t *, toCareSetArray, 0, toCareSet); image = Img_ImageInfoComputeImageWithDomainVars(imageInfo, fromLowerBound, fromUpperBound, toCareSetArray); array_free(toCareSetArray); return(image); } /**Function******************************************************************** Synopsis [Computes the forward image of a set.] Description [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.)] SideEffects [] SeeAlso [Img_ImageInfoInitialize Img_ImageInfoComputeBwd Img_ImageInfoFree Img_ImageInfoComputeFwdWithDomainVars] ******************************************************************************/ mdd_t * Img_ImageInfoComputeFwd(Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, array_t * toCareSetArray) { mdd_t *image; if (mdd_is_tautology(fromLowerBound, 0)){ mdd_manager *mddManager = Part_PartitionReadMddManager( imageInfo->functionData.mddNetwork); return (mdd_zero(mddManager)); } image = ((*imageInfo->imageComputeFwdProc) (&(imageInfo->functionData), imageInfo, fromLowerBound, fromUpperBound, toCareSetArray)); nImgComps++; #ifndef NDEBUG assert(CheckImageValidity( Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork), image, imageInfo->functionData.domainVars, imageInfo->functionData.quantifyVars)); #endif return image; } /**Function******************************************************************** Synopsis [Computes the backward image of a set expressed in terms of domain variables.] Description [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.] SideEffects [] SeeAlso [Img_ImageInfoComputeBwd] ******************************************************************************/ mdd_t * Img_ImageInfoComputePreImageWithDomainVars( Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, array_t * toCareSetArray) { mdd_t *image; if (mdd_is_tautology(fromLowerBound, 0)){ mdd_manager *mddManager = Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork); return (mdd_zero(mddManager)); } image = ((*imageInfo->imageComputeBwdWithDomainVarsProc) (&(imageInfo->functionData), imageInfo, fromLowerBound, fromUpperBound, toCareSetArray)); nPreComps++; #ifndef NDEBUG assert(CheckImageValidity( Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork), image, imageInfo->functionData.rangeVars, imageInfo->functionData.quantifyVars)); #endif return image; } /**Function******************************************************************** Synopsis [Computes the backward image of a set expressed in terms of domain variables.] Description [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.] SideEffects [] SeeAlso [Img_ImageInfoComputeBwd] ******************************************************************************/ mdd_t * Img_ImageInfoComputeEXWithDomainVars( Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, array_t * toCareSetArray) { mdd_t *image; if (mdd_is_tautology(fromLowerBound, 0)){ mdd_manager *mddManager = Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork); return (mdd_zero(mddManager)); } image = ((*imageInfo->imageComputeBwdWithDomainVarsProc) (&(imageInfo->functionData), imageInfo, fromLowerBound, fromUpperBound, toCareSetArray)); nPreComps++; return image; } /**Function******************************************************************** Synopsis [Computes the backward image of a set expressed in terms of domain variables.] Description [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.] SideEffects [] SeeAlso [Img_ImageInfoComputeBwd] ******************************************************************************/ mdd_t * Img_ImageInfoComputeBwdWithDomainVars( Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, mdd_t * toCareSet) { array_t *toCareSetArray; mdd_t *preImage; toCareSetArray = array_alloc(mdd_t *, 0); array_insert(mdd_t *, toCareSetArray, 0, toCareSet); preImage = Img_ImageInfoComputePreImageWithDomainVars(imageInfo, fromLowerBound, fromUpperBound, toCareSetArray); array_free(toCareSetArray); return(preImage); } /**Function******************************************************************** Synopsis [Computes the backward image of a set.] Description [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.] SideEffects [] SeeAlso [Img_ImageInfoInitialize Img_ImageInfoComputeFwd Img_ImageInfoFree Img_ImageInfoComputeBwdWithDomainVars] ******************************************************************************/ mdd_t * Img_ImageInfoComputeBwd(Img_ImageInfo_t * imageInfo, mdd_t * fromLowerBound, mdd_t * fromUpperBound, array_t * toCareSetArray) { mdd_t *image; if (mdd_is_tautology(fromLowerBound, 0)){ mdd_manager *mddManager = Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork); return (mdd_zero(mddManager)); } image = ((*imageInfo->imageComputeBwdProc) (&(imageInfo->functionData), imageInfo, fromLowerBound, fromUpperBound, toCareSetArray)); nPreComps++; #ifndef NDEBUG assert(CheckImageValidity( Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork), image, imageInfo->functionData.rangeVars, imageInfo->functionData.quantifyVars)); #endif return image; } /**Function******************************************************************** Synopsis [Frees the memory associated with imageInfo.] SideEffects [] SeeAlso [Img_ImageInfoInitialize Img_ImageInfoComputeFwd Img_ImageInfoComputeBwd] ******************************************************************************/ void Img_ImageInfoFree(Img_ImageInfo_t * imageInfo) { (*imageInfo->imageFreeProc) (imageInfo->methodData); if (imageInfo->functionData.domainBddVars) mdd_array_free(imageInfo->functionData.domainBddVars); if (imageInfo->functionData.rangeBddVars) mdd_array_free(imageInfo->functionData.rangeBddVars); if (imageInfo->functionData.quantifyBddVars) mdd_array_free(imageInfo->functionData.quantifyBddVars); if (imageInfo->functionData.permutD2R) FREE(imageInfo->functionData.permutD2R); if (imageInfo->functionData.permutR2D) FREE(imageInfo->functionData.permutR2D); if (imageInfo->savedRelation) mdd_array_free((array_t *) imageInfo->savedRelation); FREE(imageInfo); } /**Function******************************************************************** Synopsis [Frees the memory associated with imageInfo.] SideEffects [] SeeAlso [Img_ImageInfoInitialize Img_ImageInfoComputeFwd Img_ImageInfoComputeBwd] ******************************************************************************/ void Img_ImageInfoFreeFAFW(Img_ImageInfo_t * imageInfo) { if (imageInfo->functionData.quantifyVars) mdd_array_free(imageInfo->functionData.quantifyVars); if (imageInfo->functionData.quantifyCube) mdd_free(imageInfo->functionData.quantifyCube); } /**Function******************************************************************** Synopsis [Returns a string giving the method type of an imageInfo.] Description [Returns a string giving the method type of an imageInfo. It is the user's responsibility to free this string.] SideEffects [] SeeAlso [Img_ImageInfoInitialize] ******************************************************************************/ char * Img_ImageInfoObtainMethodTypeAsString(Img_ImageInfo_t * imageInfo) { char *methodString; Img_MethodType methodType = imageInfo->methodType; switch (methodType) { case Img_Monolithic_c: methodString = util_strsav("monolithic"); break; case Img_Tfm_c: methodString = util_strsav("tfm"); break; case Img_Hybrid_c: methodString = util_strsav("hybrid"); break; case Img_Iwls95_c: methodString = util_strsav("iwls95"); break; case Img_Mlp_c: methodString = util_strsav("mlp"); break; case Img_Linear_c: methodString = util_strsav("linear"); break; case Img_Default_c: methodString = util_strsav("default"); break; default: fail("IMG Error : Unexpected type when initalizing image method"); } return methodString; } /**Function******************************************************************** Synopsis [Returns the method type of an imageInfo.] Description [Returns the method type of an imageInfo.] SideEffects [] SeeAlso [Img_ImageInfoInitialize] ******************************************************************************/ Img_MethodType Img_ImageInfoObtainMethodType(Img_ImageInfo_t * imageInfo) { return(imageInfo->methodType); } /**Function******************************************************************** Synopsis [Returns the method type of an imageInfo.] Description [Returns the method type of an imageInfo.] SideEffects [] SeeAlso [Img_ImageInfoInitialize] ******************************************************************************/ Img_OptimizeType Img_ImageInfoObtainOptimizeType(Img_ImageInfo_t * imageInfo) { return(imageInfo->linearOptimize); } /**Function******************************************************************** Synopsis [set optimization relation flag .] Description [set optimization relation flag .] SideEffects [] SeeAlso [Img_ImageInfoInitialize] ******************************************************************************/ void Img_ImageInfoSetUseOptimizedRelationFlag(Img_ImageInfo_t * imageInfo) { imageInfo->useOptimizedRelationFlag = 1; } /**Function******************************************************************** Synopsis [reset optimization relation flag .] Description [reset optimization relation flag .] SideEffects [] SeeAlso [Img_ImageInfoInitialize] ******************************************************************************/ void Img_ImageInfoResetUseOptimizedRelationFlag(Img_ImageInfo_t * imageInfo) { imageInfo->useOptimizedRelationFlag = 0; } /**Function******************************************************************** Synopsis [Reset linear compute range flag.] Description [Reset linear compute range flag.] SideEffects [] SeeAlso [Img_ImageInfoInitialize] ******************************************************************************/ void Img_ImageInfoResetLinearComputeRange(Img_ImageInfo_t * imageInfo) { imageInfo->linearComputeRange = 0; } /**Function******************************************************************** Synopsis [Set linear compute range flag.] Description [Set linear compute range flag.] SideEffects [] SeeAlso [Img_ImageInfoInitialize] ******************************************************************************/ void Img_ImageInfoSetLinearComputeRange(Img_ImageInfo_t * imageInfo) { imageInfo->linearComputeRange = 1; } /**Function******************************************************************** Synopsis [Prints information about the image technique currently used.] Description [Prints information about the image technique currently used.] SideEffects [None.] ******************************************************************************/ void Img_ImageInfoPrintMethodParams(Img_ImageInfo_t *imageInfo, FILE *fp) { (*imageInfo->imagePrintMethodParamsProc)(imageInfo->methodData, fp); } /**Function******************************************************************** Synopsis [Resets the flag that transition relation is minimized.] Description [Resets the flag that transition relation is minimized.] SideEffects [] ******************************************************************************/ void Img_ResetTrMinimizedFlag(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType) { if (directionType == Img_Forward_c || directionType == Img_Both_c) imageInfo->fwdTrMinimizedFlag = FALSE; if (directionType == Img_Backward_c || directionType == Img_Both_c) imageInfo->bwdTrMinimizedFlag = FALSE; } /**Function******************************************************************** Synopsis [Returns current method of minimizing transition relation.] Description [Returns current method of minimizing transition relation. Default is restrict.] SideEffects [] ******************************************************************************/ Img_MinimizeType Img_ReadMinimizeMethod(void) { int value; char *flagValue; Img_MinimizeType minimizeMethod = Img_Restrict_c; flagValue = Cmd_FlagReadByName("image_minimize_method"); if (flagValue != NIL(char)) { sscanf(flagValue, "%d", &value); switch (value) { case 0 : minimizeMethod = Img_Restrict_c; break; case 1 : minimizeMethod = Img_Constrain_c; break; case 2 : if (bdd_get_package_name() != CUDD) { fprintf(vis_stderr, "** img error : Compact in image_minimize_method "); fprintf(vis_stderr, "is currently supported only by CUDD. ***\n"); fprintf(vis_stderr, "** img error : Reverting to default minimize method : restrict\n"); break; } minimizeMethod = Img_Compact_c; break; case 3 : if (bdd_get_package_name() != CUDD) { fprintf(vis_stderr, "** img error : Squeeze in image_minimize_method "); fprintf(vis_stderr, "is currently supported only by CUDD. ***\n"); fprintf(vis_stderr, "** img error : Reverting to default minimize method : restrict\n"); break; } minimizeMethod = Img_Squeeze_c; break; case 4 : minimizeMethod = Img_And_c; break; default : fprintf(vis_stderr, "** img error : invalid value %s for image_minimize_method[0-4]. ***\n", flagValue); fprintf(vis_stderr, "** img error : Reverting to default minimize method : restrict\n"); break; } } return(minimizeMethod); } /**Function******************************************************************** Synopsis [Minimizes transition relation with given constraint if it hasn't been minimized already.] Description [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.] SideEffects [] ******************************************************************************/ void Img_MinimizeTransitionRelation( Img_ImageInfo_t *imageInfo, array_t *constrainArray, Img_MinimizeType minimizeMethod, Img_DirectionType directionType, boolean reorderIwls95Clusters) { if (minimizeMethod == Img_DefaultMinimizeMethod_c) minimizeMethod = Img_ReadMinimizeMethod(); switch (imageInfo->methodType) { case Img_Monolithic_c: if (imageInfo->fwdTrMinimizedFlag) break; ImgMinimizeTransitionRelationMono(imageInfo, constrainArray, minimizeMethod, imageInfo->printMinimizeStatus); imageInfo->fwdTrMinimizedFlag = TRUE; break; case Img_Tfm_c: case Img_Hybrid_c: if (imageInfo->fwdTrMinimizedFlag) break; ImgMinimizeTransitionFunction(imageInfo->methodData, constrainArray, minimizeMethod, directionType, imageInfo->printMinimizeStatus); if (directionType == Img_Forward_c || directionType == Img_Both_c) imageInfo->fwdTrMinimizedFlag = TRUE; if (directionType == Img_Backward_c || directionType == Img_Both_c) imageInfo->bwdTrMinimizedFlag = TRUE; break; case Img_Iwls95_c: case Img_Mlp_c: case Img_Linear_c: if (directionType == Img_Forward_c || directionType == Img_Both_c) { if (imageInfo->fwdTrMinimizedFlag == FALSE) { ImgMinimizeTransitionRelationIwls95(imageInfo->methodData, &(imageInfo->functionData), constrainArray, minimizeMethod, Img_Forward_c, reorderIwls95Clusters, imageInfo->printMinimizeStatus); imageInfo->fwdTrMinimizedFlag = TRUE; } } if (directionType == Img_Backward_c || directionType == Img_Both_c) { if (imageInfo->bwdTrMinimizedFlag == FALSE) { ImgMinimizeTransitionRelationIwls95(imageInfo->methodData, &(imageInfo->functionData), constrainArray, minimizeMethod, Img_Backward_c, reorderIwls95Clusters, imageInfo->printMinimizeStatus); imageInfo->bwdTrMinimizedFlag = TRUE; } } break; default: fail("** img error: Unexpected type when minimizing transition relation"); } } /**Function******************************************************************** Synopsis [Minimizes an image with given constraint.] Description [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. ] SideEffects [] ******************************************************************************/ mdd_t * Img_MinimizeImage( mdd_t *image, mdd_t *constraint, Img_MinimizeType method, boolean underapprox) { mdd_t *newImage; mdd_t *l, *u; if (method == Img_DefaultMinimizeMethod_c) method = Img_ReadMinimizeMethod(); if(underapprox){ switch (method) { case Img_Restrict_c : newImage = bdd_minimize(image, constraint); break; case Img_Constrain_c : newImage = bdd_cofactor(image, constraint); break; case Img_Compact_c : newImage = bdd_compact(image, constraint); break; case Img_Squeeze_c : l = bdd_and(image, constraint, 1, 1); u = bdd_or(image, constraint, 1, 0); newImage = bdd_squeeze(l, u); if (bdd_size(newImage) >= bdd_size(image)) { bdd_free(newImage); newImage = bdd_dup(image); } mdd_free(l); mdd_free(u); break; case Img_And_c : newImage = bdd_and(image, constraint, 1, 1); break; default : fail("** img error : Unexpected type when minimizing an image"); } }else{ /* if underapprox */ switch (method) { case Img_Squeeze_c : l = image; u = bdd_or(image, constraint, 1, 0); newImage = bdd_squeeze(l, u); if (bdd_size(newImage) >= bdd_size(image)) { bdd_free(newImage); newImage = bdd_dup(image); } mdd_free(u); break; case Img_OrNot_c : newImage = bdd_or(image, constraint, 1, 0); break; default : fail("** img error: Unexpected type when adding dont-cares to an image"); } }/* if underapprox */ return(newImage); } /**Function******************************************************************** Synopsis [Adds a dont care set to the given image.] Description [Adds a dont care set to the given image.] SideEffects [] ******************************************************************************/ mdd_t * Img_AddDontCareToImage( mdd_t *image, mdd_t *constraint, Img_MinimizeType method) { return(Img_MinimizeImage(image, constraint, Img_Restrict_c, method)); } /**Function******************************************************************** Synopsis [Minimizes a single bdd with a set of constraint.] Description [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).] SideEffects [Img_MinimizeImage] ******************************************************************************/ mdd_t * Img_MinimizeImageArray( mdd_t *image, array_t *constraintArray, Img_MinimizeType method, boolean underapprox) { int i; mdd_t *newImage, *tmpImage; mdd_t *constraint; if (method == Img_DefaultMinimizeMethod_c) method = Img_ReadMinimizeMethod(); newImage = mdd_dup(image); arrayForEachItem(mdd_t *, constraintArray, i, constraint) { tmpImage = newImage; newImage = Img_MinimizeImage(tmpImage, constraint, method, underapprox); mdd_free(tmpImage); } return(newImage); } /**Function******************************************************************** Synopsis [Sets the flag whether to print the status of minimizing transition relation.] Description [Sets the flag whether to print the status of minimizing transition relation.] SideEffects [] ******************************************************************************/ void Img_SetPrintMinimizeStatus(Img_ImageInfo_t *imageInfo, int status) { if (status < 0 || status > 2) (void)fprintf(vis_stderr, "** img error: invalid value[%d] for status.\n", status); else imageInfo->printMinimizeStatus = status; } /**Function******************************************************************** Synopsis [Reads the flag whether to print the status of minimizing transition relation.] Description [Reads the flag whether to print the status of minimizing transition relation.] SideEffects [] ******************************************************************************/ int Img_ReadPrintMinimizeStatus(Img_ImageInfo_t *imageInfo) { return(imageInfo->printMinimizeStatus); } /**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 Img_AbstractTransitionRelation(Img_ImageInfo_t *imageInfo, array_t *abstractVars, mdd_t *abstractCube, Img_DirectionType directionType) { switch (imageInfo->methodType) { case Img_Monolithic_c: ImgAbstractTransitionRelationMono(imageInfo, abstractVars, abstractCube, imageInfo->printMinimizeStatus); break; case Img_Tfm_c: case Img_Hybrid_c: ImgAbstractTransitionFunction(imageInfo, abstractVars, abstractCube, directionType, imageInfo->printMinimizeStatus); break; case Img_Iwls95_c: case Img_Mlp_c: case Img_Linear_c: ImgAbstractTransitionRelationIwls95(imageInfo, abstractVars, abstractCube, directionType, imageInfo->printMinimizeStatus); break; default: fail("** img error : Unexpected type when abstracting transition relation"); } } /**Function******************************************************************** Synopsis [Duplicates the transition relation for backup.] Description [Duplicates the transition relation for backup. Copies transition relation as well as quantification schedule for temporary use.] SideEffects [] ******************************************************************************/ void Img_DupTransitionRelation(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType) { switch (imageInfo->methodType) { case Img_Monolithic_c: ImgDuplicateTransitionRelationMono(imageInfo); break; case Img_Tfm_c: case Img_Hybrid_c: ImgDuplicateTransitionFunction(imageInfo, directionType); break; case Img_Iwls95_c: case Img_Mlp_c: case Img_Linear_c: ImgDuplicateTransitionRelationIwls95(imageInfo, directionType); break; default: fail("** img error: Unexpected type when duplicating transition relation"); } } /**Function******************************************************************** Synopsis [Restores original transition relation from saved.] Description [Restores original transition relation from saved.] SideEffects [] ******************************************************************************/ void Img_RestoreTransitionRelation(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType) { switch (imageInfo->methodType) { case Img_Monolithic_c: ImgRestoreTransitionRelationMono(imageInfo, directionType); break; case Img_Tfm_c: case Img_Hybrid_c: ImgRestoreTransitionFunction(imageInfo, directionType); break; case Img_Iwls95_c: case Img_Mlp_c: case Img_Linear_c: ImgRestoreTransitionRelationIwls95(imageInfo, directionType); break; default: fail("** img error : Unexpected type when backup transition relation"); } } /**Function******************************************************************** Synopsis [Approximate transition relation.] Description [Approximate transition relation.] SideEffects [] ******************************************************************************/ 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) { int unchanged = 0; mdd_manager *mgr = Part_PartitionReadMddManager(imageInfo->functionData.mddNetwork); switch (imageInfo->methodType) { case Img_Monolithic_c: unchanged = ImgApproximateTransitionRelationMono(mgr, imageInfo, approxDir, approxMethod, approxThreshold, approxQuality, approxQualityBias, bias); break; case Img_Tfm_c: case Img_Hybrid_c: unchanged = ImgApproximateTransitionFunction(mgr, imageInfo->methodData, approxDir, approxMethod, approxThreshold, approxQuality, approxQualityBias, directionType, bias); break; case Img_Iwls95_c: case Img_Mlp_c: case Img_Linear_c: if (directionType == Img_Forward_c || directionType == Img_Both_c) { unchanged = ImgApproximateTransitionRelationIwls95(mgr, imageInfo->methodData, approxDir, approxMethod, approxThreshold, approxQuality, approxQualityBias, Img_Forward_c, bias); } if (directionType == Img_Backward_c || directionType == Img_Both_c) { unchanged += ImgApproximateTransitionRelationIwls95(mgr, imageInfo->methodData, approxDir, approxMethod, approxThreshold, approxQuality, approxQualityBias, Img_Backward_c, bias); } break; default: fail( "** img error : Unexpected type when approximating transition relation"); } return(unchanged); } /**Function******************************************************************** Synopsis [Approximate image.] Description [Approximate image.] SideEffects [] ******************************************************************************/ 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) { double quality; double qualityBias; int nvars = mdd_get_number_of_bdd_support(mgr, image); mdd_t *approxImage; if (approxQuality != 0.0) quality = approxQuality; else quality = 1.0; /* default */ /* based on approximation method specified, compute subset or superset */ switch (approxMethod) { case BDD_APPROX_HB: approxImage = bdd_approx_hb(image, approxDir, nvars, approxThreshold); break; case BDD_APPROX_SP: approxImage = bdd_approx_sp(image, approxDir, nvars, approxThreshold, 0); break; case BDD_APPROX_UA: approxImage = bdd_approx_ua(image, approxDir, nvars, approxThreshold, 0, quality); break; case BDD_APPROX_RUA: approxImage = bdd_approx_remap_ua(image, approxDir, nvars, approxThreshold, quality); break; case BDD_APPROX_BIASED_RUA: if (approxQualityBias != 0.0) qualityBias = approxQualityBias; else qualityBias = 0.5; /* default */ approxImage = bdd_approx_biased_rua(image, approxDir, bias, nvars, approxThreshold, quality, qualityBias); break; case BDD_APPROX_COMP: approxImage = bdd_approx_compress(image, approxDir, nvars, approxThreshold); break; default: assert(0); approxImage = NIL(mdd_t); break; } return(approxImage); } /**Function******************************************************************** Synopsis [Returns 1 if partitioned transition relation is used.] Description [Returns 1 if partitioned transition relation is used.] SideEffects [] ******************************************************************************/ int Img_IsPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo) { if (imageInfo->methodType == Img_Iwls95_c || imageInfo->methodType == Img_Mlp_c || imageInfo->methodType == Img_Linear_c) return(1); else if (imageInfo->methodType == Img_Hybrid_c) return(ImgIsPartitionedTransitionRelationTfm(imageInfo)); else return(0); } /**Function******************************************************************** Synopsis [Resets number of image/preimage computation.] Description [Resets number of image/preimage computation.] SideEffects [] ******************************************************************************/ void Img_ResetNumberOfImageComputation(Img_DirectionType imgDir) { if (imgDir == Img_Forward_c || imgDir == Img_Both_c) nImgComps = 0; if (imgDir == Img_Backward_c || imgDir == Img_Both_c) nPreComps = 0; } /**Function******************************************************************** Synopsis [Returns number of image/preimage computation.] Description [Returns number of image/preimage computation.] SideEffects [] ******************************************************************************/ int Img_GetNumberOfImageComputation(Img_DirectionType imgDir) { if (imgDir == Img_Forward_c) return(nImgComps); else if (imgDir == Img_Backward_c) return(nPreComps); else return(nImgComps + nPreComps); } /**Function******************************************************************** Synopsis [Returns current partitioned transition relation.] Description [Returns current partitioned transition relation.] SideEffects [] ******************************************************************************/ array_t * Img_GetPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo, Img_DirectionType directionType) { array_t *relationArray; switch (imageInfo->methodType) { case Img_Monolithic_c: relationArray = (array_t *)imageInfo->methodData; break; case Img_Tfm_c: case Img_Hybrid_c: relationArray = ImgGetTransitionFunction(imageInfo->methodData, directionType); break; case Img_Iwls95_c: case Img_Mlp_c: case Img_Linear_c: relationArray = ImgGetTransitionRelationIwls95(imageInfo->methodData, directionType); break; default: fail("** img error: Unexpected image method type.\n"); } return(relationArray); } /**Function******************************************************************** Synopsis [Replace ith partitioned transition relation.] Description [Replace ith partitioned transition relation.] SideEffects [] ******************************************************************************/ void Img_ReplaceIthPartitionedTransitionRelation(Img_ImageInfo_t *imageInfo, int i, mdd_t *relation, Img_DirectionType directionType) { switch (imageInfo->methodType) { case Img_Monolithic_c: break; case Img_Tfm_c: case Img_Hybrid_c: ImgReplaceIthTransitionFunction(imageInfo->methodData, i, relation, directionType); break; case Img_Iwls95_c: case Img_Mlp_c: case Img_Linear_c: ImgReplaceIthPartitionedTransitionRelationIwls95(imageInfo->methodData, i, relation, directionType); break; default: fail("** img error: Unexpected image method type.\n"); } } /**Function******************************************************************** Synopsis [Replace partitioned transition relation.] Description [Replace partitioned transition relation.] SideEffects [] ******************************************************************************/ void Img_ReplacePartitionedTransitionRelation(Img_ImageInfo_t *imageInfo, array_t *relationArray, Img_DirectionType directionType) { switch (imageInfo->methodType) { case Img_Monolithic_c: break; case Img_Tfm_c: case Img_Hybrid_c: ImgUpdateTransitionFunction(imageInfo->methodData, relationArray, directionType); break; case Img_Iwls95_c: case Img_Mlp_c: case Img_Linear_c: ImgUpdateTransitionRelationIwls95(imageInfo->methodData, relationArray, directionType); break; default: fail("** img error: Unexpected image method type.\n"); } } /**Function******************************************************************** Synopsis [Replace partitioned transition relation.] Description [Replace partitioned transition relation.] SideEffects [] ******************************************************************************/ mdd_t * Img_ComposeIntermediateNodes(graph_t *partition, mdd_t *node, array_t *psVars, array_t *nsVars, array_t *inputVars) { mdd_manager *mgr = Part_PartitionReadMddManager(partition); array_t *supportList; st_table *supportTable = st_init_table(st_numcmp, st_numhash); int i, j; int existIntermediateVars; int mddId; vertex_t *vertex; array_t *varBddFunctionArray, *varArray; mdd_t *var, *func, *tmpMdd; mdd_t *composedNode; Mvf_Function_t *mvf; if (psVars) { for (i = 0; i < array_n(psVars); i++) { mddId = array_fetch(int, psVars, i); st_insert(supportTable, (char *)(long)mddId, NULL); } } if (nsVars) { for (i = 0; i < array_n(nsVars); i++) { mddId = array_fetch(int, nsVars, i); st_insert(supportTable, (char *)(long)mddId, NULL); } } if (inputVars) { for (i = 0; i < array_n(inputVars); i++) { mddId = array_fetch(int, inputVars, i); st_insert(supportTable, (char *)(long)mddId, NULL); } } composedNode = mdd_dup(node); existIntermediateVars = 1; while (existIntermediateVars) { existIntermediateVars = 0; supportList = mdd_get_support(mgr, composedNode); for (i = 0; i < array_n(supportList); i++) { mddId = array_fetch(int, supportList, i); if (!st_lookup(supportTable, (char *)(long)mddId, NULL)) { vertex = Part_PartitionFindVertexByMddId(partition, mddId); mvf = Part_VertexReadFunction(vertex); varBddFunctionArray = mdd_fn_array_to_bdd_fn_array(mgr, mddId, mvf); varArray = mdd_id_to_bdd_array(mgr, mddId); assert(array_n(varBddFunctionArray) == array_n(varArray)); for (j = 0; j < array_n(varBddFunctionArray); j++) { var = array_fetch(mdd_t *, varArray, j); func = array_fetch(mdd_t *, varBddFunctionArray, j); tmpMdd = composedNode; composedNode = bdd_compose(composedNode, var, func); mdd_free(tmpMdd); mdd_free(var); mdd_free(func); } array_free(varBddFunctionArray); array_free(varArray); existIntermediateVars = 1; } } array_free(supportList); } st_free_table(supportTable); return(composedNode); } /**Function******************************************************************** Synopsis [Constrains/adds dont-cares to the bit relations with the given constraint and creates a new transtion relation.] Description [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] and an overapproximation of the transition relation will be in the interval [T, T+ C']. THe method used in minimization is set in Img_GuidedSearchReadUnderApproxMinimizeMethod and Img_GuidedSearchReadOverApproxMinimizeMethod. The cleanup flag cleans up the data (e.g., bit relations) stored for applying constraints repeatedly. ] SideEffects [Current transition relation and quantification schedule are freed. Bit relations are freed if indicated by the cleanUp flag.] SeeAlso [Img_GuidedSearchReadUnderApproxMinimizeMethod Img_GuidedSearchReadOverApproxMinimizeMethod] ******************************************************************************/ void Img_ImageConstrainAndClusterTransitionRelation(Img_ImageInfo_t *imageInfo, Img_DirectionType direction, mdd_t *constrain, Img_MinimizeType minimizeMethod, boolean underApprox, boolean cleanUp, boolean forceReorder, int printStatus) { switch (imageInfo->methodType) { case Img_Monolithic_c: ImgImageConstrainAndClusterTransitionRelationMono(imageInfo, constrain, minimizeMethod, underApprox, cleanUp, forceReorder, printStatus); break; case Img_Tfm_c: case Img_Hybrid_c: ImgImageConstrainAndClusterTransitionRelationTfm(imageInfo, direction, constrain, minimizeMethod, underApprox, cleanUp, forceReorder, printStatus); break; case Img_Iwls95_c: case Img_Mlp_c: case Img_Linear_c: ImgImageConstrainAndClusterTransitionRelationIwls95OrMlp(imageInfo, direction, constrain, minimizeMethod, underApprox, cleanUp, forceReorder, printStatus); break; default: fail("** img error: Unexpected image method type.\n"); } } /**Function******************************************************************** Synopsis [Returns the guided search minimize method of underapproximating the transition relation.] Description [Returns the guided search minimize method of underapproximating the transition relation. Default is And.] SideEffects [] ******************************************************************************/ Img_MinimizeType Img_GuidedSearchReadUnderApproxMinimizeMethod(void) { char *flagValue; Img_MinimizeType minimizeMethod = Img_And_c; flagValue = Cmd_FlagReadByName("guided_search_underapprox_minimize_method"); if (flagValue != NIL(char)) { if (strcmp(flagValue, "constrain") == 0) { minimizeMethod = Img_Constrain_c; } else if (strcmp(flagValue, "and") == 0) { minimizeMethod = Img_And_c; } else { fprintf(vis_stderr, "** img error : invalid value %s for guided_search_underapprox_minimize_method. ***\n", flagValue); fprintf(vis_stderr, "** img error : Reverting to default minimize method : And\n"); } } return(minimizeMethod); } /**Function******************************************************************** Synopsis [Returns the guided search minimize method of overapproximating the transition relation.] Description [Returns the guided search minimize method of overapproximating the transition relation. Default is OrNot.] SideEffects [] ******************************************************************************/ Img_MinimizeType Img_GuidedSearchReadOverApproxMinimizeMethod(void) { char *flagValue; Img_MinimizeType minimizeMethod = Img_OrNot_c; flagValue = Cmd_FlagReadByName("guided_search_overapprox_minimize_method"); if (flagValue != NIL(char)) { if (strcmp(flagValue, "ornot") == 0) { minimizeMethod = Img_OrNot_c; } else if (strcmp(flagValue, "squeeze") == 0) { minimizeMethod = Img_Squeeze_c; } else { fprintf(vis_stderr, "** img error : invalid value %s for guided_search_overapprox_minimize_method. ***\n", flagValue); fprintf(vis_stderr, "** img error : Reverting to default method : OrNot\n"); } } return(minimizeMethod); } /**Function******************************************************************** Synopsis [Substitutes variables between domain and range.] Description [Substitutes variables between domain and range.] SideEffects [] ******************************************************************************/ mdd_t * Img_Substitute(Img_ImageInfo_t *imageInfo, mdd_t *f, Img_SubstituteDir dir) { mdd_t *new_; new_ = ImgSubstitute(f, &(imageInfo->functionData), dir); return(new_); } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Minimize array of bdds wrt a set of constraints] Description [Compute a new array, such that every element corresponds to an element of imageArray minimized with all elements of careSetArray successively, using minimizeMethod. This function can be used for any array of 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.] SideEffects [] SeeAlso[Img_MinimizeImage ImgMinimizeImageArrayWithCareSetArrayInSitu] ******************************************************************************/ array_t * ImgMinimizeImageArrayWithCareSetArray( array_t *imageArray, array_t *careSetArray, Img_MinimizeType minimizeMethod, boolean underapprox, boolean printInfo, Img_DirectionType dir ) { array_t *result; /* of mdd_t * */ result = mdd_array_duplicate(imageArray); ImgMinimizeImageArrayWithCareSetArrayInSitu(result, careSetArray, minimizeMethod, underapprox, printInfo, dir); return result; } /**Function******************************************************************** Synopsis [Minimize array of bdds wrt a set of constraints] Description [Compute a new array, such that every element corresponds to an element of imageArray minimized with all elements of careSetArray successively, using minimizeMethod. This function can be used for any array of 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.

In-situ variant of ImgMinimizeImageArrayWithCareSetArray. Probably saves space. ] SideEffects [] SeeAlso[Img_MinimizeImage,ImgMinimizeImageArrayWithCareSetArray] ******************************************************************************/ void ImgMinimizeImageArrayWithCareSetArrayInSitu( array_t *imageArray, array_t *careSetArray, Img_MinimizeType minimizeMethod, boolean underapprox, boolean printInfo, Img_DirectionType dir) { int i; mdd_t *cluster = NIL(mdd_t); long constrainSize, initialTotalSize; char *dirname = NIL(char); if (minimizeMethod == Img_DefaultMinimizeMethod_c) minimizeMethod = Img_ReadMinimizeMethod(); if(printInfo){ constrainSize = mdd_size_multiple(careSetArray); initialTotalSize = mdd_size_multiple(imageArray); assert(dir != Img_Both_c); if(dir == Img_Forward_c) dirname = "fwd"; else dirname = "bwd"; } else { /* to remove uninitialized variable warnings */ constrainSize = 0; initialTotalSize = 0; } arrayForEachItem(mdd_t *, imageArray, i, cluster){ mdd_t *minimized; minimized = Img_MinimizeImageArray(cluster, careSetArray, minimizeMethod, underapprox); array_insert(mdd_t *, imageArray, i, minimized); if(printInfo) (void) fprintf(vis_stdout, "IMG Info: minimized %s relation %d | %ld => %d in component %d.\n", dirname, mdd_size(cluster), constrainSize, mdd_size(minimized), i); mdd_free(cluster); } if(printInfo) (void) fprintf(vis_stdout, "IMG Info: minimized %s relation %ld | %ld => %ld with %d components.\n", dirname, initialTotalSize, constrainSize, mdd_size_multiple(imageArray), array_n(imageArray)); return; } /**Function******************************************************************** Synopsis [Substitutes variables between domain and range.] Description [Substitutes variables between domain and range.] SideEffects [] ******************************************************************************/ mdd_t * ImgSubstitute(mdd_t *f, ImgFunctionData_t *functionData, Img_SubstituteDir dir) { mdd_t *new_; if (bdd_get_package_name() == CUDD) { if (dir == Img_D2R_c) new_ = bdd_substitute_with_permut(f, functionData->permutD2R); else new_ = bdd_substitute_with_permut(f, functionData->permutR2D); } else { if (dir == Img_D2R_c) { new_ = bdd_substitute(f, functionData->domainBddVars, functionData->rangeBddVars); } else { new_ = bdd_substitute(f, functionData->rangeBddVars, functionData->domainBddVars); } } return(new_); } /**Function******************************************************************** Synopsis [Substitutes variables between domain and range.] Description [Substitutes variables between domain and range.] SideEffects [] ******************************************************************************/ array_t * ImgSubstituteArray(array_t *f_array, ImgFunctionData_t *functionData, Img_SubstituteDir dir) { array_t *new_array; if (bdd_get_package_name() == CUDD) { if (dir == Img_D2R_c) { new_array = bdd_substitute_array_with_permut(f_array, functionData->permutD2R); } else { new_array = bdd_substitute_array_with_permut(f_array, functionData->permutR2D); } } else { if (dir == Img_D2R_c) { new_array = bdd_substitute_array(f_array, functionData->domainBddVars, functionData->rangeBddVars); } else { new_array = bdd_substitute_array(f_array, functionData->rangeBddVars, functionData->domainBddVars); } } return(new_array); } /**Function******************************************************************** Synopsis [Prints Partial Image options.] Description [Prints Partial Image options.] SideEffects [] ******************************************************************************/ void ImgPrintPartialImageOptions(void) { ImgPartialImageOption_t *PIoption; char *dummy; PIoption = ImgGetPartialImageOptions(); dummy = ALLOC(char, 25); switch (PIoption->partialImageMethod) { case Img_PIApprox_c: sprintf(dummy, "%s", "approx");break; case Img_PIClipping_c: sprintf(dummy, "%s", "clipping");break; default: sprintf(dummy, "%s", "approx");break; } fprintf(vis_stdout, "HD: Partial Image number of variables = %d\n", PIoption->nvars); fprintf(vis_stdout, "HD: Partial Image Method = %s\n", dummy); fprintf(vis_stdout, "HD: Partial Image Threshold = %d\n", PIoption->partialImageThreshold); fprintf(vis_stdout, "HD: Partial Image Size = %d\n", PIoption->partialImageSize); switch (PIoption->partialImageApproxMethod) { case BDD_APPROX_HB: sprintf(dummy, "%s", "heavy_branch"); break; case BDD_APPROX_SP: sprintf(dummy, "%s", "short_paths"); break; case BDD_APPROX_UA: sprintf(dummy, "%s", "under_approx"); break; case BDD_APPROX_RUA: sprintf(dummy, "%s", "remap_ua"); break; case BDD_APPROX_COMP: sprintf(dummy, "%s", "compress"); break; default: sprintf(dummy, "%s", "remap_ua"); break; } fprintf(vis_stdout, "HD: Partial Image Approximation Method = %s\n", dummy); fprintf(vis_stdout, "HD: Partial Image Approximation quality factor = %g\n", PIoption->quality); fprintf(vis_stdout, "HD: Partial Image Approximation Bias quality factor = %g\n", PIoption->qualityBias); fprintf(vis_stdout, "HD: Partial Image Clipping factor = %g\n", PIoption->clippingDepthFrac); FREE(dummy); FREE(PIoption); return; } /* end of ImgPrintPartialImageOptions */ /**Function******************************************************************** Synopsis [Get partial image options.] Description [Get partial image options.] SideEffects [] ******************************************************************************/ ImgPartialImageOption_t * ImgGetPartialImageOptions(void) { ImgPartialImageOption_t *options; char *qualityString; char *partialImageThresholdString, *partialImageApproxString, *partialImageSizeString; char *partialImageMethodString, *clippingDepthString; options = ALLOC(ImgPartialImageOption_t , 1); if (options == NIL(ImgPartialImageOption_t)) return NIL(ImgPartialImageOption_t); /* initialize to default values; */ options->nvars = 0; options->partialImageMethod = Img_PIApprox_c; options->partialImageThreshold = 200000; options->partialImageSize = 100000; options->partialImageApproxMethod = BDD_APPROX_RUA; options->quality = 1.0; options->qualityBias = 0.5; options->clippingDepthFrac = IMG_PI_CLIP_DEPTH; /* what kind of approximation to apply to the image */ partialImageMethodString = Cmd_FlagReadByName("hd_partial_image_method"); if (partialImageMethodString != NIL(char)) { if (strcmp(partialImageMethodString, "approx") == 0) { options->partialImageMethod = Img_PIApprox_c; } else if (strcmp(partialImageMethodString, "clipping") == 0) { options->partialImageMethod = Img_PIClipping_c; } } /* threshold to trigger partial image computation */ partialImageThresholdString = Cmd_FlagReadByName("hd_partial_image_threshold"); if (partialImageThresholdString != NIL(char)) { options->partialImageThreshold = strtol(partialImageThresholdString, NULL, 10); if (options->partialImageThreshold < 0) { options->partialImageThreshold = 200000; } } /* intended size of partial image */ partialImageSizeString = Cmd_FlagReadByName("hd_partial_image_size"); if (partialImageSizeString != NIL(char)) { options->partialImageSize = strtol(partialImageSizeString, NULL, 10); if (options->partialImageSize < 0) { options->partialImageSize = 100000; } } /* which approximation method to apply */ partialImageApproxString = Cmd_FlagReadByName("hd_partial_image_approx"); if (partialImageApproxString != NIL(char)) { if (strcmp(partialImageApproxString, "heavy_branch") == 0) { options->partialImageApproxMethod = BDD_APPROX_HB; } else if (strcmp(partialImageApproxString, "short_paths") == 0) { options->partialImageApproxMethod = BDD_APPROX_SP; } else if (strcmp(partialImageApproxString, "under_approx") == 0) { options->partialImageApproxMethod = BDD_APPROX_UA; } else if (strcmp(partialImageApproxString, "remap_ua") == 0) { options->partialImageApproxMethod = BDD_APPROX_RUA; } else if (strcmp(partialImageApproxString, "compress") == 0) { options->partialImageApproxMethod = BDD_APPROX_COMP; } else if (strcmp(partialImageApproxString, "biased_rua") == 0) { options->partialImageApproxMethod = BDD_APPROX_BIASED_RUA; } } /* quality factor for remap_ua and under_approx methods */ qualityString = Cmd_FlagReadByName("hd_partial_image_approx_quality"); if (qualityString != NIL(char)) { options->quality = strtod(qualityString, NULL); if (options->quality < 0.0) { options->quality = 1.0; } } /* quality factor for remap_ua and under_approx methods */ qualityString = Cmd_FlagReadByName("hd_partial_image_approx_bias_quality"); if (qualityString != NIL(char)) { options->qualityBias = strtod(qualityString, NULL); if (options->qualityBias < 0.0) { options->qualityBias = 0.5; } } /* fraction of depth of Bdd to clip at. */ clippingDepthString = Cmd_FlagReadByName("hd_partial_image_clipping_depth"); if (clippingDepthString != NIL(char)) { options->clippingDepthFrac = strtod(clippingDepthString, NULL); if ((options->clippingDepthFrac > 1.0) || (options->clippingDepthFrac < 0.0)) { options->clippingDepthFrac = IMG_PI_CLIP_DEPTH; } } return (options); } /* end of ImgGetPartialImageOptions */ /**Function******************************************************************** Synopsis [This function checks the validity of an array of array of BDD nodes.] SideEffects [] SeeAlso [ImgBddCheckValidity] ******************************************************************************/ int ImgArrayBddArrayCheckValidity(array_t *arrayBddArray) { int i; for(i=0; i 0xf.] SideEffects [] ******************************************************************************/ int ImgBddCheckValidity(bdd_t *bdd) { #ifndef NDEBUG int i; #endif assert(bdd_get_free(bdd) == 0); /* Bdd should not have been freed */ assert(((unsigned long)bdd_get_node(bdd, &i)) & ~0xf); /* Valid node pointer */ assert(((unsigned long)bdd_get_manager(bdd)) & ~0xf); /* Valid manager pointer */ return 1; } /**Function******************************************************************** Synopsis [Prints the content of a table containing integers.] Description [Prints the content of a table containing integers.] SideEffects [] ******************************************************************************/ void ImgPrintVarIdTable(st_table *table) { st_generator *stgen; long varId; st_foreach_item(table, stgen, &varId, NULL){ (void) fprintf(vis_stdout, "%d ", (int) varId); } (void) fprintf(vis_stdout, "\n"); } /**Function******************************************************************** Synopsis [Checks whether toCareSetArray changed.] Description [Checks whether toCareSetArray changed.] SideEffects [] ******************************************************************************/ int ImgCheckToCareSetArrayChanged(array_t *toCareSetArray1, array_t *toCareSetArray2) { int i, size1, size2; mdd_t *careSet1, *careSet2; size1 = array_n(toCareSetArray1); size2 = array_n(toCareSetArray2); if (size1 != size2) return(1); for (i = 0; i < size1; i++) { careSet1 = array_fetch(mdd_t *, toCareSetArray1, i); careSet2 = array_fetch(mdd_t *, toCareSetArray2, i); if (bdd_equal(careSet1, careSet2) == 0) return(1); } return(0); } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Checks the validity of image] Description [In a properly formed image, there should not be any domain or quantify variables in its support. This function checks for that fact.] SideEffects [] ******************************************************************************/ static int CheckImageValidity(mdd_manager *mddManager, mdd_t *image, array_t *domainVarMddIdArray, array_t *quantifyVarMddIdArray) { int i; array_t *imageSupportArray = mdd_get_support(mddManager, image); st_table *imageSupportTable = st_init_table(st_numcmp, st_numhash); for (i=0; i