src/fsm/fsmCmd.c

Go to the documentation of this file.

#include "fsmInt.h"

static char rcsid[] UNUSED = "$Id: fsmCmd.c,v 1.122 2005/05/19 03:21:37 awedh Exp $";

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/
static jmp_buf timeOutEnv;

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

static int CommandComputeReach(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandReadFairness(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandResetFairness(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandPrintFairness(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandPrintImageInfo(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandPrintHdOptions(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandPrintArdcOptions(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandPrintTfmOptions(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandPrintHybridOptions(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandPrintMlpOptions(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandPrintGuidedSearchOptions(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static void TimeOutHandle(void);

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

void
Fsm_Init(void)
{
  Cmd_CommandAdd("compute_reach",   CommandComputeReach,   0);
  Cmd_CommandAdd("read_fairness",   CommandReadFairness,   0);
  Cmd_CommandAdd("reset_fairness",  CommandResetFairness,  0);
  Cmd_CommandAdd("print_fairness",  CommandPrintFairness,  0);
  Cmd_CommandAdd("print_img_info",  CommandPrintImageInfo, 0);
  Cmd_CommandAdd("print_hd_options",  CommandPrintHdOptions, 0);
  Cmd_CommandAdd("print_guided_search_options",  CommandPrintGuidedSearchOptions, 0);
  Cmd_CommandAdd("print_ardc_options",  CommandPrintArdcOptions, 0);
  Cmd_CommandAdd("print_tfm_options",  CommandPrintTfmOptions, 0);
  Cmd_CommandAdd("print_hybrid_options",  CommandPrintHybridOptions, 0);
  Cmd_CommandAdd("print_mlp_options",  CommandPrintMlpOptions, 0);
}


void
Fsm_End(void)
{
}

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


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

static int
CommandComputeReach(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int        c;
  mdd_t      *reachableStates = NIL(mdd_t);
  mdd_t      *initialStates;
  long        initialTime;
  long        finalTime;
  static int  verbosityLevel;
  static int  printStep;
  static int  timeOutPeriod;
  Fsm_Fsm_t  *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
  static int reorderFlag;
  static int reorderThreshold;
  static int shellFlag;
  static int depthValue;
  static int incrementalFlag;
  static int approxFlag;
  static int ardc;
  static int recompute;
  Fsm_RchType_t rchType;
  FILE *guideFile = NIL(FILE); /* file of hints for guided search */
  array_t *guideArray = NIL(array_t);
  Img_MethodType imgMethod;
  
  /*
   * These are the default values.  These variables must be declared static
   * to avoid lint warnings.  Since they are static, we must reinitialize
   * them outside of the variable declarations.
   */
  verbosityLevel = 0;
  printStep      = 0;
  timeOutPeriod  = 0;
  shellFlag = 0;
  depthValue = 0;
  incrementalFlag = 0;
  rchType = Fsm_Rch_Default_c;
  approxFlag = 0;
  ardc = 0;
  recompute = 0;

  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "d:fg:hir:s:t:v:A:DF")) != EOF) {
    switch(c) {
      case 'd':
        depthValue = atoi(util_optarg);
        break;
      case 'f':
        shellFlag = 1;
        break;
      case 'g':
          guideFile = Cmd_FileOpen(util_optarg, "r", NIL(char *), 0);
          if (guideFile == NIL(FILE)) {
            fprintf(vis_stdout,
                    "** rch error: Guide file cannot be read. Check permissions and path\n");
            goto usage;
          }
          break;  
      case 'h':
        goto usage;
      case 'i':
        incrementalFlag = 1;
        break;
      case 'r':
        reorderFlag = 1;
        reorderThreshold = atoi(util_optarg);
        break;
      case 's':
        printStep = atoi(util_optarg);
        break;
      case 't':
        timeOutPeriod = atoi(util_optarg);
        break;
      case 'v':
        verbosityLevel = atoi(util_optarg);
        break;
      case 'A' :
        approxFlag = atoi(util_optarg);
        if ((approxFlag > 2) || (approxFlag < 0)) {
            goto usage;
        }
        break;
      case 'D':
        ardc = 1;
        break;
      case 'F':
        recompute = 1;
        break;
      default:
        goto usage;
    }
  }
  if (c == EOF && argc != util_optind)
    goto usage;
  
  imgMethod = Img_UserSpecifiedMethod(); 
    
  if ((approxFlag == 1) && (bdd_get_package_name() != CUDD)) {
    fprintf(vis_stderr, "** rch error: compute_reach with -A 1 option is currently supported only by CUDD.\n");
    return 1;
  }

  if (fsm == NIL(Fsm_Fsm_t)) {
    return 1;
  }

  if (incrementalFlag && approxFlag) {
      fprintf(vis_stdout,
              "** rch error: Incremental flag and approx flag are incompatible.\n");
      goto usage;
  }
  if (incrementalFlag && ardc) {
      fprintf(vis_stdout,
              "** rch error: The -i and -D flags are incompatible.\n");
      goto usage;
  }

  if (depthValue && approxFlag == 2) {
    fprintf(vis_stdout,
            "** rch error: Depth value and over-approx flag are incompatible.\n");
    goto usage;
  }
  
  if (shellFlag && approxFlag == 2) {
    fprintf(vis_stdout,
            "** rch error: Shell flag and over-approx flag are incompatible.\n");
    goto usage;
  }
  
  if (guideFile != NIL(FILE)){
    if(incrementalFlag) {
      fprintf(vis_stdout, "** rch error: Guided search is not compatible with the -i flag\n");
      goto usage;
    }
    if(approxFlag == 2){
      fprintf(vis_stdout, "** rch error: Guided search is not compatible with Over-approx flag\n");
      goto usage;
    }
    if(imgMethod != Img_Iwls95_c && imgMethod != Img_Monolithic_c &&
       imgMethod != Img_Mlp_c){
      fprintf(vis_stdout, "** rch error: Guided search can only be performed\n");
      fprintf(vis_stdout, "with IWLS95, MLP, or Monolithic image methods.\n");
    goto usage;
    }
  }/* if guided search requested */
  
  /* Start the timeOut timer. */
  if (timeOutPeriod > 0){
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(timeOutPeriod);
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stdout, "** rch info: Timeout occurred after %d seconds.\n",
                     timeOutPeriod);
      (void) fprintf(vis_stdout, "** rch warning: The time out may have "
                     "corrupted the data.\n");
     alarm(0);
      return 1;
    }
  }

  /* Make sure that the initial states can be computed without a problem. */
  error_init();
  initialStates = Fsm_FsmComputeInitialStates(fsm);
  if (initialStates == NIL(mdd_t)) {
    (void) fprintf(vis_stderr, "** rch error: Latch initialization function depends on another latch:\n");
    (void) fprintf(vis_stderr, "%s", error_string());
    (void) fprintf(vis_stderr, "\n");
    (void) fprintf(vis_stderr, "** rch error: Initial states cannot be computed.\n");
    return (1);
  }
  else {
    mdd_free(initialStates);
  }

  /* translate approx flag */
  switch(approxFlag) {
  case 0: rchType = Fsm_Rch_Bfs_c; break;
  case 1: rchType = Fsm_Rch_Hd_c; break;
  case 2: rchType = Fsm_Rch_Oa_c; break;
  default: rchType = Fsm_Rch_Default_c; break;
  }

  if (guideFile != NIL(FILE)) {
    guideArray = Mc_ComputeGuideArray(fsm, guideFile);
    if(guideArray == NIL(array_t))
      return(1);
  }

  if (rchType == Fsm_Rch_Oa_c) {
    array_t     *apprReachableStates;

    initialTime = util_cpu_time();
    apprReachableStates = Fsm_FsmComputeOverApproximateReachableStates(fsm,
        incrementalFlag, verbosityLevel, printStep, depthValue, shellFlag,
        reorderFlag, reorderThreshold, recompute);
    finalTime = util_cpu_time();

    if (apprReachableStates == NIL(array_t)) {
      (void)fprintf(vis_stdout,
        "** rch error: Reachability computation failed, no rechable states\n");
      return 1;
    }

    if (verbosityLevel > 0)
      Fsm_ArdcPrintReachabilityResults(fsm, finalTime-initialTime);
    alarm(0);
    return(0);
  }

  /* Compute the reachable states. */
  initialTime = util_cpu_time();
  reachableStates = Fsm_FsmComputeReachableStates(
    fsm, incrementalFlag, verbosityLevel, printStep, depthValue, shellFlag,
    reorderFlag, reorderThreshold, rchType, ardc, recompute, NIL(array_t),
    (verbosityLevel > 0), guideArray);  
  finalTime = util_cpu_time();
  mdd_array_free(guideArray);

  if (reachableStates == NIL(mdd_t)) {
    (void)fprintf(vis_stdout, "** rch error: Reachability computation failed, no rechable states\n");
    return 1;
  }

  if (verbosityLevel > 0){
    if (fsm->imageInfo){ 
      char *methodType =
          Img_ImageInfoObtainMethodTypeAsString(fsm->imageInfo); 
      (void) fprintf(vis_stdout, "** rch info: Computing reachable states using the ");
      (void) fprintf(vis_stdout, "%s image computation method.\n", methodType);
      FREE(methodType);
      (void)Img_ImageInfoPrintMethodParams(fsm->imageInfo,
                                           vis_stdout);
      if (Img_ImageInfoObtainMethodType(fsm->imageInfo) == Img_Tfm_c ||
          Img_ImageInfoObtainMethodType(fsm->imageInfo) == Img_Hybrid_c) {
        Img_TfmPrintStatistics(fsm->imageInfo, Img_Forward_c);
      }
    }
    Fsm_FsmReachabilityPrintResults(fsm, finalTime-initialTime, approxFlag);

  }
  mdd_free(reachableStates);

  alarm(0);
  return (0);

  usage:
  (void) fprintf(vis_stderr, "usage: compute_reach [-d depthValue] [-h] [-f] [-i] [-g <hint file>][-r thresholdValue] [-s printStep] [-t timeOut] [-v #][-A #][-D][-F]\n");
  (void) fprintf(vis_stderr, "   -d depthValue perform reachability up to depthValue steps\n");
  (void) fprintf(vis_stderr, "   -f \t\t store the onion rings ateach step\n");
  (void) fprintf(vis_stderr, "   -h \t\t print the command usage\n");
  (void) fprintf(vis_stderr, "   -g filename\t perform reachability analysis with guided search using the given file. Not allowed with -A 2\n");
  (void) fprintf(vis_stderr, "   -i \t\t builds the transition relation incrementally (not supported with -A 1,2).\n");
  (void) fprintf(vis_stderr, "   -r thresholdValue invoke dynamic reordering once when the size of the reached state set reaches this value.\n");
  (void) fprintf(vis_stderr, "   -s printStep\t print reachability information every printStep steps (0 for no information).\n");
  (void) fprintf(vis_stderr, "   -t time\t time out period (in seconds)\n");
  (void) fprintf(vis_stderr, "   -v #\t\t verbosity level\n");
  (void) fprintf(vis_stderr, "   -A #\t\t 0 (default) - BFS method.\n");
  (void) fprintf(vis_stderr, "      #\t\t 1 - HD method.\n");
  (void) fprintf(vis_stderr, "      #\t\t 2 - Over-approximation by approximate traversal.\n");
  (void) fprintf(vis_stderr, "   -D \t\t Try to minimize transition relation with ARDCs\n");
  (void) fprintf(vis_stderr, "   -F \t\t force to recompute reachable states\n");
  return 1;
}


static int
CommandReadFairness(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int       c;
  FILE      *fp;
  array_t   *formulaArray;
  Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
  
  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "h")) != EOF) {
    switch(c) {
      case 'h':
        goto usage;
      default:
        goto usage;
    }
    /* NOT REACHED */
  }

  if (fsm == NIL(Fsm_Fsm_t)) {
    (void) fprintf(vis_stderr, "** fair error: Fairness constraint not recorded.\n");
    return 1;
  }

  /*
   * Open the fairness file.
   */
  if (argc - util_optind == 0) {
    (void) fprintf(vis_stderr, "** fair error: fairness file not provided\n");
    goto usage;
  }
  else if (argc - util_optind > 1) {
    (void) fprintf(vis_stderr, "** fair error: too many arguments\n");
    goto usage;
  }

  fp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
  if (fp == NIL(FILE)) {
    return 1;
  }

  /*
   * Parse the formulas in the file.
   */
  formulaArray = Ctlp_FileParseFormulaArray(fp);
  (void) fclose(fp);

  if (formulaArray == NIL(array_t)) {
    (void) fprintf(vis_stderr, "** fair error: error reading fairness conditions.\n");
    return 1;
  }
  else if (array_n(formulaArray) == 0) {
    (void) fprintf(vis_stderr, "** fair error: fairness file is empty.\n");
    (void) fprintf(vis_stderr, "** fair error: Use reset_fairness to reset the fairness constraint.");
    return 1;
  }
  else {
    int             j;
    Fsm_Fairness_t *fairness;
    Ntk_Network_t  *network = Fsm_FsmReadNetwork(fsm);

    /*
     * First check that each formula is semantically correct wrt the network.
     */
    error_init();
    for (j = 0; j < array_n(formulaArray); j++) {
      Ctlp_Formula_t *formula;
      boolean         status; 
      
      formula  = array_fetch(Ctlp_Formula_t *, formulaArray, j);
      status = Mc_FormulaStaticSemanticCheckOnNetwork(formula, network, FALSE);
      
      if (status == FALSE) {
        (void) fprintf(vis_stderr,
                       "** fair error: error reading fairness constraint "); 
        Ctlp_FormulaPrint(vis_stderr, formula);
        (void) fprintf(vis_stderr, ":\n");
        (void) fprintf(vis_stderr, "%s", error_string());
        (void) fprintf(vis_stderr, "\n");
        return 1;
      }
    }


    /*
     * Interpret the array of CTL formulas as a set of Buchi conditions.
     * Hence, create a single disjunct, consisting of k conjuncts, where k is
     * the number of CTL formulas read in.  The jth conjunct has the jth
     * formula as its finallyInf component, and NULL as its globallyInf
     * component.
     */
    fairness = FsmFairnessAlloc(fsm);    
    for (j = 0; j < array_n(formulaArray); j++) {
      Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, formulaArray, j);

      FsmFairnessAddConjunct(fairness, formula, NIL(Ctlp_Formula_t), 0, j);
    }
    array_free(formulaArray); /* Don't free the formulas themselves. */

    /*
     * Remove any existing fairnessInfo associated with the FSM, and update
     * the fairnessInfo.constraint with the new fairness just read.
     */
    FsmFsmFairnessInfoUpdate(fsm, NIL(mdd_t), fairness, NIL(array_t));

    return 0;
  }

  usage:
  (void) fprintf(vis_stderr, "usage: read_fairness [-h] file\n");
  (void) fprintf(vis_stderr, "   -h    print the command usage\n");
  (void) fprintf(vis_stderr, "   file  file containing the list of conditions\n");
  return 1;
}


static int
CommandResetFairness(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int       c;
  Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);

  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "h")) != EOF) {
    switch(c) {
      case 'h':
        goto usage;
      default:
        goto usage;
    }
    /* NOT REACHED */
  }

  if (fsm == NIL(Fsm_Fsm_t)) {
    return 1;
  }

  /*
   * Remove any existing fairnessInfo associated with the FSM, and add back
   * the default constraint.
   */
  FsmFsmFairnessInfoUpdate(fsm, NIL(mdd_t), NIL(Fsm_Fairness_t), NIL(array_t));
  fsm->fairnessInfo.constraint = FsmFsmCreateDefaultFairnessConstraint(fsm);

  return 0;


  usage:
  (void) fprintf(vis_stderr, "usage: reset_fairness [-h]\n");
  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
  return 1;
}


