#include "fsmInt.h"

Include dependency graph for fsmFsm.c:

Functions
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)
Fsm_Fsm_t *	Fsm_FsmCreateFromNetworkWithPartition (Ntk_Network_t network, graph_t partition)
Fsm_Fsm_t *	Fsm_FsmCreateReducedFsm (Ntk_Network_t network, graph_t partition, array_t latches, array_t inputs, array_t *fairArray)
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)
void	Fsm_FsmFree (Fsm_Fsm_t *fsm)
void	Fsm_FsmSubsystemFree (Fsm_Fsm_t *fsm)
void	Fsm_FsmFreeCallback (void *data)
Ntk_Network_t *	Fsm_FsmReadNetwork (Fsm_Fsm_t *fsm)
boolean	Fsm_FsmReadUseUnquantifiedFlag (Fsm_Fsm_t *fsm)
mdd_manager *	Fsm_FsmReadMddManager (Fsm_Fsm_t *fsm)
Fsm_Fsm_t *	Fsm_NetworkReadOrCreateFsm (Ntk_Network_t *network)
Fsm_Fsm_t *	Fsm_NetworkReadFsm (Ntk_Network_t *network)
Img_ImageInfo_t *	Fsm_FsmReadImageInfo (Fsm_Fsm_t *fsm)
void	Fsm_FsmSetImageInfo (Fsm_Fsm_t fsm, Img_ImageInfo_t imageInfo)
void	Fsm_FsmFreeImageInfo (Fsm_Fsm_t *fsm)
graph_t *	Fsm_FsmReadPartition (Fsm_Fsm_t *fsm)
boolean	Fsm_FsmTestIsReachabilityDone (Fsm_Fsm_t *fsm)
boolean	Fsm_FsmTestIsOverApproximateReachabilityDone (Fsm_Fsm_t *fsm)
mdd_t *	Fsm_FsmReadReachableStates (Fsm_Fsm_t *fsm)
mdd_t *	Fsm_FsmReadCurrentReachableStates (Fsm_Fsm_t *fsm)
array_t *	Fsm_FsmReadOverApproximateReachableStates (Fsm_Fsm_t *fsm)
array_t *	Fsm_FsmReadCurrentOverApproximateReachableStates (Fsm_Fsm_t *fsm)
array_t *	Fsm_FsmReadReachabilityOnionRings (Fsm_Fsm_t *fsm)
boolean	Fsm_FsmReachabilityOnionRingsStates (Fsm_Fsm_t fsm, mdd_t *result)
boolean	Fsm_FsmTestReachabilityOnionRingsUpToDate (Fsm_Fsm_t *fsm)
Fsm_RchType_t	Fsm_FsmReadReachabilityOnionRingsMode (Fsm_Fsm_t *fsm)
Img_ImageInfo_t *	Fsm_FsmReadOrCreateImageInfo (Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag)
Img_ImageInfo_t *	Fsm_FsmReadOrCreateImageInfoFAFW (Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag)
Img_ImageInfo_t *	Fsm_FsmReadOrCreateImageInfoPrunedFAFW (Fsm_Fsm_t fsm, mdd_t Winning, int bwdImgFlag, int fwdImgFlag)
Img_ImageInfo_t *	Fsm_FsmReadOrCreateImageInfoForComputingRange (Fsm_Fsm_t *fsm, int bwdImgFlag, int fwdImgFlag)
mdd_t *	Fsm_FsmComputeInitialStates (Fsm_Fsm_t *fsm)
array_t *	Fsm_FsmReadPresentStateVars (Fsm_Fsm_t *fsm)
array_t *	Fsm_FsmReadNextStateVars (Fsm_Fsm_t *fsm)
array_t *	Fsm_FsmReadNextStateFunctionNames (Fsm_Fsm_t *fsm)
array_t *	Fsm_FsmReadInputVars (Fsm_Fsm_t *fsm)
array_t *	Fsm_FsmReadPrimaryInputVars (Fsm_Fsm_t *fsm)
array_t *	Fsm_FsmReadPseudoInputVars (Fsm_Fsm_t *fsm)
void	Fsm_FsmSetInputVars (Fsm_Fsm_t fsm, array_t inputVars)
void	Fsm_FsmSetUseUnquantifiedFlag (Fsm_Fsm_t *fsm, boolean value)
void	Fsm_FsmSetInitialStates (Fsm_Fsm_t fsm, mdd_t initStates)
int	Fsm_FsmReadFAFWFlag (Fsm_Fsm_t *fsm)
void	Fsm_FsmSetFAFWFlag (Fsm_Fsm_t *fsm, boolean FAFWFlag)
void	Fsm_FsmSetSystemVariableFAFW (Fsm_Fsm_t fsm, st_table bddIdTable)
bdd_t *	Fsm_FsmReadExtQuantifyInputCube (Fsm_Fsm_t *fsm)
bdd_t *	Fsm_FsmReadUniQuantifyInputCube (Fsm_Fsm_t *fsm)
Fsm_Fsm_t *	Fsm_HrcManagerReadCurrentFsm (Hrc_Manager_t *hmgr)
Fsm_Fsm_t *	Fsm_FsmCreateSubsystemFromNetwork (Ntk_Network_t network, graph_t partition, st_table *vertexTable, boolean independentFlag, int createPseudoVarMode)
void	Fsm_InstantiateHint (Fsm_Fsm_t fsm, mdd_t hint, int fwdFlag, int bwdFlag, Ctlp_Approx_t type, int printStatus)
void	Fsm_CleanUpHints (Fsm_Fsm_t *fsm, int fwdFlag, int bwdFlag, int printStatus)
void	Fsm_FsmFreeReachableStates (Fsm_Fsm_t *fsm)
void	Fsm_FsmFreeOverApproximateReachableStates (Fsm_Fsm_t *fsm)
int	Fsm_FsmGetReachableDepth (Fsm_Fsm_t *fsm)
boolean	Fsm_FsmCheckSameSubFsmInTotalFsm (Fsm_Fsm_t fsm, Fsm_Fsm_t subFsm1, Fsm_Fsm_t *subFsm2)
Fsm_RchStatus_t	Fsm_FsmReadReachabilityApproxComputationStatus (Fsm_Fsm_t *fsm)
void	Fsm_MinimizeTransitionRelationWithReachabilityInfo (Fsm_Fsm_t *fsm, Img_DirectionType fwdbwd, boolean verbosity)
void	FsmSetReachabilityOnionRings (Fsm_Fsm_t fsm, array_t onionRings)
void	FsmSetReachabilityOnionRingsMode (Fsm_Fsm_t *fsm, Fsm_RchType_t value)
void	FsmSetReachabilityOnionRingsUpToDateFlag (Fsm_Fsm_t *fsm, boolean value)
void	FsmSetReachabilityApproxComputationStatus (Fsm_Fsm_t *fsm, Fsm_RchStatus_t value)
void	FsmSetReachabilityOverApproxComputationStatus (Fsm_Fsm_t *fsm, Fsm_Ardc_StatusType_t status)
Fsm_Ardc_StatusType_t	FsmReadReachabilityOverApproxComputationStatus (Fsm_Fsm_t *fsm)
void	FsmSetReachabilityComputationMode (Fsm_Fsm_t *fsm, Fsm_RchType_t value)
Fsm_RchType_t	FsmReadReachabilityComputationMode (Fsm_Fsm_t *fsm)
void	FsmResetReachabilityFields (Fsm_Fsm_t *fsm, Fsm_RchType_t approxFlag)
FsmHdStruct_t *	FsmHdStructAlloc (int nvars)
void	FsmHdStructFree (FsmHdStruct_t *hdInfo)
void	FsmGuidedSearchPrintOptions (void)
Variables
static char rcsid[]	UNUSED = "$Id: fsmFsm.c,v 1.88 2007/04/02 17:03:13 hhkim Exp $"

