src/amc/amcBlock.c

Go to the documentation of this file.

#include "amcInt.h"
#include "mcInt.h"

static char rcsid[] UNUSED = "$Id: amcBlock.c,v 1.35 2005/04/25 20:24:53 fabio Exp $";

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

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

struct BlockInfoStruct {
  Amc_SubsystemInfo_t   *optimalSystem; /* temporary storage for Block method */
  int                   bestSystem;     /* temporary storage for Block method */
};

struct BlockSubsystemInfoStruct {
  int           scheduledForRefinement;
};


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/
typedef struct BlockInfoStruct BlockInfo_t;
typedef struct BlockSubsystemInfoStruct BlockSubsystemInfo_t;

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

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

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

static BlockInfo_t * AmcObtainOptimalSystemUpperBound(Amc_Info_t *amcInfo, Ctlp_Formula_t *formula, BlockInfo_t *BlockInfo, int verbosity);
static BlockInfo_t * AmcObtainOptimalSystemLowerBound(Amc_Info_t *amcInfo, Ctlp_Formula_t *formula, BlockInfo_t *BlockInfo, int verbosity);
static void AmcInitializeDependency(array_t *subSystemArray, int isMBM);
static void AmcInitializeSchedule(Amc_Info_t *amcInfo);
static int AmcIsEverySubsystemRescheduled(Amc_Info_t *amcInfo);
static void AmcPrintScheduleInformation(Amc_Info_t *amcInfo);
#if 0
static void AmcRescheduleForRefinement(st_table *fanOutSystemTable);
static mdd_t * AmcRefineWithSatisfyStatesOfFanInSystem(Amc_SubsystemInfo_t *subSystem, mdd_t *careStates);
#endif
static array_t * AmcInitializeQuantifyVars(Amc_SubsystemInfo_t *subSystem);
#if 0
static void AmcFreeBlockInfo(BlockInfo_t *BlockInfo);
#endif
static int AmcBlockSubsystemReadScheduledForRefinement(BlockSubsystemInfo_t *system);
static void AmcBlockSubsystemSetScheduledForRefinement(BlockSubsystemInfo_t *system, int data);
#if 0
static Amc_SubsystemInfo_t * AmcBlockReadOptimalSubsystem(BlockInfo_t *system);
#endif
static void AmcBlockSetOptimalSystem(BlockInfo_t *system, Amc_SubsystemInfo_t *data);
#if 0
static int AmcBlockReadBestSystem(BlockInfo_t *system);
#endif
static void AmcBlockSetBestSystem(BlockInfo_t *system, int data);
#if 0
static Amc_SubsystemInfo_t * AmcClearInputVarsFromFSM(Amc_SubsystemInfo_t *subSystem);
#endif

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


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/
int
AmcBlockTearingProc(
  Amc_Info_t     *amcInfo,
  Ctlp_Formula_t *formula,
  int            verbosity)
{
  array_t               *subSystemArray = amcInfo->subSystemArray;
  Amc_SubsystemInfo_t   *subSystem;
  BlockInfo_t           BlockInfo;


  /*
   * Update fan-in subsystems and fan-out subsystems when machine by machine 
   * method is ON.
   * Update initial states in BlockInfo.
   * Reschedule every subsystem to be evaluated.
   */

  if( amcInfo->optimalSystem == NIL(Amc_SubsystemInfo_t) ) {
    AmcInitializeDependency(subSystemArray, amcInfo->isMBM);
  }

  AmcInitializeSchedule(amcInfo);

  /* BlockInfo is a temporary storage. optimal system is not freed */
  BlockInfo.optimalSystem = NIL(Amc_SubsystemInfo_t);
    

  /*
   * Outer loop until there's no scheduled subsystem.
   */
  while(AmcIsEverySubsystemRescheduled(amcInfo)) {

    if(verbosity == Amc_VerbosityNone_c)
      AmcPrintScheduleInformation(amcInfo);


    if( !amcInfo->lowerBound ) {
        AmcObtainOptimalSystemUpperBound(amcInfo, formula, &BlockInfo, 
                                         verbosity);
        /* AmcObtainOptimalSystemUpperBoundWithDI(amcInfo, formula, &BlockInfo,
                                                  verbosity); */
    }
    else {
        AmcObtainOptimalSystemLowerBound(amcInfo, formula, &BlockInfo, 
                                         verbosity);
        /* AmcObtainOptimalSystemLowerBoundWithMBM(amcInfo, formula, &BlockInfo,
                                                   verbosity); */
    }

    if(amcInfo->isVerified) {

        int best = BlockInfo.bestSystem;
        subSystem = array_fetch(Amc_SubsystemInfo_t *, amcInfo->subSystemArray,
                                best);
        subSystem->takenIntoOptimal = 1;

      return 1;
    }

    if(!amcInfo->isMBM)
      break;

  } /* End of while() */

  if(verbosity == Amc_VerbosityNone_c)
    AmcPrintScheduleInformation(amcInfo);


  /* Update the subsystem that had been included in optimal system */
  {
    int best = BlockInfo.bestSystem;
    subSystem = array_fetch(Amc_SubsystemInfo_t *, amcInfo->subSystemArray, 
                            best);
    subSystem->takenIntoOptimal = 1;
  }

  /* Update amcInfo's optimal system */
  if(amcInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) {
#ifdef AMC_DEBUG
    {
      Amc_SubsystemInfo_t *previousOpt = amcInfo->optimalSystem;
      Amc_SubsystemInfo_t *currentOpt  = BlockInfo.optimalSystem;

      if(!amcInfo->lowerBound) {
        if(mdd_lequal(previousOpt->satisfyStates, currentOpt->satisfyStates,
                      1, 1)) {
          fprintf(vis_stdout, "\n###AMC : We are ok.");
        }
        else {
          fprintf(vis_stdout, "\n** amc error: Somethings wrong.");
        }
      }
      else {
        if( mdd_lequal(currentOpt->satisfyStates, previousOpt->satisfyStates,
                       1, 1)) {
          fprintf(vis_stdout, "\n###AMC : We are ok.");
        }
        else {
          fprintf(vis_stdout, "\n** amc error: Somethings wrong.");
        }
      }
    }
#endif 
    Amc_AmcSubsystemFree(amcInfo->optimalSystem);
  }
  AmcSetOptimalSystem(amcInfo, BlockInfo.optimalSystem);

  return 1;
}