static int
CommandPrintFairness(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  int            c;
  Fsm_Fairness_t *constraint;
  int             numDisjuncts;
  Fsm_Fsm_t      *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);

  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "h")) != EOF) {
    switch(c) {
      case 'h':
        goto usage;
      default:
        goto usage;
    }
    /* NOT REACHED */
  }

  if (fsm == NIL(Fsm_Fsm_t)) {
    return 1;
  }

  /*
   * Print the fairness constraint.  It is assumed that there is at least one
   * disjunct present.  Currently, only Buchi constraints can be printed out.
   */
  constraint = Fsm_FsmReadFairnessConstraint(fsm);
  assert(constraint != NIL(Fsm_Fairness_t));
  numDisjuncts = Fsm_FairnessReadNumDisjuncts(constraint);
  assert(numDisjuncts != 0);

  if (numDisjuncts > 1) {
    (void) fprintf(vis_stdout, "Fairness constraint not Buchi...");
    (void) fprintf(vis_stdout, "don't know how to print.\n");
  }
  else {
    int i;
    int numConjuncts = Fsm_FairnessReadNumConjunctsOfDisjunct(constraint, 0);

    (void) fprintf(vis_stdout, "Fairness constraint:\n");
    for (i = 0; i < numConjuncts; i++) {
      if (Fsm_FairnessReadGloballyInfFormula(constraint, 0, i) !=
          NIL(Ctlp_Formula_t)) {
        (void) fprintf(vis_stdout, "Fairness constraint not Buchi...");
        (void) fprintf(vis_stdout, "don't know how to print.\n");
      }
        
      Ctlp_FormulaPrint(vis_stdout,
                        Fsm_FairnessReadFinallyInfFormula(constraint, 0, i));
      (void) fprintf(vis_stdout, ";\n");
    }
  }

  return 0;

  usage:
  (void) fprintf(vis_stderr, "usage: print_fairness [-h]\n");
  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
  return 1;
}