Function Documentation

void Fsm_CleanUpHints	(	Fsm_Fsm_t *	fsm,
		int	fwdFlag,
		int	bwdFlag,
		int	printStatus
	)

Function********************************************************************

Synopsis [Clean up after hints]

Description [Clean up after hints.]

SideEffects []

SeeAlso [Fsm_InstantiateHint]

Definition at line 1864 of file fsmFsm.c.

{
  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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

boolean Fsm_FsmCheckSameSubFsmInTotalFsm	(	Fsm_Fsm_t *	fsm,
		Fsm_Fsm_t *	subFsm1,
		Fsm_Fsm_t *	subFsm2
	)

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 []

Definition at line 1975 of file fsmFsm.c.

{
  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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

mdd_t* Fsm_FsmComputeInitialStates ( Fsm_Fsm_t * fsm )

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) = u \[ (x_i = g_i(u))\]).]

SideEffects [The result of the initial state computation is stored with the FSM.]

SeeAlso [Fsm_FsmComputeReachableStates]

Definition at line 1168 of file fsmFsm.c.

{
  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; i<numLatches; i++){
    int latchMddId = array_fetch(int, psVars, i);
    Ntk_Node_t *latch = Ntk_NetworkFindNodeByMddId(network, latchMddId);
    Ntk_Node_t *initNode   = Ntk_LatchReadInitialInput(latch);
    vertex_t   *initVertex = Part_PartitionFindVertexByName(partition,
                                Ntk_NodeReadName(initNode));
    array_insert(Ntk_Node_t *, initNodes, i, initNode);
    array_insert(vertex_t *, initVertices, i, initVertex);
    array_insert(int, latchMddIds, i, Ntk_NodeReadMddId(latch));
  }

  /*
   * Get the table of legal support nodes, both as network nodes and
   * as partition vertices. Inputs (both primary and pseudo) and constants
   * constitute the legal support nodes.
   */
  supportNodes    = st_init_table(st_ptrcmp, st_ptrhash);
  supportVertices = st_init_table(st_ptrcmp, st_ptrhash);
  Ntk_NetworkForEachNode(network, gen, node) {
    vertex_t *vertex = Part_PartitionFindVertexByName(partition,
                                                      Ntk_NodeReadName(node));

    if (Ntk_NodeTestIsConstant(node) || Ntk_NodeTestIsInput(node)) {
      st_insert(supportNodes, (char *) node, NIL(char));
      st_insert(supportVertices, (char *) vertex, NIL(char));
    }
  }

  /*
   * If the initial nodes are not covered by the legal support nodes, then
   * return NIL.
   */
  if (!Ntk_NetworkTestLeavesCoverSupportOfRoots(network, initNodes,
                                                supportNodes)) {
    array_free(initNodes);
    array_free(initVertices);
    array_free(latchMddIds);
    st_free_table(supportNodes);
    st_free_table(supportVertices);
    return NIL(mdd_t);
  }

  /*
   * At this point, we are certain that the initialization functions are
   * well-defined. Get the MVF for each initialization node, in terms of the
   * support vertices.  Note that the MVF for each initial node is guaranteed to
   * exist in the partition, since an initial node is a combinational
   * output.
   */
  array_free(initNodes);
  st_free_table(supportNodes);
  initMvfs = Part_PartitionCollapse(partition, initVertices,
                                    supportVertices, NIL(mdd_t)); 
  array_free(initVertices);
  st_free_table(supportVertices);

  /* Compute the relation (x_i = g_i(u)) for each latch. */
  initRelnArray = array_alloc(mdd_t*, numLatches);
  for (i = 0; i < numLatches; i++) {
    int latchMddId = array_fetch(int, latchMddIds, i);
    Mvf_Function_t *initMvf = array_fetch(Mvf_Function_t *, initMvfs, i);
    mdd_t *initLatchReln = Mvf_FunctionBuildRelationWithVariable(initMvf,
                                                                latchMddId);
    array_insert(mdd_t *, initRelnArray, i, initLatchReln);
  }

  array_free(latchMddIds);
  Mvf_FunctionArrayFree(initMvfs);

  /* init_states(x) = \exists u \[\prod (x_i = g_i(u))\] */
  /*initStates = Fsm_MddMultiwayAndSmooth(mddManager, initRelnArray,
                                        fsm->fsmData.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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

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
	)

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]

Definition at line 256 of file fsmFsm.c.

{
  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; i<array_n(latches); i++){
    latch = array_fetch(Ntk_Node_t*, latches, i);
    array_insert_last(char*, fsm->fsmData.nextStateFunctions,
                      Ntk_NodeReadName(latch));
  }
  array_sort(fsm->fsmData.nextStateFunctions, nameCompare);

  for(i=0; i<array_n(latches); i++){
    char *nodeName;
    nodeName = array_fetch(char *, fsm->fsmData.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; i<array_n(inputs); i++){
    input = array_fetch(Ntk_Node_t*, inputs, i);
    array_insert_last(int, fsm->fsmData.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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fsm_Fsm_t* Fsm_FsmCreateFromNetworkWithPartition	(	Ntk_Network_t *	network,
		graph_t *	partition
	)

AutomaticEnd 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]

Definition at line 85 of file fsmFsm.c.

{
  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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fsm_Fsm_t* Fsm_FsmCreateReducedFsm	(	Ntk_Network_t *	network,
		graph_t *	partition,
		array_t *	latches,
		array_t *	inputs,
		array_t *	fairArray
	)

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]

Definition at line 150 of file fsmFsm.c.

{
  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; i<array_n(latches); i++){
    latch = array_fetch(Ntk_Node_t*, latches, i);
    array_insert_last(char*, fsm->fsmData.nextStateFunctions,
                      Ntk_NodeReadName(latch));
  }
  array_sort(fsm->fsmData.nextStateFunctions, nameCompare);

  for(i=0; i<array_n(latches); i++){
    char *nodeName;
    nodeName = array_fetch(char *, fsm->fsmData.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; i<array_n(inputs); i++){
    input = array_fetch(Ntk_Node_t*, inputs, i);
    array_insert_last(int, fsm->fsmData.inputVars, Ntk_NodeReadMddId(input));
  }

  FsmCreateVariableCubes(fsm);
  return (fsm);
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fsm_Fsm_t* Fsm_FsmCreateSubsystemFromNetwork	(	Ntk_Network_t *	network,
		graph_t *	partition,
		st_table *	vertexTable,
		boolean	independentFlag,
		int	createPseudoVarMode
	)

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]

Definition at line 1659 of file fsmFsm.c.

{
  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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Fsm_FsmFree ( Fsm_Fsm_t * 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]

Definition at line 368 of file fsmFsm.c.

{
  Part_PartitionFree(fsm->partition);
  Fsm_FsmSubsystemFree(fsm);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Fsm_FsmFreeCallback ( void * data )

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]

Definition at line 463 of file fsmFsm.c.

{
  Fsm_FsmFree((Fsm_Fsm_t *) data);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Fsm_FsmFreeImageInfo ( Fsm_Fsm_t * fsm )

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]

Definition at line 627 of file fsmFsm.c.

{
  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);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Fsm_FsmFreeOverApproximateReachableStates ( Fsm_Fsm_t * fsm )

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]

Definition at line 1918 of file fsmFsm.c.

{
  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);
  }
}

Here is the caller graph for this function:

void Fsm_FsmFreeReachableStates ( Fsm_Fsm_t * fsm )

Function********************************************************************

Synopsis [Frees the reachable states of an FSM.]

Description [Frees the reachable states of an FSM.]

SideEffects []

SeeAlso [Fsm_FsmFree, Fsm_FsmFreeOverApproximateReachableStates]

Definition at line 1898 of file fsmFsm.c.

{
  if (fsm->reachabilityInfo.reachableStates) {
    mdd_free(fsm->reachabilityInfo.reachableStates);
    fsm->reachabilityInfo.reachableStates = NIL(mdd_t);
  }
}

Here is the caller graph for this function:

int Fsm_FsmGetReachableDepth ( Fsm_Fsm_t * fsm )

Function********************************************************************

Synopsis [Returns the reachable depth of an FSM.]

Description [Returns the reachable depth of an FSM.]

SideEffects []

SeeAlso []

Definition at line 1951 of file fsmFsm.c.

{
    return(fsm->reachabilityInfo.depth);
}

Here is the caller graph for this function:

boolean Fsm_FsmReachabilityOnionRingsStates	(	Fsm_Fsm_t *	fsm,
		mdd_t **	result
	)

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]

Definition at line 815 of file fsmFsm.c.

{
  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));
}

Here is the call graph for this function:

Here is the caller graph for this function:

array_t* Fsm_FsmReadCurrentOverApproximateReachableStates ( Fsm_Fsm_t * fsm )

Function********************************************************************

Synopsis [Returns the current approximate reachable states of an FSM.]

SideEffects []

SeeAlso [Fsm_ArdcComputeOverApproximateReachableStates]

Definition at line 774 of file fsmFsm.c.

{
  return(fsm->reachabilityInfo.apprReachableStates);
}

Here is the caller graph for this function:

mdd_t* Fsm_FsmReadCurrentReachableStates ( Fsm_Fsm_t * fsm )

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]

Definition at line 737 of file fsmFsm.c.

{
  return(fsm->reachabilityInfo.reachableStates);
}

Here is the caller graph for this function:

bdd_t* Fsm_FsmReadExtQuantifyInputCube ( Fsm_Fsm_t * fsm )

Function********************************************************************

Synopsis [Read input variables that is controlled by environment in the FSM structure.]

Description [This is function for FateAndFreeWill counterexample generation.]

SideEffects []

SeeAlso []

Definition at line 1570 of file fsmFsm.c.

{
  return(fsm->extQuantifyInputCube);
}

Here is the caller graph for this function:

int Fsm_FsmReadFAFWFlag ( Fsm_Fsm_t * fsm )

Function********************************************************************

Synopsis [Read FAFWFlag from the FSM structure.]

Description [This is function for FateAndFreeWill counterexample generation.]

SideEffects []

SeeAlso []

Definition at line 1471 of file fsmFsm.c.

{
  return((int)(fsm->FAFWFlag));
}

Here is the caller graph for this function:

Img_ImageInfo_t* Fsm_FsmReadImageInfo ( Fsm_Fsm_t * fsm )

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]

Definition at line 590 of file fsmFsm.c.

{
  return (fsm->imageInfo);
}

Here is the caller graph for this function:

array_t* Fsm_FsmReadInputVars ( Fsm_Fsm_t * fsm )

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]

Definition at line 1369 of file fsmFsm.c.

{
  return fsm->fsmData.inputVars;
}

Here is the caller graph for this function:

mdd_manager* Fsm_FsmReadMddManager ( Fsm_Fsm_t * fsm )

Function********************************************************************

Synopsis [Returns the MDD manager of the corresponding network of an FSM.]

SideEffects []

SeeAlso [Fsm_FsmCreateFromNetwork]

Definition at line 514 of file fsmFsm.c.

{
  return (Ntk_NetworkReadMddManager(fsm->network));
}

Here is the call graph for this function:

Ntk_Network_t* Fsm_FsmReadNetwork ( Fsm_Fsm_t * fsm )

Function********************************************************************

Synopsis [Returns the corresponding network of an FSM.]

SideEffects []

SeeAlso [Fsm_FsmCreateFromNetwork]

Definition at line 480 of file fsmFsm.c.

{
  return (fsm->network);
}

Here is the caller graph for this function:

array_t* Fsm_FsmReadNextStateFunctionNames ( Fsm_Fsm_t * fsm )

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]

Definition at line 1348 of file fsmFsm.c.

{
  return fsm->fsmData.nextStateFunctions;
}

Here is the caller graph for this function:

array_t* Fsm_FsmReadNextStateVars ( Fsm_Fsm_t * fsm )

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]

Definition at line 1327 of file fsmFsm.c.

{
  return fsm->fsmData.nextStateVars;
}

Here is the caller graph for this function:

Img_ImageInfo_t* Fsm_FsmReadOrCreateImageInfo	(	Fsm_Fsm_t *	fsm,
		int	bwdImgFlag,
		int	fwdImgFlag
	)

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]

Definition at line 901 of file fsmFsm.c.

{
  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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

Img_ImageInfo_t* Fsm_FsmReadOrCreateImageInfoFAFW	(	Fsm_Fsm_t *	fsm,
		int	bwdImgFlag,
		int	fwdImgFlag
	)

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]

Definition at line 967 of file fsmFsm.c.

{
  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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

Img_ImageInfo_t* Fsm_FsmReadOrCreateImageInfoForComputingRange	(	Fsm_Fsm_t *	fsm,
		int	bwdImgFlag,
		int	fwdImgFlag
	)

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]

Definition at line 1093 of file fsmFsm.c.

{
  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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

Img_ImageInfo_t* Fsm_FsmReadOrCreateImageInfoPrunedFAFW	(	Fsm_Fsm_t *	fsm,
		mdd_t *	Winning,
		int	bwdImgFlag,
		int	fwdImgFlag
	)

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]

Definition at line 1029 of file fsmFsm.c.

{
  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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

array_t* Fsm_FsmReadOverApproximateReachableStates ( Fsm_Fsm_t * fsm )

Function********************************************************************

Synopsis [Returns the approximate reachable states of an FSM.]

SideEffects []

SeeAlso [Fsm_ArdcComputeOverApproximateReachableStates]

Definition at line 754 of file fsmFsm.c.

{
  if (fsm->reachabilityInfo.overApprox >= 2)
    return(fsm->reachabilityInfo.apprReachableStates);
  else
    return(NIL(array_t));
}

Here is the caller graph for this function:

graph_t* Fsm_FsmReadPartition ( Fsm_Fsm_t * fsm )

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]

Definition at line 654 of file fsmFsm.c.

{
  return (fsm->partition);
}

Here is the caller graph for this function:

array_t* Fsm_FsmReadPresentStateVars ( Fsm_Fsm_t * fsm )

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]

Definition at line 1307 of file fsmFsm.c.

{
  return fsm->fsmData.presentStateVars;
}

array_t* Fsm_FsmReadPrimaryInputVars ( Fsm_Fsm_t * fsm )

Definition at line 1375 of file fsmFsm.c.

{
  return fsm->fsmData.primaryInputVars;
}

array_t* Fsm_FsmReadPseudoInputVars ( Fsm_Fsm_t * fsm )

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]

Definition at line 1396 of file fsmFsm.c.

{
  return fsm->fsmData.pseudoInputVars;
}

Here is the caller graph for this function:

Fsm_RchStatus_t Fsm_FsmReadReachabilityApproxComputationStatus ( Fsm_Fsm_t * fsm )

Function********************************************************************

Synopsis [Returns whether reachability analysis was an approximation or exact.]

Description [Returns whether reachability analysis was an approximation or exact.]

SideEffects []

SeeAlso []

Definition at line 2034 of file fsmFsm.c.

{
  return fsm->reachabilityInfo.rchStatus;
}

Here is the caller graph for this function:

array_t* Fsm_FsmReadReachabilityOnionRings ( Fsm_Fsm_t * fsm )

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]

Definition at line 794 of file fsmFsm.c.

{
  return fsm->reachabilityInfo.onionRings;
}

Here is the caller graph for this function:

Fsm_RchType_t Fsm_FsmReadReachabilityOnionRingsMode ( Fsm_Fsm_t * fsm )

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]

Definition at line 876 of file fsmFsm.c.

{
  return fsm->reachabilityInfo.onionRingsMode;
}

Here is the caller graph for this function:

mdd_t* Fsm_FsmReadReachableStates ( Fsm_Fsm_t * fsm )

Function********************************************************************

Synopsis [Returns the reachable states of an FSM.]

SideEffects [Returns the reachable states of an FSM.]

SeeAlso [Fsm_FsmComputeReachableStates]

Definition at line 716 of file fsmFsm.c.

{
  if (fsm->reachabilityInfo.rchStatus == Fsm_Rch_Exact_c)
    return(fsm->reachabilityInfo.reachableStates);
  else
    return(NIL(mdd_t));
}

Here is the caller graph for this function:

bdd_t* Fsm_FsmReadUniQuantifyInputCube ( Fsm_Fsm_t * fsm )

Function********************************************************************

Synopsis [Read input variables that is controlled by system in the FSM structure.]

Description [This is function for FateAndFreeWill counterexample generation.]

SideEffects []

SeeAlso []

Definition at line 1588 of file fsmFsm.c.

{
  return(fsm->uniQuantifyInputCube);
}

Here is the caller graph for this function:

boolean Fsm_FsmReadUseUnquantifiedFlag ( Fsm_Fsm_t * fsm )

Function********************************************************************

Synopsis [Read UnquantifiedFlag of an FSM.]

Description [This is function for FateAndFreeWill counterexample generation.]

SideEffects []

SeeAlso [Fsm_FsmCreateFromNetwork]

Definition at line 498 of file fsmFsm.c.

{
  return (fsm->useUnquantifiedFlag);
}

Here is the caller graph for this function:

void Fsm_FsmSetFAFWFlag	(	Fsm_Fsm_t *	fsm,
		boolean	FAFWFlag
	)

Function********************************************************************

Synopsis [Set FAFWFlag in the FSM structure.]

Description [This is function for FateAndFreeWill counterexample generation.]

SideEffects []

SeeAlso []

Definition at line 1488 of file fsmFsm.c.

{
  fsm->FAFWFlag = FAFWFlag;
}

Here is the caller graph for this function:

void Fsm_FsmSetImageInfo	(	Fsm_Fsm_t *	fsm,
		Img_ImageInfo_t *	imageInfo
	)

Function********************************************************************

Synopsis [Set the imageInfo.]

Description [Set the imageInfo. ]

SideEffects []

SeeAlso [Img_ImageInfoInitialize Fsm_FsmReadOrCreateImageInfo]

Definition at line 608 of file fsmFsm.c.

{
  fsm->imageInfo = imageInfo;
}

void Fsm_FsmSetInitialStates	(	Fsm_Fsm_t *	fsm,
		mdd_t *	initStates
	)

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 []

Definition at line 1448 of file fsmFsm.c.

{
  mdd_t *init;
  
  init = fsm->reachabilityInfo.initialStates;
  if (init != NIL(mdd_t)) {
    mdd_free(init);
  }
  fsm->reachabilityInfo.initialStates = initStates;
}

Here is the caller graph for this function:

void Fsm_FsmSetInputVars	(	Fsm_Fsm_t *	fsm,
		array_t *	inputVars
	)

Function********************************************************************

Synopsis [Set input variables into the FSM structure.]

Description []

SideEffects []

SeeAlso []

Definition at line 1413 of file fsmFsm.c.

{
  fsm->fsmData.inputVars = inputVars;
}

void Fsm_FsmSetSystemVariableFAFW	(	Fsm_Fsm_t *	fsm,
		st_table *	bddIdTable
	)

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 []

Definition at line 1506 of file fsmFsm.c.

{
  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; i<array_n(inputVars); i++) {
    mddId = array_fetch(int, inputVars, i);
    bddIdArray = mdd_id_to_bdd_id_array(mgr, mddId);
    for(j=0; j<array_n(bddIdArray); j++) {
      bddId = array_fetch(int, bddIdArray, j);
      if(bddIdTable && st_lookup_int(bddIdTable, (char *)(long)bddId, &tbddId)) {
        continue;
      }
      varBdd = bdd_get_variable(mgr, bddId);
      newCube = bdd_and(extCube, varBdd, 1, 1);
      bdd_free(extCube); bdd_free(varBdd);
      extCube = newCube;
    }
    array_free(bddIdArray);
  }
  uniCube = mdd_one(mgr);
  if(bddIdTable) {
    st_foreach_item(bddIdTable, gen, &bddId, &bddId) {
      varBdd = bdd_get_variable(mgr, bddId);
      newCube = bdd_and(uniCube, varBdd, 1, 1);
      bdd_free(uniCube); bdd_free(varBdd);
      uniCube = newCube;
    }
  }
  fsm->extQuantifyInputCube = extCube;
  fsm->uniQuantifyInputCube = uniCube;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Fsm_FsmSetUseUnquantifiedFlag	(	Fsm_Fsm_t *	fsm,
		boolean	value
	)

Function********************************************************************

Synopsis [Set useUnquantifiedFlag into the FSM structure.]

Description [This is function for FateAndFreeWill counterexample generation.]

SideEffects []

SeeAlso []

Definition at line 1430 of file fsmFsm.c.

{
  fsm->useUnquantifiedFlag = value;
}

Here is the caller graph for this function:

void Fsm_FsmSubsystemFree ( Fsm_Fsm_t * 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]

Definition at line 387 of file fsmFsm.c.

{

  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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

boolean Fsm_FsmTestIsOverApproximateReachabilityDone ( Fsm_Fsm_t * fsm )

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]

Definition at line 695 of file fsmFsm.c.

{
  
  if (Fsm_FsmReadOverApproximateReachableStates(fsm) != NIL(array_t)) {
        return TRUE;
  }
  return FALSE;
}

Here is the call graph for this function:

Here is the caller graph for this function:

boolean Fsm_FsmTestIsReachabilityDone ( Fsm_Fsm_t * fsm )

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]

Definition at line 672 of file fsmFsm.c.

{
  
  if (Fsm_FsmReadReachableStates(fsm) != NIL(mdd_t)) {
        return TRUE;
  }
  return FALSE;
}

Here is the call graph for this function:

Here is the caller graph for this function:

boolean Fsm_FsmTestReachabilityOnionRingsUpToDate ( Fsm_Fsm_t * 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]

Definition at line 858 of file fsmFsm.c.

{
  return fsm->reachabilityInfo.onionRingsUpToDate;
}

Here is the caller graph for this function:

Fsm_Fsm_t* Fsm_HrcManagerReadCurrentFsm ( Hrc_Manager_t * hmgr )

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]

Definition at line 1612 of file fsmFsm.c.

{
  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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Fsm_InstantiateHint	(	Fsm_Fsm_t *	fsm,
		mdd_t *	hint,
		int	fwdFlag,
		int	bwdFlag,
		Ctlp_Approx_t	type,
		int	printStatus
	)

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]

Definition at line 1802 of file fsmFsm.c.

{
  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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Fsm_MinimizeTransitionRelationWithReachabilityInfo	(	Fsm_Fsm_t *	fsm,
		Img_DirectionType	fwdbwd,
		boolean	verbosity
	)

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 []

Definition at line 2053 of file fsmFsm.c.

{
  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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fsm_Fsm_t* Fsm_NetworkReadFsm ( Ntk_Network_t * network )

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]

Definition at line 569 of file fsmFsm.c.

{
  return ((Fsm_Fsm_t*) Ntk_NetworkReadApplInfo(network,
                                               FSM_NETWORK_APPL_KEY));
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fsm_Fsm_t* Fsm_NetworkReadOrCreateFsm ( Ntk_Network_t * 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]

Definition at line 538 of file fsmFsm.c.

{
  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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

static void FsmCreateVariableCubes ( Fsm_Fsm_t * fsm ) [static]

Function********************************************************************

Synopsis [Allocates structure]

Description [Allocates structure]

SideEffects []

SeeAlso []

Definition at line 2482 of file fsmFsm.c.

{
  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);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void FsmGuidedSearchPrintOptions ( void )

Function********************************************************************

Synopsis [Prints all options that are related to guided search.]

Description [Prints all options that are related to guided search.]

SideEffects []

SeeAlso [CommandGuidedSearchOptions]

Definition at line 2392 of file fsmFsm.c.

{
  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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

FsmHdStruct_t* FsmHdStructAlloc ( int nvars )

Function********************************************************************

Synopsis [Allocates HD Info structure.]

Description [Allocates HD Info structure.]

SideEffects []

SeeAlso [Fsm_FsmHdStructFree]

Definition at line 2332 of file fsmFsm.c.

{
  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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void FsmHdStructFree ( FsmHdStruct_t * hdInfo )

Function********************************************************************

Synopsis [Frees HD info struct.]

Description [Frees HD info struct.]

SideEffects []

SeeAlso [Fsm_FsmHdStructAllocate]

Definition at line 2367 of file fsmFsm.c.

{
  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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fsm_RchType_t FsmReadReachabilityComputationMode ( Fsm_Fsm_t * fsm )

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 []

Definition at line 2267 of file fsmFsm.c.

{
  return fsm->reachabilityInfo.reachabilityMode;
}

Here is the caller graph for this function:

Fsm_Ardc_StatusType_t FsmReadReachabilityOverApproxComputationStatus ( Fsm_Fsm_t * fsm )

Function********************************************************************

Synopsis [Reads the status of overapproxiate reachable computation.]

Description [Reads the status of overapproxiate reachable computation.]

SideEffects []

SeeAlso []

Definition at line 2228 of file fsmFsm.c.

{
  return(fsm->reachabilityInfo.overApprox);
}

Here is the caller graph for this function:

void FsmResetReachabilityFields	(	Fsm_Fsm_t *	fsm,
		Fsm_RchType_t	approxFlag
	)

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 []

Definition at line 2286 of file fsmFsm.c.

{
  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 */