void
AmcFreeBlock(
  Amc_Info_t *amcInfo)
{
  Amc_SubsystemInfo_t   *subSystem; 
  BlockSubsystemInfo_t  *BlockSubsystem;
  int i ;

  /* what if amc doesn't free partition */
  arrayForEachItem(Amc_SubsystemInfo_t *, amcInfo->subSystemArray, i, 
                   subSystem) {
    BlockSubsystem = (BlockSubsystemInfo_t *)AmcSubsystemReadMethodSpecificData(subSystem);
    if(BlockSubsystem != NIL(BlockSubsystemInfo_t))
      FREE(BlockSubsystem);

    Amc_AmcSubsystemFree(subSystem); 
  }
  array_free(amcInfo->subSystemArray);

  if(amcInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) {
    Amc_AmcSubsystemFree(amcInfo->optimalSystem);
    amcInfo->optimalSystem = NIL(Amc_SubsystemInfo_t);
  }

  if( amcInfo->initialStates != NIL(mdd_t)) {
    mdd_free(amcInfo->initialStates);
    amcInfo->initialStates = NIL(mdd_t);
  }

  FREE(amcInfo);

}

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



static BlockInfo_t *
AmcObtainOptimalSystemUpperBound(
Amc_Info_t              *amcInfo,
Ctlp_Formula_t          *formula,
BlockInfo_t             *BlockInfo,
int                     verbosity)
{
  array_t               *subSystemArray = amcInfo->subSystemArray;
  Amc_SubsystemInfo_t   *subSystem, *bestCombinedSystem;
  mdd_t                 *initialStates;
  mdd_t                 *smallestStates, *currentErrorStates, *careStates;
  int                   i, best = 0;
  graph_t               *partition = Part_NetworkReadPartition(amcInfo->network);
  mdd_manager           *mddManager = Part_PartitionReadMddManager(partition);
  mdd_t                 *mddOne = mdd_one(mddManager);
  array_t               *quantifyVars;
  Mc_DcLevel            dcLevel;
  char  *flagValue;


  /* 
   * Initial states must be set before coming into this routine.
   */
  initialStates = amcInfo->initialStates;
  if( initialStates == NIL(mdd_t) ) {
    (void)fprintf(vis_stderr, "** amc error: \n");
    return(NIL(BlockInfo_t));
  }
 
  /* Read in the usage of don't care level */
  flagValue = Cmd_FlagReadByName("amc_DC_level");
  if(flagValue != NIL(char)){
    dcLevel = (Mc_DcLevel) atoi(flagValue); 
    if( dcLevel > McDcLevelRchFrontier_c ) dcLevel = McDcLevelRchFrontier_c;
  }
  else{
    /* default value set to McDcLevelNone_c. Mc's default is McDcLevelRch_c. */
    dcLevel = McDcLevelNone_c; 
  }

  /*
   * Update the set of states satisfying the formula for each sub-systems.
   * The process of "combining sub-systems" is equivalent of taking a 
   * "synchronous product" of multiple sub-subsystems.
   */
  smallestStates = NIL(mdd_t);
  bestCombinedSystem  = NIL(Amc_SubsystemInfo_t);

  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {

    mdd_t                       *reachableStates, *fairStates, *satisfyStates;
    Fsm_Fsm_t                   *combinedFsm;
    Fsm_Fairness_t              *fairCond;
    Amc_SubsystemInfo_t         *combinedSystem; 

    /* Proceed if the subsystem had not yet been taken into the optimal system. */
    if(!subSystem->takenIntoOptimal) {

      /* 
       * Combine subsystems. If optimal subsystem is NIL, duplicate the
       * subsystem.
       */  
      combinedSystem = Amc_CombineSubsystems(amcInfo->network,
                                             amcInfo->optimalSystem,
                                             subSystem);
      combinedFsm = AmcSubsystemReadFsm(combinedSystem);

      quantifyVars = AmcInitializeQuantifyVars(combinedSystem);
      
      /* 
       * Currently forced not to compute reachable states. This is to reduce
       * computational overhead of computing it when dealing with complex
       * examples.
       */
      reachableStates = mdd_one(mddManager);
      fairStates = mdd_one(mddManager);
      fairCond = Fsm_FsmReadFairnessConstraint(combinedFsm);


      /* Obtain new care set from fan-in systems */
      careStates = mdd_dup(reachableStates);

      Ctlp_FlushStates(formula);
      satisfyStates = mdd_dup(Amc_AmcEvaluateCTLFormula(combinedSystem,
                                                        subSystemArray, 
                                                        formula, fairStates,
                                                        fairCond,
                                                        careStates,
                                                        amcInfo->lowerBound, 
                                                        quantifyVars,
                                                        /*NIL(array_t),*/
                                                        (Mc_VerbosityLevel)
                                                        verbosity, dcLevel));

      {
        int x; array_t *quantifyStateVars;
        arrayForEachItem(array_t *, quantifyVars, x, quantifyStateVars) {
          array_free(quantifyStateVars); 
        }
        array_free(quantifyVars);
      }
      /* Free */
      mdd_free(careStates);
      mdd_free(reachableStates); mdd_free(fairStates); 
      

      /* 
       * Update the set of states satisfying the formula for each subsystems
       * when newly computed states are tighter than the one already stored.
       * Notice, "satisfySates" holds the set of states satisfying the formula
       * computed with the combined_system(optimal_system || current_subsystem). 
       * 
       */
      if( subSystem->satisfyStates != NIL(mdd_t) ) {

        if( !(mdd_equal(subSystem->satisfyStates, satisfyStates )) &&
            (mdd_lequal(subSystem->satisfyStates, satisfyStates, 1, 1)) ) {
          /* We got a tighter approximation. */
          mdd_free(subSystem->satisfyStates);
          AmcSubsystemSetSatisfy(subSystem, mdd_dup(satisfyStates));
        }
         
      }     
      else {
        /* We are in the first level of the lattice */
        AmcSubsystemSetSatisfy(subSystem, mdd_dup(satisfyStates));

      }

      /* Update the set of states satisfying the formula for the combined_system. */
      if( AmcSubsystemReadSatisfy(combinedSystem) != NIL(mdd_t) )
        mdd_free( AmcSubsystemReadSatisfy(combinedSystem) );
      AmcSubsystemSetSatisfy(combinedSystem, mdd_dup(satisfyStates));


      if( verbosity == Amc_VerbosityVomit_c) {
         mdd_manager *mddMgr = Fsm_FsmReadMddManager(combinedSystem->fsm);
         array_t     *psVars = Fsm_FsmReadPresentStateVars(combinedSystem->fsm);

         fprintf(vis_stdout, "\n#AMC STATUS: The states satisfying the formula : %10g",
                        mdd_count_onset(  mddMgr, combinedSystem->satisfyStates, psVars ) );
         fflush(vis_stdout);
       }

      /* 
       * Check whether the formula evaluates to TRUE. 
       */
      { 
        mdd_t *notSatisfyStates = mdd_not(satisfyStates);
        currentErrorStates = mdd_and(initialStates, notSatisfyStates, 1, 1);
        mdd_free(notSatisfyStates);
        mdd_free(satisfyStates);
      }

      if ( mdd_is_tautology(currentErrorStates, 0) ) { 
        /* The formula is verified TRUE!! */

        AmcBlockSetBestSystem(BlockInfo, i);
        amcInfo->isVerified = 1; 
        amcInfo->amcAnswer = Amc_Verified_True_c;
        fprintf(vis_stdout, "\n# AMC: formula passed --- ");
        Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));

        if(currentErrorStates != NIL(mdd_t))
          mdd_free(currentErrorStates); 
        if(smallestStates != NIL(mdd_t))
          mdd_free(smallestStates);
        if( bestCombinedSystem != NIL(Amc_SubsystemInfo_t) )
          Amc_AmcSubsystemFree(bestCombinedSystem); 

        mdd_free(mddOne); Amc_AmcSubsystemFree(combinedSystem); 
        Ctlp_FlushStates(formula);

        return BlockInfo;
      } /* end of if */
      else if (amcInfo->currentLevel == array_n(amcInfo->subSystemArray)){
        /* The formula is verified FALSE!! */
        array_t *careStatesArray;

        AmcBlockSetBestSystem(BlockInfo, i);
        amcInfo->isVerified = 1;
        amcInfo->amcAnswer = Amc_Verified_False_c;
        fprintf(vis_stdout, "\n# AMC: formula failed --- ");
        Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));

        if(currentErrorStates != NIL(mdd_t)) mdd_free(currentErrorStates);
        if(smallestStates != NIL(mdd_t))     mdd_free(smallestStates);

        if( bestCombinedSystem != NIL(Amc_SubsystemInfo_t) )
          Amc_AmcSubsystemFree(bestCombinedSystem);

        {
          /* Temporarily stay here until the damn thing becomes visible. */
          McOptions_t *mcOptions = ALLOC(McOptions_t, 1);
          mcOptions->useMore = FALSE;
          mcOptions->fwdBwd = McFwd_c;
          mcOptions->reduceFsm = FALSE;
          mcOptions->printInputs = FALSE;
          mcOptions->simFormat = FALSE;
          mcOptions->verbosityLevel = McVerbosityNone_c;
          mcOptions->dbgLevel = McDbgLevelMin_c;
          mcOptions->dcLevel   = McDcLevelNone_c;
          mcOptions->ctlFile = NIL(FILE);
          mcOptions->debugFile = NIL(FILE);

          careStatesArray = array_alloc(mdd_t *, 0);
          array_insert(mdd_t *, careStatesArray, 0, mddOne);
          fprintf(vis_stdout, "\n");
          McFsmDebugFormula((McOptions_t *)mcOptions, formula,
                            combinedSystem->fsm, careStatesArray);
          array_free(careStatesArray);
          FREE(mcOptions);
        }
        mdd_free(mddOne);
        Amc_AmcSubsystemFree(combinedSystem);
        Ctlp_FlushStates(formula);

        return BlockInfo;       
      }

      /* 
       * Get the locally optimal subsystem by choosing a subsystem that produces
       * smallest error states.
       */
      if( smallestStates == NIL(mdd_t) ||
         mdd_count_onset(mddManager, currentErrorStates, Fsm_FsmReadPresentStateVars(subSystem->fsm)) <=
         mdd_count_onset(mddManager, smallestStates, Fsm_FsmReadPresentStateVars(subSystem->fsm)) ) {

        if( smallestStates != NIL(mdd_t) )
          mdd_free(smallestStates);

        smallestStates = currentErrorStates;

        if(bestCombinedSystem != NIL(Amc_SubsystemInfo_t)) {
          Amc_AmcSubsystemFree(bestCombinedSystem);
          bestCombinedSystem = NIL(Amc_SubsystemInfo_t);
        }
        bestCombinedSystem = combinedSystem; 
        best = i;
      }

      else { /* Free combined system, current error states */
        Amc_AmcSubsystemFree(combinedSystem);
        combinedSystem = NIL(Amc_SubsystemInfo_t);
        mdd_free(currentErrorStates); 
      }

    
    } /* end of if(!takenIntoOptimal) */

  } /* end of arrayForEachItem(subSystemArray) */


  /* 
   * Flush the formula that was kept in last iteration.
   * Update Block Info.  
   */
  Ctlp_FlushStates(formula);

  /* Update the inital states */
  {
    mdd_t *initialStates;
    if((initialStates = AmcReadInitialStates(amcInfo)) != NIL(mdd_t))
      mdd_free(initialStates);
    AmcSetInitialStates(amcInfo, smallestStates);
  }

  if( verbosity == Amc_VerbositySpit_c ) {
    mdd_manager *mddMgr = Fsm_FsmReadMddManager(bestCombinedSystem->fsm);
    array_t     *psVars = Fsm_FsmReadPresentStateVars(bestCombinedSystem->fsm);

    fprintf(vis_stdout, "\n#AMC : The BDD size of the states satisfying the formula : %d", 
                                  mdd_size(bestCombinedSystem->satisfyStates) );
    fprintf(vis_stdout, "\n#AMC : The cardinality of the states satisfying the formula : %10g ",
                          mdd_count_onset(  mddMgr, bestCombinedSystem->satisfyStates, psVars ) );
    fprintf(vis_stdout, "\n#AMC : The BDD size of the states new initial states : %d",
                                  mdd_size(smallestStates) );
    fprintf(vis_stdout, "\n#AMC : The cardinality of the new initial states : %10g ",
                          mdd_count_onset(  mddMgr, smallestStates, psVars ) );
  }


  /* 
   * Update the optimal system BlockInfo->optimalSystem. BlockInfo is a temporary 
   * storage that survive through single level of the lattice.
   */
  if(BlockInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) {
    Amc_AmcSubsystemFree(BlockInfo->optimalSystem);
    AmcBlockSetOptimalSystem(BlockInfo, NIL(Amc_SubsystemInfo_t));
  }
  AmcSetOptimalSystem(BlockInfo, bestCombinedSystem);

  /* Set the best system. */
  AmcBlockSetBestSystem(BlockInfo, best);

  mdd_free(mddOne);
  
  return BlockInfo;

}


