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

  FileName    [mcDnC.c]

  PackageName [mc]

  Synopsis    [The Divide and Compose (D'n'C) Approach of SCC Enumeration.]

  Description [This file contains the functions to compute the fair
  Strongly Connected Components (SCCs) of the state translation graph
  of an FSM by Divide and Compose.  Knowledge of the fair SCCs can be
  used to decide language emptiness.  For more information, please
  check the CONCUR'01 paper of Wang et al., "Divide and Compose: SCC
  refinement for language emptiness." Other applications are also
  possible.]

  SeeAlso     []

  Author      [Chao Wang]

  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
  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.]

******************************************************************************/
#include "mcInt.h"

static char rcsid[] UNUSED = "$Id: mcDnC.c,v 1.9 2005/05/18 18:12:00 jinh Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

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

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/
static int SccIsStrong(mdd_manager *mddMgr, array_t *buechiFairness, mdd_t *SCC);
static array_t * SortMddArrayBySize(Fsm_Fsm_t *fsm, array_t *mddArray);
static int stringCompare(const void * s1, const void * s2);
/**AutomaticEnd***************************************************************/


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

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

  Synopsis [Compute all the states that lead to a fair cycle by
  Compositional SCC analysis (DnC -- Divide and Compose).]

  Comment [Used by LE/LTL/CTL* model checking. The Divide and Compose
  (D'n'C) approach is used for the symbolic SCC enumeration, which
  first creates SCC-closed sets on an abstract model and then
  successively refines these sets on the refined abstract models,
  until either no fair SCC exists or the concrete (original) model is
  reached.

  Strength reduction is also applied during the process -- as soon as
  the SCC-closed sets become weak/terminal, special decision
  procedures will be used to determine their language emptiness.

  For more information, please check the CONCUR'01 paper of Wang et
  al., "Divide and Compose: SCC refinement for language emptiness."
  
  Debugging information will be print out if dbgLevel is non-zero.

  Return the set of initial states from where fair paths exist.]
  
  SideEffects []