Here is the call graph for this function:

Here is the caller graph for this function:

void FsmSetReachabilityApproxComputationStatus	(	Fsm_Fsm_t *	fsm,
		Fsm_RchStatus_t	value
	)

Function********************************************************************

Synopsis [Sets whether reachability analysis was an approximation.]

Description [Sets whether reachability analysis was an approximation.]

SideEffects []

SeeAlso []

Definition at line 2192 of file fsmFsm.c.

{
  fsm->reachabilityInfo.rchStatus = value;
}

Here is the caller graph for this function:

void FsmSetReachabilityComputationMode	(	Fsm_Fsm_t *	fsm,
		Fsm_RchType_t	value
	)

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 []

Definition at line 2247 of file fsmFsm.c.

{
  fsm->reachabilityInfo.reachabilityMode = value;
}

Here is the caller graph for this function:

void FsmSetReachabilityOnionRings	(	Fsm_Fsm_t *	fsm,
		array_t *	onionRings
	)

Function********************************************************************

Synopsis [Sets array of onion rings from reachability computation]

Description [Sets array of onion rings from reachability computation.]

SideEffects []

SeeAlso [Fsm_FsmReadReachabilityOnionRings]

Definition at line 2138 of file fsmFsm.c.

{
  fsm->reachabilityInfo.onionRings = onionRings;
}