static BlockInfo_t *
AmcObtainOptimalSystemLowerBound(
Amc_Info_t              *amcInfo,
Ctlp_Formula_t          *formula,
BlockInfo_t             *BlockInfo,
int                     verbosity)
{
  array_t               *subSystemArray = amcInfo->subSystemArray;
  Amc_SubsystemInfo_t   *subSystem, *bestCombinedSystem;
  mdd_t                 *initialStates;
  mdd_t                 *smallestStates, *currentErrorStates, *careStates;
  int                   i, best = 0;
  graph_t               *partition = Part_NetworkReadPartition(amcInfo->network);
  mdd_manager           *mddManager = Part_PartitionReadMddManager(partition);
  mdd_t                 *mddOne = mdd_one(mddManager);
  array_t               *quantifyVars;
  Mc_DcLevel            dcLevel;
  char                  *flagValue;
  
  /* 
   * Initial states must be set before coming into this routine.
   */
  initialStates = amcInfo->initialStates;
  if( initialStates == NIL(mdd_t) ) {
    (void)fprintf(vis_stderr, "** amc error: \n");
    return(NIL(BlockInfo_t));
  }

  /* Read in the usage of don't care level. Do not want to pass parameters. */
  flagValue = Cmd_FlagReadByName("amc_DC_level");
  if(flagValue != NIL(char)){
    dcLevel = (Mc_DcLevel) atoi(flagValue);
    if( dcLevel > McDcLevelRchFrontier_c ) dcLevel = McDcLevelRchFrontier_c;
  }
  else{
    /* default value set to McDcLevelNone_c. Mc's default is McDcLevelRch_c. */
    dcLevel = McDcLevelNone_c;
  }

  /*
   * Update the set of states satisfying the formula for each subsystem.
   * The process of "combining sub-systems" is equivalent of taking a 
   * "synchronous product" of multiple subsystems.
   */
  smallestStates = NIL(mdd_t);
  bestCombinedSystem  = NIL(Amc_SubsystemInfo_t);

  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {

    mdd_t                       *reachableStates, *fairStates, *satisfyStates;
    Fsm_Fsm_t                   *combinedFsm;
    Fsm_Fairness_t              *fairCond;
    Amc_SubsystemInfo_t         *combinedSystem; 

    /* Proceed if the subsystem has not yet been taken into the optimal system. */
    if(!subSystem->takenIntoOptimal) {

      /* 
       * Combine subsystems. If optimal subsystem is NIL, duplicate the
       * subsystem.
       */
      combinedSystem = Amc_CombineSubsystems(amcInfo->network,
                                             amcInfo->optimalSystem,
                                             subSystem);
      /* Remove input variables from the FSM */
      /*      combinedSystem = AmcClearInputVarsFromFSM(combinedSystem);*/
      combinedFsm = AmcSubsystemReadFsm(combinedSystem);

      /*
       * Use takenIntoOptimal field for the purpose of excluding current block
       * when universally quantifying variables from transition relation. 
       * Obtain lower bound of transition relation by universal quantification.
       */

      quantifyVars = AmcInitializeQuantifyVars(combinedSystem);
      combinedSystem->takenIntoOptimal = i;


      /*
       * Currently forced not to compute reachable states. This is to reduce
       * computational burden of computing it when dealing with complex
       * examples.
       */
      reachableStates = mdd_one(mddManager);
      fairStates = mdd_one(mddManager);
      fairCond = Fsm_FsmReadFairnessConstraint(combinedFsm);
      careStates = mdd_dup(reachableStates);

      Ctlp_FlushStates(formula);
      satisfyStates = mdd_dup(Amc_AmcEvaluateCTLFormula(combinedSystem,
                                                        subSystemArray, 
                                                        formula, fairStates,
                                                        fairCond, careStates,
                                                        amcInfo->lowerBound, 
                                                        quantifyVars,
                                                        (Mc_VerbosityLevel)
                                                        verbosity, dcLevel));
      {
        int x; array_t *quantifyStateVars;
        arrayForEachItem(array_t *, quantifyVars, x, quantifyStateVars) {
          array_free(quantifyStateVars); 
        }
        array_free(quantifyVars);
      }
      mdd_free(careStates); mdd_free(reachableStates); mdd_free(fairStates); 
      

      /*
       */
      if( subSystem->satisfyStates != NIL(mdd_t) ) {
        if( !(mdd_equal(satisfyStates, subSystem->satisfyStates )) &&
             (mdd_lequal(satisfyStates, subSystem->satisfyStates, 1, 1)) ) {
          /* We got a tighter approximation. */
          mdd_free(subSystem->satisfyStates);
          AmcSubsystemSetSatisfy(subSystem, mdd_dup(satisfyStates));
        }
      }     /* end of if( subSystem->satisfyStates != NIL(mdd_t) ) */
      else {
        /* Update subsystem when we are in level 1 of the lattice */
        AmcSubsystemSetSatisfy(subSystem, mdd_dup(satisfyStates));
      }

      if( AmcSubsystemReadSatisfy(combinedSystem) != NIL(mdd_t) )
        mdd_free( AmcSubsystemReadSatisfy(combinedSystem) );
      AmcSubsystemSetSatisfy(combinedSystem, mdd_dup(satisfyStates));


      /* Test if the formula is verified */
      {
        mdd_t *notSatisfyStates = mdd_not(satisfyStates);
        currentErrorStates      = mdd_and(initialStates, notSatisfyStates, 1, 1);
        mdd_free(notSatisfyStates);
        mdd_free(satisfyStates);
      }

      if( verbosity == Amc_VerbosityVomit_c) {
        mdd_manager *mddMgr = Fsm_FsmReadMddManager(combinedSystem->fsm);
        array_t *psVars     = Fsm_FsmReadPresentStateVars(combinedSystem->fsm);

        fprintf(vis_stdout,
                "\n#AMC STATUS: The states satisfying the formula : %10g",
                mdd_count_onset(mddMgr, combinedSystem->satisfyStates, psVars ) );
        fflush(vis_stdout);
      }

      if ( !mdd_is_tautology(currentErrorStates, 0) ) {
        array_t *careStatesArray;

        /* Verified the formula FALSE!! */
        AmcBlockSetBestSystem(BlockInfo, i);
        amcInfo->isVerified = 1;
        amcInfo->amcAnswer = Amc_Verified_False_c;
        fprintf(vis_stdout, "\n# AMC: formula failed --- ");
        Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));


        if(currentErrorStates != NIL(mdd_t)) mdd_free(currentErrorStates);
        if(smallestStates != NIL(mdd_t))     mdd_free(smallestStates);

        if( bestCombinedSystem != NIL(Amc_SubsystemInfo_t) )
          Amc_AmcSubsystemFree(bestCombinedSystem);

        {
          /* Temporarily stay here until the damn thing becomes visible. */
          McOptions_t *mcOptions = ALLOC(McOptions_t, 1);
          mcOptions->useMore = FALSE;
          mcOptions->fwdBwd = McFwd_c;
          mcOptions->reduceFsm = FALSE;
          mcOptions->printInputs = FALSE;
          mcOptions->simFormat = FALSE;
          mcOptions->verbosityLevel = McVerbosityNone_c;
          mcOptions->dbgLevel = McDbgLevelMinVerbose_c;
          mcOptions->dcLevel   = McDcLevelNone_c;
          mcOptions->ctlFile = NIL(FILE);
          mcOptions->debugFile = NIL(FILE);

          careStatesArray = array_alloc(mdd_t *, 0);
          array_insert(mdd_t *, careStatesArray, 0, mddOne);
          fprintf(vis_stdout, "\n");
          McFsmDebugFormula((McOptions_t *)mcOptions, formula,
                            combinedSystem->fsm, careStatesArray);
          array_free(careStatesArray);
          FREE(mcOptions);
        }
        mdd_free(mddOne);
        Amc_AmcSubsystemFree(combinedSystem);
        Ctlp_FlushStates(formula);

        return BlockInfo;

      }else if (amcInfo->currentLevel == array_n(amcInfo->subSystemArray)){
        /* The formula is verified true!! */
        AmcBlockSetBestSystem(BlockInfo, i);
        amcInfo->isVerified = 1; 
        amcInfo->amcAnswer = Amc_Verified_True_c;
        fprintf(vis_stdout, "\n# AMC: formula passed --- ");
        Ctlp_FormulaPrint(vis_stdout, Ctlp_FormulaReadOriginalFormula(formula));


        if(currentErrorStates != NIL(mdd_t))
          mdd_free(currentErrorStates); 
        if(smallestStates != NIL(mdd_t))
          mdd_free(smallestStates);
        if( bestCombinedSystem != NIL(Amc_SubsystemInfo_t) )
          Amc_AmcSubsystemFree(bestCombinedSystem); 

        mdd_free(mddOne); Amc_AmcSubsystemFree(combinedSystem); 
        Ctlp_FlushStates(formula);

        return BlockInfo;
      }

      mdd_free(currentErrorStates);


      /*
       * Choose a subsystem that produces smallest satisfying states.
       */
      if( smallestStates == NIL(mdd_t) ||
          mdd_count_onset(mddManager, subSystem->satisfyStates, Fsm_FsmReadPresentStateVars(subSystem->fsm)) <= 
          mdd_count_onset(mddManager, smallestStates, Fsm_FsmReadPresentStateVars(subSystem->fsm)) ) {
        /*
         * Found locally optimal subsystem. 
         * Free smallest-error-state, best combined system so far. 
         * Update smallest-error-states and best combined system. 
         */
        if( smallestStates != NIL(mdd_t) ) mdd_free(smallestStates);

        smallestStates = mdd_dup(subSystem->satisfyStates);

        if(bestCombinedSystem != NIL(Amc_SubsystemInfo_t)) {
          Amc_AmcSubsystemFree(bestCombinedSystem);
          bestCombinedSystem = NIL(Amc_SubsystemInfo_t);
        }
        bestCombinedSystem = combinedSystem; 
        best = i;
      }

      else { /* Free combined system, current error states */
        Amc_AmcSubsystemFree(combinedSystem); combinedSystem = NIL(Amc_SubsystemInfo_t);
      }

    } /* end of if(!takenIntoOptimal) */

  } /* end of arrayForEachItem(subSystemArray) */

  mdd_free(smallestStates);

  /* 
   * Flush formula that was kept in last iteration. Update Block Info.  
   */
  Ctlp_FlushStates(formula);

  /*
   * Update optimal system BlockInfo->optimalSystem. BlockInfo is a temporary 
   * storage that survive through single level of the lattice.
   */
  if(BlockInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) {
    Amc_AmcSubsystemFree(BlockInfo->optimalSystem);
    AmcBlockSetOptimalSystem(BlockInfo, NIL(Amc_SubsystemInfo_t));
  }
  AmcSetOptimalSystem(BlockInfo, bestCombinedSystem);

  /* Set best system. */
  AmcBlockSetBestSystem(BlockInfo, best);
  mdd_free(mddOne);

  return BlockInfo;

}



