/**CFile***********************************************************************

  FileName    [eqvVerify.c]

  PackageName [eqv]

  Synopsis    [This file contains the two routines which do combinational and
  sequential verification.]

  Description []

  SeeAlso     []

  Author      [Shaz Qadeer]

  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 "eqvInt.h"

static char rcsid[] UNUSED = "$Id: eqvVerify.c,v 1.10 2009/04/11 01:40:06 fabio Exp $";

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/


/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [This function does combinational verification between network1
  and network2.]

  Description [roootsMap and leavesMap contain corresponding nodes in network1
  and network2. It is assumed that the set of leaf nodes forms a complete
  support of the set of root nodes in both the networks. This function
  verifies the combinational equivalence of corresponding roots in terms of
  the leaves. method1 and method2 specify the partition methods to be used for
  partitioning network1 and network2 respectively. AssignCommonOrder is a
  pointer to a function which takes two networks, whose mdd managers are
  identical, and a hash table containing corresponding leaf nodes whose mdd Id
  should be the same. AssignCommonOrder() orders the two networks ensuring
  that identical mddIds are assigned to the corresponding leaf nodes in the
  hash table. This function has to be supplied by the user.

  This function returns TRUE if all the root pairs are combinationally
  equivalent otherwise it returns FALSE. It is assumed that network1 already
  has a mdd manager. If a partition is registered with network1, and it has
  vertices corresponding to the specified roots and leaves it is used
  otherwise a new partition is created. A new partition is always created for
  network2.]

  SideEffects []

******************************************************************************/
boolean
Eqv_NetworkVerifyCombinationalEquivalence(
  Ntk_Network_t *network1,
  Ntk_Network_t *network2,
  st_table *leavesMap,  /* the mapping between the inputs of the networks;
			 * hash table from Ntk_Node_t * to Ntk_Node_t * */
  st_table *rootsMap,   /* the mapping between the outputs of the networks;
			 * hash table from Ntk_Node_t * to Ntk_Node_t * */
  OFT AssignCommonOrder,
  Part_PartitionMethod method1,
  Part_PartitionMethod method2)
{
  mdd_manager *mddMgr;
  lsList leavesList1, leavesList2;
  lsList rootsList1, rootsList2;
  st_table *leaves1, *leaves2;
  array_t *roots1, *roots2;
  st_generator *gen;
  lsGen listGen;
  graph_t *rootsToLeaves1, *rootsToLeaves2;
  Ntk_Node_t *node1, *node2;
  char *name1, *name2, *name;
  Mvf_Function_t *func1, *func2;
  int num, i, j;
  array_t *mvfRoots1, *mvfRoots2;
  boolean equivalent = TRUE;
  lsList dummy = (lsList) 0;
  int mddId1, mddId2;
  vertex_t *vertex;
  lsGeneric data;
  boolean partValid = FALSE;
  mdd_manager *mgr;
  int mddId;
  array_t *mddIdArray;
  mdd_t *aMinterm, *diff;
  char *mintermName;
  mdd_t *comp1, *comp2;
  int numComponents;

  /* First check whether a partition is registered with network1 */
  if(Ntk_NetworkReadApplInfo(network1, PART_NETWORK_APPL_KEY) != NIL(void)) {
    /*
     * Check whether the registered partition can be used to compute the roots
     * in terms of the leaves. If it can be used, then i won't create a new
     * one.
     */
    partValid = TestPartitionIsValid(network1, rootsMap, leavesMap);
    /*
     * If a partition already exists, an mddManager also exists.
     * So, don't allocate a new one.
     */
    mddMgr = Ntk_NetworkReadMddManager(network1);
  }
  else {
    mddMgr = Ntk_NetworkInitializeMddManager(network1);
  }
  assert(mddMgr != NIL(mdd_manager));
  Ntk_NetworkSetMddManager(network2, mddMgr);
  (*AssignCommonOrder)(network1, network2, leavesMap);

  /* Create lists of leaves and roots for creating partitions. */
  leavesList1 = lsCreate();
  leavesList2 = lsCreate();
  st_foreach_item(leavesMap, gen, &node1, &node2) {
    mddId1 = Ntk_NodeReadMddId(node1);
    mddId2 = Ntk_NodeReadMddId(node2);
    assert(mddId1 == mddId2);
    lsNewEnd(leavesList1, (lsGeneric) node1, LS_NH);
    lsNewEnd(leavesList2, (lsGeneric) node2, LS_NH);
  }

  rootsList1 = lsCreate();
  rootsList2 = lsCreate();
  st_foreach_item(rootsMap, gen, &node1, &node2) {
    lsNewEnd(rootsList1, (lsGeneric) node1, LS_NH);
    lsNewEnd(rootsList2, (lsGeneric) node2, LS_NH);
  }

  if(partValid) {
    rootsToLeaves1 = Part_NetworkReadPartition(network1);
  }
  else {
    rootsToLeaves1 = Part_NetworkCreatePartition(network1, NIL(Hrc_Node_t),
						 "dummy", rootsList1,
						 leavesList1, NIL(mdd_t),
						 method1, dummy,
						 FALSE, FALSE, TRUE);
  }

  /*
   * Generate arrays of root and leaf vertices in the first partition
   * to pass as arguments to Part_PartitionCollapse().
   */
  roots1 = array_alloc(vertex_t *, 0);
  lsForEachItem(rootsList1, listGen, data) {
    name = Ntk_NodeReadName((Ntk_Node_t *) data);
    vertex = Part_PartitionFindVertexByName(rootsToLeaves1, name);
    assert(vertex != NIL(vertex_t));
    array_insert_last(vertex_t *, roots1, vertex);
  }
  leaves1 = st_init_table(st_ptrcmp, st_ptrhash);
  lsForEachItem(leavesList1, listGen, data) {
    name = Ntk_NodeReadName((Ntk_Node_t *) data);
    vertex = Part_PartitionFindVertexByName(rootsToLeaves1, name);
/*    assert(vertex != NIL(vertex_t)); */
    if(vertex != NIL(vertex_t)) {
      /*
       * If a leaf is not actually in the support of the roots then
       * it will not be present in the partition.
       */
      mddId = Part_VertexReadMddId(vertex);
      st_insert(leaves1, (char *) vertex, (char *) (long) mddId);
    }
  }

  lsDestroy(rootsList1, (void (*) (lsGeneric)) 0);
  lsDestroy(leavesList1, (void (*) (lsGeneric)) 0);
  rootsToLeaves2 = Part_NetworkCreatePartition(network2, NIL(Hrc_Node_t),
					       "dummy", rootsList2,
					       leavesList2, NIL(mdd_t),
					       method2, dummy, FALSE,
					       FALSE, TRUE);

  /*
   * Generate arrays of root and leaf vertices in the second partition
   * to pass as arguments to Part_PartitionCollapse().
   */
  roots2 = array_alloc(vertex_t *, 0);
  lsForEachItem(rootsList2, listGen, data) {
    name = Ntk_NodeReadName((Ntk_Node_t *) data);
    vertex = Part_PartitionFindVertexByName(rootsToLeaves2, name);
    assert(vertex != NIL(vertex_t));
    array_insert_last(vertex_t *, roots2, vertex);
  }
  leaves2 = st_init_table(st_ptrcmp, st_ptrhash);
  lsForEachItem(leavesList2, listGen, data) {
    name = Ntk_NodeReadName((Ntk_Node_t *) data);
    vertex = Part_PartitionFindVertexByName(rootsToLeaves2, name);
/*    assert(vertex != NIL(vertex_t)); */
    if(vertex != NIL(vertex_t)) {
      /*
       * If a leaf is not actually in the support of the roots then
       * it will not be present in the partition.
       */
      mddId = Part_VertexReadMddId(vertex);
      st_insert(leaves2, (char *) vertex, (char *) (long) mddId);
    }
  }
  lsDestroy(rootsList2, (void (*) (lsGeneric)) 0);
  lsDestroy(leavesList2, (void (*) (lsGeneric)) 0);
  assert(Part_PartitionReadMddManager(rootsToLeaves1) ==
	 Part_PartitionReadMddManager(rootsToLeaves2));

  mvfRoots1 = Part_PartitionCollapse(rootsToLeaves1, roots1, leaves1, NIL(mdd_t));
  mvfRoots2 = Part_PartitionCollapse(rootsToLeaves2, roots2, leaves2, NIL(mdd_t));

  assert(array_n(mvfRoots1) == array_n(mvfRoots2));
  num = array_n(mvfRoots1);
  mddIdArray = array_alloc(int, 0);
  st_foreach_item_int(leaves1, gen, &vertex, &mddId) {
    array_insert_last(int, mddIdArray, mddId);
  }

  /*
   * For each pair of corresponding outputs in the two arrays mvfRoots1 and
   * mvfRoots2, I will compute the mdd representing all the input combinations
   * for which they are different. For each pair, I will print one input
   * combination for which they are different.
   */

  for(i = 0; i<num; ++i) {
    func1 = array_fetch(Mvf_Function_t *, mvfRoots1, i);
    func2 = array_fetch(Mvf_Function_t *, mvfRoots2, i);
    if(!Mvf_FunctionTestIsEqualToFunction(func1, func2)) {
      mgr = Mvf_FunctionReadMddManager(func1);
      assert(mgr == Mvf_FunctionReadMddManager(func2));
      numComponents = Mvf_FunctionReadNumComponents(func1);
      for(j=0; j<numComponents; ++j) {
	comp1 = Mvf_FunctionReadComponent(func1, j);
	comp2 = Mvf_FunctionReadComponent(func2, j);
	diff = mdd_xor(comp1, comp2);
	if(!mdd_is_tautology(diff, 0)) {
	  aMinterm = Mc_ComputeAMinterm(diff, mddIdArray, mddMgr);
	  mintermName = Mc_MintermToString(aMinterm, mddIdArray, network1);
	  vertex = array_fetch(vertex_t *, roots1, i);
	  name1 = Part_VertexReadName(vertex);
	  vertex = array_fetch(vertex_t *, roots2, i);
	  name2 = Part_VertexReadName(vertex);
	  (void) fprintf(vis_stdout, "%s from network1 and %s from network2 differ on input values\n%s",
			 name1, name2, mintermName);
	  FREE(mintermName);
	  mdd_free(aMinterm);
	  mdd_free(diff);
	  break;
	}
	mdd_free(diff);
      }
      equivalent = FALSE;
    }
  }
  array_free(mddIdArray);
  if(!partValid) {
    Part_PartitionFree(rootsToLeaves1);
  }
  Part_PartitionFree(rootsToLeaves2);
  array_free(roots1);
  array_free(roots2);
  st_free_table(leaves1);
  st_free_table(leaves2);
  arrayForEachItem(Mvf_Function_t *, mvfRoots1, i, func1) {
    Mvf_FunctionFree(func1);
  }
  array_free(mvfRoots1);
  arrayForEachItem(Mvf_Function_t *, mvfRoots2, i, func2) {
    Mvf_FunctionFree(func2);
  }
  array_free(mvfRoots2);
  Ntk_NetworkSetMddManager(network2, NIL(mdd_manager));
  /*
   * This is needed because Ntk_NetworkFree() will be called on both network1
   * and network2.
   */
  return equivalent;
}