static int
CommandPrintImageInfo(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
{
  int c;
  Img_ImageInfo_t *imageInfo;
  Fsm_Fsm_t       *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
  int bwdImgFlag = 0;
  int fwdImgFlag = 0;

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "bfh")) != EOF) {
    switch(c) {
      case 'b':
        bwdImgFlag = 1;
        break;
      case 'f':
        fwdImgFlag = 1;
        break;
      case 'h':
        goto usage;
      default:
        goto usage;
    }
  }

  if (fsm == NIL(Fsm_Fsm_t)) {
    return 1;
  }

  if (!(bwdImgFlag || fwdImgFlag)){
    fwdImgFlag = 1;
  }

  imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, bwdImgFlag, fwdImgFlag);
  Img_ImageInfoPrintMethodParams(imageInfo, vis_stdout);
  return 0;

usage:
  (void) fprintf(vis_stderr,"usage: print_image_method [-b] [-f] [-h]\n");
  (void) fprintf(vis_stderr, "  -b  create the backward transition relation\n");
  (void) fprintf(vis_stderr, "  -f  create the forward transition relation\n");
  (void) fprintf(vis_stderr, "  -h  print the command usage\n");
  return 1;
}

static int
CommandPrintHdOptions(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
{
  int c;

  if (*hmgr == NULL) {
    fprintf(vis_stderr,"** hrc error: Hierarchy manager is empty\n");
    return 1;
  }

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "h")) != EOF) {
    switch(c) {
      case 'h':
        goto usage;
      default:
        goto usage;
    }
     /* NOT REACHED */
 }

  /* print hd options */
  FsmHdPrintOptions();
  return 0;