static void
AmcInitializeDependency(
array_t         *subSystemArray,
int             isMBM)
{
  Amc_SubsystemInfo_t   *subSystem;  
  BlockSubsystemInfo_t  *BlockSubsystem;
  int   i;

  if(!isMBM) {
    int i;
    arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {
      AmcSubsystemSetMethodSpecificData(subSystem, NIL(BlockSubsystemInfo_t));
    }
    return;
  }

  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {

    BlockSubsystem = ALLOC(BlockSubsystemInfo_t, 1);

    AmcSubsystemSetMethodSpecificData(subSystem, BlockSubsystem);

  }

}

static void
AmcInitializeSchedule(
Amc_Info_t *amcInfo)
{
  array_t                 *subSystemArray = amcInfo->subSystemArray;
  Amc_SubsystemInfo_t     *subSystem;  
  BlockSubsystemInfo_t    *BlockSubsystem;
  int i;

  /* If MBM flag is not set just return */
  if(!amcInfo->isMBM)
    return;

  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {

    BlockSubsystem = (BlockSubsystemInfo_t *) AmcSubsystemReadMethodSpecificData(subSystem);
    if(!subSystem->takenIntoOptimal)
      AmcBlockSubsystemSetScheduledForRefinement(BlockSubsystem, 1);
    
  }

}