******************************************************************************/
mdd_t *
Mc_FsmCheckLanguageEmptinessByDnC(
  Fsm_Fsm_t *modelFsm,
  array_t *modelCareStates,
  Mc_AutStrength_t automatonStrength,
  int dcLevel,
  int dbgLevel,
  int printInputs,
  int verbosity,
  Mc_GSHScheduleType GSHschedule,
  Mc_FwdBwdAnalysis GSHdirection,
  int lockstep,
  FILE *dbgFile,
  int UseMore,
  int SimValue,
  char *driverName)
{
  Ntk_Network_t   *network = Fsm_FsmReadNetwork(modelFsm);
  mdd_manager     *mddManager = Fsm_FsmReadMddManager(modelFsm);
  Fsm_Fairness_t  *modelFairness = NIL(Fsm_Fairness_t);
  array_t         *buechiFairness = NIL(array_t);
  int             isExactReachableStatesAvailable = 0;
  mdd_t           *reachableStates, *initialStates = NIL(mdd_t);
  mdd_t           *fairStates, *fairInitialStates = NIL(mdd_t);
  array_t         *onionRings = NIL(array_t);
  array_t         *strongSccClosedSets = NIL(array_t);
  array_t         *absLatchNameTableArray = NIL(array_t);
  int             numOfAbstractModels, iter, i, exitFlag;
  array_t         *arrayOfOnionRings = NIL(array_t);
  array_t         *ctlArray = array_alloc(Ctlp_Formula_t *, 0);
  array_t         *modelCareStatesArray = mdd_array_duplicate(modelCareStates);
  Mc_SccGen_t     *sccgen;
  int             composeIncSize, numOfLatches, maxLatchesToCompose;

  int             maxComposePercentage = 30;
  int             maxSccsToEnum = 100;


  /*
   * Read fairness constraints.
   */
  modelFairness = Fsm_FsmReadFairnessConstraint(modelFsm);
  buechiFairness = array_alloc(mdd_t *, 0);
  if (modelFairness != NIL(Fsm_Fairness_t)) {
    if (!Fsm_FairnessTestIsBuchi(modelFairness)) {
      (void) fprintf(vis_stdout, 
		     "** non-Buechi fairness constraints not supported\n");
      array_free(buechiFairness);
      assert(0);
    } else {
      int j;
      int numBuchi = Fsm_FairnessReadNumConjunctsOfDisjunct(modelFairness, 0);
      for (j = 0; j < numBuchi; j++) {
	Ctlp_Formula_t *tmpFormula;
	mdd_t *tempMdd;
	tmpFormula = Fsm_FairnessReadFinallyInfFormula(modelFairness, 0, j );
	tempMdd = Fsm_FairnessObtainFinallyInfMdd(modelFairness, 0, j,
						  modelCareStatesArray, 
						  (Mc_DcLevel) dcLevel);
	array_insert_last(mdd_t *, buechiFairness, tempMdd);
        array_insert_last( Ctlp_Formula_t *, ctlArray, 
			   Ctlp_FormulaDup(tmpFormula));
#if 1
	fprintf(vis_stdout,"\nFairness[%d]:",j);
	Ctlp_FormulaPrint(vis_stdout, tmpFormula);
	fprintf(vis_stdout,"\n");
#endif
      }
    }
  } else {
    array_insert_last(mdd_t *, buechiFairness, mdd_one(mddManager));
  }

  /*
   * If we need debugging information, arrayOfOnionRings != NIL(array_t), 
   */
  if (dbgLevel != McDbgLevelNone_c)
    arrayOfOnionRings = array_alloc(array_t *, 0);
  else
    arrayOfOnionRings = NIL(array_t);

  /* 
   * If exact/approximate reachable states are available, use them.
   */
  initialStates = Fsm_FsmComputeInitialStates(modelFsm);
  reachableStates = Fsm_FsmReadReachableStates(modelFsm);
  isExactReachableStatesAvailable = (reachableStates != NIL(mdd_t));
  if (!isExactReachableStatesAvailable) 
    reachableStates = McMddArrayAnd(modelCareStatesArray);
  else
    reachableStates = mdd_dup(reachableStates);
  onionRings = Fsm_FsmReadReachabilityOnionRings(modelFsm);
  if (onionRings == NIL(array_t)) {
    onionRings = array_alloc(mdd_t *, 0);
    array_insert(mdd_t *, onionRings, 0, mdd_dup(reachableStates));
  }else
    onionRings = mdd_array_duplicate(onionRings);

  strongSccClosedSets = array_alloc(mdd_t *, 0);
  array_insert(mdd_t *, strongSccClosedSets, 0, mdd_dup(reachableStates));

  /*
   * Compute a series of over-approximated abstract models
   */
  numOfLatches = array_n(Fsm_FsmReadPresentStateVars(modelFsm));
  maxLatchesToCompose = (numOfLatches * maxComposePercentage/100);
  maxLatchesToCompose = (maxLatchesToCompose > 20)? maxLatchesToCompose:20;
  composeIncSize = maxLatchesToCompose/10;
  composeIncSize = (composeIncSize > 4)? composeIncSize:4;

  absLatchNameTableArray = 
    Mc_CreateStaticRefinementScheduleArray(network,
					   ctlArray,
					   NIL(array_t),
					   NIL(array_t),
					   FALSE,
					   FALSE,
					   ((verbosity<McVerbosityMax_c)?
					    0:McVerbositySome_c),
					   composeIncSize,
					   Part_CorrelationWithSupport);
  numOfAbstractModels = (array_n(absLatchNameTableArray) - 1);
  if (verbosity >= McVerbosityLittle_c) {
    fprintf(vis_stdout, 
	    "-- DnC: scheduled total %d abs models with %d latches\n",
	    numOfAbstractModels, numOfLatches);
  }

  if (verbosity >= McVerbositySome_c) {
    fprintf(vis_stdout, "-- DnC:\n");
    fprintf(vis_stdout, 
	    "-- DnC: maxComposePercentage = %d\n", maxComposePercentage);
    fprintf(vis_stdout, 
	    "-- DnC: numOfLatches         = %d\n", numOfLatches);
    fprintf(vis_stdout, 
	    "-- DnC: composeIncSize       = %d\n", composeIncSize);
    fprintf(vis_stdout, 
	    "-- DnC: numOfAbstractModels  = %d\n", numOfAbstractModels);
    fprintf(vis_stdout, 
	    "-- DnC: maxLatchesToCompose  = %d\n", maxLatchesToCompose);
    fprintf(vis_stdout, 
	    "-- DnC: maxSccsToEnum        = %d\n", maxSccsToEnum);
    fprintf(vis_stdout, "-- Dnc: \n");
  }

  exitFlag = 0;
  for (iter=0; iter<numOfAbstractModels; iter++) {
    Fsm_Fsm_t *absFsm = NIL(Fsm_Fsm_t);
    st_table  *absLatchNameTable = NIL(st_table);
    array_t   *absOnionRings;
    array_t   *tempArray = NIL(array_t);
    mdd_t     *sccClosedSet = NIL(mdd_t);
    mdd_t     *tempMdd = NIL(mdd_t);
    mdd_t     *absReachableStates = NIL(mdd_t);

    absLatchNameTable = array_fetch(st_table *, absLatchNameTableArray, iter);
    absFsm = Fsm_FsmCreateSubsystemFromNetwork(network, NIL(graph_t),
					       absLatchNameTable, TRUE, 1);

    if (!isExactReachableStatesAvailable) {
      absReachableStates = Fsm_FsmComputeReachableStates(absFsm, 0, 0, 0, 0,
							 1, 0, 0,
							 Fsm_Rch_Default_c, 
							 0, 0,
							 NIL(array_t), FALSE,
							 NIL(array_t));
      absOnionRings = Fsm_FsmReadReachabilityOnionRings(absFsm);
      assert(absOnionRings);
      absOnionRings = mdd_array_duplicate(absOnionRings);
    }else {
      absReachableStates = McComputeAbstractStates(absFsm, reachableStates);
      absOnionRings = array_alloc(mdd_t *, array_n(onionRings));
      arrayForEachItem(mdd_t *, onionRings, i, tempMdd) {
	array_insert(mdd_t *, absOnionRings, i, 
		     McComputeAbstractStates(absFsm, tempMdd) );
      }
    }

    tempArray = strongSccClosedSets;
    strongSccClosedSets = array_alloc(mdd_t *, 0);
    arrayForEachItem(mdd_t *, tempArray, i, sccClosedSet) {
      sccClosedSet = (iter == 0)? 
	McComputeAbstractStates(absFsm, sccClosedSet): mdd_dup(sccClosedSet);
      tempMdd = mdd_and(sccClosedSet, absReachableStates, 1, 1);
      if (mdd_is_tautology(tempMdd, 0)) 
	mdd_free(tempMdd);
      else
	array_insert_last(mdd_t *, strongSccClosedSets, tempMdd);
      mdd_free(sccClosedSet);
    }
    mdd_array_free(tempArray);

    /* Refine SCC-closed sets, but up to a certain number */
    tempArray = strongSccClosedSets;
    strongSccClosedSets = array_alloc(mdd_t *, 0);
    Mc_FsmForEachFairScc(absFsm, sccgen, sccClosedSet, tempArray, 
			 strongSccClosedSets, /* new scc-closed sets */
			 buechiFairness, absOnionRings, FALSE,
			 ((verbosity<McVerbosityMax_c)?
			  McVerbosityNone_c:McVerbositySome_c),
			 (Mc_DcLevel) dcLevel) {
      if (SccIsStrong(mddManager, buechiFairness, sccClosedSet)) {
	array_insert_last(mdd_t *, strongSccClosedSets, sccClosedSet);
	if (maxSccsToEnum>0 && array_n(strongSccClosedSets)>maxSccsToEnum) {
	  Mc_FsmSccGenFree(sccgen, strongSccClosedSets);
	  break;
	}

      }else {
	array_t  *newCareStatesArray;
	newCareStatesArray = mdd_array_duplicate(modelCareStatesArray);
	if (!isExactReachableStatesAvailable) 
	  array_insert_last(mdd_t *, newCareStatesArray, absReachableStates);

	if (verbosity >= McVerbositySome_c) 
	  fprintf(vis_stdout, "-- DnC: search in a weak SCC-closed set\n");

	fairStates = McFsmRefineWeakFairSCCs(modelFsm, sccClosedSet, 
					     newCareStatesArray, 
					     arrayOfOnionRings, FALSE, 
					     dcLevel, 
                         ((verbosity<McVerbosityMax_c)? 0:McVerbositySome_c) );
	fairInitialStates = mdd_and(initialStates, fairStates, 1, 1);
	mdd_free(fairStates);
	if (!mdd_is_tautology(fairInitialStates, 0)) { 
	  /* Done, find a reachable fair cycle */
	  exitFlag = 2;  
	  if (verbosity >= McVerbosityLittle_c) 
	    fprintf(vis_stdout, "-- DnC: find a weak SCC!\n");
	  Mc_FsmSccGenFree(sccgen, NIL(array_t));
	  break;
	}else {
	  mdd_free(fairInitialStates); 
	}
      }

    }/*Mc_FsmForEachFairScc( ) {*/ 
    mdd_array_free(tempArray);

    SortMddArrayBySize(absFsm, strongSccClosedSets);
	  
    if (verbosity >= McVerbosityLittle_c && exitFlag != 2) {
      fprintf(vis_stdout, 
	      "-- DnC: found %d SCC-closed sets in abs model %d with %d latches\n",
	      array_n(strongSccClosedSets), iter+1, 
	      st_count(absLatchNameTable));
      if (verbosity >= McVerbositySome_c) {
	array_t *absPSvars = Fsm_FsmReadPresentStateVars(absFsm);
	array_t *PSvars = Fsm_FsmReadPresentStateVars(modelFsm);
	arrayForEachItem(mdd_t *, strongSccClosedSets, i, tempMdd) {
	  fprintf(vis_stdout, "-- An SCC-closed set with %5g abs (%5g concrete) states\n",
		  mdd_count_onset(mddManager, tempMdd, absPSvars),
		  mdd_count_onset(mddManager, tempMdd, PSvars)
		  );
	}
      }
    }

    if(exitFlag == 0 && array_n(strongSccClosedSets) == 0) {
      /* Done, no reachable fair cycle exists */
      exitFlag = 1; 
    }

    mdd_array_free(absOnionRings);
    Fsm_FsmFree(absFsm);

    /* existFlag: 0 --> unknown;  1 --> no fair SCC; 2 --> find a fair SCC */
    if ( exitFlag != 0 || st_count(absLatchNameTable) > maxLatchesToCompose ) {
      if (!isExactReachableStatesAvailable) {
	array_insert_last(mdd_t *, modelCareStatesArray, absReachableStates);
	tempMdd = reachableStates;
	reachableStates = mdd_and(reachableStates, absReachableStates,1,1);
	mdd_free(tempMdd);
      }
      break;
    }

    mdd_free(absReachableStates);
	
  }/*for (iter=0; iter<numOfAbstractModels; iter++) {*/

  for (i=0; i<array_n(absLatchNameTableArray); i++) {
    st_free_table( array_fetch(st_table *, absLatchNameTableArray, i) );
  }
  array_free(absLatchNameTableArray);


  /*
   * Compute fair SCCs on the concrete model if necessary
   */
  if (exitFlag == 0) {
    array_t *tempArray;
    mdd_t   *sccClosedSet = NIL(mdd_t);
    mdd_t   *tempMdd = NIL(mdd_t);

    if (verbosity >= McVerbosityLittle_c) 
      fprintf(vis_stdout, "-- DnC: check the concrete model\n");

    tempArray = strongSccClosedSets;
    strongSccClosedSets = array_alloc(mdd_t *, 0);
    arrayForEachItem(mdd_t *, tempArray, i, sccClosedSet) {
      tempMdd = mdd_and(sccClosedSet, reachableStates, 1, 1);
      if (mdd_is_tautology(tempMdd, 0)) 
	mdd_free(tempMdd);
      else
	array_insert_last(mdd_t *, strongSccClosedSets, tempMdd);
      mdd_free(sccClosedSet);
    }
    array_free(tempArray);

    if (lockstep != MC_LOCKSTEP_OFF) {
      tempArray = array_alloc(mdd_t *, 0);
      fairStates = McFsmRefineFairSCCsByLockStep(modelFsm, lockstep,
						 tempArray, 
						 strongSccClosedSets,
						 NIL(array_t),
						 arrayOfOnionRings,
						 (Mc_VerbosityLevel) verbosity,
						 (Mc_DcLevel) dcLevel);
      mdd_array_free(tempArray);
    }else{
      mdd_t   *fairStates0, *sccClosedSet;
      array_t *EUonionRings;
      mdd_t   *mddOne = mdd_one(mddManager);
      Mc_EarlyTermination_t *earlyTermination;

      sccClosedSet = McMddArrayOr(strongSccClosedSets);
      fairStates0 = Mc_FsmEvaluateEGFormula(modelFsm, sccClosedSet,
					    NIL(mdd_t), mddOne,
					    modelFairness,
					    modelCareStatesArray,
					    MC_NO_EARLY_TERMINATION,
					    NIL(array_t),
					    Mc_None_c, 
					    &arrayOfOnionRings,
					    (Mc_VerbosityLevel) verbosity,
					    (Mc_DcLevel) dcLevel,
					    NIL(boolean),
					    GSHschedule);
      mdd_free(sccClosedSet);

      EUonionRings = ( (arrayOfOnionRings == NIL(array_t))? 
		       NIL(array_t):array_alloc(mdd_t *,0) );

      earlyTermination = Mc_EarlyTerminationAlloc(McSome_c, initialStates);
      fairStates = Mc_FsmEvaluateEUFormula(modelFsm, mddOne,
					   fairStates0, NIL(mdd_t), mddOne,
					   modelCareStatesArray,
					   earlyTermination,
					   NIL(array_t), Mc_None_c,
					   EUonionRings,
					   (Mc_VerbosityLevel) verbosity,
					   (Mc_DcLevel) dcLevel,
					   NIL(boolean));
      mdd_free(fairStates0);
      mdd_free(mddOne);
      Mc_EarlyTerminationFree(earlyTermination);

      if (arrayOfOnionRings != NIL(array_t)) {
	int j;
	arrayForEachItem(array_t *, arrayOfOnionRings, i, tempArray) {
#ifndef NDEBUG
	  mdd_t *mdd1 = array_fetch_last(mdd_t *, tempArray);
#endif
	  arrayForEachItem(mdd_t *, EUonionRings, j, tempMdd) {
	    if (j != 0) 
	      array_insert_last(mdd_t *, tempArray, mdd_dup(tempMdd));
	    else    
	      assert( mdd_equal(tempMdd, mdd1) );
	  }
	}
	mdd_array_free(EUonionRings);
      }
    }

    fairInitialStates = mdd_and(initialStates, fairStates, 1, 1);
    mdd_free(fairStates);
    exitFlag = mdd_is_tautology(fairInitialStates, 0)? 1:2;
  }
  
  /* Clean-Ups */
  mdd_array_free(modelCareStatesArray);
  mdd_array_free(strongSccClosedSets);
  mdd_array_free(onionRings);
  mdd_free(reachableStates);
  mdd_free(initialStates);

  /*
   * Print out the verification result (pass/fail, empty/non-empty)
   */
  if (exitFlag == 1) {
    if (strcmp(driverName, "LE") == 0)
      fprintf(vis_stdout, "# LE: language emptiness check passes\n");
    else
      fprintf(vis_stdout, "# %s: formula passed\n", driverName);
    if (arrayOfOnionRings != NIL(array_t))
      mdd_array_array_free(arrayOfOnionRings);
    return fairInitialStates;

  }else if (exitFlag == 2) {
    if (strcmp(driverName, "LE") == 0)
      fprintf(vis_stdout, "# LE: language is not empty\n");
    else
      fprintf(vis_stdout, "# %s: formula failed\n", driverName);
 
  }else {
    fprintf(vis_stderr, "* DnC error, result is unknown!\n");
    assert(0);
  }

  /*
   * Print out the debugging information if requested
   */
  if (dbgLevel == McDbgLevelNone_c) {
    if (arrayOfOnionRings != NIL(array_t)) 
      mdd_array_array_free(arrayOfOnionRings);
    return fairInitialStates;

  }else {
    mdd_t    *badStates, *aBadState, *mddOne;
    McPath_t *fairPath, *normalPath;
    array_t  *stemArray, *cycleArray;
    FILE     *tmpFile = vis_stdout;
    extern  FILE *vis_stdpipe;
    fprintf(vis_stdout, "# %s: generating path to fair cycle\n", driverName);

    /* Generate witness. */
    badStates = mdd_dup(fairInitialStates);
    aBadState = Mc_ComputeAState(badStates, modelFsm);
    mdd_free(badStates);
    
    mddOne = mdd_one(mddManager);
    fairPath = McBuildFairPath(aBadState, mddOne, arrayOfOnionRings, modelFsm,
			       modelCareStates, 
			       (Mc_VerbosityLevel) verbosity,
			       (Mc_DcLevel) dcLevel,
			       McFwd_c);
    mdd_free(mddOne);
    mdd_free(aBadState);
    mdd_array_array_free(arrayOfOnionRings);
    
    /* Print witness. */
    normalPath = McPathNormalize(fairPath);
    McPathFree(fairPath);
    
    stemArray = McPathReadStemArray(normalPath);
    cycleArray = McPathReadCycleArray(normalPath);
    
    /* we should pass dbgFile/UseMore as parameters 
       dbgFile = McOptionsReadDebugFile(options);*/
    if (dbgFile != NIL(FILE)) {
      vis_stdpipe = dbgFile;
    } else if (UseMore == TRUE) {
      vis_stdpipe = popen("more","w");
    } else {
      vis_stdpipe = vis_stdout;
    }
    vis_stdout = vis_stdpipe;
    
    /* We should also pass SimValue as a parameter */
    if (SimValue == FALSE) {
      (void) fprintf(vis_stdout, "# %s: path to fair cycle:\n\n", driverName);
      Mc_PrintPath(stemArray, modelFsm, printInputs);
      fprintf (vis_stdout, "\n");
      
      (void) fprintf(vis_stdout, "# %s: fair cycle:\n\n", driverName);
      Mc_PrintPath(cycleArray, modelFsm, printInputs);
      fprintf (vis_stdout, "\n");
    }else {
      array_t *completePath = McCreateMergedPath(stemArray, cycleArray);
      (void) fprintf(vis_stdout, "# %s: counter-example\n", driverName);
      McPrintSimPath(vis_stdout, completePath, modelFsm);
      mdd_array_free(completePath);
    }

    if (dbgFile == NIL(FILE) && UseMore == TRUE) {
      (void) pclose(vis_stdpipe);
    }  
    vis_stdout = tmpFile;
    
    McPathFree(normalPath);
  }

  return fairInitialStates;
}

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

  Synopsis           [Create a refinement schedule array.] 

  Description [If dynamicIncrease is true, the first element of return
  array includes varibales appeared in formula. The size of the first
  element should be less than or equal to incrementalSize. The second
  element includes all variables in formula's cone of influence. When
  dynamicIncrease is false, all variables in formula's cone of
  influence (let's say n variables) are partitioned into
  ceil(n/incrementalSize) elements. Then one more element which
  includes all n variables are added to return array.]

  SideEffects        []

  SeeAlso            [Part_SubsystemInfo_t]

******************************************************************************/
array_t	*
Mc_CreateStaticRefinementScheduleArray(
  Ntk_Network_t         *network,
  array_t               *ctlArray,
  array_t               *ltlArray,
  array_t               *fairArray,
  boolean               dynamicIncrease,
  boolean               isLatchNameSort,
  int                   verbosity,
  int                   incrementalSize,
  Part_CMethod          correlationMethod)
{
  array_t		*partitionArray;
  Part_Subsystem_t	*partitionSubsystem;
  Part_SubsystemInfo_t  *subsystemInfo; 
  st_table	        *latchNameTable;
  st_table	        *latchNameTableSum, *latchNameTableSumCopy;
  char		        *flagValue;
  st_generator          *stGen;
  char                  *name;
  double		affinityFactor;
  array_t               *scheduleArray;
  boolean               dynamicAndDependency = isLatchNameSort;
  array_t               *tempArray, *tempArray2;
  int                   i, count;

  /* affinity factor to decompose state space */
  flagValue = Cmd_FlagReadByName("part_group_affinity_factor");
  if(flagValue != NIL(char)){
    affinityFactor = atof(flagValue); 
  }
  else{
    /* default value */
    affinityFactor = 0.5; 
  }

  /* 
   * Obtain submachines as array: The first sub-system includes
   * variables in CTL/LTL/fair formulas and other latches are grouped
   * in the same way as Part_PartCreateSubsystems()
   */
  subsystemInfo = Part_PartitionSubsystemInfoInit(network);
  Part_PartitionSubsystemInfoSetBound(subsystemInfo, incrementalSize);
  Part_PartitionSubsystemInfoSetVerbosity(subsystemInfo, verbosity);
  Part_PartitionSubsystemInfoSetCorrelationMethod(subsystemInfo,
    correlationMethod); 
  Part_PartitionSubsystemInfoSetAffinityFactor(subsystemInfo, affinityFactor);
  partitionArray = Part_PartCreateSubsystemsWithCtlAndLtl(subsystemInfo,
                   ctlArray, ltlArray, fairArray, 
		   dynamicIncrease,dynamicAndDependency,FALSE);
  Part_PartitionSubsystemInfoFree(subsystemInfo);

  scheduleArray = array_alloc(st_table *, 0);


  /* 
   * For each partitioned submachines build an FSM. 
   */
  latchNameTableSum = st_init_table(strcmp, st_strhash);
  if (!dynamicAndDependency){
    for (i=0;i<array_n(partitionArray);i++){
      partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, i);
      if (partitionSubsystem != NIL(Part_Subsystem_t)) {
        latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
        st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
          if (!st_lookup(latchNameTableSum, name, NIL(char *))){ 
            st_insert(latchNameTableSum, name, NIL(char));
          }
        }
        Part_PartitionSubsystemFree(partitionSubsystem);
      } 
      latchNameTableSumCopy = st_copy(latchNameTableSum);
      array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
    }
  }else{
    partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 0);
    latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
    st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
      st_insert(latchNameTableSum, name, NIL(char));
    }
    latchNameTableSumCopy = st_copy(latchNameTableSum);
    array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
    Part_PartitionSubsystemFree(partitionSubsystem);
    
    partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 1);
    tempArray = array_alloc(char *, 0);    
    if (partitionSubsystem != NIL(Part_Subsystem_t)){
      latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
      st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
        array_insert_last(char *, tempArray, name);
      }
      array_sort(tempArray, stringCompare);
      Part_PartitionSubsystemFree(partitionSubsystem);
    }
    
    partitionSubsystem = array_fetch(Part_Subsystem_t *, partitionArray, 2);
    tempArray2 = array_alloc(char *, 0);
    if (partitionSubsystem != NIL(Part_Subsystem_t)) {
      latchNameTable = Part_PartitionSubsystemReadVertexTable(partitionSubsystem);
      st_foreach_item(latchNameTable, stGen, &name, NIL(char *)) {
        array_insert_last(char *, tempArray2, name);
      }
      array_sort(tempArray2, stringCompare);
      Part_PartitionSubsystemFree(partitionSubsystem);
    }

    array_append(tempArray, tempArray2);
    array_free(tempArray2);
    
    count = 0;
    arrayForEachItem(char *, tempArray, i, name){   
      if (!st_lookup(latchNameTableSum, name, NIL(char *))){ 
        st_insert(latchNameTableSum, (char *)name, (char *)0);
        count++;
      }
      if ((count == incrementalSize) && (i < array_n(tempArray)-1)){
        latchNameTableSumCopy = st_copy(latchNameTableSum);
        array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
        count = 0;
      }
    }
    array_free(tempArray);
    latchNameTableSumCopy = st_copy(latchNameTableSum);
    array_insert_last(st_table *, scheduleArray, latchNameTableSumCopy);
  }
  
  array_free(partitionArray);
  st_free_table(latchNameTableSum);
  
  return (scheduleArray);
}


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

  Synopsis [Compute the fair SCCs within the given weak SCC-closed
  set.]

  Description [Used by the Divide and Compose (D'n'C) approach for
  language emptiness checking. Because it's a weak SCC-closed set,
  fair states can be computed through the evaluation of EF EG
  (sccClosedSet). 
  
  Debugging information will be returned if arrayOfOnionRings is not NIL.

  Return the fair states leading to a fair cycle within the given
  SCC-closed set.]
  
  SideEffects [arrayOfOnionRings will be changed if it is not NIL and
  the initial states intersect the fair states.]

