src/fsm/fsmCmd.c File Reference

#include "fsmInt.h"

Include dependency graph for fsmCmd.c:

Go to the source code of this file.

Functions
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)
void	Fsm_Init (void)
void	Fsm_End (void)
Variables
static char rcsid[]	UNUSED = "$Id: fsmCmd.c,v 1.122 2005/05/19 03:21:37 awedh Exp $"
static jmp_buf	timeOutEnv

---

Function Documentation

static int CommandComputeReach	(	Hrc_Manager_t **	hmgr,
		int	argc,
		char **	argv
	)		[static]

AutomaticStart

Function********************************************************************

Synopsis [Implements the compute_reach command.]

Description [If no network or FSM exists, does nothing. Otherwise, the set of reachablestates is calculated by computing least fixed point of the initial states under the next state functions of the FSM. The option [-v n] specifies the verbosity level. If n is greater than 0, summary information is printed. If n is greater than 1, intermediate information is printed.]

CommandName [compute_reach]

CommandSynopsis [compute the set of reachable states of the FSM]

CommandArguments [\[-d <depthValue>\] \[-f\] \[-g <file>\] \[-h\] \[-i\] \[-r <thresholdValue>\] \[-s <printStep>\] \[-t <timeOut>\] \[-v #\] \[-A #\] \[-D\] \[-F\]]

CommandDescription [Compute the set of reachable states of the FSM associated with the flattened network. The command build_partition_mdds (or init_verify) must have already been invoked on the flattened network, before this command is called. On subsequent calls to compute_reach, the reachable states will not be recomputed, but statistics can be printed using -v. To force recomputation with a different set of options, for example a depth value with -d, use -F option.

The method used for image computation is displayed by the option -v 1. To change the image computation method, use the command set image_method, and then start again with the command flatten_hierarchy. The reachability computation makes extensive use of image computation. There are several user-settable options that can be used to affect the performance of image computation. See the documentation for the set command for these options.

Command options:

-d <depthValue>

Perform reachability for depthValue steps only - this option specifies the number of unit operations (image computations) to be performed in the reachability computation. The depthValue used in successive calls proceeds from the previous state. For example, compute_reach -d 3; compute_reach -d 4; will perform 7 steps of reachability in total, the second call to compute_reach proceeding from the result of the first. While using only -A 0 option (default), this additionally corresponds to the depth in the state graph, starting from the initial state. For the -A 1 option, the above may not be true. This option is not compatible with -A 2.

-f

Store the set of new states (onion rings) reached at each step of reachability. If this flag is specified, then the computation proceeds with the previously set of onion rings, if any exist (not any prior computation without onion rings). This option is likely to use more memory during reachability analysis. This is not compatible with -A 2.

-g <hints_file>

Use guided search. The file hints_file contains a series of hints. A hint is a formula that does not contain any temporal operators, so hints_file has the same syntax as a file of invariants used for check_invariant. The hints are used in the order given to change the transition relation. The transition relation is conjoined with the hint to yield an underapproximation of the transition relation. If the hints are cleverly chosen, this may speed up the computation considerably, because a search with the changed transition relation may be much simpler than one with the original transition relation, and results obtained can be reused, so that we may never have to do an expensive search with the original relation. See also: Ravi and Somenzi, Hints to accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and Somenzi, Efficient Decision Procedures for Model Checking of Linear Time Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, Symbolic Guided Search for CTL Model Checking, DAC'00. Not allowed with -A 2 or -i, and will only work with iwls95 or monolithic image methods. The description of some options for guided search can be found in the help page for print_guided_search_options.

-h

Print the command usage.

-i

This option is useful when it's not possible to build the complete transition relation. Using this option, the transition relation is rebuilt at every itereation using the current reached set of states as the care set. This option is not compatible with the -A > 0 options, the -D option and the -g option.

-r <thresholdValue>

Dynamic reordering (with method sift) is invoked once when the size of the reachable state set reaches the threshold value.

-s <printStep>

At every printStep of the reachability computation, print the total number of states reached thus far, and the size of the MDD representing this set.

-t <timeOut>

Time allowed to perform reachability (in seconds). Default is infinity.

-v #

Print debug information. 0: (default) Nothing is printed out.

1: Print a summary of reachability analysis and some information about the image computation method (see print_img_info) and summarizes results of reachability:

FSM depth: the farthest reachable state reachable states: the number of reachable states MDD size: the size of the MDD representing the reachable states analysis time: number of CPU seconds taken to compute the reachable states

2: Prints the detailed information about reachability analysis. For each printStep, it prints the MDD size of the reachable state set and the number of states in the set.

-A #

This option allows specification of approximate reachability computation.

0: (default) Breadth First Search. No approximate reachability computation.

1: High Density Reachability Analysis (HD). Computes reachable states in a manner that keeps BDD sizes under control. May be faster than BFS in some cases. For larger circuits, this option should compute more reachable states. For help on controlling options for HD, look up help on the command: print_hd_options print_hd_options. Refer to Ravi and Somenzi, ICCAD95. This option is available only when VIS is linked with the CUDD package.

2. Approximate Reachability Don't Cares(ARDC). Computes over-approximate reachable states. For help on controlling options for ARDC, look up help on the command: print_ardc_options print_ardc_options. Refer Moon's paper, ICCAD98 and 2 papers by Cho et al, December TCAD96: one is for State Space Decomposition and the other is for Approximate FSM Traversal. The options -d, -g and -f are not compatible with this option.

-D

First compute an overapproximation to the reachable states. Minimize transition relation using this approximation, and then compute the set of reachable states exactly. This may accelerate reachability analysis. Refer to the paper by Moon et al, ICCAD98. The BDD minimizing method can be chosen by using "set image_minimize_method <method>" set. This option is incompatible with -i.

-F

Force to recompute reachable states.

Related "set" options:

rch_simulate <#>

The set option can be used to set this flag rch_simulate to specify the number of random vectors to be simulated. Default value for this number is 0.

]

SideEffects [The reachable states, depth, initial states of the FSM are stored.]

Definition at line 284 of file fsmCmd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

static int CommandPrintArdcOptions	(	Hrc_Manager_t **	hmgr,
		int	argc,
		char **	argv
	)		[static]

Function********************************************************************

Synopsis [Implements the print_ardc_options command.]

CommandName [print_ardc_options]

CommandSynopsis [print information about the ARDC options currently in use]

CommandArguments [\[-h\] \[-H\]]

CommandDescription [Prints information about the current ARDC options.

Command options:

-h

Print the command usage.

-H

Print the ARDC set command usage.

Set parameters: The ARDC options are specified with the set command.

ardc_traversal_method <method>

Specify a method for approximate FSM traversal.

method must be one of the following:

0 : MBM (machine by machine).

1 : RFBF(reached frame by frame).

2 : TFBF(to frame by frame).

3 : TMBM(combination of MBM and TFBF).

4 : LMBM(least fixpoint MBM, default).

5 : TLMBM(combination of LMBM and TFBF).

ardc_group_size <size>

Specify the number of latches per group for ARDCS.

size must be a positive integer (default = 8).

ardc_affinity_factor <affinity>

Specify affinity factor to make a group for ARDCs. The available factor is from 0.0(use only correlation) to 1.0(use only dependency).

affinity must be a positive real (default = 0.5).

ardc_max_iteration <iteration>

Specify the maximum iteration count during approximate FSM traversal. Default is 0 which means infinite.

iteration must be a positive integer or zero.

ardc_constrain_target <target>

Specify where image constraining will be applied to.

target must be one of the following:

0 : constrain transition relation (default).

1 : constrain initial states.

2 : constrain both.

ardc_constrain_method <method>

Specify an image constraining method to compute ARDCs.

method must be one of the following:

0 : restrict (default).

1 : constrain

2 : compact (currently supported by only CUDD)

3 : squeeze (currently supported by only CUDD)

ardc_constrain_reorder <method>

Specify whether to enable variable reorderings during consecutive image constraining operations.

method must be one of the following:

yes : allow variable reorderings during consecutive image constraining operations (default)

no : don't allow variable reorderings during consecutive image constraining operations

ardc_abstract_pseudo_input <method>

Specify when to abstract pseudo primary input variables out from transition relation.

method must be one of the following:

0 : do not abstract pseudo input variables

1 : abstract pseudo inputs before image computation (default)

2 : abstract pseudo inputs at every end of image computation

3 : abstract pseudo inputs at the end of approximate traversal

ardc_decompose_flag <method>

Specify whether to use decomposed approximate reachable states or single conjuncted reachable states.

method must be one of the following:

yes : keep decomposed reachable stateses (default)

no : make a conjunction of reachable states of all submachines

ardc_projected_initial_flag <method>

Specify which initial states is going to be used.

method must be one of the following:

yes : use projected initial states for submachine (default)

no : use original initial states for submachine

ardc_image_method <method>

Specify image_mathod during computing reachable states of submachines.

method must be one of the following:

monolithic : use monolithic image computation

iwls95 : use iwls95 image computation (default)

mlp : use mlp image computation

tfm : use tfm image computation

hybrid : use hybrid image computation

ardc_use_high_density <method>

Specify whether to use high density in computing reachable states of submachines.

method must be one of the following:

yes : use High Density for reachable states of submachines

no : use BFS for reachable states of submachines (default)

ardc_reorder_ptr <method>

Specify whether to reorder partitioned transition relation after constraining fanin submachines.

method must be one of the following:

yes : whenever partitioned transition relation changes, reorders partitioned transition relation

no : no reordering of partitioned transition relation (default)

ardc_fanin_constrain_mode <method>

Specify which method will be used in constraining fanin submachines.

method must be one of the following:

0 : constrain w.r.t. the reachable states of fanin submachines (default)

1 : constrain w.r.t. the reachable states of both fanin submachines and itself

ardc_create_pseudo_var_mode <method>

Specify which method will be used to create pseudo input variables of submachines.

method must be one of the following:

0 : makes pseudo input variables with exact support (default)

1 : makes pseudo input variables from all state variables of the other submachines

2 : makes pseudo input variables from all state variables of fanin submachines

ardc_lmbm_initial_mode <method>

Specify which method will be used as initial states in LMBM computation.

method must be one of the following:

0 : use given initial states all the time

1 : use current reached states as initial states (default)

2 : use current frontier as initial states

set ardc_mbm_reuse_tr <method>

Specify whether to reuse already constrained transition relation for next iteratrion in MBM.

method must be one of the following:

yes : use constrained transition relation for next iteration

no : use original transition relation for next iteration (default)

ardc_read_group <filename>

Specify a filename containing grouping information

filename containing grouping information

ardc_write_group <filename>

Specify a filename to write grouping information

filename to write grouping information

ardc_verbosity <verbosity>

Specify the level of printing information during computing ARDCs.

verbosity must be 0 - 3 (default = 0).

The default settings correspond to the fast variants of LMBM and MBM. MBM never produces a more accurate approximation than LMBM for the same state-space decomposition. However, the corresponding statement does not hold for the fast versions. (That is, FastMBM will occasionally outperform FastLMBM.) To get the slower, but more accurate versions of LMBM and MBM use the following settings:

• set ardc_constrain_method 1
• set ardc_constrain_reorder no
• set ardc_abstract_pseudo_input 0

]

SideEffects []

Definition at line 1473 of file fsmCmd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

static int CommandPrintFairness	(	Hrc_Manager_t **	hmgr,
		int	argc,
		char **	argv
	)		[static]

Function********************************************************************

Synopsis [Implements the print_fairness command.]

Description [If no network or FSM exists, does nothing. Otherwise, prints the fairness constraint associated with the FSM. If no fairness constraint exists, then prints a message to that affect.]

CommandName [print_fairness]

CommandSynopsis [print the fairness constraint of the flattened network]

CommandArguments [\[-h\]]

CommandDescription [Print the fairness constraint (i.e the set of Buchi conditions) associated with the FSM of the flattened network. By default, the flattened network has the single constraint TRUE, indicating that all paths are fair.

Command options:

-h

Print the command usage.

]

SideEffects []

Definition at line 853 of file fsmCmd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

static int CommandPrintGuidedSearchOptions	(	Hrc_Manager_t **	hmgr,
		int	argc,
		char **	argv
	)		[static]

Function********************************************************************

Synopsis [Implements the print_guided_search_options command.]

CommandName [print_guided_search_options]

CommandSynopsis [print information about guided_search_options in use]

CommandArguments [\[-h\] ]

CommandDescription [Prints information about current Guided Search options. Guided search is an alternate method to compute fixpoints by modifying the fixpoint computation with restrictions. It is applicable to the compute_reach, check_invariant and model_check commands (refer to their help pages on the use of guided search). See also for details: Ravi and Somenzi, Hints to accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and Somenzi, Efficient Decision Procedures for Model Checking of Linear Time Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, Symbolic Guided Search for CTL Model Checking, DAC'00. Not allowed with -A 2 or -i, and will only work with iwls95 or monolithic image methods. The description of some options can be found in the help page for set.

Command options:

guided_search_hint_type

Choose from local (default) or global. If this flag is set to local, then every subformula is evaluated to completion, using all hints in order, before the next subformula is started. For pure ACTL or pure ECTL formulae, we can also set guided_search_hint_type to global, in which case the entire formula is evaluated for one hint before moving on to the next hint, using underapproximations.

guided_search_underapprox_minimize_method

Choose from "constrain" and "and" (default). Sets the method with which the transition relation is minimized when underapproximations are used. The option constrain is incompatible with hints that use signals other than inputs.

guided_search_overapprox_minimize_method

Choose from "squeeze" and "ornot" (default). Sets the method with which the transition relation is minimized when underapproximations are used. The option squeeze is incompatible with hints that use signals other than inputs. Ornot implies that the transition relation will be disjoined with the negation of the hint: T' = T + ~h, whereas squeeze will find a small BDD between T and T'.

guided_search_sequence

For compute_reach and check_invariant only. Set this flag to a list of comma-separated integers i1,i2,...,in, with n at most the number of hints that you specify . The k'th hint will be used for ik iterations (images). A value of 0 causes the hint to be applied to convergence. Not setting this option is like setting it to 0,0,...,0. If length of the specified sequence is less than the number of hints, the sequence is padded with zeroes.

Guided search also uses the High Density traversal options that are germane to dead-ends. The relevant flags are hd_dead_end, hd_dead_end_approx_method, hd_frontier_approx_threshold, hd_approx_quality, hd_approx_bias_quality. Use help on the print_hd_options command for explanation of these flags. If guided search is used with HD using the -A 1 options in compute_reach and check_invariant, the HD options are used by both HD and guided search. ]

SideEffects []

Definition at line 2678 of file fsmCmd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

static int CommandPrintHdOptions	(	Hrc_Manager_t **	hmgr,
		int	argc,
		char **	argv
	)		[static]

Function********************************************************************

Synopsis [Implements the print_hd_options command.]

CommandName [print_hd_options]

CommandSynopsis [print information about the HD options currently in use]

CommandArguments [\[-h\] ]

CommandDescription [Prints information about the current HD options. The HD method is an alternate method to compute a least fixpoint and is provided with the compute_reach and check_invariant commands. The method is described in Ravi and Somenzi, ICCAD95. The command can be used only when compiled with the CUDD package.

Command options:

-h Print the command usage.

Set parameters: The HD options are specified with the set command.

hd_frontier_approx_method <method>

This option specifes the method to approximate the frontier set.

Methods:

remap_ua : (Default) The BDD approximation method of DAC98 Ravi, Shiple, McMillan, Somenzi.

biased_rua : Approximation method similar to remap_ua, but uses a bias function. The bias function is set appropriate to the context.

under_approx : The BDD approximation method of Shiple's thesis.

heavy_branch : The BDD approximation method of ICCAD95 Ravi, Somenzi.

short_paths : The BDD approximation method of ICCAD95 Ravi, Somenzi.

compress : An approximation method that runs short_paths first and then remap_ua.

hd_frontier_approx_threshold <number>

This option specifes the size of the frontier to be used for image computation. The threshold for the various methods is approximate (not strictly adhered to). For the remap_ua and biased_rua method, this threshold is a lower bound and the default is 3500. For the short_paths and heavy_branch methods, this threshold is an upper bound. Therefore, a default of 2000 is set to obtain a meaningful result. Any value lower than 2000 is corrected to this default. This value is also relevant for dead-end computations. In a dead-end, the threshold for each image computation (of a disjunct of Reached) is five times the frontier approximation threshold. When the frontier approximation threshold is 0, the threshold for each dead-end image computation is 5000.

hd_approx_quality <double&gt

This option specifies the quality factor for the under_approx and remap_ua methods. Default value is 1.0. The range is any double value greater than 0. Smaller quality factors produce smaller results. Meaningful values are between 1 and 2.

hd_approx_bias_quality <double&gt

This option specifies the quality factor for the biased_rua method. Default value is 0.5. The range is any double value greater than 0. Smaller quality factors produce smaller results. Meaningful values are between 0 and 1.

hd_dead_end <method&gt

This option specifies the method used for dead-end computation. A "dead-end" is characterized by an empty frontier. A dead-end computation involves generating new states from the reached set.

Methods:

brute_force : Computes the image of the entire reached set. May be fatal if the reached set is very large.

conjuncts : (Default) Computes the image of reached by decomposing into parts.

hybrid : Computes the image of a subset of reached. If no new states, then the reaminder is decomposed in parts.

hd_dead_end_approx_method <method>

This option allows the specification of the approximation method to use to compute the subset of Reached at the dead-end. The threshold used is the same as hd_frontier_approx_threshold.

For methods, refer hd_frontier_approx_method methods. Default is remap_ua.

hd_no_scrap_states

This allows the option of not adding the "scrap" states. Scrap states are residues from the approximation of the frontier set. Default is to add the scrap states.

hd_new_only

This allows the option of adding considering only new states of each iteration for image computation. The default is to take a set in the interval of the new states and the reached set.

hd_only_partial_image

This allows the option of HD with partial image computation only (no approximation of the frontier set). Default is to allow both partial images and approximation of the frontier set.

Partial Image options:

hd_partial_image_method <method&gt

This option allows the image computation to approximate the image with the specified method.

Methods:

approx : (Default) Computes a partial image by under-approximating the intermediate products of image computation.

clipping : Computes a partial image by "clipping" the depth of recursion of the and-abstract computations during image computation.

hd_partial_image_threshold <number&gt

This options allows the specification of a threshold (in terms of bdd node size of the intermediate product) that will trigger approximation of the intermediate product. Default is 200000. This option has to be used in conjunction with hd_partial_image_size. If the value of hd_partial_image_size is larger than this option, then the approximation of the intermediate size will be as large as the hd_partial_image_size number.

hd_partial_image_size <number&gt

This options allows the specification of a size (in terms of bdd node size of the intermediate product) that is the target size of the approximated intermediate product. Default is 100000. For the short_paths and heavy_branch methods, the size of the approximation is corrected to 10000 if the size specified is lower. This is because the short_paths and heavy_branch methods consider this size as an upper bound on the approximation. This option has to be used in conjunction with hd_partial_image_threshold. If the value of hd_partial_image_threshold is much larger than this option, then the desired size will not be obtained as approximation may not be triggered.

hd_partial_image_approx <method&gt

This options allows the specification of the method to be used to approximate the intermediate product.

For methods, refer hd_frontier_approx_method methods. Default is remap_ua.

hd_partial_image_approx_quality <double&gt

This option specifies the quality factor for the under_approx and remap_ua methods for partial image computation. Default value is 1.0. Range of values is any double greater than 0. Smaller quality factors produce smaller results. Meaningful values are between 1 and 2.

hd_partial_image_approx_bias_quality <double&gt

This option specifies the quality factor for the biased_rua method for partial image computation. Default value is 0.5. Range of values is any double greater than 0. Smaller quality factors produce smaller results. Meaningful values are between 0 and 1.

hd_partial_image_clipping_depth <double&gt

This option allows the specification of the depth at which the recursion can be clipped when _hd_partial_image_method_ is clipping. Range of values is between 0 and 1. The clipping depth is then calculated as the specified fraction of the number of variables. Default is 0.4.

]

SideEffects []

Definition at line 1179 of file fsmCmd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

static int CommandPrintHybridOptions	(	Hrc_Manager_t **	hmgr,
		int	argc,
		char **	argv
	)		[static]

Function********************************************************************

Synopsis [Implements the print_hybrid_options command.]

CommandName [print_hybrid_options]

CommandSynopsis [print information about the hybrid image computation options currently in use]

CommandArguments [\[-h\] \[-H\]]

CommandDescription [Prints information about the current hybrid image computation options.

Command options:

-h

Print the command usage.

-H

Print the hybrid image computation set command usage.

Set parameters: The hybrid image computation options are specified with the set command.

hybrid_mode <mode<m>>

Specify a mode how to start hybrid computation.

mode must be one of the following:

0 : start with only transition function and build transition relation on demand

1 : start with both transition function and relation (default)

2 : start with only transition relation. Only this mode can deal with nondeterminism.

hybrid_tr_split_method <method<m>>

Specify a method to choose a splitting variable in hybrid mode = 2.

method must be one of the following:

0 : use support (default)

1 : use estimate BDD size

hybrid_build_partial_tr <method<m>>

Specify whether to build full or partial transition relation in hybrid mode = 2. This option is used to use less memory. When we use partial transition relation, for the variables excluded in the transition relation, we build each bit transition relation on demand. When nondeterminism exists in the circuit, this can not be used. method must be one of the following:

yes : build partial transition relation

no : build full transition relation (default)

hybrid_partial_num_vars <number>

Specify how many variables are going to be excluded in building partial transition relation. The default is 8.

hybrid_partial_method <method<m>>

Specify a method to choose variables to be excluded in building partial transition relation.

method must be one of the following:

0 : use BDD size (default)

1 : use support

hybrid_delayed_split <method<m>>

Specify a method whether to split transition relation immediately or just all at once before AndExist.

method must be one of the following:

yes : apply splitting to transition relation at once

no : do not apply (default)

hybrid_split_min_depth <number>

Specify the minimum depth to apply dynamic hybrid method. If a depth is smaller than this minimum depth, just split. The default is 1.

hybrid_split_max_depth <number>

Specify the maximum depth to apply dynamic hybrid method. If a depth is bigger than this maximum depth, just conjoin. The default is 5.

hybrid_pre_split_min_depth <number>

Specify the minimum depth to apply dynamic hybrid method in preimage computation. If a depth is smaller than this minimum depth, just split. The default is 0.

hybrid_pre_split_max_depth <number>

Specify the maximum depth to apply dynamic hybrid method in preimage computation. If a depth is bigger than this maximum depth, just conjoin. The default is 4.

hybrid_lambda_threshold <number>

Specify a threshold in floating between 0.0 and 1.0 to determine to split or to conjoin after computing variable lifetime lambda for image computation. If lambda is equal or smaller than this threshold, we conjoin. Otherwise we split. The default is 0.6

hybrid_pre_lambda_threshold <number>

Specify a threshold in floating between 0.0 and 1.0 to determine to split or to conjoin after computing variable lifetime lambda for preimage computation. If lambda is equal or smaller than this threshold, we conjoin. Otherwise we split. The default is 0.65

hybrid_conjoin_vector_size <number>

If the number of components in transition function vector is equal or smaller than this threshold, we just conjoin. This check is performed before computing lambda. The default is 10.

hybrid_conjoin_relation_size <number>

If the number of clusters in transition relation is equal or smaller than this threshold, we just conjoin. This check is performed before computing lambda. The default is 2.

hybrid_conjoin_relation_bdd_size <number>

If the shared BDD size of transition relation is equal or smaller than this threshold, we conjoin. This check is performed before computing lambda. The default is 200.

hybrid_improve_lambda <number>

When variable lifetime lambda is bigger than lambda threshold, if the difference between previous and current lambda is equal or smaller than this threshold, then we conjoin. The default is 0.1.

hybrid_improve_vector_size <number>

When variable lifetime lambda is bigger than lambda threshold, if the difference between the previous and current number of components in transition function vector is equal or smaller than this threshold, then we conjoin. The default is 3.

hybrid_improve_vector_bdd_size <number>

When variable lifetime lambda is bigger than lambda threshold, if the difference between the previous and current shared BDD size of transition function vector is equal or smaller than this threshold, then we conjoin. The default is 30.0.

hybrid_decide_mode <method<m>>

Specify a method to decide whether to split or to conjoin.

method must be one of the following:

0 : use only lambda

1 : use lambda and also special checks to conjoin

2 : use lambda and also improvement

3 : use all (default)

hybrid_reorder_with_from <method<m>>

Specify a method to reorder transition relation to conjoin in image computation, whether to include from set in the computation.

method must be one of the following:

yes : reorder relation array with from to conjoin (default)

no : reorder relation array without from to conjoin

hybrid_pre_reorder_with_from <method<m>>

Specify a method to reorder transition relation to conjoin in preimage computation, whether to include from set in the computation.

method must be one of the following:

yes : reorder relation array with from to conjoin

no : reorder relation array without from to conjoin (default)

hybrid_lambda_mode <method<m>>

Specify a method to decide which variable lifetime to be used for image computation.

method must be one of the following:

0 : total lifetime with ps/pi variables (default)

1 : active lifetime with ps/pi variables

2 : total lifetime with ps/ns/pi variables

hybrid_pre_lambda_mode <method<m>>

Specify a method to decide which variable lifetime to be used for preimage computation.

method must be one of the following:

0 : total lifetime with ns/pi variables

1 : active lifetime with ps/pi variables

2 : total lifetime with ps/ns/pi variables (default)

3 : total lifetime with ps/pi variables

hybrid_lambda_with_from <method<m>>

Specify a method to compute variable lifetime lambda, whether to include from set in the computation.

method must be one of the following:

yes : include from set in lambda computation (default)

no : do not include

hybrid_lambda_with_tr <method<m>>

Specify a method to compute variable lifetime lambda, whether to use transition relation or transition function vector, when both exist.

method must be one of the following:

yes : use transition relation (default)

no : use transition function vector

hybrid_lambda_with_clustering <method<m>>

Specify a method whether to include clustering to compute variable lifetime lambda.

method must be one of the following:

yes : compute lambda after clustering

no : do not cluster (default)

hybrid_synchronize_tr <method<m>>

Specify a method to keep transition relation. This option is only for when hybrid mode is 1.

method must be one of the following:

yes : rebuild transition relation from function vector whenever the function vector changes

no : do not rebuild (default)

hybrid_img_keep_pi <method<m>>

Specify a method to build forward transition relation.

method must be one of the following:

yes : keep all primary input variables in forward transition relation.

no : quantify out local primary input variables from the transition relation. (default)

hybrid_pre_keep_pi <method<m>>

Specify a method to build backward transition relation.

method must be one of the following:

yes : keep all primary input variables in backward transition relation and preimages.

no : quantify out local primary input variables from the transition relation. (default)

hybrid_pre_canonical <method<m>>

Specify a method whether to canonicalize the function vector for preimage computation.

method must be one of the following:

yes : canonicalize the function vector

no : do not canonicalize (default)

hybrid_tr_method lt;method<m>gt;

Specify an image method for AndExist operation in hybrid method.

method must be one of the following:

iwls95 (default)

mlp

]

SideEffects []

Definition at line 2344 of file fsmCmd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

static int CommandPrintImageInfo	(	Hrc_Manager_t **	hmgr,
		int	argc,
		char **	argv
	)		[static]

Function********************************************************************

Synopsis [Implements the print_img_info command.]

CommandName [print_img_info]

CommandSynopsis [print information about the image method currently in use]

CommandArguments [\[-b\] \[-f\] \[-h\] ]

CommandDescription [Prints information about the image computation method currently being used by the FSM. This includes the particular values of parameters used by the method for initialization. If the image information does not exist, then this command forces the information to be computed. If none of the flags (-b or -f) is set, forward transition relation is computed.

Command options:

-b

Compute the transition relation for backward image computation (if needed).

-f

Compute the transition relation for forward image computation (if needed).

-h

Print the command usage.

]

SideEffects []

Definition at line 960 of file fsmCmd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

static int CommandPrintMlpOptions	(	Hrc_Manager_t **	hmgr,
		int	argc,
		char **	argv
	)		[static]

Function********************************************************************

Synopsis [Implements the print_mlp_options command.]

CommandName [print_mlp_options]

CommandSynopsis [print information about the MLP image computation options currently in use]

CommandArguments [\[-h\] \[-H\]]

CommandDescription [Prints information about the current MLP image computation options.

Command options:

-h

Print the command usage.

-H

Print the MLP image computation set command usage.

Set parameters: The MLP image computation options are specified with the set command.

mlp_cluster <method<m>>

Specify a method for clustering.

method must be one of the following:

0 : linear clustering

1 : affinity based tree clustering (default)

mlp_reorder <method<m>>

Specify a method for reordering after clustering for image computation.

method must be one of the following:

0 : no reordering after clustering (default)

1 : reorder using MLP after clustering (inside)

2 : reorder using MLP after clustering (outside)

3 : reorder using IWLS95 after clustering

mlp_pre_reorder <method<m>>

Specify a method for reordering after clustering for preimage computation.

method must be one of the following:

0 : no reordering after clustering (default)

1 : reorder using MLP after clustering (inside)

2 : reorder using MLP after clustering (outside)

3 : reorder using IWLS95 after clustering

mlp_postprocess <method<m>>

Specify when to do postprocessing.

method must be one of the following:

0 : no postprocessing (default)

1 : do postprocesing after ordering

2 : do postprocesing after clustering or reordering

3 : do both 1 and 2

]

SideEffects []

Definition at line 2546 of file fsmCmd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

static int CommandPrintTfmOptions	(	Hrc_Manager_t **	hmgr,
		int	argc,
		char **	argv
	)		[static]

Function********************************************************************

Synopsis [Implements the print_tfm_options command.]

CommandName [print_tfm_options]

CommandSynopsis [print information about the transition function based image computation options currently in use]

CommandArguments [\[-h\] \[-H\]]

CommandDescription [Prints information about the current transition function based image computation options.

Command options:

-h

Print the command usage.

-H

Print the transition function based image computation set command usage.

Set parameters: The transition function based image computation options are specified with the set command.

tfm_split_method <method>

Specify a splitting method.

method must be one of the following:

0 : input splitting (default)

1 : output splitting

2 : mixed (input split + output split)

tfm_input_split <method>

Specify an input splitting method.

method must be one of the following:

0 : support before splitting (default)

1 : support after splitting

2 : estimate BDD size after splitting

3 : top variable

tfm_pi_split_flag <method>

Specify whether to allow primary input variables to be chosen as a splitting variable.

method must be one of the following:

yes : choose either state or input variable as splitting variable (default)

no : choose only state variable as splitting variable

tfm_range_comp <method>

Specify a method whether to convert image to range computataion.

method must be one of the following:

0 : do not convert to range computation

1 : convert image to range computation (default)

2 : use a threshold (tfm_range_threshold, default for hybrid)

tfm_range_threshold <number>

This option is valid only when the tfm_range_comp is set to 2. This threshold is used to determine whether to convert to range computation by comparing the shared BDD size of function vector after constraining w.r.t. from set to its original size. If the size is less than the origianl size * <number>, then we convert to range computation. The default value is 10.

tfm_range_try_threshold <number>

This option is valid only when the tfm_range_comp is set to 2. This option is used to disable checking the condition if it fails to convert consecutively <number> times. The default value is 2.

tfm_range_check_reorder <method>

Specify whether to force to call variable reordering after constraining function vector w.r.t. from set and before checking the condition.

method must be one of the following:

yes : force to reorder before checking tfm_range_threshold

no : do not reorder (default)

tfm_tie_break_mode <method>

Specify a tie breaking method when we have a tie in choosing a splitting variable in input and output splitting method.

method must be one of the following:

0 : the closest variable to top (default)

1 : the smallest BDD size after splitting

tfm_output_split <method>

Specify an output splitting method.

method must be one of the following:

0 : smallest BDD size (default)

1 : largest BDD size

2 : top variable

tfm_turn_depth <number>

This option is valid only when mixed or hybrid method is chosen. This is used to determine when to switch to the other method at which depth of recursion. The default is 5 for tfm and -1 for hybrid method.

tfm_find_decomp_var <method>

Specify a method whether to try to find a decomposable variable (meaning articulation point) first if any.

method must be one of the following:

yes : try to find a decomposable variable (articulation point)

no : do not try (default)

tfm_sort_vector_flag <method>

Specify a method whether to sort function vectors to increase cache performance.

method must be one of the following:

yes : sort function vectors (default for tfm)

no : do not sort (default for hybrid)

tfm_print_stats <method>

Specify a method whether to print statistics for cache and recursions at the end of job.

method must be one of the following:

yes : print statistics

no : do not print (default)

tfm_print_bdd_size <method>

Specify a method whether to print the BDD size of all intermediate product.

method must be one of the following:

yes : print BDD size

no : do not print (default)

tfm_split_cube_func <method>

Specify a method whether to try to find a cube in function vector in input splitting, then perform output splitting once w.r.t. the cube.

method must be one of the following:

yes : try cube splitting

no : do not try (default)

tfm_find_essential <method>

Specify a method whether to try to find essential variables in from set. If a variable occurs in all cubes of a BDD, the variable is called essential. If exists, minimize both function vector and the from set with the essential cube.

method must be one of the following:

0 : do not try (default)

1 : try to find essential variables

2 : on and off dynamically

tfm_print_essential <method>

Specify a method whether to print information about essential variables.

method must be one of the following:

0 : do not print (default)

1 : print only at end

2 : print at every image computation

tfm_use_cache <method>

Specify whether to use an image cache.

method must be one of the following:

0 : do not use cache (default for hybrid)

1 : use cache (default)

2 : store all intermediate results

tfm_global_cache <method>

Specify a method whether to use one global image cache, or one image cache per each machine.

method must be one of the following:

yes : use only one global cache (default)

no : use one cache per machine

tfm_max_chain_length <number>

This option is used to set the maximum number of items in a slot for conflict. The default is 2.

tfm_init_cache_size <number>

This option is used to set the initial cache size. The number is recommended to be a prime number. Currently, we do not resize the cache size, but for the future extension, we named initial. The default is 1001.

tfm_auto_flush_cache <method>

Specify a method to flush image cache.

method must be one of the following:

0 : flush cache only when requested

1 : flush cache at the end of image computation (default)

2 : flush cache before reordering

tfm_compose_intermediate_vars <method>

Specify a method whether to compose all intermediate variables.

method must be one of the following:

yes : compose all

no : do not compose (default)

tfm_pre_split_method <method>

Specify a splitting method for preimage computation.

method must be one of the following:

0 : input splitting (domain cofactoring, default)

1 : output splitting (constraint cofactoring)

2 : mixed (input split + output split)

3 : substitution

tfm_pre_input_split <method>

Specify an input splitting method for preimage computation.

method must be one of the following:

0 : support before splitting (default)

1 : support after splitting

2 : estimate BDD size after splitting

3 : top variable

tfm_pre_output_split <method>

Specify an output splitting method for preimage computation.

method must be one of the following:

0 : smallest BDD size (default)

1 : largest BDD size

2 : top variable

tfm_pre_dc_leaf_method <method>

Specify a method to switch to another method to complete preimage computation in domain cofactoring method when no more splitting variable exist.

method must be one of the following:

0 : substitution (default)

1 : constraint cofactoring

2 : hybrid

tfm_pre_minimize <method>

Specify a method whether to minimize transition function vector w.r.t a chosen function in constraint cofactoring method. This option is recommended to use when image cache is disabled, because even though this option can minimize the BDD size of function vector, this may degrade cache performance.

method must be one of the following:

yes : minimize function vector w.r.t. a chosen function in constraint cofactoring

no : do not minimize (default)

tfm_verbosity <verbosity>

Specify the level of printing information related with transition function method.

verbosity must be 0 - 2 (default = 0).

]

SideEffects []

Definition at line 1907 of file fsmCmd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

static int CommandReadFairness	(	Hrc_Manager_t **	hmgr,
		int	argc,
		char **	argv
	)		[static]

Function********************************************************************

Synopsis [Implements the read_fairness command.]

Description [If no network or FSM exists, does nothing. Otherwise, parses the CTL formulas in the input file, and creates a fairness constraint data structure to store them. Currently, only Buchi constraints are parsed. This command does not do any computation on the fairness constraint.]

Comment [To support Streett conditions, we need a delimiter in the input file to group finallyInf/globallyInf pairs (a "horizontal" delimiter). To support canonical fairness constraints, we additionally need a "vertical" delimiter to group different disjuncts.]

CommandName [read_fairness]

CommandSynopsis [read a fairness constraint]

CommandArguments [\[-h\] <file>]

CommandDescription [Read a fairness constraint, and associate this constraint with the FSM of the flattened network. An existing constraint associated with the FSM is lost. Subsequent verification procedures are performed relative to the new constraint. Note that, by default, the flattened network has the constraint TRUE, indicating that all paths are fair. The command build_partition_mdds (or init_verify) must have already been invoked on the flattened network, before this command is called.

Currently, only Buchi constraints are supported. A Buchi fairness constraint is given by a list of individual Buchi conditions, B1, B2, ..., Bk, where Bi is a set of FSM states. A state is fair if there exists an infinite path from that state that intersects each Bi infinitely often.

The conditions are specified by a file containing at least one CTL formula (see the VIS CTL and LTL syntax manual). In particular, Bi is defined by a CTL formula, which represents the set of states that makes the formula true (in the absence of any fairness constraint). References to signal names in the network should be made using the full hierarchical names. Note that the support of any wire referred to in a formula should consist only of latches. Each CTL formula is terminated by a semicolon.

Example: In the three conditions below, B1 contains those states that have a next state where cntr.out is RED, B2 contains those where timer.active is 1, and B3 contains those states for which every path from the state has tlc.request=1 until tlc.acknowledge=1.

  EX(cntr.out=RED);
  (timer.active=1);
  A(tlc.request=1 U tlc.acknowledge=1);
  

Command options:

-h

Print the command usage.

<file>

File containing the set of Buchi conditions.

]

SideEffects []

Definition at line 625 of file fsmCmd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

static int CommandResetFairness	(	Hrc_Manager_t **	hmgr,
		int	argc,
		char **	argv
	)		[static]

Function********************************************************************

Synopsis [Implements the reset_fairness command.]

Description [If no network or FSM exists, does nothing. Otherwise, resets the fairnessInfo associated with the FSM to the default case.]

CommandName [reset_fairness]

CommandSynopsis [reset the fairness constraint]

CommandArguments [\[-h\]]

CommandDescription [Remove any existing fairness constraint associated with the FSM of the flattened network, and impose a single constraint, TRUE, indicating that all states are "accepting".

Command options:

-h

Print the command usage.

]

SideEffects []

Definition at line 777 of file fsmCmd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void Fsm_End

(

void

)

Function********************************************************************

Synopsis [Ends the FSM package.]

SideEffects []

SeeAlso [Fsm_Init]

Definition at line 103 of file fsmCmd.c.

{
}

Here is the caller graph for this function:

void Fsm_Init

(

void

)

AutomaticEnd Function********************************************************************

Synopsis [Initializes the FSM package.]

SideEffects []

SeeAlso [Fsm_End]

Definition at line 77 of file fsmCmd.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

static void TimeOutHandle

(

void

)

[static]

Function********************************************************************

Synopsis [Handle function for timeout.]

Description [This function is called when the time out occurs.]

SideEffects []

Definition at line 2717 of file fsmCmd.c.

{
  longjmp(timeOutEnv, 1);
}

Here is the caller graph for this function:

---

Variable Documentation

jmp_buf timeOutEnv [static]

Definition at line 39 of file fsmCmd.c.

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

CFile***********************************************************************

FileName [fsmCmd.c]

PackageName [fsm]

Synopsis [Commands for the FSM package.]

Author [Shaker Sarwary, Tom Shiple, Rajeev Ranjan, In-Ho Moon, Kavita Ravi]

Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Definition at line 34 of file fsmCmd.c.