usage:
  (void) fprintf(vis_stderr,"usage: print_hd_options [-h]\n");
  (void) fprintf(vis_stderr, "  -h  print the command usage\n");
  return 1;
} /* end of CommandPrintHdOptions */


static int
CommandPrintArdcOptions(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
{
  int c;

  if (*hmgr == NULL) {
    fprintf(vis_stderr,"** hrc error: Hierarchy manager is empty\n");
    return 1;
  }

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "hH")) != EOF) {
    switch(c) {
      case 'h':
        goto usage;
      case 'H':
        goto usage_ardc;
      default:
        goto usage;
    }
    /* NOT REACHED */
  }

  /* print ARDC options */
  FsmArdcPrintOptions();
  return 0;

usage:
  (void) fprintf(vis_stderr,"usage: print_ardc_options [-h] [-H]\n");
  (void) fprintf(vis_stderr, "  -h  print the command usage\n");
  (void) fprintf(vis_stderr, "  -H  print the ARDC set command usage\n");
  return 1;
usage_ardc:
  (void) fprintf(vis_stderr, "   set ardc_traversal_method <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : MBM (machine by machine)\n");
  (void) fprintf(vis_stderr, "       m = 1 : RFBF(reached frame by frame)\n");
  (void) fprintf(vis_stderr, "       m = 2 : TFBF(to frame by frame)\n");
  (void) fprintf(vis_stderr, "       m = 3 : TMBM(TFBF + MBM)\n");
  (void) fprintf(vis_stderr, "       m = 4 : LMBM(least fixpoint MBM, default)\n");
  (void) fprintf(vis_stderr, "       m = 5 : TLMBM(TFBF + LMBM)\n");
  (void) fprintf(vis_stderr, "   set ardc_group_size <n>\n");
  (void) fprintf(vis_stderr, "       n (default = 8)\n");
  (void) fprintf(vis_stderr, "   set ardc_affinity_factor <f>\n");
  (void) fprintf(vis_stderr, "       f = 0.0 - 1.0 (default = 0.5)\n");
  (void) fprintf(vis_stderr, "   set ardc_max_iteration <n>\n");
  (void) fprintf(vis_stderr, "       n (default = 0(infinity))\n");
  (void) fprintf(vis_stderr, "   set ardc_constrain_target <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : constrain transition relation (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : constrain initial states\n");
  (void) fprintf(vis_stderr, "       m = 2 : constrain both\n");
  (void) fprintf(vis_stderr, "   set ardc_constrain_method <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : restrict (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : constrain\n");
  (void) fprintf(vis_stderr,
                 "       m = 2 : compact (currently supported by only CUDD)\n");
  (void) fprintf(vis_stderr,
                 "       m = 3 : squeeze (currently supported by only CUDD)\n");
  (void) fprintf(vis_stderr, "   set ardc_constrain_reorder <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : allow variable reorderings during consecutive\n");
  (void) fprintf(vis_stderr, "                 image constraining operations (default)\n");
  (void) fprintf(vis_stderr, "       m = no  : don't allow variable reorderings during consecutive\n");
  (void) fprintf(vis_stderr, "                 image constraining operations\n");
  (void) fprintf(vis_stderr, "   set ardc_abstract_pseudo_input <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : do not abstract pseudo input variables\n");
  (void) fprintf(vis_stderr, "       m = 1 : abstract pseudo inputs before image computation (default)\n");
  (void) fprintf(vis_stderr, "       m = 2 : abstract pseudo inputs at every end of image computation\n");
  (void) fprintf(vis_stderr, "       m = 3 : abstract pseudo inputs at the end of approximate traversal\n");
  (void) fprintf(vis_stderr, "   set ardc_decompose_flag <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : keep decomposed reachable stateses (default)\n");
  (void) fprintf(vis_stderr, "       m = no  : make a conjunction of reachable states of all submachines\n");
  (void) fprintf(vis_stderr, "   set ardc_projected_initial_flag <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : use projected initial states for submachine (default)\n");
  (void) fprintf(vis_stderr, "       m = no  : use original initial states for submachine\n");
  (void) fprintf(vis_stderr, "   set ardc_image_method <m>\n");
  (void) fprintf(vis_stderr, "       m = monolithic : use monolithic image computation for submachines\n");
  (void) fprintf(vis_stderr, "       m = iwls95     : use iwls95 image computation for submachines (default)\n");
  (void) fprintf(vis_stderr, "       m = mlp        : use mlp image computation for submachines\n");
  (void) fprintf(vis_stderr, "       m = tfm        : use tfm image computation for submachines\n");
  (void) fprintf(vis_stderr, "       m = hybrid     : use hybrid image computation for submachines\n");
  (void) fprintf(vis_stderr, "   set ardc_use_high_density <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : use High Density for reachable states of submachines\n");
  (void) fprintf(vis_stderr, "       m = no  : use BFS for reachable states of submachines (default)\n");
  (void) fprintf(vis_stderr, "   set ardc_create_pseudo_var_mode <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : makes pseudo input variables with exact support (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : makes pseudo input variables from all state variables of\n");
  (void) fprintf(vis_stderr, "               the other machines\n");
  (void) fprintf(vis_stderr, "       m = 2 : makes pseudo input variables from all state variables of\n");
  (void) fprintf(vis_stderr, "               fanin machines\n");
  (void) fprintf(vis_stderr, "   set ardc_reorder_ptr <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : whenever partitioned transition relation changes,\n");
  (void) fprintf(vis_stderr, "                 reorders partitioned transition relation\n");
  (void) fprintf(vis_stderr, "       m = no  : no reordering of partitioned transition relation (default)\n");
  (void) fprintf(vis_stderr, "   set ardc_fanin_constrain_mode <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : constrains w.r.t. the reachable states of fanin machines\n");
  (void) fprintf(vis_stderr, "               (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : constrains w.r.t. the reachable states of both fanin machines\n");
  (void) fprintf(vis_stderr, "               and itself\n");
  (void) fprintf(vis_stderr, "   set ardc_lmbm_initial_mode <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : use given initial states all the time\n");
  (void) fprintf(vis_stderr, "       m = 1 : use current reached states as initial states (default)\n");
  (void) fprintf(vis_stderr, "       m = 2 : use current frontier as initial states\n");
  (void) fprintf(vis_stderr, "   set ardc_mbm_reuse_tr <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : use constrained transition relation for next iteration\n");
  (void) fprintf(vis_stderr, "       m = no  : use original transition relation for next iteration (default)\n");
  (void) fprintf(vis_stderr, "   set ardc_read_group <filename>\n");
  (void) fprintf(vis_stderr, "       <filename> file containing grouping information\n");
  (void) fprintf(vis_stderr, "   set ardc_write_group <filename>\n");
  (void) fprintf(vis_stderr, "       <filename> file to write grouping information\n");
  (void) fprintf(vis_stderr, "   set ardc_verbosity <n>\n");
  (void) fprintf(vis_stderr, "       n = 0 - 3 (default = 0)\n");
  return 1;
} /* end of CommandPrintArdcOptions */