******************************************************************************/
mdd_t *
McFsmRefineWeakFairSCCs(
  Fsm_Fsm_t *modelFsm, 
  mdd_t *sccClosedSet, 
  array_t *modelCareStatesArray, 
  array_t *arrayOfOnionRings,
  boolean isSccTerminal,
  int dcLevel, 
  int verbosity) 
{
  mdd_manager *mddManager = Fsm_FsmReadMddManager(modelFsm);
  mdd_t *initialStates;
  mdd_t *mddOne, *mddEgFair, *mddEfEgFair, *fairInitStates, *mdd1;
  array_t *EFonionRings, *EGArrayOfOnionRings, *EGonionRings;
  array_t *newOnionRings;
  int i, j;
  Mc_EarlyTermination_t *earlyTermination;

  initialStates = Fsm_FsmComputeInitialStates(modelFsm);
  mddOne = mdd_one(mddManager);

  /* if debugging information is requested, arrayOfOnionRings!=NIL(array_t) */
  if (arrayOfOnionRings != NIL(array_t)) {
    EGArrayOfOnionRings = array_alloc(array_t *, 0);
    EFonionRings = array_alloc(mdd_t *, 0);
  }else {
    EGArrayOfOnionRings = NIL(array_t);
    EFonionRings = NIL(array_t);
  }

  if (isSccTerminal)
    mddEgFair = mdd_dup(sccClosedSet);
  else
    mddEgFair = Mc_FsmEvaluateEGFormula(modelFsm, sccClosedSet, 
					NIL(mdd_t), mddOne, 
					NIL(Fsm_Fairness_t),
					modelCareStatesArray, 
					NIL(Mc_EarlyTermination_t),
					NIL(array_t), Mc_None_c,
					&EGArrayOfOnionRings,
					(Mc_VerbosityLevel) verbosity,
					(Mc_DcLevel) dcLevel,
					NIL(boolean), McGSH_EL_c);

  earlyTermination = Mc_EarlyTerminationAlloc(McSome_c, initialStates);
  mddEfEgFair = Mc_FsmEvaluateEUFormula(modelFsm, mddOne,
					mddEgFair, NIL(mdd_t), mddOne,
					modelCareStatesArray,
					earlyTermination,
					NIL(array_t), Mc_None_c,
					EFonionRings,
					(Mc_VerbosityLevel) verbosity,
					(Mc_DcLevel) dcLevel,
					NIL(boolean));
  mdd_free(mddEgFair);
  Mc_EarlyTerminationFree(earlyTermination);

  fairInitStates = mdd_and(mddEfEgFair, initialStates, 1, 1);

  /* create the arrayOfOnionRings */
  if (arrayOfOnionRings!=NIL(array_t) && !mdd_is_tautology(fairInitStates,0)) {
    if (isSccTerminal) 
      array_insert_last(array_t *, 
			arrayOfOnionRings, mdd_array_duplicate(EFonionRings));
    else {
      arrayForEachItem(array_t *, EGArrayOfOnionRings, i, EGonionRings) {
	newOnionRings = mdd_array_duplicate(EGonionRings);
	arrayForEachItem(mdd_t *, EFonionRings, j, mdd1) {
	  if (j != 0)
	    array_insert_last(mdd_t *, newOnionRings, mdd_dup(mdd1));
	}
	array_insert_last(array_t *, arrayOfOnionRings, newOnionRings);
      }
    }
  }
  mdd_free(fairInitStates);
  
  if (arrayOfOnionRings != NIL(array_t)) {
    mdd_array_free(EFonionRings);
    mdd_array_array_free(EGArrayOfOnionRings);
  }

  mdd_free(initialStates);
  mdd_free(mddOne);

  return mddEfEgFair;
}


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

  Synopsis [Compute the abstract states from the concrete states.]

  Description [By existentially quantify out the invisible
  variables. Invisible variables are those state variables (or
  latches) that are not in the supports of the abstract states---they
  have been abstracted away.]

  SideEffects []