static int
AmcIsEverySubsystemRescheduled(
Amc_Info_t *amcInfo)
{
  array_t               *subSystemArray = amcInfo->subSystemArray;
  Amc_SubsystemInfo_t   *subSystem;  
  BlockSubsystemInfo_t  *BlockSubsystem;
  int i;

  /* If MBM flag is not set just return */
  if( !amcInfo->isMBM )
    return 1;

  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {

    BlockSubsystem = (BlockSubsystemInfo_t *) AmcSubsystemReadMethodSpecificData(subSystem);
    if( AmcBlockSubsystemReadScheduledForRefinement(BlockSubsystem) )
      return 1;
    
  }
  return 0;

}

static void
AmcPrintScheduleInformation(
Amc_Info_t *amcInfo)
{
  array_t                 *subSystemArray = amcInfo->subSystemArray;
  Amc_SubsystemInfo_t     *subSystem;  
  BlockSubsystemInfo_t    *BlockSubsystem;
  int i;

  /* If MBM flag is not set just return */
  if(!amcInfo->isMBM)
    return;

  fprintf(vis_stdout, "\nSchedule information : ");

  arrayForEachItem(Amc_SubsystemInfo_t *, subSystemArray, i, subSystem) {

    BlockSubsystem = (BlockSubsystemInfo_t *) AmcSubsystemReadMethodSpecificData(subSystem);
    fprintf(vis_stdout, " %d ", AmcBlockSubsystemReadScheduledForRefinement(BlockSubsystem) );
    
  }

}


