src/mc/mcDnC.c

Go to the documentation of this file.

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

/*---------------------------------------------------------------------------*/
/* 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);
/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

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

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                                          */
/*---------------------------------------------------------------------------*/
    
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;
}


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


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

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

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

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

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