******************************************************************************/
mdd_t * 
McComputeAbstractStates(
  Fsm_Fsm_t *absFsm, 
  mdd_t *states)
{
  mdd_t	      *result;
  mdd_manager *mddManager = Fsm_FsmReadMddManager(absFsm);
  array_t     *psVars = Fsm_FsmReadPresentStateVars(absFsm);
  array_t     *supportVars;
  array_t     *invisibleVars = array_alloc(long, 0);
  st_table    *psVarTable = st_init_table(st_numcmp, st_numhash);
  int         i;
  long        mddId;

  arrayForEachItem(long, psVars, i, mddId) {
    st_insert(psVarTable, (char *)mddId, NIL(char));
  }
  
  supportVars = mdd_get_support(mddManager, states);
  arrayForEachItem(long, supportVars, i, mddId) {
    if (!st_is_member(psVarTable, (char *)mddId)) 
      array_insert_last(long, invisibleVars, mddId);
  }
  array_free(supportVars);
  st_free_table(psVarTable);

  result = mdd_smooth(mddManager, states, invisibleVars);

  array_free(invisibleVars);

  return result;
}


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

  Synopsis [Return true if the Divide and Compose (D'n'C) approach for
  language emptiness checking is enabled.]

  Description [Return true if the D'n'C approach for language emptiness
  is enabled.]

  SideEffects []