#if 0

static void
AmcRescheduleForRefinement(
st_table        *fanOutSystemTable)
{
  Amc_SubsystemInfo_t   *subSystem;
  BlockSubsystemInfo_t  *BlockSubsystem;
  st_generator *stGen;

  st_foreach_item(fanOutSystemTable, stGen, &subSystem, NIL(char *)) {

    /* reschedule only ones that are not taken */
    if(!subSystem->takenIntoOptimal) {
      BlockSubsystem = (BlockSubsystemInfo_t *) AmcSubsystemReadMethodSpecificData(subSystem);
      AmcBlockSubsystemSetScheduledForRefinement(BlockSubsystem, 1);
    }

  }

}

static mdd_t *
AmcRefineWithSatisfyStatesOfFanInSystem(
Amc_SubsystemInfo_t     *subSystem,
mdd_t                   *careStates)
{
  st_table              *fanInTable = AmcSubsystemReadFanInTable(subSystem);
  Amc_SubsystemInfo_t   *fanInSystem;
  st_generator          *stGen;

  mdd_t                 *oldCareStates = careStates;
  st_foreach_item(fanInTable, stGen, &fanInSystem, NIL(char *)) {

    if(fanInSystem->satisfyStates != NIL(mdd_t)) {
      mdd_t     *fanInSatisfyStates = mdd_dup(fanInSystem->satisfyStates);
      careStates = mdd_and(fanInSatisfyStates, oldCareStates, 1, 1);
      mdd_free(oldCareStates); mdd_free(fanInSatisfyStates);
      oldCareStates = careStates;
    }

  }

  return(careStates);
} /* end of "machine by machine" refinement of the careset */
#endif