Here is the caller graph for this function:

void FsmSetReachabilityOnionRingsMode	(	Fsm_Fsm_t *	fsm,
		Fsm_RchType_t	value
	)

Function********************************************************************

Synopsis [Sets whether onion rings are due to BFS.]

Description [Sets whether onion rings are due to BFS.]

SideEffects []

SeeAlso [Fsm_FsmReadReachabilityOnionRingsMode]

Definition at line 2156 of file fsmFsm.c.

{
  fsm->reachabilityInfo.onionRingsMode = value;
}

Here is the caller graph for this function:

void FsmSetReachabilityOnionRingsUpToDateFlag	(	Fsm_Fsm_t *	fsm,
		boolean	value
	)

Function********************************************************************

Synopsis [Sets whether onion rings are up to date.]

Description [Sets whether onion rings are up to date.]

SideEffects []

SeeAlso [Fsm_FsmReachabilityOnionRingsUpToDate]

Definition at line 2174 of file fsmFsm.c.

{
  fsm->reachabilityInfo.onionRingsUpToDate = value;
}

Here is the caller graph for this function:

void FsmSetReachabilityOverApproxComputationStatus	(	Fsm_Fsm_t *	fsm,
		Fsm_Ardc_StatusType_t	status
	)

Function********************************************************************