******************************************************************************/
boolean
McGetDncEnabled(void)
{
  char *flagValue;
  boolean result = FALSE;
 
  flagValue = Cmd_FlagReadByName("divide_and_compose");
  if (flagValue != NIL(char)) {
    if (strcmp(flagValue, "true") == 0)
      result = TRUE;
    else if (strcmp(flagValue, "false") == 0)
      result = FALSE;
    else {
      fprintf(vis_stderr, "** dnc error: invalid dnc_enable flag %s, dnc is disabled. \n", flagValue);
    }
  }

  return result;
}


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

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

  Synopsis    [Return true if the given SCC is strong.]

  Description [Return true if the given SCC is strong. Note that the
  check is conservative -- for the purpose of efficiency -- When it
  returns false, the SCC is definitely weak; when it returns true, the
  SCC may be still be weak. For the language emptiness checking, this
  is not going to hurt us.]

  SideEffects []

******************************************************************************/
static boolean
SccIsStrong(mdd_manager *mddMgr, array_t *buechiFairness, mdd_t *SCC)
{
  boolean strength;
  mdd_t *LabeledAllFairness = mdd_dup(SCC);
  mdd_t *NotLabeledAllFairness;
  mdd_t *fairSet;
  int i;
    
  /*
   * check whether SCC intersects all the fairness constraints
   * if yes, WEAK
   * if no,  WEAK or STRONG
   */
  arrayForEachItem(mdd_t *, buechiFairness, i, fairSet) {
    mdd_t *tmpMdd = LabeledAllFairness;
    LabeledAllFairness = mdd_and(LabeledAllFairness, fairSet, 1,1 );
    mdd_free( tmpMdd );
  }
  NotLabeledAllFairness = mdd_and(SCC, LabeledAllFairness, 1, 0);
  mdd_free(LabeledAllFairness);
  
  if(mdd_is_tautology(NotLabeledAllFairness, 0)) {
    mdd_free(NotLabeledAllFairness);
    strength = FALSE; /* WEAK*/
  }
  else {
    mdd_free(NotLabeledAllFairness);
    strength = TRUE;
  }
  
  return strength;
}

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

  Synopsis    [Compare the size of two mdds.]

  Description [Used to sort the array of mdds by their number of minterms.]

  SideEffects [SortMddArrayBySize]

