/**CFile*********************************************************************** FileName [fsmFsm.c] PackageName [fsm] Synopsis [Routines to create and manipulate the FSM structure.] Author [Shaker Sarwary, Tom Shiple, Rajeev Ranjan, 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 "fsmInt.h" static char rcsid[] UNUSED = "$Id: fsmFsm.c,v 1.88 2007/04/02 17:03:13 hhkim Exp $"; /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static Fsm_Fsm_t * FsmStructAlloc(Ntk_Network_t *network, graph_t *partition); static void FsmCreateVariableCubes(Fsm_Fsm_t *fsm); static int nameCompare(const void * name1, const void * name2); static boolean VarIdArrayCompare(mdd_manager *mddMgr, array_t *vars1, array_t *vars2); static boolean NSFunctionNamesCompare(mdd_manager *mddMgr, array_t *names1, array_t *names2); static array_t * GetMddSupportIdArray(Fsm_Fsm_t *fsm, st_table *mddIdTable, st_table *pseudoMddIdTable); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Creates an FSM from a network.] Description [Creates an FSM from a network and a partition. The FSM is initialized to the single fairness constraint TRUE, indicating that all states are "accepting". Reachability information, fair states, and imageInfo, are initialized to NIL, since these items are computed on demand. If the network has no latches, then NULL is returned and a message is written to error_string.

The partition gives the MVFs defining the next state functions of the network. If the partition is NULL, then a duplicate of the default partition of the network (found using Part_NetworkReadPartition) is used. If the network has no default partition, then NULL is returned and a message is written to error_string. Having the partition as a parameter gives the calling application the flexibility of using a different partition from the default, possibly one representing different functions than those given by the network (say for the purpose of computing approximations). However, it is assumed (though not checked), that the partition has the same combinational input variables and next state function names as the network. Finally, note that the given partition will be freed when the FSM is freed.] SideEffects [] SeeAlso [Fsm_FsmFree] ******************************************************************************/ Fsm_Fsm_t * Fsm_FsmCreateFromNetworkWithPartition( Ntk_Network_t *network, graph_t *partition) { lsGen gen; Ntk_Node_t *latch; Ntk_Node_t *input; Fsm_Fsm_t *fsm; int i; fsm = FsmStructAlloc(network, partition); if (fsm == NIL(Fsm_Fsm_t)) return NIL(Fsm_Fsm_t); fsm->fairnessInfo.constraint = FsmFsmCreateDefaultFairnessConstraint(fsm); /* sort by name of latch */ Ntk_NetworkForEachLatch(network, gen, latch){ array_insert_last(char*, fsm->fsmData.nextStateFunctions, Ntk_NodeReadName(latch)); } array_sort(fsm->fsmData.nextStateFunctions, nameCompare); for (i = 0; i < array_n(fsm->fsmData.nextStateFunctions); i ++) { char *nodeName; nodeName = array_fetch(char *, fsm->fsmData.nextStateFunctions, i); latch = Ntk_NetworkFindNodeByName(network, nodeName); array_insert(char*, fsm->fsmData.nextStateFunctions, i, Ntk_NodeReadName(Ntk_LatchReadDataInput(latch))); array_insert_last(int, fsm->fsmData.presentStateVars, Ntk_NodeReadMddId(latch)); array_insert_last(int, fsm->fsmData.nextStateVars, Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch))); } Ntk_NetworkForEachInput(network, gen, input){ array_insert_last(int, fsm->fsmData.inputVars, Ntk_NodeReadMddId(input)); } FsmCreateVariableCubes(fsm); return (fsm); } /**Function******************************************************************** Synopsis [Creates a FSM given the set of latches and the inputs.] Description [This function is primarily used to create a "reduced" FSM specific to a particular property during model checking. The given array of latches and inputs are associated with the FSM. If partition is NIL, the default partition from network is obtained. This partition will be used to obtain the next state functions of the latches. The last argument is an arry of fairness constraints which is used to restrict the reduced fsm to fair paths.

For a detailed desription of various fields of FSM, please refer to the function Fsm_FsmCreateFromNetworkWithPartition.] SideEffects [] SeeAlso [Fsm_FsmFree Fsm_FsmCreateFromNetworkWithPartition] ******************************************************************************/ Fsm_Fsm_t * Fsm_FsmCreateReducedFsm( Ntk_Network_t *network, graph_t *partition, array_t *latches, array_t *inputs, array_t *fairArray) { Ntk_Node_t *latch; Ntk_Node_t *input; Fsm_Fsm_t *fsm; Fsm_Fairness_t *fairness; int i,j; if (array_n(latches) == 0){ error_append("Number of latches passed = 0. Cannot create sub-FSM."); return (NIL(Fsm_Fsm_t)); } fsm = FsmStructAlloc(network, partition); if (fsm == NIL(Fsm_Fsm_t)) return NIL(Fsm_Fsm_t); /* initialize fairness constraints */ if (fairArray != NIL(array_t)){ fairness = FsmFairnessAlloc(fsm); for (j = 0; j < array_n(fairArray); j++) { Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, fairArray, j); FsmFairnessAddConjunct(fairness, formula, NIL(Ctlp_Formula_t), 0, j); } fsm->fairnessInfo.constraint = fairness; } else { fsm->fairnessInfo.constraint = FsmFsmCreateDefaultFairnessConstraint(fsm); } /* sort latches by name */ for(i=0; ifsmData.nextStateFunctions, Ntk_NodeReadName(latch)); } array_sort(fsm->fsmData.nextStateFunctions, nameCompare); for(i=0; ifsmData.nextStateFunctions, i); latch = Ntk_NetworkFindNodeByName(network, nodeName); array_insert_last(int, fsm->fsmData.presentStateVars, Ntk_NodeReadMddId(latch)); array_insert_last(int, fsm->fsmData.nextStateVars, Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch))); array_insert(char*, fsm->fsmData.nextStateFunctions, i, Ntk_NodeReadName(Ntk_LatchReadDataInput(latch))); } for(i=0; ifsmData.inputVars, Ntk_NodeReadMddId(input)); } FsmCreateVariableCubes(fsm); return (fsm); } /**Function******************************************************************** Synopsis [Creates a FSM given the set of latches and the inputs.] Description [This function is primarily used to create an "abstract" FSM specific to a particular property during invariant checking with abstraction refinement method Grab. The given array of latches and inputs are associated with the FSM. the array of invisible latches can be treated either as inputs (independentFlag==TRUE), or as latches (independentFlag==FALSE). It is the user's responsibility to make sure that latches, invisibleVars, and inputs are mutually disjoint. When independentFlag==TRUE, the FSM is defined by the pair (fsmData.presentStateVars, fsmData.inputVars); when independentFlag==FALSE, the FSM is defined by the pair (fsmData.globalPsVars, fsmData.primaryInputVars). For more information, please check the function Fsm_FsmReadOrCreateImageInfo(). The two pairs are defined as follows: presentStateVars inputVars globalPsVars primaryInputVars ----------------------------------------------------------------------- absLatches | X X invisibleVars| X X inputs | X X ----------------------------------------------------------------------- If partition is NIL, the default partition from network is obtained. This partition will be used to obtain the next state functions of the latches. The last argument is an arry of fairness constraints which is used to restrict the reduced fsm to fair paths.

For a detailed desription of various fields of FSM, please refer to the function Fsm_FsmCreateFromNetworkWithPartition.] SideEffects [] SeeAlso [Fsm_FsmFree Fsm_FsmCreateReducedFsm] ******************************************************************************/ Fsm_Fsm_t * Fsm_FsmCreateAbstractFsm( Ntk_Network_t *network, graph_t *partition, array_t *latches, array_t *invisibleVars, array_t *inputs, array_t *fairArray, boolean independentFlag) { Ntk_Node_t *latch; Ntk_Node_t *input; Ntk_Node_t *node; Fsm_Fsm_t *fsm; Fsm_Fairness_t *fairness; int i,j; if (FALSE && array_n(latches) == 0){ error_append("Number of latches passed = 0. Cannot create sub-FSM."); return (NIL(Fsm_Fsm_t)); } fsm = FsmStructAlloc(network, partition); if (fsm == NIL(Fsm_Fsm_t)) return NIL(Fsm_Fsm_t); /* initialize fairness constraints */ if (fairArray != NIL(array_t)){ fairness = FsmFairnessAlloc(fsm); for (j = 0; j < array_n(fairArray); j++) { Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, fairArray, j); FsmFairnessAddConjunct(fairness, formula, NIL(Ctlp_Formula_t), 0, j); } fsm->fairnessInfo.constraint = fairness; } else { fsm->fairnessInfo.constraint = FsmFsmCreateDefaultFairnessConstraint(fsm); } /* when independentFlag==FALSE, use globalPsVars and * primaryInputVars (instead of presentStateVars and inputVars) to * build the transition relation */ if (!independentFlag) { fsm->fsmData.globalPsVars = array_alloc(int, 0); fsm->fsmData.primaryInputVars = array_alloc(int, 0); } /* sort latches by name */ for(i=0; ifsmData.nextStateFunctions, Ntk_NodeReadName(latch)); } array_sort(fsm->fsmData.nextStateFunctions, nameCompare); for(i=0; ifsmData.nextStateFunctions, i); latch = Ntk_NetworkFindNodeByName(network, nodeName); array_insert_last(int, fsm->fsmData.presentStateVars, Ntk_NodeReadMddId(latch)); array_insert_last(int, fsm->fsmData.nextStateVars, Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch))); array_insert(char*, fsm->fsmData.nextStateFunctions, i, Ntk_NodeReadName(Ntk_LatchReadDataInput(latch))); if (!independentFlag) array_insert_last(int, fsm->fsmData.globalPsVars, Ntk_NodeReadMddId(latch)); } for(i=0; ifsmData.inputVars, Ntk_NodeReadMddId(input)); if (!independentFlag) array_insert_last(int, fsm->fsmData.primaryInputVars, Ntk_NodeReadMddId(input)); } arrayForEachItem(Ntk_Node_t *, invisibleVars, i, node) { array_insert_last(int, fsm->fsmData.inputVars, Ntk_NodeReadMddId(node)); if (!independentFlag) { array_insert_last(int, fsm->fsmData.globalPsVars, Ntk_NodeReadMddId(node)); } } FsmCreateVariableCubes(fsm); return (fsm); } /**Function******************************************************************** Synopsis [Frees the memory associated with an FSM.] Description [Frees the memory associated with an FSM. In particular, frees all the MDDs, and frees the associated partition. The FSM's corresponding network is not modified in any way.] SideEffects [] SeeAlso [Fsm_FsmCreateFromNetwork] ******************************************************************************/ void Fsm_FsmFree( Fsm_Fsm_t * fsm) { Part_PartitionFree(fsm->partition); Fsm_FsmSubsystemFree(fsm); } /**Function******************************************************************** Synopsis [Frees the memory associated with an FSM.] Description [Identical to Fsm_FsmFree() but does not free the partition.] SideEffects [] SeeAlso [Fsm_FsmCreateSubsystemFromNetwork] ******************************************************************************/ void Fsm_FsmSubsystemFree( Fsm_Fsm_t * fsm) { Fsm_FsmFreeImageInfo(fsm); /* Free reachability info. */ if (fsm->reachabilityInfo.initialStates != NIL(mdd_t)){ mdd_free(fsm->reachabilityInfo.initialStates); } if (fsm->reachabilityInfo.reachableStates != NIL(mdd_t)){ mdd_free(fsm->reachabilityInfo.reachableStates); } if (fsm->reachabilityInfo.apprReachableStates != NIL(array_t)) mdd_array_free(fsm->reachabilityInfo.apprReachableStates); if (fsm->reachabilityInfo.subPsVars != NIL(array_t)){ int i; array_t *psVars; arrayForEachItem(array_t *, fsm->reachabilityInfo.subPsVars, i, psVars) { array_free(psVars); } array_free(fsm->reachabilityInfo.subPsVars); } if (Fsm_FsmReadReachabilityOnionRings(fsm) != NIL(array_t)){ mdd_array_free(Fsm_FsmReadReachabilityOnionRings(fsm)); } /* Free fairness info. */ FsmFsmFairnessInfoUpdate(fsm, NIL(mdd_t), NIL(Fsm_Fairness_t), NIL(array_t)); array_free(fsm->fsmData.presentStateVars); array_free(fsm->fsmData.nextStateVars); array_free(fsm->fsmData.inputVars); array_free(fsm->fsmData.nextStateFunctions); if (fsm->fsmData.pseudoInputVars) array_free(fsm->fsmData.pseudoInputVars); if (fsm->fsmData.primaryInputVars) array_free(fsm->fsmData.primaryInputVars); if (fsm->fsmData.globalPsVars) array_free(fsm->fsmData.globalPsVars); if (fsm->fsmData.presentStateCube) mdd_free(fsm->fsmData.presentStateCube); if (fsm->fsmData.nextStateCube) mdd_free(fsm->fsmData.nextStateCube); if (fsm->fsmData.inputCube) mdd_free(fsm->fsmData.inputCube); if (fsm->fsmData.pseudoInputCube) mdd_free(fsm->fsmData.pseudoInputCube); if (fsm->fsmData.primaryInputCube) mdd_free(fsm->fsmData.primaryInputCube); if (fsm->fsmData.globalPsCube) mdd_free(fsm->fsmData.globalPsCube); if (fsm->fsmData.pseudoInputBddVars) mdd_array_free(fsm->fsmData.pseudoInputBddVars); if (fsm->fsmData.presentStateBddVars) mdd_array_free(fsm->fsmData.presentStateBddVars); FREE(fsm); } /**Function******************************************************************** Synopsis [Callback function to free an FSM.] Description [Typecasts data to (Fsm_Fsm_t *) and then calls Fsm_FsmFree. This function should only be used as a callback for other applications that don't know the FSM type, for example the network ApplInfoTable.] SideEffects [] SeeAlso [Fsm_FsmFree] ******************************************************************************/ void Fsm_FsmFreeCallback( void * data /* an object of type Fsm_Fsm_t* type casted to void* */) { Fsm_FsmFree((Fsm_Fsm_t *) data); } /**Function******************************************************************** Synopsis [Returns the corresponding network of an FSM.] SideEffects [] SeeAlso [Fsm_FsmCreateFromNetwork] ******************************************************************************/ Ntk_Network_t * Fsm_FsmReadNetwork( Fsm_Fsm_t * fsm) { return (fsm->network); } /**Function******************************************************************** Synopsis [Read UnquantifiedFlag of an FSM.] Description [This is function for FateAndFreeWill counterexample generation.] SideEffects [] SeeAlso [Fsm_FsmCreateFromNetwork] ******************************************************************************/ boolean Fsm_FsmReadUseUnquantifiedFlag( Fsm_Fsm_t * fsm) { return (fsm->useUnquantifiedFlag); } /**Function******************************************************************** Synopsis [Returns the MDD manager of the corresponding network of an FSM.] SideEffects [] SeeAlso [Fsm_FsmCreateFromNetwork] ******************************************************************************/ mdd_manager * Fsm_FsmReadMddManager( Fsm_Fsm_t * fsm) { return (Ntk_NetworkReadMddManager(fsm->network)); } /**Function******************************************************************** Synopsis [Returns the FSM of a network; creates FSM if necessary.] Description [If there is an FSM associated with network, then returns it. Otherwise, creates an FSM from network (using a duplicate of the partition associated with the network), registers the FSM with the network, and then returns the newly created FSM. Note that if the network has no latches or the network has no partition, then a NULL FSM is returned.] SideEffects [] SeeAlso [Fsm_FsmCreateFromNetwork Ntk_NetworkReadApplInfo Fsm_NetworkReadFsm] ******************************************************************************/ Fsm_Fsm_t * Fsm_NetworkReadOrCreateFsm( Ntk_Network_t * network) { Fsm_Fsm_t *fsm = (Fsm_Fsm_t*) Ntk_NetworkReadApplInfo(network, FSM_NETWORK_APPL_KEY); if (fsm == NIL(Fsm_Fsm_t)) { fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t)); if (fsm != NIL(Fsm_Fsm_t)) { (void) Ntk_NetworkAddApplInfo(network, FSM_NETWORK_APPL_KEY, (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback, (void *) fsm); } } return fsm; } /**Function******************************************************************** Synopsis [Returns the FSM of a network.] Description [Returns the FSM of a network, which may be NULL.] SideEffects [] SeeAlso [Fsm_FsmCreateFromNetwork Ntk_NetworkReadApplInfo Fsm_NetworkReadOrCreateFsm] ******************************************************************************/ Fsm_Fsm_t * Fsm_NetworkReadFsm( Ntk_Network_t * network) { return ((Fsm_Fsm_t*) Ntk_NetworkReadApplInfo(network, FSM_NETWORK_APPL_KEY)); } /**Function******************************************************************** Synopsis [Returns the imageInfo struct stored by the FSM.] Description [Returns the imageInfo struct stored by the FSM, which may be NULL.] SideEffects [] SeeAlso [Img_ImageInfoInitialize Fsm_FsmReadOrCreateImageInfo] ******************************************************************************/ Img_ImageInfo_t * Fsm_FsmReadImageInfo( Fsm_Fsm_t *fsm) { return (fsm->imageInfo); } /**Function******************************************************************** Synopsis [Set the imageInfo.] Description [Set the imageInfo. ] SideEffects [] SeeAlso [Img_ImageInfoInitialize Fsm_FsmReadOrCreateImageInfo] ******************************************************************************/ void Fsm_FsmSetImageInfo( Fsm_Fsm_t *fsm, Img_ImageInfo_t *imageInfo) { fsm->imageInfo = imageInfo; } /**Function******************************************************************** Synopsis [Returns the imageInfo struct stored by the FSM.] Description [Returns the imageInfo struct stored by the FSM, which may be NULL.] SideEffects [] SeeAlso [Img_ImageInfoInitialize Fsm_FsmReadOrCreateImageInfo] ******************************************************************************/ void Fsm_FsmFreeImageInfo( Fsm_Fsm_t *fsm) { if(fsm->imageInfo) { Img_ImageInfoFree(fsm->imageInfo); fsm->imageInfo = NIL(Img_ImageInfo_t); } if(fsm->unquantifiedImageInfo) { Img_ImageInfoFree(fsm->unquantifiedImageInfo); fsm->unquantifiedImageInfo = NIL(Img_ImageInfo_t); } } /**Function******************************************************************** Synopsis [Returns the partition associated with the FSM.] Description [Returns the partition associated with the FSM. This is the graph of MVFs defining the combinational output functions of the FSM.] SideEffects [] SeeAlso [Fsm_FsmCreateFromNetwork] ******************************************************************************/ graph_t * Fsm_FsmReadPartition( Fsm_Fsm_t *fsm) { return (fsm->partition); } /**Function******************************************************************** Synopsis [Test if reachability has been performed on the FSM.] Description [Return TRUE if reachability has already been performed, else FALSE.] SideEffects [] SeeAlso [Fsm_FsmComputeReachableStates] ******************************************************************************/ boolean Fsm_FsmTestIsReachabilityDone( Fsm_Fsm_t *fsm) { if (Fsm_FsmReadReachableStates(fsm) != NIL(mdd_t)) { return TRUE; } return FALSE; } /**Function******************************************************************** Synopsis [Test if approximate reachability has been performed on the FSM.] Description [Return TRUE if approximate reachability has already been performed, else FALSE.] SideEffects [] SeeAlso [Fsm_FsmComputeReachableStates] ******************************************************************************/ boolean Fsm_FsmTestIsOverApproximateReachabilityDone( Fsm_Fsm_t *fsm) { if (Fsm_FsmReadOverApproximateReachableStates(fsm) != NIL(array_t)) { return TRUE; } return FALSE; } /**Function******************************************************************** Synopsis [Returns the reachable states of an FSM.] SideEffects [Returns the reachable states of an FSM.] SeeAlso [Fsm_FsmComputeReachableStates] ******************************************************************************/ mdd_t * Fsm_FsmReadReachableStates( Fsm_Fsm_t *fsm) { if (fsm->reachabilityInfo.rchStatus == Fsm_Rch_Exact_c) return(fsm->reachabilityInfo.reachableStates); else return(NIL(mdd_t)); } /**Function******************************************************************** Synopsis [Returns the reachable states of an FSM.] SideEffects [Returns the reachable states of an FSM. May be an under approximation or an over approximation.] SeeAlso [Fsm_FsmComputeReachableStates] ******************************************************************************/ mdd_t * Fsm_FsmReadCurrentReachableStates( Fsm_Fsm_t *fsm) { return(fsm->reachabilityInfo.reachableStates); } /**Function******************************************************************** Synopsis [Returns the approximate reachable states of an FSM.] SideEffects [] SeeAlso [Fsm_ArdcComputeOverApproximateReachableStates] ******************************************************************************/ array_t * Fsm_FsmReadOverApproximateReachableStates( Fsm_Fsm_t *fsm) { if (fsm->reachabilityInfo.overApprox >= 2) return(fsm->reachabilityInfo.apprReachableStates); else return(NIL(array_t)); } /**Function******************************************************************** Synopsis [Returns the current approximate reachable states of an FSM.] SideEffects [] SeeAlso [Fsm_ArdcComputeOverApproximateReachableStates] ******************************************************************************/ array_t * Fsm_FsmReadCurrentOverApproximateReachableStates( Fsm_Fsm_t *fsm) { return(fsm->reachabilityInfo.apprReachableStates); } /**Function******************************************************************** Synopsis [Return array of onion rings from reachability computation] Description [Return array of onion rings from reachability computation; NIL if reachability has not been performed. DO NOT free this array.] SideEffects [] SeeAlso [Fsm_FsmComputeReachableStates] ******************************************************************************/ array_t * Fsm_FsmReadReachabilityOnionRings( Fsm_Fsm_t *fsm) { return fsm->reachabilityInfo.onionRings; } /**Function******************************************************************** Synopsis [Checks whether the onion rings are consistent with the reachable states.] Description [Checks whether the onion rings are consistent with the reachable states. Returns FALSE if no states in onion rings.] SideEffects [result is set to the union of the onion rings] SeeAlso [Fsm_FsmbtainBFSShells] ******************************************************************************/ boolean Fsm_FsmReachabilityOnionRingsStates( Fsm_Fsm_t *fsm, mdd_t ** result) { int i; mdd_t *tmpMdd; mdd_t *ring; array_t *onionRings; onionRings = Fsm_FsmReadReachabilityOnionRings(fsm); if ( onionRings == NIL(array_t) ) { *result = NIL(mdd_t); return 0; } *result = bdd_zero(Fsm_FsmReadMddManager(fsm)); arrayForEachItem(mdd_t *, onionRings, i, ring) { tmpMdd = mdd_or(*result, ring, 1, 1); mdd_free(*result); *result = tmpMdd; } if (Fsm_FsmReadCurrentReachableStates(fsm)) { if (mdd_lequal(Fsm_FsmReadCurrentReachableStates(fsm), *result, 1,1)) { FsmSetReachabilityOnionRingsUpToDateFlag(fsm, TRUE); } } return (Fsm_FsmTestReachabilityOnionRingsUpToDate(fsm)); } /**Function******************************************************************** Synopsis [Checks if the onion rings are consistent with the reachable states.] Description [Checks if the onion rings are consistent with the reachable states.] SideEffects [] SeeAlso [Fsm_FsmComputeReachableStates] ******************************************************************************/ boolean Fsm_FsmTestReachabilityOnionRingsUpToDate( Fsm_Fsm_t *fsm) { return fsm->reachabilityInfo.onionRingsUpToDate; } /**Function******************************************************************** Synopsis [Checks if the onion rings are due to BFS or not.] Description [Checks if the onion rings are due to BFS or not.] SideEffects [] SeeAlso [Fsm_FsmComputeReachableStates] ******************************************************************************/ Fsm_RchType_t Fsm_FsmReadReachabilityOnionRingsMode( Fsm_Fsm_t *fsm) { return fsm->reachabilityInfo.onionRingsMode; } /**Function******************************************************************** Synopsis [Returns the imageInfo struct stored by the FSM; creates if necessary.] Description [Returns the imageInfo struct stored by the FSM. If one doesn't currently exist in the FSM, then one is initialized and set, before it is returned. The imageInfo is initialized using the default image method, and is initialized for both forward and backward image computations. It uses the partition with which this FSM was created when the function Fsm_FsmCreateFromNetwork was called.] SideEffects [] SeeAlso [Img_ImageInfoInitialize Fsm_FsmReadImageInfo] ******************************************************************************/ Img_ImageInfo_t * Fsm_FsmReadOrCreateImageInfo(Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag) { Img_DirectionType imgFlag = Img_Forward_c; array_t *presentStateVars, *inputVars; mdd_t *presentStateCube, *inputCube; if (bwdImgFlag && fwdImgFlag) imgFlag = Img_Both_c; else if (bwdImgFlag) imgFlag = Img_Backward_c; if (fsm->fsmData.globalPsVars) { presentStateVars = fsm->fsmData.globalPsVars; inputVars = fsm->fsmData.primaryInputVars; presentStateCube = fsm->fsmData.globalPsCube; inputCube = fsm->fsmData.primaryInputCube; } else { presentStateVars = fsm->fsmData.presentStateVars; inputVars = fsm->fsmData.inputVars; presentStateCube = fsm->fsmData.presentStateCube; inputCube = fsm->fsmData.inputCube; } fsm->imageInfo = Img_ImageInfoInitialize(fsm->imageInfo, fsm->partition, fsm->fsmData.nextStateFunctions, presentStateVars, fsm->fsmData.nextStateVars, inputVars, presentStateCube, fsm->fsmData.nextStateCube, inputCube, fsm->network, Img_Default_c, imgFlag, 0, 0); if (fsm->fsmData.globalPsVars) { Img_ImageInfoUpdateVariables(fsm->imageInfo, fsm->partition, fsm->fsmData.presentStateVars, fsm->fsmData.inputVars, fsm->fsmData.presentStateCube, fsm->fsmData.inputCube); } return(fsm->imageInfo); } /**Function******************************************************************** Synopsis [Returns the imageInfo struct stored by the FSM; creates if necessary.] Description [Returns the imageInfo struct stored by the FSM. If one doesn't currently exist in the FSM, then one is initialized and set, before it is returned. The imageInfo is initialized using the default image method, and is initialized for both forward and backward image computations. It uses the partition with which this FSM was created when the function Fsm_FsmCreateFromNetwork was called. In this function we create the ImageInfo that has no quntified input for Fate and Free will.] SideEffects [] SeeAlso [Img_ImageInfoInitialize Fsm_FsmReadImageInfo] ******************************************************************************/ Img_ImageInfo_t * Fsm_FsmReadOrCreateImageInfoFAFW(Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag) { Img_DirectionType imgFlag = Img_Forward_c; array_t *presentStateVars, *inputVars; mdd_t *presentStateCube, *inputCube; mdd_manager *mgr; mgr = Fsm_FsmReadMddManager(fsm); if (bwdImgFlag && fwdImgFlag) imgFlag = Img_Both_c; else if (bwdImgFlag) imgFlag = Img_Backward_c; presentStateVars = fsm->fsmData.presentStateVars; inputVars = array_alloc(int , 0); presentStateCube = fsm->fsmData.presentStateCube; inputCube = mdd_one(mgr); fsm->unquantifiedImageInfo = Img_ImageInfoInitialize( fsm->unquantifiedImageInfo, fsm->partition, fsm->fsmData.nextStateFunctions, presentStateVars, fsm->fsmData.nextStateVars, inputVars, presentStateCube, fsm->fsmData.nextStateCube, inputCube, fsm->network, Img_Default_c, imgFlag, 1, 0); if(!Img_IsQuantifyArraySame(fsm->unquantifiedImageInfo, inputVars)) { array_free(inputVars); } if(!Img_IsQuantifyCubeSame(fsm->unquantifiedImageInfo, inputCube)) { mdd_free(inputCube); } return(fsm->unquantifiedImageInfo); } /**Function******************************************************************** Synopsis [Returns the imageInfo struct stored by the FSM; creates if necessary.] Description [Returns the imageInfo struct stored by the FSM. If one doesn't currently exist in the FSM, then one is initialized and set, before it is returned. The imageInfo is initialized using the default image method, and is initialized for both forward and backward image computations. It uses the partition with which this FSM was created when the function Fsm_FsmCreateFromNetwork was called. In this function we create the ImageInfo that has no quntified input for Fate and Free will.] SideEffects [] SeeAlso [Img_ImageInfoInitialize Fsm_FsmReadImageInfo] ******************************************************************************/ Img_ImageInfo_t * Fsm_FsmReadOrCreateImageInfoPrunedFAFW(Fsm_Fsm_t *fsm, mdd_t *Winning, int bwdImgFlag, int fwdImgFlag) { Img_DirectionType imgFlag = Img_Forward_c; array_t *presentStateVars, *inputVars; mdd_t *presentStateCube, *inputCube; mdd_manager *mgr; Img_ImageInfo_t *imageInfo; mgr = Fsm_FsmReadMddManager(fsm); if (bwdImgFlag && fwdImgFlag) imgFlag = Img_Both_c; else if (bwdImgFlag) imgFlag = Img_Backward_c; presentStateVars = fsm->fsmData.presentStateVars; inputVars = array_alloc(int , 0); presentStateCube = fsm->fsmData.presentStateCube; inputCube = mdd_one(mgr); imageInfo = Img_ImageInfoInitialize( 0, fsm->partition, fsm->fsmData.nextStateFunctions, presentStateVars, fsm->fsmData.nextStateVars, inputVars, presentStateCube, fsm->fsmData.nextStateCube, inputCube, fsm->network, Img_Default_c, imgFlag, 0, Winning); if(!Img_IsQuantifyArraySame(imageInfo, inputVars)) { array_free(inputVars); } if(!Img_IsQuantifyCubeSame(imageInfo, inputCube)) { mdd_free(inputCube); } return(imageInfo); } /**Function******************************************************************** Synopsis [Returns the imageInfo struct stored by the FSM; creates if necessary.] Description [Returns the imageInfo struct stored by the FSM. If one doesn't currently exist in the FSM, then one is initialized and set, before it is returned. The imageInfo is initialized using the default image method, and is initialized for both forward and backward image computations. It uses the partition with which this FSM was created when the function Fsm_FsmCreateFromNetwork was called. In this function we create the ImageInfo that has no quntified input for Fate and Free will.] SideEffects [] SeeAlso [Img_ImageInfoInitialize Fsm_FsmReadImageInfo] ******************************************************************************/ Img_ImageInfo_t * Fsm_FsmReadOrCreateImageInfoForComputingRange(Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag) { Img_DirectionType imgFlag = Img_Forward_c; array_t *presentStateVars, *inputVars; mdd_t *presentStateCube, *inputCube; if (bwdImgFlag && fwdImgFlag) imgFlag = Img_Both_c; else if (bwdImgFlag) imgFlag = Img_Backward_c; if (fsm->fsmData.globalPsVars) { presentStateVars = fsm->fsmData.globalPsVars; inputVars = fsm->fsmData.primaryInputVars; presentStateCube = fsm->fsmData.globalPsCube; inputCube = fsm->fsmData.primaryInputCube; } else { presentStateVars = fsm->fsmData.presentStateVars; inputVars = fsm->fsmData.inputVars; presentStateCube = fsm->fsmData.presentStateCube; inputCube = fsm->fsmData.inputCube; } fsm->imageInfo = Img_ImageInfoInitialize(fsm->imageInfo, fsm->partition, fsm->fsmData.nextStateFunctions, presentStateVars, fsm->fsmData.nextStateVars, inputVars, presentStateCube, fsm->fsmData.nextStateCube, inputCube, fsm->network, Img_Linear_Range_c, imgFlag, 0, 0); if (fsm->fsmData.globalPsVars) { Img_ImageInfoUpdateVariables(fsm->imageInfo, fsm->partition, fsm->fsmData.presentStateVars, fsm->fsmData.inputVars, fsm->fsmData.presentStateCube, fsm->fsmData.inputCube); } return(fsm->imageInfo); } /**Function******************************************************************** Synopsis [Computes the set of initial states of an FSM.] Description [Computes the set of initial states of an FSM. If this set has already been computed, then just returns the result of the previous computation. The calling application is responsible for freeing the returned MDD in all cases.

The nodes driving the initial inputs of the latches, called the initial nodes, must not have latches in their support. If an initial node is found that has a latch in its transitive fanin, then a NULL MDD is returned, and a message is written to the error_string.

The initial states are computed as follows. For each latch i, the relation (x_i = g_i(u)) is built, where x_i is the present state variable of latch i, and g_i(u) is the multi-valued initialization function of latch i, in terms of the input variables u. These relations are then conjuncted, and the input variables are existentially quantified from the result (i.e. init_states(x) = \exists u \[\prod (x_i = g_i(u))\]).] SideEffects [The result of the initial state computation is stored with the FSM.] SeeAlso [Fsm_FsmComputeReachableStates] ******************************************************************************/ mdd_t * Fsm_FsmComputeInitialStates(Fsm_Fsm_t *fsm) { int i = 0; lsGen gen; mdd_t *initStates; Ntk_Node_t *node; array_t *initRelnArray; array_t *initMvfs; array_t *initNodes; array_t *initVertices; array_t *latchMddIds; st_table *supportNodes; st_table *supportVertices; mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); graph_t *partition = fsm->partition; Ntk_Network_t *network = fsm->network; int numLatches; array_t *psVars; Img_MethodType imageMethod; /* If already computed, just return a copy. */ if (fsm->reachabilityInfo.initialStates != NIL(mdd_t)){ return (mdd_dup(fsm->reachabilityInfo.initialStates)); } psVars = fsm->fsmData.presentStateVars; numLatches = array_n(psVars); /* * Get the array of initial nodes, both as network nodes and as partition * vertices. */ initNodes = array_alloc(Ntk_Node_t *, numLatches); initVertices = array_alloc(vertex_t *, numLatches); latchMddIds = array_alloc(int, numLatches); for (i=0; ifsmData.inputVars); */ imageMethod = Img_UserSpecifiedMethod(); if (imageMethod != Img_Iwls95_c && imageMethod != Img_Mlp_c) imageMethod = Img_Iwls95_c; initStates = Img_MultiwayLinearAndSmooth(mddManager, initRelnArray, fsm->fsmData.inputVars, psVars, imageMethod, Img_Forward_c); mdd_array_free(initRelnArray); fsm->reachabilityInfo.initialStates = initStates; return mdd_dup(initStates); } /**Function******************************************************************** Synopsis [Returns the array of MDD ids of the present state variables of an FSM.] Description [Returns the array of MDD ids of the present state variables of an FSM. This array should not be modified or freed in any way.] SideEffects [] SeeAlso [Fsm_FsmReadNextStateVars Fsm_FsmReadInputVars Fsm_FsmReadNextStateFunctionNames] ******************************************************************************/ array_t * Fsm_FsmReadPresentStateVars(Fsm_Fsm_t *fsm) { return fsm->fsmData.presentStateVars; } /**Function******************************************************************** Synopsis [Returns the array of MDD ids of the next state variables of an FSM.] Description [Returns the array of MDD ids of the next state variables of an FSM. This array should not be modified or freed in any way.] SideEffects [] SeeAlso [Fsm_FsmReadPresentStateVars Fsm_FsmReadInputVars Fsm_FsmReadNextStateFunctionNames] ******************************************************************************/ array_t * Fsm_FsmReadNextStateVars(Fsm_Fsm_t *fsm) { return fsm->fsmData.nextStateVars; } /**Function******************************************************************** Synopsis [Returns an array of strings containing the names of the nodes driving the data inputs of the latches.] Description [Returns the array of strings containing the names of the nodes driving the data inputs of the latches. This array should not be modified or freed in any way.] SideEffects [] SeeAlso [Fsm_FsmReadPresentStateVars Fsm_FsmReadNextStateVars Fsm_FsmReadInputVars] ******************************************************************************/ array_t * Fsm_FsmReadNextStateFunctionNames(Fsm_Fsm_t *fsm) { return fsm->fsmData.nextStateFunctions; } /**Function******************************************************************** Synopsis [Returns the array of MDD ids of the input variables of an FSM.] Description [Returns the array of MDD ids of the input variables of an FSM. This includes both primary inputs and pseudo inputs. This array should not be modified or freed in any way.] SideEffects [] SeeAlso [Fsm_FsmReadPresentStateVars Fsm_FsmReadNextStateVars Fsm_FsmReadNextStateFunctionNames] ******************************************************************************/ array_t * Fsm_FsmReadInputVars(Fsm_Fsm_t *fsm) { return fsm->fsmData.inputVars; } array_t * Fsm_FsmReadPrimaryInputVars(Fsm_Fsm_t *fsm) { return fsm->fsmData.primaryInputVars; } /**Function******************************************************************** Synopsis [Returns the array of MDD ids of the pseudo input variables of a sub FSM.] Description [Returns the array of MDD ids of the pseudo input variables of a sub FSM. This array should not be modified or freed in any way.] SideEffects [] SeeAlso [Fsm_FsmReadNextStateVars Fsm_FsmReadInputVars Fsm_FsmReadNextStateFunctionNames] ******************************************************************************/ array_t * Fsm_FsmReadPseudoInputVars(Fsm_Fsm_t *fsm) { return fsm->fsmData.pseudoInputVars; } /**Function******************************************************************** Synopsis [Set input variables into the FSM structure.] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_FsmSetInputVars(Fsm_Fsm_t *fsm, array_t *inputVars) { fsm->fsmData.inputVars = inputVars; } /**Function******************************************************************** Synopsis [Set useUnquantifiedFlag into the FSM structure.] Description [This is function for FateAndFreeWill counterexample generation.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_FsmSetUseUnquantifiedFlag(Fsm_Fsm_t *fsm, boolean value) { fsm->useUnquantifiedFlag = value; } /**Function******************************************************************** Synopsis [Set the initial states of an FSM.] Description [] SideEffects [Old mdd_t representing the initial states is deleted and replaced by the argument provided.] SeeAlso [] ******************************************************************************/ void Fsm_FsmSetInitialStates(Fsm_Fsm_t *fsm, mdd_t *initStates) { mdd_t *init; init = fsm->reachabilityInfo.initialStates; if (init != NIL(mdd_t)) { mdd_free(init); } fsm->reachabilityInfo.initialStates = initStates; } /**Function******************************************************************** Synopsis [Read FAFWFlag from the FSM structure.] Description [This is function for FateAndFreeWill counterexample generation.] SideEffects [] SeeAlso [] ******************************************************************************/ int Fsm_FsmReadFAFWFlag(Fsm_Fsm_t *fsm) { return((int)(fsm->FAFWFlag)); } /**Function******************************************************************** Synopsis [Set FAFWFlag in the FSM structure.] Description [This is function for FateAndFreeWill counterexample generation.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_FsmSetFAFWFlag(Fsm_Fsm_t *fsm, boolean FAFWFlag) { fsm->FAFWFlag = FAFWFlag; } /**Function******************************************************************** Synopsis [Set input variables that are controlled by system and environment in the FSM structure.] Description [This is function for FateAndFreeWill counterexample generation.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_FsmSetSystemVariableFAFW(Fsm_Fsm_t *fsm, st_table *bddIdTable) { mdd_manager *mgr; array_t *inputVars, *bddIdArray; bdd_t *extCube, *uniCube; bdd_t *newCube, *varBdd; st_generator *gen; int mddId, bddId, tbddId, i, j; if(bddIdTable == 0 && fsm->FAFWFlag == 0) { if(fsm->extQuantifyInputCube) bdd_free(fsm->extQuantifyInputCube); if(fsm->uniQuantifyInputCube) bdd_free(fsm->uniQuantifyInputCube); fsm->extQuantifyInputCube = 0; fsm->uniQuantifyInputCube = 0; return; } mgr = Fsm_FsmReadMddManager(fsm); inputVars = Fsm_FsmReadInputVars(fsm); extCube = mdd_one(mgr); for(i=0; iextQuantifyInputCube = extCube; fsm->uniQuantifyInputCube = uniCube; } /**Function******************************************************************** Synopsis [Read input variables that is controlled by environment in the FSM structure.] Description [This is function for FateAndFreeWill counterexample generation.] SideEffects [] SeeAlso [] ******************************************************************************/ bdd_t * Fsm_FsmReadExtQuantifyInputCube(Fsm_Fsm_t *fsm) { return(fsm->extQuantifyInputCube); } /**Function******************************************************************** Synopsis [Read input variables that is controlled by system in the FSM structure.] Description [This is function for FateAndFreeWill counterexample generation.] SideEffects [] SeeAlso [] ******************************************************************************/ bdd_t * Fsm_FsmReadUniQuantifyInputCube(Fsm_Fsm_t *fsm) { return(fsm->uniQuantifyInputCube); } /**Function******************************************************************** Synopsis [Returns the current FSM of a hierarchy manager.] Description [Returns the FSM of the network of the current node of a hierarchy manager. If the 1) hmgr is NULL, 2) current node is NULL, 3) network is NULL, 4) the variables of the network have not been ordered, 5) a partition doesn't exist for the network, or 6) the network does not have any latches, then a message is printed to vis_stderr, and NULL is returned. If all the above conditions have been satisfied, and the network doesn't already have an FSM, then one is created.] SideEffects [] SeeAlso [Hrc_ManagerReadCurrentNode Ntk_HrcManagerReadCurrentNetwork Fsm_NetworkReadOrCreateFsm] ******************************************************************************/ Fsm_Fsm_t * Fsm_HrcManagerReadCurrentFsm(Hrc_Manager_t *hmgr) { Fsm_Fsm_t *fsm; Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(hmgr); if (network == NIL(Ntk_Network_t)) { return NIL(Fsm_Fsm_t); } if (Ord_NetworkTestAreVariablesOrdered(network, Ord_InputAndLatch_c) == FALSE) { (void) fprintf(vis_stderr, "** fsm error: The MDD variables have not been ordered. "); (void) fprintf(vis_stderr, "Use static_order.\n"); return NIL(Fsm_Fsm_t); } if (Part_NetworkReadPartition(network) == NIL(graph_t)){ (void) fprintf(vis_stderr, "** fsm error: Network has not been partitioned. "); (void) fprintf(vis_stderr, "Use build_partition_mdds.\n"); return NIL(Fsm_Fsm_t); } error_init(); fsm = Fsm_NetworkReadOrCreateFsm(network); if (fsm == NIL(Fsm_Fsm_t)) { (void) fprintf(vis_stderr, "%s", error_string()); (void) fprintf(vis_stderr, "\n"); } return fsm; } /**Function******************************************************************** Synopsis [Creates a subFSM from a network.] Description [Given a vertex table, the routine creates a subFSM. The routine reads in the vertex table and stores only corresponding next state functions into the subFSM. Every present, next state and input variables in the system are stored into the subFSM. ] SideEffects [] SeeAlso [Fsm_FsmCreateFromNetworkWithPartition, Fsm_FsmFree] ******************************************************************************/ Fsm_Fsm_t * Fsm_FsmCreateSubsystemFromNetwork( Ntk_Network_t *network, graph_t *partition, st_table *vertexTable, boolean independentFlag, int createPseudoVarMode) { lsGen gen; Ntk_Node_t *latch; Ntk_Node_t *input; Fsm_Fsm_t *fsm; char *latchName; int i; st_table *pseudoMddIdTable = NIL(st_table); fsm = FsmStructAlloc(network, partition); if (fsm == NIL(Fsm_Fsm_t)) return NIL(Fsm_Fsm_t); fsm->fairnessInfo.constraint = FsmFsmCreateDefaultFairnessConstraint(fsm); /* * Creates an FSM for the subsystem. */ /* sort latches by name. */ Ntk_NetworkForEachLatch(network, gen, latch) { latchName = Ntk_NodeReadName(latch); if(st_lookup(vertexTable, latchName, (char **)0)) { array_insert_last(char*, fsm->fsmData.nextStateFunctions, latchName); } /* end of if(st_lookup(vertexTable)) */ } if (independentFlag && createPseudoVarMode) { fsm->fsmData.pseudoInputVars = array_alloc(int, 0); fsm->fsmData.primaryInputVars = array_alloc(int, 0); fsm->fsmData.globalPsVars = array_alloc(int, 0); if (createPseudoVarMode == 2) pseudoMddIdTable = st_init_table(st_numcmp, st_numhash); } array_sort(fsm->fsmData.nextStateFunctions, nameCompare); arrayForEachItem(char *, fsm->fsmData.nextStateFunctions, i, latchName) { latch = Ntk_NetworkFindNodeByName(network, latchName); array_insert(char*, fsm->fsmData.nextStateFunctions, i, Ntk_NodeReadName(Ntk_LatchReadDataInput(latch))); array_insert_last(int, fsm->fsmData.nextStateVars, Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch))); array_insert_last(int, fsm->fsmData.presentStateVars, Ntk_NodeReadMddId(latch)); } /* end of Ntk_NetworkForEachLatch(network, gen, latch) */ /* Fill in remaining latch for nextStateVars */ if (!independentFlag || createPseudoVarMode) { Ntk_NetworkForEachLatch(network, gen, latch) { char *latchName = Ntk_NodeReadName(latch); if(!st_lookup(vertexTable, latchName, (char **)0)) { if (independentFlag) { if (createPseudoVarMode == 1) { array_insert_last(int, fsm->fsmData.pseudoInputVars, Ntk_NodeReadMddId(latch)); array_insert_last(int, fsm->fsmData.inputVars, Ntk_NodeReadMddId(latch)); } else { st_insert(pseudoMddIdTable, (char *)(long)Ntk_NodeReadMddId(latch), NIL(char)); } } else { array_insert_last(int, fsm->fsmData.nextStateVars, Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch))); array_insert_last(int, fsm->fsmData.presentStateVars, Ntk_NodeReadMddId(latch)); } } } } /* Input variables are identical for every subsystems */ Ntk_NetworkForEachInput(network, gen, input){ array_insert_last(int, fsm->fsmData.inputVars, Ntk_NodeReadMddId(input)); if (independentFlag && createPseudoVarMode) { array_insert_last(int, fsm->fsmData.primaryInputVars, Ntk_NodeReadMddId(input)); } } if (independentFlag && createPseudoVarMode) { if (createPseudoVarMode == 2) { int mddId; array_t *supportMddIdArray; st_table *mddIdTable; mddIdTable = st_init_table(st_numcmp, st_numhash); arrayForEachItem(int, fsm->fsmData.presentStateVars, i, mddId) { st_insert(mddIdTable, (char *)(long)mddId, NIL(char)); } arrayForEachItem(int, fsm->fsmData.inputVars, i, mddId) { st_insert(mddIdTable, (char *)(long)mddId, NIL(char)); } supportMddIdArray = GetMddSupportIdArray(fsm, mddIdTable, pseudoMddIdTable); arrayForEachItem(int, supportMddIdArray, i, mddId) { if (!st_lookup(mddIdTable, (char *)(long)mddId, NIL(char *))) { array_insert_last(int, fsm->fsmData.pseudoInputVars, mddId); array_insert_last(int, fsm->fsmData.inputVars, mddId); } } st_free_table(mddIdTable); st_free_table(pseudoMddIdTable); array_free(supportMddIdArray); } array_append(fsm->fsmData.globalPsVars, fsm->fsmData.presentStateVars); array_append(fsm->fsmData.globalPsVars, fsm->fsmData.pseudoInputVars); } FsmCreateVariableCubes(fsm); fsm->fsmData.presentStateBddVars = mdd_id_array_to_bdd_array( Fsm_FsmReadMddManager(fsm), fsm->fsmData.presentStateVars); return (fsm); } /**Function******************************************************************** Synopsis [Instantiate a given hint] Description [Instantiate a given hint. The fwd and bwd flags indicate whether the fwd transition relation or the backward transition relation is created. A non-zero value will cause the hint to be instantiated in that direction. The type flag indicates whether the hint should be applied as an overapproximation or an underapproximation. After minimization wrt the hint is done, the TR is minimized wrt the conjunction of the care states in careStatesArray (an array of mdd_t *), unless this array is NULL, in which case it is ignored.] SideEffects [] SeeAlso [Fsm_CleanUpHints] ******************************************************************************/ void Fsm_InstantiateHint( Fsm_Fsm_t *fsm, mdd_t *hint, int fwdFlag, int bwdFlag, Ctlp_Approx_t type, int printStatus) { boolean underApprox = FALSE; Img_DirectionType imgFlag = Img_Forward_c; assert(type != Ctlp_Incomparable_c); if (bwdFlag && fwdFlag) imgFlag = Img_Both_c; else if (bwdFlag) imgFlag = Img_Backward_c; switch (type) { case (Ctlp_Underapprox_c): underApprox = TRUE; break; case (Ctlp_Overapprox_c): underApprox = FALSE; break; case (Ctlp_Exact_c): underApprox = TRUE; hint = mdd_one(Fsm_FsmReadMddManager(fsm)); break; default: assert(0); break; } /* If we reach this point, underApprox has been explicitly assigned * by the switch. */ Img_ImageConstrainAndClusterTransitionRelation( Fsm_FsmReadOrCreateImageInfo(fsm, bwdFlag, fwdFlag), imgFlag, hint, ((underApprox == TRUE) ? Img_GuidedSearchReadUnderApproxMinimizeMethod() : Img_GuidedSearchReadOverApproxMinimizeMethod()), underApprox, /* underapprox */ 0, /* dont clean up */ 0, /* no variable reordering */ printStatus); Fsm_MinimizeTransitionRelationWithReachabilityInfo(fsm, imgFlag, printStatus); if (type == Ctlp_Exact_c) mdd_free(hint); return; } /**Function******************************************************************** Synopsis [Clean up after hints] Description [Clean up after hints.] SideEffects [] SeeAlso [Fsm_InstantiateHint] ******************************************************************************/ void Fsm_CleanUpHints( Fsm_Fsm_t *fsm, int fwdFlag, int bwdFlag, int printStatus) { Img_DirectionType imgFlag = Img_Forward_c; mdd_t *one = bdd_one(Fsm_FsmReadMddManager(fsm)); if (bwdFlag && fwdFlag) imgFlag = Img_Both_c; else if (bwdFlag) imgFlag = Img_Backward_c; Img_ImageConstrainAndClusterTransitionRelation(fsm->imageInfo, imgFlag, one, Img_GuidedSearchReadUnderApproxMinimizeMethod(), 1, /* under approx */ 1, /* clean up */ 0, /* no variable reordering */ printStatus); mdd_free(one); return; } /**Function******************************************************************** Synopsis [Frees the reachable states of an FSM.] Description [Frees the reachable states of an FSM.] SideEffects [] SeeAlso [Fsm_FsmFree, Fsm_FsmFreeOverApproximateReachableStates] ******************************************************************************/ void Fsm_FsmFreeReachableStates(Fsm_Fsm_t *fsm) { if (fsm->reachabilityInfo.reachableStates) { mdd_free(fsm->reachabilityInfo.reachableStates); fsm->reachabilityInfo.reachableStates = NIL(mdd_t); } } /**Function******************************************************************** Synopsis [Frees the approximate reachable states of an FSM.] Description [Frees the approximate reachable states of an FSM.] SideEffects [] SeeAlso [Fsm_FsmFree, Fsm_FsmFreeReachableStates] ******************************************************************************/ void Fsm_FsmFreeOverApproximateReachableStates(Fsm_Fsm_t *fsm) { if (fsm->reachabilityInfo.apprReachableStates) { mdd_array_free(fsm->reachabilityInfo.apprReachableStates); fsm->reachabilityInfo.apprReachableStates = NIL(array_t); fsm->reachabilityInfo.overApprox = Fsm_Ardc_NotConverged_c; } if (fsm->reachabilityInfo.subPsVars) { int i; array_t *psVars; for (i = 0; i < array_n(fsm->reachabilityInfo.subPsVars); i++) { psVars = array_fetch(array_t *, fsm->reachabilityInfo.subPsVars, i); array_free(psVars); } array_free(fsm->reachabilityInfo.subPsVars); fsm->reachabilityInfo.subPsVars = NIL(array_t); } } /**Function******************************************************************** Synopsis [Returns the reachable depth of an FSM.] Description [Returns the reachable depth of an FSM.] SideEffects [] SeeAlso [] ******************************************************************************/ int Fsm_FsmGetReachableDepth(Fsm_Fsm_t *fsm) { return(fsm->reachabilityInfo.depth); } /**Function******************************************************************** Synopsis [Checks if the 2 given fsms are the same, given that they are from the same total fsm. ] Description [Checks if the 2 given fsms are the same, given that they are from the same total fsm. Compares present, next state, input, real present state and abstract variables. Also compares the next state function NAMES ONLY. Since the 2 fsms are guaranteed to be parts of te same total fsm and they share the same network, the mdds of next state function nodes with the same name are guaranteed to be the same. ] SideEffects [] SeeAlso [] ******************************************************************************/ boolean Fsm_FsmCheckSameSubFsmInTotalFsm(Fsm_Fsm_t *fsm, Fsm_Fsm_t *subFsm1, Fsm_Fsm_t *subFsm2) { mdd_manager *mddMgr = Fsm_FsmReadMddManager(fsm); boolean result; assert(Fsm_FsmReadNetwork(fsm) == Fsm_FsmReadNetwork(subFsm1)); assert(Fsm_FsmReadNetwork(fsm) == Fsm_FsmReadNetwork(subFsm2)); assert(Fsm_FsmReadMddManager(subFsm1) == mddMgr); assert(Fsm_FsmReadMddManager(subFsm2) == mddMgr); /* compare present state variables */ result = VarIdArrayCompare(mddMgr, Fsm_FsmReadPresentStateVars(subFsm1), Fsm_FsmReadPresentStateVars(subFsm2)); if (!result) return FALSE; /* compare next state variables */ result = VarIdArrayCompare(mddMgr, Fsm_FsmReadNextStateVars(subFsm1), Fsm_FsmReadNextStateVars(subFsm2)); if (!result) return FALSE; /* compare input variables */ result = VarIdArrayCompare(mddMgr, Fsm_FsmReadInputVars(subFsm1), Fsm_FsmReadInputVars(subFsm2)); if (!result) return FALSE; /* compare the pseudo input variables */ result = VarIdArrayCompare(mddMgr, Fsm_FsmReadPseudoInputVars(subFsm1), Fsm_FsmReadPseudoInputVars(subFsm2)); if (!result) return FALSE; /* compare next state functions */ result = NSFunctionNamesCompare(mddMgr, Fsm_FsmReadNextStateFunctionNames(subFsm1), Fsm_FsmReadNextStateFunctionNames(subFsm2)); if (!result) return FALSE; return TRUE; } /**Function******************************************************************** Synopsis [Returns whether reachability analysis was an approximation or exact.] Description [Returns whether reachability analysis was an approximation or exact.] SideEffects [] SeeAlso [] ******************************************************************************/ Fsm_RchStatus_t Fsm_FsmReadReachabilityApproxComputationStatus(Fsm_Fsm_t *fsm) { return fsm->reachabilityInfo.rchStatus; } /**Function******************************************************************** Synopsis [Minimize the transition relation wrt either ARDCs or exact reachability information] Description [Prefers exact rdcs when available, if neither exact nor approximate rdcs are availablem, the TR is not touched.] SideEffects [] SeeAlso [] ******************************************************************************/ void Fsm_MinimizeTransitionRelationWithReachabilityInfo( Fsm_Fsm_t *fsm, Img_DirectionType fwdbwd, boolean verbosity) { Img_ImageInfo_t *imageInfo; array_t *minimizeArray = NIL(array_t); boolean fwd = FALSE; boolean bwd = FALSE; int oldVerbosity; Fsm_RchStatus_t status; boolean freeArray; mdd_t *exactrdc; switch (fwdbwd) { case Img_Forward_c: fwd = 1; break; case Img_Backward_c: bwd = 1; break; case Img_Both_c: fwd = 1; bwd= 1; break; default: assert(0); break; } imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, bwd, fwd); oldVerbosity = Img_ReadPrintMinimizeStatus(imageInfo); status = Fsm_FsmReadReachabilityApproxComputationStatus(fsm); exactrdc = Fsm_FsmReadCurrentReachableStates(fsm); if((status == Fsm_Rch_Exact_c || status == Fsm_Rch_Over_c) && exactrdc != NIL(mdd_t) ){ freeArray = TRUE; minimizeArray = array_alloc(mdd_t *, 1); array_insert_last(mdd_t *, minimizeArray, mdd_dup(exactrdc)); }else{ freeArray = FALSE; minimizeArray = Fsm_FsmReadCurrentOverApproximateReachableStates(fsm); if(minimizeArray == NIL(array_t)) return; } if(verbosity) Img_SetPrintMinimizeStatus(imageInfo, 1); /* We never reorder the clusters of the iwls structure. It is probably better to reorder them, but as this is written, there is no time to evaluate the effect of reordering. */ Img_MinimizeTransitionRelation(imageInfo, minimizeArray, Img_DefaultMinimizeMethod_c, fwdbwd, FALSE); if(verbosity) Img_SetPrintMinimizeStatus(imageInfo, oldVerbosity); if(freeArray) mdd_array_free(minimizeArray); return; } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Sets array of onion rings from reachability computation] Description [Sets array of onion rings from reachability computation.] SideEffects [] SeeAlso [Fsm_FsmReadReachabilityOnionRings] ******************************************************************************/ void FsmSetReachabilityOnionRings( Fsm_Fsm_t *fsm, array_t *onionRings) { fsm->reachabilityInfo.onionRings = onionRings; } /**Function******************************************************************** Synopsis [Sets whether onion rings are due to BFS.] Description [Sets whether onion rings are due to BFS.] SideEffects [] SeeAlso [Fsm_FsmReadReachabilityOnionRingsMode] ******************************************************************************/ void FsmSetReachabilityOnionRingsMode( Fsm_Fsm_t *fsm, Fsm_RchType_t value) { fsm->reachabilityInfo.onionRingsMode = value; } /**Function******************************************************************** Synopsis [Sets whether onion rings are up to date.] Description [Sets whether onion rings are up to date.] SideEffects [] SeeAlso [Fsm_FsmReachabilityOnionRingsUpToDate] ******************************************************************************/ void FsmSetReachabilityOnionRingsUpToDateFlag( Fsm_Fsm_t *fsm, boolean value) { fsm->reachabilityInfo.onionRingsUpToDate = value; } /**Function******************************************************************** Synopsis [Sets whether reachability analysis was an approximation.] Description [Sets whether reachability analysis was an approximation.] SideEffects [] SeeAlso [] ******************************************************************************/ void FsmSetReachabilityApproxComputationStatus( Fsm_Fsm_t *fsm, Fsm_RchStatus_t value) { fsm->reachabilityInfo.rchStatus = value; } /**Function******************************************************************** Synopsis [Sets the status of overapproxiate reachable computation.] Description [Sets the status of overapproxiate reachable computation.] SideEffects [] SeeAlso [] ******************************************************************************/ void FsmSetReachabilityOverApproxComputationStatus( Fsm_Fsm_t *fsm, Fsm_Ardc_StatusType_t status) { fsm->reachabilityInfo.overApprox = status; } /**Function******************************************************************** Synopsis [Reads the status of overapproxiate reachable computation.] Description [Reads the status of overapproxiate reachable computation.] SideEffects [] SeeAlso [] ******************************************************************************/ Fsm_Ardc_StatusType_t FsmReadReachabilityOverApproxComputationStatus(Fsm_Fsm_t *fsm) { return(fsm->reachabilityInfo.overApprox); } /**Function******************************************************************** Synopsis [Sets the mode field to indicate whether computation has always been BFS.] Description [Sets the mode field to indicate whether computation has always been BFS.] SideEffects [] SeeAlso [] ******************************************************************************/ void FsmSetReachabilityComputationMode( Fsm_Fsm_t *fsm, Fsm_RchType_t value) { fsm->reachabilityInfo.reachabilityMode = value; } /**Function******************************************************************** Synopsis [Reads the mode field to indicate whether computation has always been BFS.] Description [Reads the mode field to indicate whether computation has always been BFS.] SideEffects [] SeeAlso [] ******************************************************************************/ Fsm_RchType_t FsmReadReachabilityComputationMode( Fsm_Fsm_t *fsm) { return fsm->reachabilityInfo.reachabilityMode; } /**Function******************************************************************** Synopsis [Reset fsm fields] Description [Reset fsm fields. Free reachable states, onion rings. Reset the onion ring up-to-date flag, onion rings BFS, depth and under approximation flag.] SideEffects [] ******************************************************************************/ void FsmResetReachabilityFields(Fsm_Fsm_t *fsm, Fsm_RchType_t approxFlag) { int i; mdd_t *reachableStates; /* free reachable states if it is necessary to recompute anyway. */ if (approxFlag != Fsm_Rch_Oa_c) { if (Fsm_FsmReadCurrentReachableStates(fsm)) { Fsm_FsmFreeReachableStates(fsm); } } else if (Fsm_FsmReadCurrentOverApproximateReachableStates(fsm)) { Fsm_FsmFreeOverApproximateReachableStates(fsm); } /* free onion rings */ if (Fsm_FsmReadReachabilityOnionRings(fsm) != NIL(array_t)) { arrayForEachItem(mdd_t *, Fsm_FsmReadReachabilityOnionRings(fsm), i, reachableStates) { mdd_free(reachableStates); } array_free(Fsm_FsmReadReachabilityOnionRings(fsm)); FsmSetReachabilityOnionRings(fsm, NIL(array_t)); } fsm->reachabilityInfo.depth = 0; FsmSetReachabilityComputationMode(fsm, Fsm_Rch_Default_c); FsmSetReachabilityApproxComputationStatus(fsm, Fsm_Rch_Under_c); FsmSetReachabilityOnionRingsUpToDateFlag(fsm, FALSE); FsmSetReachabilityOnionRingsMode(fsm, Fsm_Rch_Default_c); return; } /* end of FsmResetReachabilityFields */ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Allocates HD Info structure.] Description [Allocates HD Info structure.] SideEffects [] SeeAlso [Fsm_FsmHdStructFree] ******************************************************************************/ FsmHdStruct_t * FsmHdStructAlloc(int nvars) { FsmHdStruct_t *hdInfo = ALLOC(FsmHdStruct_t, 1); if (hdInfo == NIL(FsmHdStruct_t)) return hdInfo; hdInfo->numDeadEnds = 0; hdInfo->firstSubset = TRUE; hdInfo->lastIter = -1; hdInfo->partialImage = FALSE; hdInfo->residueCount = 0; hdInfo->interiorStates = NIL(mdd_t); hdInfo->interiorStateCandidate = NIL(mdd_t); hdInfo->deadEndResidue = NIL(mdd_t); hdInfo->options = Fsm_FsmHdGetTravOptions(nvars); hdInfo->stats = FsmHdStatsStructAlloc(); hdInfo->imageOfReachedComputed = FALSE; hdInfo->onlyPartialImage = FALSE; hdInfo->slowGrowth = 0; hdInfo->deadEndWithOriginalTR = FALSE; hdInfo->deadEndComputation = FALSE; return hdInfo; } /**Function******************************************************************** Synopsis [Frees HD info struct.] Description [Frees HD info struct.] SideEffects [] SeeAlso [Fsm_FsmHdStructAllocate] ******************************************************************************/ void FsmHdStructFree(FsmHdStruct_t *hdInfo) { if (hdInfo->interiorStates != NULL) mdd_free(hdInfo->interiorStates); if (hdInfo->interiorStateCandidate != NULL) mdd_free(hdInfo->interiorStateCandidate); if (hdInfo->deadEndResidue != NULL) mdd_free(hdInfo->deadEndResidue); FsmHdStatsStructFree(hdInfo->stats); Fsm_FsmHdFreeTravOptions(hdInfo->options); FREE(hdInfo); return; } /**Function******************************************************************** Synopsis [Prints all options that are related to guided search.] Description [Prints all options that are related to guided search.] SideEffects [] SeeAlso [CommandGuidedSearchOptions] ******************************************************************************/ void FsmGuidedSearchPrintOptions(void) { char *string = Cmd_FlagReadByName("guided_search_hint_type"); if (string == NIL(char)) string = "local"; fprintf(vis_stdout, "Flag guided_search_hint_type is set to %s.\n", string); string = Cmd_FlagReadByName("guided_search_underapprox_minimize_method"); if (string == NIL(char)) string = "and"; fprintf(vis_stdout, "Flag guided_search_underapprox_minimize_method is set to %s.\n", string); string = Cmd_FlagReadByName("guided_search_overapprox_minimize_method"); if (string == NIL(char)) string = "ornot"; fprintf(vis_stdout, "Flag guided_search_overapprox_minimize_method is set to %s.\n", string); string = Cmd_FlagReadByName("guided_search_sequence"); if (string == NIL(char)) string = "all hints to convergence"; fprintf(vis_stdout, "Flag guided_search_overapprox_minimize_method is set to %s.\n", string); return; } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Allocates structure] Description [Allocates structure] SideEffects [] SeeAlso [] ******************************************************************************/ static Fsm_Fsm_t * FsmStructAlloc(Ntk_Network_t *network, graph_t *partition) { Fsm_Fsm_t *fsm; if (Ntk_NetworkReadNumLatches(network) == 0) { error_append("Network has no latches. Cannot create FSM."); return (NIL(Fsm_Fsm_t)); } fsm = ALLOC(Fsm_Fsm_t, 1); if (fsm == NIL(Fsm_Fsm_t)) return NIL(Fsm_Fsm_t); memset(fsm, 0, sizeof(Fsm_Fsm_t)); fsm->network = network; if (partition == NIL(graph_t)) { partition = Part_NetworkReadPartition(network); if (partition == NIL(graph_t)) { error_append("Network has no partition. Cannot create FSM."); return (NIL(Fsm_Fsm_t)); } else { fsm->partition = Part_PartitionDuplicate(partition); } } else { fsm->partition = partition; } FsmSetReachabilityOnionRings(fsm, NIL(array_t)); FsmSetReachabilityOnionRingsUpToDateFlag(fsm, FALSE); FsmSetReachabilityOnionRingsMode(fsm, Fsm_Rch_Default_c); FsmSetReachabilityApproxComputationStatus(fsm, Fsm_Rch_Under_c); FsmSetReachabilityComputationMode(fsm, Fsm_Rch_Default_c); FsmSetReachabilityOverApproxComputationStatus(fsm, Fsm_Ardc_NotConverged_c); fsm->fsmData.presentStateVars = array_alloc(int, 0); fsm->fsmData.nextStateVars = array_alloc(int, 0); fsm->fsmData.inputVars = array_alloc(int, 0); fsm->fsmData.nextStateFunctions = array_alloc(char *, 0); return (fsm); } /* end of FsmStructAlloc */ /**Function******************************************************************** Synopsis [Allocates structure] Description [Allocates structure] SideEffects [] SeeAlso [] ******************************************************************************/ static void FsmCreateVariableCubes(Fsm_Fsm_t *fsm) { mdd_manager *manager = Fsm_FsmReadMddManager(fsm); char *flagValue; boolean createVariableCubesFlag = TRUE; if (bdd_get_package_name() != CUDD) return; flagValue = Cmd_FlagReadByName("fsm_create_var_cubes"); if (flagValue != NIL(char)) { if (strcmp(flagValue, "yes") == 0) createVariableCubesFlag = TRUE; else if (strcmp(flagValue, "no") == 0) createVariableCubesFlag = FALSE; else { fprintf(vis_stderr, "** ardc error : invalid value %s for create_var_cubes[yes/no]. **\n", flagValue); } } if (!createVariableCubesFlag) return; fsm->fsmData.createVarCubesFlag = TRUE; fsm->fsmData.presentStateCube = mdd_id_array_to_bdd_cube(manager, fsm->fsmData.presentStateVars); fsm->fsmData.nextStateCube = mdd_id_array_to_bdd_cube(manager, fsm->fsmData.nextStateVars); fsm->fsmData.inputCube = mdd_id_array_to_bdd_cube(manager, fsm->fsmData.inputVars); if (fsm->fsmData.pseudoInputVars) { fsm->fsmData.pseudoInputCube = mdd_id_array_to_bdd_cube(manager, fsm->fsmData.pseudoInputVars); } if (fsm->fsmData.primaryInputVars) { fsm->fsmData.primaryInputCube = mdd_id_array_to_bdd_cube(manager, fsm->fsmData.primaryInputVars); } if (fsm->fsmData.globalPsVars) { fsm->fsmData.globalPsCube = mdd_id_array_to_bdd_cube(manager, fsm->fsmData.globalPsVars); } } /**Function******************************************************************** Synopsis [Compare procedure for name comparison.] Description [Compare procedure for name comparison.] SideEffects [] ******************************************************************************/ static int nameCompare( const void * name1, const void * name2) { return(strcmp(*(char **)name1, *(char **)name2)); } /* end of signatureCompare */ /**Function******************************************************************** Synopsis [ Checks that 2 arrays of variables ids are the same.] Description [ Checks that 2 arrays of variables ids are the same by computing the bdd of the cube.] SideEffects [] SeeAlso [Fsm_FsmCheckSameSubFsmInTotalFsm] ******************************************************************************/ static boolean VarIdArrayCompare(mdd_manager *mddMgr, array_t *vars1, array_t *vars2) { mdd_t *cube1, *cube2; boolean result = FALSE; cube1 = bdd_compute_cube(mddMgr, vars1); cube2 = bdd_compute_cube(mddMgr, vars2); if ((cube1 == NIL(mdd_t)) || (cube2 == NIL(mdd_t))) { result = (cube1 == cube2) ? TRUE : FALSE; } else { result = bdd_equal(cube1, cube2) ? TRUE : FALSE; } if (cube1 != NIL(bdd_t)) bdd_free(cube1); if (cube2 != NIL(bdd_t)) bdd_free(cube2); return result; } /* end of VarIdArrayCompare */ /**Function******************************************************************** Synopsis [ Checks that 2 arrays of variables ids are the same.] Description [ Checks that 2 arrays of variables ids are the same by computing the bdd of the cube.] SideEffects [] SeeAlso [Fsm_FsmCheckSameSubFsmInTotalFsm] ******************************************************************************/ static boolean NSFunctionNamesCompare(mdd_manager *mddMgr, array_t *names1, array_t *names2) { int sizeArray = array_n(names1); int i, count; char *name; st_table *nameTable = st_init_table(strcmp, st_strhash); if (sizeArray != array_n(names2)) return FALSE; /* check if elements in names2 is in names1 */ arrayForEachItem(char *, names1, i, name) { if (st_lookup_int(nameTable, name, &count)) { count++; } else { count = 1; } st_insert(nameTable, name, (char *)(long)count); } arrayForEachItem(char *, names2, i, name) { if (!st_lookup_int(nameTable, name, &count)) { st_free_table(nameTable); return FALSE; } else if (count == 0) { st_free_table(nameTable); return FALSE; } else { count--; st_insert(nameTable, name, (char *)(long)count); } } st_free_table(nameTable); /* check if elements in names1 is in names2 */ nameTable = st_init_table(strcmp, st_strhash); arrayForEachItem(char *, names2, i, name) { if (st_lookup_int(nameTable, name, &count)) { count++; } else { count = 1; } st_insert(nameTable, name, (char *)(long)count); } arrayForEachItem(char *, names1, i, name) { if (!st_lookup_int(nameTable, name, &count)) { st_free_table(nameTable); return FALSE; } else if (count == 0) { st_free_table(nameTable); return FALSE; } else { count--; st_insert(nameTable, name, (char *)(long)count); } } st_free_table(nameTable); return TRUE; } /* end of NSFunctionNamesCompare */ /**Function******************************************************************** Synopsis [Returns an array of mdd Ids of an FSM.] Description [Returns an array of mdd Ids of an FSM.] SideEffects [] SeeAlso [] ******************************************************************************/ static array_t * GetMddSupportIdArray(Fsm_Fsm_t *fsm, st_table *mddIdTable, st_table *pseudoMddIdTable) { mdd_t *func; char *nodeName; vertex_t *vertex; Mvf_Function_t *mvf; int i, j, k; long mddId; array_t *varBddFunctionArray; mdd_manager *mddManager; array_t *supportMddIdArray, *support; st_table *supportMddIdTable; st_generator *stGen; supportMddIdTable = st_init_table(st_numcmp, st_numhash); mddManager = Part_PartitionReadMddManager(fsm->partition); for (i = 0; i < array_n(fsm->fsmData.nextStateFunctions); i++) { nodeName = array_fetch(char*, fsm->fsmData.nextStateFunctions, i); vertex = Part_PartitionFindVertexByName(fsm->partition, nodeName); mvf = Part_VertexReadFunction(vertex); mddId = (long) array_fetch(int, fsm->fsmData.nextStateVars, i); varBddFunctionArray = mdd_fn_array_to_bdd_fn_array(mddManager, (int) mddId, mvf); for (j = 0; j < array_n(varBddFunctionArray); j++) { func = array_fetch(mdd_t *, varBddFunctionArray, j); support = mdd_get_support(mddManager, func); arrayForEachItem(int, support, k, mddId) { if (!st_lookup(supportMddIdTable, (char *)mddId, NIL(char *))) { if (st_lookup(mddIdTable, (char *)mddId, NIL(char *)) || st_lookup(pseudoMddIdTable, (char *)mddId, NIL(char *))) { st_insert(supportMddIdTable, (char *)mddId, NIL(char)); } else { /* intermediate variables */ /* NEEDS to get the supports of an intermediate variable */ assert(0); } } } } array_free(varBddFunctionArray); } supportMddIdArray = array_alloc(int, 0); st_foreach_item(supportMddIdTable, stGen, &mddId, NIL(char *)) { array_insert_last(int, supportMddIdArray, (int) mddId); } return(supportMddIdArray); }