static int
CommandPrintTfmOptions(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
{
  int c;

  if (*hmgr == NULL) {
    fprintf(vis_stderr,"** hrc error: Hierarchy manager is empty\n");
    return 1;
  }

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "hH")) != EOF) {
    switch(c) {
      case 'h':
        goto usage;
      case 'H':
        goto usage_tfm;
      default:
        goto usage;
    }
     /* NOT REACHED */
 }

  /* print transition function based image computation options */
  Img_PrintTfmOptions();
  return 0;

usage:
  (void) fprintf(vis_stderr,"usage: print_tfm_options [-h] [-H]\n");
  (void) fprintf(vis_stderr, "  -h  print the command usage\n");
  (void) fprintf(vis_stderr, "  -H  print the transition function based ");
  (void) fprintf(vis_stderr, "image computation set command usage\n");
  return 1;
usage_tfm:
  (void) fprintf(vis_stderr, "   set tfm_split_method <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : input splitting (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : output splitting\n");
  (void) fprintf(vis_stderr, "       m = 2 : mixed (input split + output split)\n");
  (void) fprintf(vis_stderr, "   set tfm_input_split <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : support before splitting (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : support after splitting\n");
  (void) fprintf(vis_stderr, "       m = 2 : estimate BDD size after splitting\n");
  (void) fprintf(vis_stderr, "       m = 3 : top variable\n");
  (void) fprintf(vis_stderr, "   set tfm_pi_split_flag <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : choose either state or input variable as splitting variable\n");
  (void) fprintf(vis_stderr, "                 (default)\n");
  (void) fprintf(vis_stderr, "       m = no  : choose only state variable as splitting variable\n");
  (void) fprintf(vis_stderr, "   set tfm_range_comp <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : do not convert to range computation\n");
  (void) fprintf(vis_stderr, "       m = 1 : convert image to range computation (default)\n");
  (void) fprintf(vis_stderr, "       m = 2 : use a threshold (tfm_range_threshold, default for hybrid)\n");
  (void) fprintf(vis_stderr, "   set tfm_range_threshold <n>\n");
  (void) fprintf(vis_stderr, "       n (default = 10)\n");
  (void) fprintf(vis_stderr, "   set tfm_range_try_threshold <n>\n");
  (void) fprintf(vis_stderr, "       n (default = 2)\n");
  (void) fprintf(vis_stderr, "   set tfm_range_check_reorder <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : force to reorder before checking tfm_range_threshold\n");
  (void) fprintf(vis_stderr, "       m = no  : do not reorder (default)\n");
  (void) fprintf(vis_stderr, "   set tfm_tie_break_mode <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : the closest variable to top (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : the smallest BDD size after splitting\n");
  (void) fprintf(vis_stderr, "   set tfm_output_split <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : smallest BDD size (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : largest BDD size\n");
  (void) fprintf(vis_stderr, "       m = 2 : top variable\n");
  (void) fprintf(vis_stderr, "   set tfm_turn_depth <n>\n");
  (void) fprintf(vis_stderr, "       n (default = 5, -1 for hybrid)\n");
  (void) fprintf(vis_stderr, "   set tfm_find_decomp_var <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : try to find a decomposable variable (articulation point)\n");
  (void) fprintf(vis_stderr, "       m = no  : do not try (default)\n");
  (void) fprintf(vis_stderr, "   set tfm_sort_vector_flag <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : sort function vectors to utilize cache (default for tfm)\n");
  (void) fprintf(vis_stderr, "       m = no  : do not sort (default for hybrid)\n");
  (void) fprintf(vis_stderr, "   set tfm_print_stats <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : print statistics for cache and recursions\n");
  (void) fprintf(vis_stderr, "       m = no  : do not print (default)\n");
  (void) fprintf(vis_stderr, "   set tfm_print_bdd_size <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : print BDD size of all intermediate product\n");
  (void) fprintf(vis_stderr, "       m = no  : do not print (default)\n");
  (void) fprintf(vis_stderr, "   set tfm_split_cube_func <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : find a cube function element,\n");
  (void) fprintf(vis_stderr, "                 then apply output splitting in input splitting\n");
  (void) fprintf(vis_stderr, "       m = no  : do not try (default)\n");
  (void) fprintf(vis_stderr, "   set tfm_find_essential <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : do not try (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : try to find essential variables\n");
  (void) fprintf(vis_stderr, "       m = 2 : on and off dynamically\n");
  (void) fprintf(vis_stderr, "   set tfm_print_essential <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : do not print (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : print only at end\n");
  (void) fprintf(vis_stderr, "       m = 2 : print at every image computation\n");
  (void) fprintf(vis_stderr, "   set tfm_use_cache <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : do not use cache (default for hybrid)\n");
  (void) fprintf(vis_stderr, "       m = 1 : use cache (default)\n");
  (void) fprintf(vis_stderr, "       m = 2 : store all intermediate results\n");
  (void) fprintf(vis_stderr, "   set tfm_global_cache <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : use only one global cache (default)\n");
  (void) fprintf(vis_stderr, "       m = no  : use one cache per machine\n");
  (void) fprintf(vis_stderr, "   set tfm_max_chain_length <n>\n");
  (void) fprintf(vis_stderr, "       n (default = 2)\n");
  (void) fprintf(vis_stderr, "   set tfm_init_cache_size <n>\n");
  (void) fprintf(vis_stderr, "       n (default = 1001)\n");
  (void) fprintf(vis_stderr, "   set tfm_auto_flush_cache <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : flush cache only when requested\n");
  (void) fprintf(vis_stderr, "       m = 1 : flush cache at the end of image computation (default)\n");
  (void) fprintf(vis_stderr, "       m = 2 : flush cache before reordering\n");
  (void) fprintf(vis_stderr, "   set tfm_compose_intermediate_vars <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : compose all intermediate vars\n");
  (void) fprintf(vis_stderr, "       m = no  : do not compose (default)\n");
  (void) fprintf(vis_stderr, "   set tfm_pre_split_method <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : input splitting (domain cofactoring, default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : output splitting (constraint cofactoring)\n");
  (void) fprintf(vis_stderr, "       m = 2 : mixed (input split + output split)\n");
  (void) fprintf(vis_stderr, "       m = 3 : substitution\n");
  (void) fprintf(vis_stderr, "   set tfm_pre_input_split <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : support before splitting (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : support after splitting\n");
  (void) fprintf(vis_stderr, "       m = 2 : estimate BDD size after splitting\n");
  (void) fprintf(vis_stderr, "       m = 3 : top variable\n");
  (void) fprintf(vis_stderr, "   set tfm_pre_output_split <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : smallest BDD size (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : largest BDD size\n");
  (void) fprintf(vis_stderr, "       m = 2 : top variable\n");
  (void) fprintf(vis_stderr, "   set tfm_pre_dc_leaf_method <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : substitution (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : constraint cofactoring\n");
  (void) fprintf(vis_stderr, "       m = 2 : hybrid\n");
  (void) fprintf(vis_stderr, "   set tfm_pre_minimize <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : minimize function vector w.r.t. a chosen function\n");
  (void) fprintf(vis_stderr, "                 in constraint cofactoring\n");
  (void) fprintf(vis_stderr, "       m = no  : do not minimize (default)\n");
  (void) fprintf(vis_stderr, "   set tfm_verbosity <n>\n");
  (void) fprintf(vis_stderr, "       n = 0 - 2 (default = 0)\n");
  return 1;
} /* end of CommandPrintTfmOptions */