/**Function********************************************************************

  Synopsis    [This function does sequential verification between network1 and
  network2.]

  Description [It accepts as input the two networks, and two hash tables of
  node names - rootsTable and leavesTable. leavesTable gives the names of
  corresponding primary inputs in the two networks. If leavesTable is NULL,
  the inputs are simply matched by names. rootsTable gives the names of
  corresponding nodes in the two networks whose sequential equivalence has to
  be verified. If rootsTable is NULL, it is assumed that all the
  primary outputs need to be verified and that they are to be associated by
  names. The function returns TRUE if the all the corresponding nodes are
  sequentially equivalent otherwise it returns FALSE. The verification is done
  by appending network1 to network2, thereby forming the product machine. A
  set of states in which the corresponding outputs to be verified are
  different for some input is calculated and it is checked whether any of
  these states is reachable from an initial state of the product machine.]

  SideEffects [network2 is modified in this function.]

******************************************************************************/
boolean
Eqv_NetworkVerifySequentialEquivalence(
  Ntk_Network_t *network1,
  Ntk_Network_t *network2,
  st_table *rootsTable,    /* the mapping between the outputs of the networks;
			    * hash table from char * to char * */
  st_table *leavesTable,   /* the mapping between the inputs of the networks;
			    * hash table from char * to char * */
  Part_PartitionMethod partMethod,
  boolean useBackwardReach,
  boolean reordering)
{
  array_t *roots;
  st_table *leaves;
  lsList rootsList;
  lsList rootsPartList = (lsList) 0;
  st_table *outputMap = NIL(st_table);
  Ntk_Node_t *node1, *node2, *node;
  char *name1, *name2, *temp;
  st_generator *gen;
  lsGen listGen;
  graph_t *partition;
  vertex_t *vertex;
  mdd_manager *mddMgr;
  array_t *mvfArray;
  Mvf_Function_t *mvf1, *mvf2;
  mdd_t *badStates, *initialStates;
  mdd_t *mddTemp, *mdd1, *mdd2, *tautology;
  mdd_t *mddComp1, *mddComp2;
  int n, i, j, numComponents;
  int id;
  array_t *inputIdArray;
  lsList dummy = (lsList) 0;
  lsGeneric data;
  Ntk_Node_t *input;
  Fsm_Fsm_t *modelFsm;
  array_t *onionRings;
  array_t *aPath;
  boolean inequivalent;
  boolean rootsFlag = (rootsTable == NIL(st_table)) ? FALSE : TRUE;
  array_t *careStatesArray = array_alloc(mdd_t *, 0);

  /* If rootsFlag is FALSE, all primary outputs are to be verified */
  if(rootsFlag == FALSE) {
    outputMap = MapPrimaryOutputsByName(network1, network2);
  }

  /*
   * If leavesFlag is FALSE, the primary inputs in the two networks are
   * assumed to have same names. In the network returned by
   * Ntk_NetworkAppendNetwork(), the two corresponding nodes will be merged.
   * If leavesFlag is TRUE, the name correspondence between the primary inputs
   * in the two networks is specified in leavesTable.
   */
  if(leavesTable == NIL(st_table)) {
    st_table *emptyTable = st_init_table(strcmp, st_strhash);
    Ntk_NetworkAppendNetwork(network2, network1, emptyTable);
    st_free_table(emptyTable);
  }
  else {
    Ntk_NetworkAppendNetwork(network2, network1, leavesTable);
  }

  /*
   * network1 has been appended to the erstwhile network2, and the new network
   * is now called network2.
   */

  mddMgr = Ntk_NetworkInitializeMddManager(network2);

  Ord_NetworkOrderVariables(network2, Ord_RootsByDefault_c,
			    Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c,
			    Ord_Unassigned_c, dummy, FALSE);

  if (reordering)
    Ntk_NetworkSetDynamicVarOrderingMethod(network2, BDD_REORDER_SIFT,
					   BDD_REORDER_VERBOSITY);
  /*
   * Ntk_NetworkAppendNetwork() adds $NTK2 to the names of all the
   * appended nodes. I want to find the appended nodes in new network2
   * corresponding to the roots in network1. I will add all these nodes to
   * rootsList. I will also add all the roots of the erstwhile network2, which
   * exist in the network2 also. rootsList will finally contain all the nodes
   * in network2 whose mdds have to be created by Part_Partition Collapse().
   */

  rootsList = lsCreate();
  if(rootsFlag == FALSE) {
    st_foreach_item(outputMap, gen, &node1, &node2) {
      name1 = Ntk_NodeReadName(node1);
      temp = util_strcat3(name1, "$NTK2", "");
      name1 = temp;
      node1 = Ntk_NetworkFindNodeByName(network2, name1);
      assert(node1 != NIL(Ntk_Node_t));
      FREE(name1);
      lsNewEnd(rootsList, (lsGeneric) node1, LS_NH);
      lsNewEnd(rootsList, (lsGeneric) node2, LS_NH);
    }
  }
  else {
    st_foreach_item(rootsTable, gen, &name1, &name2) {
      /* I am finding the node in the new network2 */
      temp = util_strcat3(name1, "$NTK2", "");
      name1 = temp;
      node1 = Ntk_NetworkFindNodeByName(network2, name1);
      FREE(name1);
      lsNewEnd(rootsList, (lsGeneric) node1, LS_NH);
      node2 = Ntk_NetworkFindNodeByName(network2, name2);
      lsNewEnd(rootsList, (lsGeneric) node2, LS_NH);
    }
  }
  if(outputMap) {
    st_free_table(outputMap);
  }
  /* rootsPartList is the list of nodes which will passed to
   * Part_NetworkCreatePartition(). I want all the next state functions i.e.
   * latch data inputs as well as everything in rootsList to be in
   * rootsPartList. If rootsFlag is FALSE, rootsPartList is simply passed as
   * (lsList) 0.
   */
  if(rootsFlag) {
    rootsPartList = lsCreate();
    Ntk_NetworkForEachCombOutput(network2, listGen, node) {
      if(Ntk_NodeTestIsLatchDataInput(node) ||
	 Ntk_NodeTestIsLatchInitialInput(node)){
	lsNewEnd(rootsPartList, (lsGeneric) node, LS_NH);
      }
    }
    lsForEachItem(rootsList, listGen, node) {
      if(!Ntk_NodeTestIsLatchDataInput(node) &&
	 !Ntk_NodeTestIsLatchInitialInput(node)) {
	lsNewEnd(rootsPartList, (lsGeneric) node, LS_NH);
      }
    }
  }
  partition = Part_NetworkCreatePartition(network2, NIL(Hrc_Node_t), "dummy",
					  rootsPartList,
					  (lsList) 0, NIL(mdd_t), partMethod,
					  dummy, FALSE, FALSE, TRUE);

  Ntk_NetworkAddApplInfo(network2, PART_NETWORK_APPL_KEY,
			 (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
			 (void *) partition);
  if(rootsPartList) {
    lsDestroy(rootsPartList, (void (*) (lsGeneric)) 0);
  }
  /* Create roots and leaves for Part_PartitionCollapse().
   */
  roots = array_alloc(vertex_t *, 0);
  lsForEachItem(rootsList, listGen, data) {
    name1 = Ntk_NodeReadName((Ntk_Node_t *) data);
    vertex = Part_PartitionFindVertexByName(partition, name1);
    assert(vertex != NIL(vertex_t));
    array_insert_last(vertex_t *, roots, vertex);
  }
  lsDestroy(rootsList, (void (*) (lsGeneric)) 0);
  leaves = st_init_table(st_ptrcmp, st_ptrhash);
  Ntk_NetworkForEachCombInput(network2, listGen, node1) {
    name1 = Ntk_NodeReadName(node1);
    vertex = Part_PartitionFindVertexByName(partition, name1);
    if(vertex != NIL(vertex_t)) {
      /* A combinational input might not be present in the support of any
	 node in rootsPartList. If so, it will not be present in the partition
	 also. */
      st_insert(leaves, (char *) vertex, (char *) (long) 0);
    }
  }
  mvfArray = Part_PartitionCollapse(partition, roots, leaves, NIL(mdd_t));
  array_free(roots);
  st_free_table(leaves);
  n = array_n(mvfArray);
  assert(n%2 == 0);
  n = n/2;
  assert(mddMgr != NULL);

/* In mvfArray, the mvfs of corresponding nodes occur one after the other,
   * because of the way rootsList was created. badStates will ultimately
   * contain all the states for which  any pair of corresponding nodes differ
   * for some input.
   */
  badStates = mdd_zero(mddMgr);
  for(i=0; i<n; i++) {
    mvf1 = array_fetch(Mvf_Function_t *, mvfArray, 2*i);
    mvf2 = array_fetch(Mvf_Function_t *, mvfArray, 2*i +1);
    numComponents = Mvf_FunctionReadNumComponents(mvf1);
    mdd2 = mdd_zero(mddMgr);
    /*
     * Hopefully, mddMgr of the partition is the same as the mddMgr of the
     * MVFs.
     */
    for(j=0; j<numComponents; j++) {
      mddComp1 = Mvf_FunctionObtainComponent(mvf1, j);
      mddComp2 = Mvf_FunctionObtainComponent(mvf2, j);
      mdd1 = mdd_and(mddComp1, mddComp2, 1, 1);
      mdd_free(mddComp1);
      mdd_free(mddComp2);
      mddTemp = mdd_or(mdd2, mdd1, 1, 1);
      mdd_free(mdd1);
      mdd_free(mdd2);
      mdd2 = mddTemp;
    }

   /*
    * At this point, mdd2 represents the set of input and present state
    * combinations in which mvf1 and mvf2 produce the same value. I want the
    * set for which mvf1 and mvf2 are different.
    */
    mddTemp = mdd_or(badStates, mdd2, 1, 0);
    mdd_free(mdd2);
    mdd_free(badStates);
    badStates = mddTemp;
  }
  arrayForEachItem(Mvf_Function_t *, mvfArray, i, mvf1) {
    Mvf_FunctionFree(mvf1);
  }
  array_free(mvfArray);
  /* existentially quantify out the input variables */
  inputIdArray = array_alloc(int, 0);

  Ntk_NetworkForEachPrimaryInput(network2, listGen, input) {
    id = Ntk_NodeReadMddId(input);
    assert(id >= 0);
    array_insert_last(int, inputIdArray, id);
  }

  mddTemp = mdd_smooth(mddMgr, badStates, inputIdArray);
  mdd_free(badStates);
  badStates = mddTemp;
  array_free(inputIdArray);
  modelFsm = Fsm_FsmCreateFromNetworkWithPartition(network2, NIL(graph_t));
  assert(modelFsm != NIL(Fsm_Fsm_t));
  Ntk_NetworkAddApplInfo(network2, FSM_NETWORK_APPL_KEY,
			 (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
			 (void *) modelFsm);

  onionRings = array_alloc(mdd_t *, 0);
  initialStates = Fsm_FsmComputeInitialStates(modelFsm);
  tautology = mdd_one(mddMgr);

  /* Model checking function */
  if (useBackwardReach == TRUE) {
    array_insert(mdd_t *, careStatesArray, 0, tautology);
    inequivalent = Mc_FsmComputeStatesReachingToSet(modelFsm, badStates,
			careStatesArray, initialStates,
			onionRings, McVerbosityNone_c, McDcLevelNone_c);
    array_free(careStatesArray);
    mdd_free(badStates);
    mdd_free(tautology);

    if (inequivalent) {
      mdd_t *outerOnionRing = array_fetch_last(mdd_t *, onionRings);
      mdd_t *badInitialStates = mdd_and(initialStates, outerOnionRing, 1, 1);
      array_t *psVarMddIdArray = Fsm_FsmReadPresentStateVars(modelFsm);
      mdd_t *aBadInitialState = Mc_ComputeAMinterm(initialStates, psVarMddIdArray, mddMgr);
      mdd_free(badInitialStates);
      aPath = Mc_BuildPathToCore(aBadInitialState, onionRings, modelFsm,
				 McGreaterOrEqualZero_c);
      (void) Mc_PrintPath(aPath, modelFsm, TRUE); /* TRUE -> print inputs on path */
      mdd_free(aBadInitialState);
      mdd_free(initialStates);
      mdd_array_free(aPath);
      mdd_array_free(onionRings);
      return FALSE;
    }
    else {
      mdd_free(initialStates);
      return TRUE;
    }
  }
  else { /* do forward search */
    array_insert(mdd_t *, careStatesArray, 0, tautology);
    inequivalent = Mc_FsmComputeStatesReachableFromSet(modelFsm, initialStates,
			careStatesArray, badStates, onionRings,
			McVerbosityNone_c, McDcLevelNone_c);
    array_free(careStatesArray);
    mdd_free(tautology);
    mdd_free(initialStates);

    if (inequivalent) {
      mdd_t *outerOnionRing = array_fetch_last(mdd_t *, onionRings);
      mdd_t *reachableBadStates = mdd_and(badStates, outerOnionRing, 1, 1);
      array_t *psVarMddIdArray = Fsm_FsmReadPresentStateVars(modelFsm);
      mdd_t *aBadReachableState = Mc_ComputeAMinterm(reachableBadStates, psVarMddIdArray, mddMgr);
      mdd_free(reachableBadStates);
      psVarMddIdArray = Fsm_FsmReadPresentStateVars(modelFsm);
      aPath = Mc_BuildPathFromCore(aBadReachableState, onionRings, modelFsm,
				 McGreaterOrEqualZero_c);
      (void) Mc_PrintPath(aPath, modelFsm, TRUE); /* TRUE -> print inputs on path */
      mdd_free(aBadReachableState);
      mdd_free(badStates);
      mdd_array_free(aPath);
      mdd_array_free(onionRings);
      return FALSE;
    }
    else {
      mdd_free(badStates);
      return TRUE;
    }
  }
}

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/