Synopsis [Sets the status of overapproxiate reachable computation.]

Description [Sets the status of overapproxiate reachable computation.]

SideEffects []

SeeAlso []

Definition at line 2210 of file fsmFsm.c.

{
  fsm->reachabilityInfo.overApprox = status;
}

Here is the caller graph for this function:

static Fsm_Fsm_t * FsmStructAlloc	(	Ntk_Network_t *	network,
		graph_t *	partition
	)		`[static]`

AutomaticStart

Function********************************************************************

Synopsis [Allocates structure]

Description [Allocates structure]

SideEffects []

SeeAlso []

Definition at line 2426 of file fsmFsm.c.

{
  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 */

Here is the call graph for this function:

Here is the caller graph for this function:

static array_t * GetMddSupportIdArray	(	Fsm_Fsm_t *	fsm,
		st_table *	mddIdTable,
		st_table *	pseudoMddIdTable
	)		`[static]`

Function********************************************************************

Synopsis [Returns an array of mdd Ids of an FSM.]

Description [Returns an array of mdd Ids of an FSM.]

SideEffects []

SeeAlso []

Definition at line 2668 of file fsmFsm.c.

{
  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);
}

Here is the call graph for this function:

Here is the caller graph for this function:

static int nameCompare	(	const void *	name1,
		const void *	name2
	)		`[static]`

Function********************************************************************

Synopsis [Compare procedure for name comparison.]

Description [Compare procedure for name comparison.]

SideEffects []

Definition at line 2539 of file fsmFsm.c.

{
    return(strcmp(*(char **)name1, *(char **)name2));

} /* end of signatureCompare */

Here is the caller graph for this function:

static boolean NSFunctionNamesCompare	(	mdd_manager *	mddMgr,
		array_t *	names1,
		array_t *	names2
	)		`[static]`

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]

Definition at line 2594 of file fsmFsm.c.

{
  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 */

Here is the caller graph for this function:

static boolean VarIdArrayCompare	(	mdd_manager *	mddMgr,
		array_t *	vars1,
		array_t *	vars2
	)		`[static]`

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]

Definition at line 2561 of file fsmFsm.c.

{
  
  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 */

Here is the caller graph for this function:

Variable Documentation

char rcsid [] UNUSED = "$Id: fsmFsm.c,v 1.88 2007/04/02 17:03:13 hhkim Exp $" [static]

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]

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Definition at line 34 of file fsmFsm.c.

src/fsm/fsmFsm.c File Reference

Functions

Variables

Function Documentation

Variable Documentation