static int
CommandPrintHybridOptions(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
{
  int c;

  if (*hmgr == NULL) {
    fprintf(vis_stderr,"** hrc error: Hierarchy manager is empty\n");
    return 1;
  }

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "hH")) != EOF) {
    switch(c) {
      case 'h':
        goto usage;
      case 'H':
        goto usage_hybrid;
      default:
        goto usage;
    }
  }

  /* print hybrid image computation options */
  Img_PrintHybridOptions();
  return 0;

usage:
  (void) fprintf(vis_stderr,"usage: print_hybrid_options [-h] [-H]\n");
  (void) fprintf(vis_stderr, "  -h  print the command usage\n");
  (void) fprintf(vis_stderr,
                "  -H  print the hybrid image computation set command usage\n");
  return 1;
usage_hybrid:
  (void) fprintf(vis_stderr, "   set hybrid_mode <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : start with only transition function\n");
  (void) fprintf(vis_stderr, "       m = 1 : start with both transition function and relation at the beginning (default)\n");
  (void) fprintf(vis_stderr, "       m = 2 : start with only transition relation\n");
  (void) fprintf(vis_stderr, "   set hybrid_tr_split_method <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : use support (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : use estimate BDD size\n");
  (void) fprintf(vis_stderr, "   set hybrid_build_partial_tr <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : build partial transition relation\n");
  (void) fprintf(vis_stderr, "       m = no  : build full transition relation (default)\n");
  (void) fprintf(vis_stderr, "   set hybrid_partial_num_vars <n>\n");
  (void) fprintf(vis_stderr, "       n (default = 8)\n");
  (void) fprintf(vis_stderr, "   set hybrid_partial_method <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : use BDD size (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : use support\n");
  (void) fprintf(vis_stderr, "   set hybrid_delayed_split <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : apply splitting to transition relation at once\n");
  (void) fprintf(vis_stderr, "       m = no  : do not apply (default)\n");
  (void) fprintf(vis_stderr, "   set hybrid_split_min_depth <n>\n");
  (void) fprintf(vis_stderr, "       n (default = 1)\n");
  (void) fprintf(vis_stderr, "   set hybrid_split_max_depth <n>\n");
  (void) fprintf(vis_stderr, "       n (default = 5)\n");
  (void) fprintf(vis_stderr, "   set hybrid_pre_split_min_depth <n>\n");
  (void) fprintf(vis_stderr, "       n (default = 0)\n");
  (void) fprintf(vis_stderr, "   set hybrid_pre_split_max_depth <n>\n");
  (void) fprintf(vis_stderr, "       n (default = 4)\n");
  (void) fprintf(vis_stderr, "   set hybrid_lambda_threshold <f>\n");
  (void) fprintf(vis_stderr, "       f (default = 0.6)\n");
  (void) fprintf(vis_stderr, "   set hybrid_pre_lambda_threshold <f>\n");
  (void) fprintf(vis_stderr, "       f (default = 0.65)\n");
  (void) fprintf(vis_stderr, "   set hybrid_conjoin_vector_size <n>\n");
  (void) fprintf(vis_stderr, "       n (default = 10)\n");
  (void) fprintf(vis_stderr, "   set hybrid_conjoin_relation_size <n>\n");
  (void) fprintf(vis_stderr, "       n (default = 2)\n");
  (void) fprintf(vis_stderr, "   set hybrid_conjoin_relation_bdd_size <n>\n");
  (void) fprintf(vis_stderr, "       n (default = 200)\n");
  (void) fprintf(vis_stderr, "   set hybrid_improve_lambda <f>\n");
  (void) fprintf(vis_stderr, "       f (default = 0.1)\n");
  (void) fprintf(vis_stderr, "   set hybrid_improve_vector_size <n>\n");
  (void) fprintf(vis_stderr, "       n (default = 3)\n");
  (void) fprintf(vis_stderr, "   set hybrid_improve_vector_bdd_size <f>\n");
  (void) fprintf(vis_stderr, "       f (default = 30.0)\n");
  (void) fprintf(vis_stderr, "   set hybrid_decide_mode <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : use only lambda\n");
  (void) fprintf(vis_stderr, "       m = 1 : use lambda and special checks\n");
  (void) fprintf(vis_stderr, "       m = 2 : use lambda and improvement\n");
  (void) fprintf(vis_stderr, "       m = 3 : use all (default)\n");
  (void) fprintf(vis_stderr, "   set hybrid_reorder_with_from <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : include from set in reordering relation array (default)\n");
  (void) fprintf(vis_stderr, "       m = no  : do not include\n");
  (void) fprintf(vis_stderr, "   set hybrid_pre_reorder_with_from <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : include from set in reordering relation array\n");
  (void) fprintf(vis_stderr, "       m = no  : do not include (default)\n");
  (void) fprintf(vis_stderr, "   set hybrid_lambda_mode <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : total lifetime with ps/pi variables (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : active lifetime with ps/pi variables\n");
  (void) fprintf(vis_stderr, "       m = 2 : total lifetime with ps/ns/pi variables\n");
  (void) fprintf(vis_stderr, "   set hybrid_pre_lambda_mode <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : total lifetime with ns/pi variables\n");
  (void) fprintf(vis_stderr, "       m = 1 : active lifetime with ps/pi variables\n");
  (void) fprintf(vis_stderr, "       m = 2 : total lifetime with ps/ns/pi variables (default)\n");
  (void) fprintf(vis_stderr, "       m = 3 : total lifetime with ps/pi variables\n");
  (void) fprintf(vis_stderr, "   set hybrid_lambda_with_from <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : include from set in lambda computation (default)\n");
  (void) fprintf(vis_stderr, "       m = no  : do not include\n");
  (void) fprintf(vis_stderr, "   set hybrid_lambda_with_clustering <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : compute lambda after clustering\n");
  (void) fprintf(vis_stderr, "       m = no  : do not cluster (default)\n");
  (void) fprintf(vis_stderr, "   set hybrid_synchronize_tr <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : rebuild transition relation whenever function vector changes\n");
  (void) fprintf(vis_stderr, "       m = no  : do not rebuild (default)\n");
  (void) fprintf(vis_stderr, "   set hybrid_img_keep_pi <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : keep all pi variables in forward tr\n");
  (void) fprintf(vis_stderr, "       m = no  : quantify out local pi variables (default)\n");
  (void) fprintf(vis_stderr, "   set hybrid_pre_keep_pi <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : keep all pi variables in backward tr and preimages\n");
  (void) fprintf(vis_stderr, "       m = no  : quantify out local pi variables (default)\n");
  (void) fprintf(vis_stderr, "   set hybrid_pre_canonical <m>\n");
  (void) fprintf(vis_stderr, "       m = yes : canonicalize the function vector for preimage\n");
  (void) fprintf(vis_stderr, "       m = no  : do not canonicalize (default)\n");
  (void) fprintf(vis_stderr, "   set hybrid_tr_method <m>\n");
  (void) fprintf(vis_stderr, "       m = iwls95 (default)\n");
  (void) fprintf(vis_stderr, "       m = mlp\n");
  return 1;
} /* end of CommandPrintHybridOptions */