static array_t *
AmcInitializeQuantifyVars(
Amc_SubsystemInfo_t *subSystem)
{
  array_t             *quantifyVars             = array_alloc(array_t *, 0);
  array_t             *quantifyPresentVars      = array_alloc(int, 0);
  array_t             *quantifyNextVars         = array_alloc(int, 0);
  array_t             *quantifyInputVars        = array_alloc(int, 0);
  Ntk_Network_t       *network = Fsm_FsmReadNetwork(AmcSubsystemReadFsm(subSystem));
  Ntk_Node_t          *latch;
  st_table            *vertexTable = AmcSubsystemReadVertexTable(subSystem);
  lsGen               gen;
    
  Ntk_NetworkForEachLatch(network, gen, latch) {
    char *latchName = Ntk_NodeReadName(latch); 
#ifdef AMC_DEBUG
        fprintf(vis_stdout, "\nlatch name: %s", latchName);
        fprintf(vis_stdout, "\n latch id: %d", Ntk_NodeReadMddId(latch));
        fprintf(vis_stdout, "\n latch id: %d", Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
        fflush(vis_stdout);
#endif
    if(!st_lookup(vertexTable, latchName, (char **)0)) {
    
      /* Next state variables. */
      array_insert_last(int, quantifyNextVars, Ntk_NodeReadMddId(Ntk_NodeReadShadow(latch)));
      /* Present state variables. */
      array_insert_last(int, quantifyPresentVars, Ntk_NodeReadMddId(latch));

    } /* end of if(st_lookup(vertexTable)) */
  } /* end of Ntk_NetworkForEachLatch */


  {
    st_table    *inputVarTable = st_init_table(st_numcmp, st_numhash);
    Ntk_Node_t  *primaryInput;
    /* Build the hash table of input vars of this subsystem. */
    /* arrayForEachItem(int, inputVarArray, i, inputVar) {
      st_insert(inputVarTable, (char *)(long)inputVar, (char *)0);
    } */

    Ntk_NetworkForEachInput(network, gen, primaryInput) {
      int       mddId = Ntk_NodeReadMddId(primaryInput);
#ifdef AMC_DEBUG
      char *inputName = Ntk_NodeReadName(primaryInput); 
      int       testMddId = Ntk_NodeReadMddId(primaryInput);
      fprintf(vis_stdout, "\nprimary input name : %s", inputName);
      fprintf(vis_stdout, "\nprimary input mdd id : %d", testMddId);
      fflush(vis_stdout);
#endif
      /* if(!st_lookup(inputVarTable, (char *)(long)mddId, (char **)0)) { */
        array_insert_last(int, quantifyInputVars, mddId);
      /* } */
    }
    st_free_table(inputVarTable);
  }

  array_insert_last(array_t *, quantifyVars, quantifyPresentVars); 
  array_insert_last(array_t *, quantifyVars, quantifyNextVars); 
  array_insert_last(array_t *, quantifyVars, quantifyInputVars); 
 
  return quantifyVars;

}


#if 0

static void
AmcFreeBlockInfo(
BlockInfo_t     *BlockInfo)
{

  if(BlockInfo->optimalSystem != NIL(Amc_SubsystemInfo_t)) {
    Amc_AmcSubsystemFree(BlockInfo->optimalSystem);
  }

}
#endif


static int
AmcBlockSubsystemReadScheduledForRefinement(
BlockSubsystemInfo_t        *system)
{
  return system->scheduledForRefinement;
}

static void
AmcBlockSubsystemSetScheduledForRefinement(
BlockSubsystemInfo_t        *system,
int                   data)
{
  system->scheduledForRefinement = data;
}


#if 0

static Amc_SubsystemInfo_t *
AmcBlockReadOptimalSubsystem(
BlockInfo_t        *system)
{
  return system->optimalSystem;
}
#endif

static void
AmcBlockSetOptimalSystem(
BlockInfo_t                  *system,
Amc_SubsystemInfo_t  *data)
{
  system->optimalSystem = data;
}

#if 0

static int
AmcBlockReadBestSystem(
BlockInfo_t        *system)
{
  return system->bestSystem;
}
#endif

static void
AmcBlockSetBestSystem(
BlockInfo_t                *system,
int                  data)
{
  system->bestSystem = data;
}

#if 0

static Amc_SubsystemInfo_t *
AmcClearInputVarsFromFSM(
Amc_SubsystemInfo_t   *subSystem)
{
  Fsm_Fsm_t     *fsm = subSystem->fsm;
  array_t       *inputVarArray = Fsm_FsmReadInputVars(fsm);
  array_t       *newInputVarArray = array_alloc(int, 0);

  array_free(inputVarArray);
  (void) Fsm_FsmSetInputVars(fsm, newInputVarArray);

  return(subSystem);
}
#endif