******************************************************************************/
static st_table *array_mdd_compare_table = NIL(st_table);
static int 
array_mdd_compare_size(
  const void *obj1, 
  const void *obj2) 
{
  double *val1, *val2;
  int flag1, flag2;

  flag1 = st_lookup(array_mdd_compare_table, *((char **)obj1), &val1);
  flag2 = st_lookup(array_mdd_compare_table, *((char **)obj2), &val2);
  assert(flag1 && flag2);

  if (*val1 < *val2)
    return -1;
  else if (*val1> *val2)
    return +1;
  else 
    return 0;
}

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

  Synopsis    [Sort the array of mdds by their number of minterms.]

  Description [Sort the array of mdds by their number of minterms. The
  present state variables of the given FSM is used to count the
  minterms. The sorting will be skipped if the number of present state
  variables is larger than 1024.]

  SideEffects [array_mdd_compare_size]

******************************************************************************/
static array_t *
SortMddArrayBySize(Fsm_Fsm_t *fsm, array_t *mddArray)
{
  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
  array_t     *psVars = Fsm_FsmReadPresentStateVars(fsm);
  
  if (array_n(psVars) < 1024) {
    st_table    *mddToSizeTable =st_init_table(st_ptrcmp, st_ptrhash);
    double      *sizes = ALLOC(double, array_n(mddArray));
    mdd_t       *mdd1;
    int         i;

    arrayForEachItem(mdd_t *, mddArray, i, mdd1) {
      *(sizes+i) = mdd_count_onset(mddManager, mdd1, psVars);
      st_insert(mddToSizeTable, (char *)mdd1, (char *)(sizes+i));
    }
    
    array_mdd_compare_table = mddToSizeTable;
    array_sort(mddArray, array_mdd_compare_size);

    FREE(sizes);
    st_free_table(mddToSizeTable);
  }

  return mddArray;
}

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

  Synopsis [Compare two strings]

  SideEffects []

******************************************************************************/
static int
stringCompare(
  const void * s1,
  const void * s2)
{
  return(strcmp(*(char **)s1, *(char **)s2));
}