static int
CommandPrintMlpOptions(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
{
  int c;

  if (*hmgr == NULL) {
    fprintf(vis_stderr,"** hrc error: Hierarchy manager is empty\n");
    return 1;
  }

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "hH")) != EOF) {
    switch(c) {
      case 'h':
        goto usage;
      case 'H':
        goto usage_mlp;
      default:
        goto usage;
    }
  }

  /* print hybrid image computation options */
  Img_PrintMlpOptions();
  return 0;

usage:
  (void) fprintf(vis_stderr,"usage: print_mlp_options [-h] [-H]\n");
  (void) fprintf(vis_stderr, "  -h  print the command usage\n");
  (void) fprintf(vis_stderr,
                "  -H  print the MLP image computation set command usage\n");
  return 1;
usage_mlp:
  (void) fprintf(vis_stderr, "   set mlp_cluster <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : linear clustering\n");
  (void) fprintf(vis_stderr, "       m = 1 : affinity based tree clustering (default)\n");
  (void) fprintf(vis_stderr, "   set mlp_reorder <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : no reordering after clustering (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : reorder using MLP after clustering (inside)\n");
  (void) fprintf(vis_stderr, "       m = 2 : reorder using MLP after clustering (outside)\n");
  (void) fprintf(vis_stderr, "       m = 3 : reorder using IWLS95 after clustering\n");
  (void) fprintf(vis_stderr, "   set mlp_pre_reorder <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : no reordering after clustering (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : reorder using MLP after clustering (inside)\n");
  (void) fprintf(vis_stderr, "       m = 2 : reorder using MLP after clustering (outside)\n");
  (void) fprintf(vis_stderr, "       m = 3 : reorder using IWLS95 after clustering\n");
  (void) fprintf(vis_stderr, "   set mlp_postprocess <m>\n");
  (void) fprintf(vis_stderr, "       m = 0 : no postprocessing (default)\n");
  (void) fprintf(vis_stderr, "       m = 1 : do postprocessing after ordering\n");
  (void) fprintf(vis_stderr, "       m = 2 : do postprocessing after clustering or reordering\n");
  (void) fprintf(vis_stderr, "       m = 3 : do both 1 and 2\n");
  return 1;
} /* end of CommandPrintMlpOptions */


static int
CommandPrintGuidedSearchOptions(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
{
  int c;
  if (*hmgr == NULL) {
    fprintf(vis_stderr,"** hrc error: Hierarchy manager is empty\n");
    return 1;
  }

  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "h")) != EOF) {
    switch(c) {
      case 'h':
        goto usage;
      default:
        goto usage;
    }
     /* NOT REACHED */
  }

  FsmGuidedSearchPrintOptions();
  return 0;
 usage:
  (void) fprintf(vis_stderr,"usage: print_guided_search_options [-h]\n");
  (void) fprintf(vis_stderr, "  -h  print the command usage\n");
  return 1;

} /* end of CommandGuidedSearchPrintOptions */


static void
TimeOutHandle(void)
{
  longjmp(timeOutEnv, 1);
}