source: vis_dev/vis-2.3/src/fsm/fsmCmd.c @ 14

Last change on this file since 14 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 103.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [fsmCmd.c]
4
5  PackageName [fsm]
6
7  Synopsis    [Commands for the FSM package.]
8
9  Author      [Shaker Sarwary, Tom Shiple, Rajeev Ranjan, In-Ho Moon, Kavita Ravi]
10
11  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
12  All rights reserved.
13
14  Permission is hereby granted, without written agreement and without license
15  or royalty fees, to use, copy, modify, and distribute this software and its
16  documentation for any purpose, provided that the above copyright notice and
17  the following two paragraphs appear in all copies of this software.
18
19  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
20  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
21  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
22  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
23
24  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
25  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
26  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
27  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
28  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
29
30******************************************************************************/
31
32#include "fsmInt.h"
33
34static char rcsid[] UNUSED = "$Id: fsmCmd.c,v 1.122 2005/05/19 03:21:37 awedh Exp $";
35
36/*---------------------------------------------------------------------------*/
37/* Variable declarations                                                     */
38/*---------------------------------------------------------------------------*/
39static jmp_buf timeOutEnv;
40
41/**AutomaticStart*************************************************************/
42
43/*---------------------------------------------------------------------------*/
44/* Static function prototypes                                                */
45/*---------------------------------------------------------------------------*/
46
47static int CommandComputeReach(Hrc_Manager_t ** hmgr, int argc, char ** argv);
48static int CommandReadFairness(Hrc_Manager_t ** hmgr, int argc, char ** argv);
49static int CommandResetFairness(Hrc_Manager_t ** hmgr, int argc, char ** argv);
50static int CommandPrintFairness(Hrc_Manager_t ** hmgr, int argc, char ** argv);
51static int CommandPrintImageInfo(Hrc_Manager_t ** hmgr, int argc, char ** argv);
52static int CommandPrintHdOptions(Hrc_Manager_t ** hmgr, int argc, char ** argv);
53static int CommandPrintArdcOptions(Hrc_Manager_t ** hmgr, int argc, char ** argv);
54static int CommandPrintTfmOptions(Hrc_Manager_t ** hmgr, int argc, char ** argv);
55static int CommandPrintHybridOptions(Hrc_Manager_t ** hmgr, int argc, char ** argv);
56static int CommandPrintMlpOptions(Hrc_Manager_t ** hmgr, int argc, char ** argv);
57static int CommandPrintGuidedSearchOptions(Hrc_Manager_t ** hmgr, int argc, char ** argv);
58static void TimeOutHandle(void);
59
60/**AutomaticEnd***************************************************************/
61
62
63/*---------------------------------------------------------------------------*/
64/* Definition of exported functions                                          */
65/*---------------------------------------------------------------------------*/
66
67/**Function********************************************************************
68
69  Synopsis    [Initializes the FSM package.]
70
71  SideEffects []
72
73  SeeAlso     [Fsm_End]
74
75******************************************************************************/
76void
77Fsm_Init(void)
78{
79  Cmd_CommandAdd("compute_reach",   CommandComputeReach,   0);
80  Cmd_CommandAdd("read_fairness",   CommandReadFairness,   0);
81  Cmd_CommandAdd("reset_fairness",  CommandResetFairness,  0);
82  Cmd_CommandAdd("print_fairness",  CommandPrintFairness,  0);
83  Cmd_CommandAdd("print_img_info",  CommandPrintImageInfo, 0);
84  Cmd_CommandAdd("print_hd_options",  CommandPrintHdOptions, 0);
85  Cmd_CommandAdd("print_guided_search_options",  CommandPrintGuidedSearchOptions, 0);
86  Cmd_CommandAdd("print_ardc_options",  CommandPrintArdcOptions, 0);
87  Cmd_CommandAdd("print_tfm_options",  CommandPrintTfmOptions, 0);
88  Cmd_CommandAdd("print_hybrid_options",  CommandPrintHybridOptions, 0);
89  Cmd_CommandAdd("print_mlp_options",  CommandPrintMlpOptions, 0);
90}
91
92
93/**Function********************************************************************
94
95  Synopsis    [Ends the FSM package.]
96
97  SideEffects []
98
99  SeeAlso     [Fsm_Init]
100
101******************************************************************************/
102void
103Fsm_End(void)
104{
105}
106
107/*---------------------------------------------------------------------------*/
108/* Definition of internal functions                                          */
109/*---------------------------------------------------------------------------*/
110
111
112/*---------------------------------------------------------------------------*/
113/* Definition of static functions                                            */
114/*---------------------------------------------------------------------------*/
115
116/**Function********************************************************************
117
118  Synopsis    [Implements the compute_reach command.]
119
120  Description [If no network or FSM exists, does nothing. Otherwise, the set
121  of reachablestates is calculated by computing least fixed point of the
122  initial states under the next state functions of the FSM.  The option [-v n]
123  specifies the verbosity level.  If n is greater than 0, summary information
124  is printed.  If n is greater than 1, intermediate information is printed.]
125
126  CommandName [compute_reach]
127
128  CommandSynopsis [compute the set of reachable states of the FSM]
129
130  CommandArguments [\[-d <depthValue>\] \[-f\] \[-g <file>\] \[-h\] \[-i\] \[-r <thresholdValue>\] \[-s <printStep>\] \[-t <timeOut>\] \[-v #\] \[-A #\] \[-D\] \[-F\]]
131
132  CommandDescription [Compute the set of reachable states of the FSM
133  associated with the flattened network.  The command
134  <tt>build_partition_mdds</tt> (or <tt>init_verify</tt>) must have
135  already been invoked on the flattened network, before this command
136  is called.  On subsequent calls to compute_reach, the reachable
137  states will not be recomputed, but statistics can be printed using
138  -v. To force recomputation with a different set of options, for
139  example a depth value with -d, use -F option. <p>
140
141  The method used for image computation is displayed by the option
142  <tt>-v 1</tt>.  To change the image computation method, use the
143  command <tt>set image_method</tt>, and then start again with the
144  command <tt>flatten_hierarchy</tt>.  The reachability computation
145  makes extensive use of image computation. There are several
146  user-settable options that can be used to affect the performance of
147  image computation.  See the documentation for the <tt>set</tt>
148  command for these options.<p>
149 
150  Command options:<p>
151
152  <dl>
153
154  <dt> -d &lt;depthValue&gt;
155  <dd> Perform reachability for depthValue steps only - this option
156  specifies the number of unit operations (image computations) to be
157  performed in the reachability computation. The depthValue used in
158  successive calls proceeds from the previous state. For example,
159  compute_reach -d 3; compute_reach -d 4; will perform 7 steps of
160  reachability in total, the second call to compute_reach proceeding
161  from the result of the first. While using only -A 0 option
162  (default), this additionally corresponds to the depth in the state
163  graph, starting from the initial state.  For the -A 1 option, the
164  above may not be true. This option is not compatible with -A 2. <p>
165
166  <dt> -f
167  <dd> Store the set of new states (onion rings) reached at each step
168  of reachability. If this flag is specified, then the computation
169  proceeds with the previously set of onion rings, if any exist (not
170  any prior computation without onion rings). This option is likely to
171  use more memory during reachability analysis. This is not compatible
172  with -A 2. <p>
173
174  <dt> -g &lt;<code>hints_file</code>&gt; <dd> Use guided search.  The
175  file <code>hints_file</code> contains a series of hints.  A hint is
176  a formula that does not contain any temporal operators, so
177  <code>hints_file</code> has the same syntax as a file of invariants
178  used for check_invariant.  The hints are used in the order given to
179  change the transition relation.  The transition relation is
180  conjoined with the hint to yield an underapproximation of the
181  transition relation.  If the hints are cleverly chosen, this may
182  speed up the computation considerably, because a search with the
183  changed transition relation may be much simpler than one with the
184  original transition relation, and results obtained can be reused, so
185  that we may never have to do an expensive search with the original
186  relation.  See also: Ravi and Somenzi, Hints to accelerate symbolic
187  traversal. CHARME'99; Bloem, Ravi, and Somenzi, Efficient Decision
188  Procedures for Model Checking of Linear Time Logic Properties,
189  CAV'99; Bloem, Ravi, and Somenzi, Symbolic Guided Search for CTL
190  Model Checking, DAC'00. Not allowed with -A 2 or -i, and will only
191  work with iwls95 or monolithic image methods.  The description of
192  some options for guided search can be found in the help page for
193  print_guided_search_options. <p>
194 
195  <dt> -h
196  <dd> Print the command usage.<p>
197
198  <dt> -i <dd> This option is useful when it's not possible to build the
199  complete transition relation. Using this option, the transition relation is
200  rebuilt at every itereation using the current reached set of states as the
201  care set. This option is not compatible with the -A > 0 options, the -D
202  option and the -g option.<p>
203
204  <dt> -r &lt;thresholdValue&gt;
205  <dd> Dynamic reordering (with method sift) is invoked once when the size
206  of the reachable state set reaches the threshold value.<p>
207
208  <dt> -s &lt;printStep&gt;
209  <dd> At every printStep of the reachability computation, print the total
210  number of states reached thus far, and the size of the MDD representing this
211  set.<p>
212
213  <dt> -t &lt;timeOut&gt;
214  <dd> Time allowed to perform reachability (in seconds).  Default is infinity.<p>
215
216  <dt> -v #
217  <dd> Print debug information.
218  <dd>
219  0: (default) Nothing is printed out.<p>
220
221  1: Print a summary of reachability analysis and some information
222  about the image computation method (see <tt>print_img_info</tt>) and
223  summarizes results of reachability:
224
225  <dd>
226  <dd> <b>FSM depth:</b> the farthest reachable state
227  <dd> <b>reachable states:</b> the number of reachable states
228  <dd> <b>MDD size:</b> the size of the MDD representing the reachable states
229  <dd> <b>analysis time:</b> number of CPU seconds taken to compute the
230  reachable states<p>
231
232  2: Prints the detailed information about reachability analysis. For
233  each <tt> printStep</tt>, it prints the MDD size of the reachable
234  state set and the number of states in the set. <p>
235
236  <dt> -A #
237  <dd> This option allows specification of approximate reachability
238  computation. <p>
239
240  0:  (default) Breadth First Search. No approximate reachability
241  computation. <p>
242
243  1: High Density Reachability Analysis (HD). Computes reachable states in a
244  manner that keeps BDD sizes under control. May be faster than BFS in some
245  cases. For larger circuits, this option should compute more reachable
246  states. For help on controlling options for HD, look up help on the command:
247  print_hd_options <A HREF="print_hd_optionsCmd.html">
248  <code>print_hd_options</code></A>.  Refer to Ravi and Somenzi, ICCAD95. This
249  option is available only when VIS is linked with the CUDD package.  <p>
250 
251  2. Approximate Reachability Don't Cares(ARDC). Computes over-approximate
252  reachable states. For help on controlling options for ARDC, look up help on
253  the command: print_ardc_options <A HREF="print_ardc_optionsCmd.html">
254  <code>print_ardc_options</code></A>.  Refer Moon's paper, ICCAD98 and 2
255  papers by Cho et al, December TCAD96: one is for State Space Decomposition
256  and the other is for Approximate FSM Traversal. The options -d, -g and -f are
257  not compatible with this option. <p>
258
259  <dt> -D <dd> First compute an overapproximation to the reachable states.
260  Minimize transition relation using this approximation, and then compute the
261  set of reachable states exactly. This may accelerate reachability
262  analysis. Refer to the paper by Moon et al, ICCAD98. The BDD minimizing
263  method can be chosen by using "set image_minimize_method <method>" <A HREF =
264  "setCmd.html"><code>set</code></A>.  This option is incompatible with -i.
265  <p>
266
267  <dt> -F
268  <dd> Force to recompute reachable states.
269  <p>
270
271  <dt> Related "set" options: <p>
272  <dt> rch_simulate &lt;#&gt;
273  <dd> The set option can be used to set this flag rch_simulate to specify the
274  number of random vectors to be simulated. Default value for this number is 0.
275  <p>
276 
277  ]
278
279  SideEffects [The reachable states, depth, initial states of the FSM are
280  stored.]
281
282******************************************************************************/
283static int
284CommandComputeReach(
285  Hrc_Manager_t ** hmgr,
286  int  argc,
287  char ** argv)
288{
289  int        c;
290  mdd_t      *reachableStates = NIL(mdd_t);
291  mdd_t      *initialStates;
292  long        initialTime;
293  long        finalTime;
294  static int  verbosityLevel;
295  static int  printStep;
296  static int  timeOutPeriod;
297  Fsm_Fsm_t  *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
298  static int reorderFlag;
299  static int reorderThreshold;
300  static int shellFlag;
301  static int depthValue;
302  static int incrementalFlag;
303  static int approxFlag;
304  static int ardc;
305  static int recompute;
306  Fsm_RchType_t rchType;
307  FILE *guideFile = NIL(FILE); /* file of hints for guided search */
308  array_t *guideArray = NIL(array_t);
309  Img_MethodType imgMethod;
310 
311  /*
312   * These are the default values.  These variables must be declared static
313   * to avoid lint warnings.  Since they are static, we must reinitialize
314   * them outside of the variable declarations.
315   */
316  verbosityLevel = 0;
317  printStep      = 0;
318  timeOutPeriod  = 0;
319  shellFlag = 0;
320  depthValue = 0;
321  incrementalFlag = 0;
322  rchType = Fsm_Rch_Default_c;
323  approxFlag = 0;
324  ardc = 0;
325  recompute = 0;
326
327  /*
328   * Parse command line options.
329   */
330  util_getopt_reset();
331  while ((c = util_getopt(argc, argv, "d:fg:hir:s:t:v:A:DF")) != EOF) {
332    switch(c) {
333      case 'd':
334        depthValue = atoi(util_optarg);
335        break;
336      case 'f':
337        shellFlag = 1;
338        break;
339      case 'g':
340          guideFile = Cmd_FileOpen(util_optarg, "r", NIL(char *), 0);
341          if (guideFile == NIL(FILE)) {
342            fprintf(vis_stdout,
343                    "** rch error: Guide file cannot be read. Check permissions and path\n");
344            goto usage;
345          }
346          break; 
347      case 'h':
348        goto usage;
349      case 'i':
350        incrementalFlag = 1;
351        break;
352      case 'r':
353        reorderFlag = 1;
354        reorderThreshold = atoi(util_optarg);
355        break;
356      case 's':
357        printStep = atoi(util_optarg);
358        break;
359      case 't':
360        timeOutPeriod = atoi(util_optarg);
361        break;
362      case 'v':
363        verbosityLevel = atoi(util_optarg);
364        break;
365      case 'A' :
366        approxFlag = atoi(util_optarg);
367        if ((approxFlag > 2) || (approxFlag < 0)) {
368            goto usage;
369        }
370        break;
371      case 'D':
372        ardc = 1;
373        break;
374      case 'F':
375        recompute = 1;
376        break;
377      default:
378        goto usage;
379    }
380  }
381  if (c == EOF && argc != util_optind)
382    goto usage;
383 
384  imgMethod = Img_UserSpecifiedMethod(); 
385   
386  if ((approxFlag == 1) && (bdd_get_package_name() != CUDD)) {
387    fprintf(vis_stderr, "** rch error: compute_reach with -A 1 option is currently supported only by CUDD.\n");
388    return 1;
389  }
390
391  if (fsm == NIL(Fsm_Fsm_t)) {
392    return 1;
393  }
394
395  if (incrementalFlag && approxFlag) {
396      fprintf(vis_stdout,
397              "** rch error: Incremental flag and approx flag are incompatible.\n");
398      goto usage;
399  }
400  if (incrementalFlag && ardc) {
401      fprintf(vis_stdout,
402              "** rch error: The -i and -D flags are incompatible.\n");
403      goto usage;
404  }
405
406  if (depthValue && approxFlag == 2) {
407    fprintf(vis_stdout,
408            "** rch error: Depth value and over-approx flag are incompatible.\n");
409    goto usage;
410  }
411 
412  if (shellFlag && approxFlag == 2) {
413    fprintf(vis_stdout,
414            "** rch error: Shell flag and over-approx flag are incompatible.\n");
415    goto usage;
416  }
417 
418  if (guideFile != NIL(FILE)){
419    if(incrementalFlag) {
420      fprintf(vis_stdout, "** rch error: Guided search is not compatible with the -i flag\n");
421      goto usage;
422    }
423    if(approxFlag == 2){
424      fprintf(vis_stdout, "** rch error: Guided search is not compatible with Over-approx flag\n");
425      goto usage;
426    }
427    if(imgMethod != Img_Iwls95_c && imgMethod != Img_Monolithic_c &&
428       imgMethod != Img_Mlp_c){
429      fprintf(vis_stdout, "** rch error: Guided search can only be performed\n");
430      fprintf(vis_stdout, "with IWLS95, MLP, or Monolithic image methods.\n");
431    goto usage;
432    }
433  }/* if guided search requested */
434 
435  /* Start the timeOut timer. */
436  if (timeOutPeriod > 0){
437    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
438    (void) alarm(timeOutPeriod);
439    if (setjmp(timeOutEnv) > 0) {
440      (void) fprintf(vis_stdout, "** rch info: Timeout occurred after %d seconds.\n",
441                     timeOutPeriod);
442      (void) fprintf(vis_stdout, "** rch warning: The time out may have "
443                     "corrupted the data.\n");
444     alarm(0);
445      return 1;
446    }
447  }
448
449  /* Make sure that the initial states can be computed without a problem. */
450  error_init();
451  initialStates = Fsm_FsmComputeInitialStates(fsm);
452  if (initialStates == NIL(mdd_t)) {
453    (void) fprintf(vis_stderr, "** rch error: Latch initialization function depends on another latch:\n");
454    (void) fprintf(vis_stderr, "%s", error_string());
455    (void) fprintf(vis_stderr, "\n");
456    (void) fprintf(vis_stderr, "** rch error: Initial states cannot be computed.\n");
457    return (1);
458  }
459  else {
460    mdd_free(initialStates);
461  }
462
463  /* translate approx flag */
464  switch(approxFlag) {
465  case 0: rchType = Fsm_Rch_Bfs_c; break;
466  case 1: rchType = Fsm_Rch_Hd_c; break;
467  case 2: rchType = Fsm_Rch_Oa_c; break;
468  default: rchType = Fsm_Rch_Default_c; break;
469  }
470
471  if (guideFile != NIL(FILE)) {
472    guideArray = Mc_ComputeGuideArray(fsm, guideFile);
473    if(guideArray == NIL(array_t))
474      return(1);
475  }
476
477  if (rchType == Fsm_Rch_Oa_c) {
478    array_t     *apprReachableStates;
479
480    initialTime = util_cpu_time();
481    apprReachableStates = Fsm_FsmComputeOverApproximateReachableStates(fsm,
482        incrementalFlag, verbosityLevel, printStep, depthValue, shellFlag,
483        reorderFlag, reorderThreshold, recompute);
484    finalTime = util_cpu_time();
485
486    if (apprReachableStates == NIL(array_t)) {
487      (void)fprintf(vis_stdout,
488        "** rch error: Reachability computation failed, no rechable states\n");
489      return 1;
490    }
491
492    if (verbosityLevel > 0)
493      Fsm_ArdcPrintReachabilityResults(fsm, finalTime-initialTime);
494    alarm(0);
495    return(0);
496  }
497
498  /* Compute the reachable states. */
499  initialTime = util_cpu_time();
500  reachableStates = Fsm_FsmComputeReachableStates(
501    fsm, incrementalFlag, verbosityLevel, printStep, depthValue, shellFlag,
502    reorderFlag, reorderThreshold, rchType, ardc, recompute, NIL(array_t),
503    (verbosityLevel > 0), guideArray); 
504  finalTime = util_cpu_time();
505  mdd_array_free(guideArray);
506
507  if (reachableStates == NIL(mdd_t)) {
508    (void)fprintf(vis_stdout, "** rch error: Reachability computation failed, no rechable states\n");
509    return 1;
510  }
511
512  if (verbosityLevel > 0){
513    if (fsm->imageInfo){ 
514      char *methodType =
515          Img_ImageInfoObtainMethodTypeAsString(fsm->imageInfo); 
516      (void) fprintf(vis_stdout, "** rch info: Computing reachable states using the ");
517      (void) fprintf(vis_stdout, "%s image computation method.\n", methodType);
518      FREE(methodType);
519      (void)Img_ImageInfoPrintMethodParams(fsm->imageInfo,
520                                           vis_stdout);
521      if (Img_ImageInfoObtainMethodType(fsm->imageInfo) == Img_Tfm_c ||
522          Img_ImageInfoObtainMethodType(fsm->imageInfo) == Img_Hybrid_c) {
523        Img_TfmPrintStatistics(fsm->imageInfo, Img_Forward_c);
524      }
525    }
526    Fsm_FsmReachabilityPrintResults(fsm, finalTime-initialTime, approxFlag);
527
528  }
529  mdd_free(reachableStates);
530
531  alarm(0);
532  return (0);
533
534  usage:
535  (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");
536  (void) fprintf(vis_stderr, "   -d depthValue perform reachability up to depthValue steps\n");
537  (void) fprintf(vis_stderr, "   -f \t\t store the onion rings ateach step\n");
538  (void) fprintf(vis_stderr, "   -h \t\t print the command usage\n");
539  (void) fprintf(vis_stderr, "   -g filename\t perform reachability analysis with guided search using the given file. Not allowed with -A 2\n");
540  (void) fprintf(vis_stderr, "   -i \t\t builds the transition relation incrementally (not supported with -A 1,2).\n");
541  (void) fprintf(vis_stderr, "   -r thresholdValue invoke dynamic reordering once when the size of the reached state set reaches this value.\n");
542  (void) fprintf(vis_stderr, "   -s printStep\t print reachability information every printStep steps (0 for no information).\n");
543  (void) fprintf(vis_stderr, "   -t time\t time out period (in seconds)\n");
544  (void) fprintf(vis_stderr, "   -v #\t\t verbosity level\n");
545  (void) fprintf(vis_stderr, "   -A #\t\t 0 (default) - BFS method.\n");
546  (void) fprintf(vis_stderr, "      #\t\t 1 - HD method.\n");
547  (void) fprintf(vis_stderr, "      #\t\t 2 - Over-approximation by approximate traversal.\n");
548  (void) fprintf(vis_stderr, "   -D \t\t Try to minimize transition relation with ARDCs\n");
549  (void) fprintf(vis_stderr, "   -F \t\t force to recompute reachable states\n");
550  return 1;
551}
552
553
554/**Function********************************************************************
555
556  Synopsis    [Implements the read_fairness command.]
557
558  Description [If no network or FSM exists, does nothing. Otherwise, parses
559  the CTL formulas in the input file, and creates a fairness constraint data
560  structure to store them.  Currently, only Buchi constraints are parsed.
561  This command does not do any computation on the fairness constraint.]
562
563  Comment [To support Streett conditions, we need a delimiter in the input
564  file to group finallyInf/globallyInf pairs (a "horizontal" delimiter).  To
565  support canonical fairness constraints, we additionally need a "vertical"
566  delimiter to group different disjuncts.]
567
568  CommandName [read_fairness]
569
570  CommandSynopsis [read a fairness constraint]
571
572  CommandArguments [\[-h\] &lt;file&gt;]
573 
574  CommandDescription [Read a fairness constraint, and associate this
575  constraint with the FSM of the flattened network.  An existing constraint
576  associated with the FSM is lost. Subsequent verification procedures are
577  performed relative to the new constraint. Note that, by default, the
578  flattened network has the constraint TRUE, indicating that all paths are
579  fair. The command <tt>build_partition_mdds</tt> (or <tt>init_verify</tt>)
580  must have already been invoked on the flattened network, before this command
581  is called.<p>
582
583  Currently, only Buchi constraints are supported. A Buchi fairness constraint
584  is given by a list of individual Buchi conditions, B1, B2, ..., Bk, where Bi
585  is a set of FSM states.  A state is fair if there exists an infinite path
586  from that state that intersects each Bi infinitely often.<p>
587
588  The conditions are specified by a file containing at least one CTL formula
589  (see the <A HREF="../ctl/ctl/ctl.html"> VIS CTL and LTL syntax manual</A>).  In
590  particular, Bi is defined by a CTL formula, which represents the set of
591  states that makes the formula true (in the absence of any fairness
592  constraint).  References to signal names in the network should be made using
593  the full hierarchical names.  Note that the support of any wire referred to
594  in a formula should consist only of latches. Each CTL formula is terminated
595  by a semicolon.<p>
596
597  Example: In the three conditions below, B1 contains those states that have a
598  next state where cntr.out is RED, B2 contains those where timer.active is 1,
599  and B3 contains those states for which every path from the state has
600  tlc.request=1 until tlc.acknowledge=1.<p>
601
602  <pre>
603  EX(cntr.out=RED);
604  (timer.active=1);
605  A(tlc.request=1 U tlc.acknowledge=1);
606  </pre>
607
608  Command options:<p> 
609
610  <dl>
611
612  <dt> -h
613  <dd> Print the command usage.<p>
614
615  <dt> &lt;file&gt;
616  <dd> File containing the set of Buchi conditions.<p>
617 
618  </dl>
619  ]
620
621  SideEffects []
622
623******************************************************************************/
624static int
625CommandReadFairness(
626  Hrc_Manager_t ** hmgr,
627  int  argc,
628  char ** argv)
629{
630  int       c;
631  FILE      *fp;
632  array_t   *formulaArray;
633  Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
634 
635  /*
636   * Parse command line options.
637   */
638  util_getopt_reset();
639  while ((c = util_getopt(argc, argv, "h")) != EOF) {
640    switch(c) {
641      case 'h':
642        goto usage;
643      default:
644        goto usage;
645    }
646    /* NOT REACHED */
647  }
648
649  if (fsm == NIL(Fsm_Fsm_t)) {
650    (void) fprintf(vis_stderr, "** fair error: Fairness constraint not recorded.\n");
651    return 1;
652  }
653
654  /*
655   * Open the fairness file.
656   */
657  if (argc - util_optind == 0) {
658    (void) fprintf(vis_stderr, "** fair error: fairness file not provided\n");
659    goto usage;
660  }
661  else if (argc - util_optind > 1) {
662    (void) fprintf(vis_stderr, "** fair error: too many arguments\n");
663    goto usage;
664  }
665
666  fp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
667  if (fp == NIL(FILE)) {
668    return 1;
669  }
670
671  /*
672   * Parse the formulas in the file.
673   */
674  formulaArray = Ctlp_FileParseFormulaArray(fp);
675  (void) fclose(fp);
676
677  if (formulaArray == NIL(array_t)) {
678    (void) fprintf(vis_stderr, "** fair error: error reading fairness conditions.\n");
679    return 1;
680  }
681  else if (array_n(formulaArray) == 0) {
682    (void) fprintf(vis_stderr, "** fair error: fairness file is empty.\n");
683    (void) fprintf(vis_stderr, "** fair error: Use reset_fairness to reset the fairness constraint.");
684    return 1;
685  }
686  else {
687    int             j;
688    Fsm_Fairness_t *fairness;
689    Ntk_Network_t  *network = Fsm_FsmReadNetwork(fsm);
690
691    /*
692     * First check that each formula is semantically correct wrt the network.
693     */
694    error_init();
695    for (j = 0; j < array_n(formulaArray); j++) {
696      Ctlp_Formula_t *formula;
697      boolean         status; 
698     
699      formula  = array_fetch(Ctlp_Formula_t *, formulaArray, j);
700      status = Mc_FormulaStaticSemanticCheckOnNetwork(formula, network, FALSE);
701     
702      if (status == FALSE) {
703        (void) fprintf(vis_stderr,
704                       "** fair error: error reading fairness constraint "); 
705        Ctlp_FormulaPrint(vis_stderr, formula);
706        (void) fprintf(vis_stderr, ":\n");
707        (void) fprintf(vis_stderr, "%s", error_string());
708        (void) fprintf(vis_stderr, "\n");
709        return 1;
710      }
711    }
712
713
714    /*
715     * Interpret the array of CTL formulas as a set of Buchi conditions.
716     * Hence, create a single disjunct, consisting of k conjuncts, where k is
717     * the number of CTL formulas read in.  The jth conjunct has the jth
718     * formula as its finallyInf component, and NULL as its globallyInf
719     * component.
720     */
721    fairness = FsmFairnessAlloc(fsm);   
722    for (j = 0; j < array_n(formulaArray); j++) {
723      Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, formulaArray, j);
724
725      FsmFairnessAddConjunct(fairness, formula, NIL(Ctlp_Formula_t), 0, j);
726    }
727    array_free(formulaArray); /* Don't free the formulas themselves. */
728
729    /*
730     * Remove any existing fairnessInfo associated with the FSM, and update
731     * the fairnessInfo.constraint with the new fairness just read.
732     */
733    FsmFsmFairnessInfoUpdate(fsm, NIL(mdd_t), fairness, NIL(array_t));
734
735    return 0;
736  }
737
738  usage:
739  (void) fprintf(vis_stderr, "usage: read_fairness [-h] file\n");
740  (void) fprintf(vis_stderr, "   -h    print the command usage\n");
741  (void) fprintf(vis_stderr, "   file  file containing the list of conditions\n");
742  return 1;
743}
744
745
746/**Function********************************************************************
747
748  Synopsis    [Implements the reset_fairness command.]
749
750  Description [If no network or FSM exists, does nothing. Otherwise, resets
751  the fairnessInfo associated with the FSM to the default case.]
752
753  CommandName [reset_fairness]
754
755  CommandSynopsis [reset the fairness constraint]
756
757  CommandArguments [\[-h\]]
758 
759  CommandDescription [Remove any existing fairness constraint associated with
760  the FSM of the flattened network, and impose a single constraint, TRUE,
761  indicating that all states are "accepting".<p>
762
763  Command options:<p> 
764
765  <dl>
766
767  <dt> -h
768  <dd> Print the command usage.<p> 
769
770  </dl>
771  ]
772
773  SideEffects []
774
775******************************************************************************/
776static int
777CommandResetFairness(
778  Hrc_Manager_t ** hmgr,
779  int  argc,
780  char ** argv)
781{
782  int       c;
783  Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
784
785  /*
786   * Parse command line options.
787   */
788  util_getopt_reset();
789  while ((c = util_getopt(argc, argv, "h")) != EOF) {
790    switch(c) {
791      case 'h':
792        goto usage;
793      default:
794        goto usage;
795    }
796    /* NOT REACHED */
797  }
798
799  if (fsm == NIL(Fsm_Fsm_t)) {
800    return 1;
801  }
802
803  /*
804   * Remove any existing fairnessInfo associated with the FSM, and add back
805   * the default constraint.
806   */
807  FsmFsmFairnessInfoUpdate(fsm, NIL(mdd_t), NIL(Fsm_Fairness_t), NIL(array_t));
808  fsm->fairnessInfo.constraint = FsmFsmCreateDefaultFairnessConstraint(fsm);
809
810  return 0;
811
812
813  usage:
814  (void) fprintf(vis_stderr, "usage: reset_fairness [-h]\n");
815  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
816  return 1;
817}
818
819
820/**Function********************************************************************
821
822  Synopsis    [Implements the print_fairness command.]
823
824  Description [If no network or FSM exists, does nothing. Otherwise, prints
825  the fairness constraint associated with the FSM.  If no fairness
826  constraint exists, then prints a message to that affect.]
827
828  CommandName [print_fairness]
829
830  CommandSynopsis [print the fairness constraint of the flattened network]
831
832  CommandArguments [\[-h\]]
833 
834  CommandDescription [Print the fairness constraint (i.e the set of Buchi
835  conditions) associated with the FSM of the flattened network.  By default,
836  the flattened network has the single constraint TRUE, indicating that all
837  paths are fair.<p>
838
839  Command options:<p> 
840
841  <dl>
842
843  <dt> -h
844  <dd> Print the command usage.<p> 
845
846  </dl>
847  ]
848
849  SideEffects []
850
851******************************************************************************/
852static int
853CommandPrintFairness(
854  Hrc_Manager_t ** hmgr,
855  int  argc,
856  char ** argv)
857{
858  int            c;
859  Fsm_Fairness_t *constraint;
860  int             numDisjuncts;
861  Fsm_Fsm_t      *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
862
863  /*
864   * Parse command line options.
865   */
866  util_getopt_reset();
867  while ((c = util_getopt(argc, argv, "h")) != EOF) {
868    switch(c) {
869      case 'h':
870        goto usage;
871      default:
872        goto usage;
873    }
874    /* NOT REACHED */
875  }
876
877  if (fsm == NIL(Fsm_Fsm_t)) {
878    return 1;
879  }
880
881  /*
882   * Print the fairness constraint.  It is assumed that there is at least one
883   * disjunct present.  Currently, only Buchi constraints can be printed out.
884   */
885  constraint = Fsm_FsmReadFairnessConstraint(fsm);
886  assert(constraint != NIL(Fsm_Fairness_t));
887  numDisjuncts = Fsm_FairnessReadNumDisjuncts(constraint);
888  assert(numDisjuncts != 0);
889
890  if (numDisjuncts > 1) {
891    (void) fprintf(vis_stdout, "Fairness constraint not Buchi...");
892    (void) fprintf(vis_stdout, "don't know how to print.\n");
893  }
894  else {
895    int i;
896    int numConjuncts = Fsm_FairnessReadNumConjunctsOfDisjunct(constraint, 0);
897
898    (void) fprintf(vis_stdout, "Fairness constraint:\n");
899    for (i = 0; i < numConjuncts; i++) {
900      if (Fsm_FairnessReadGloballyInfFormula(constraint, 0, i) !=
901          NIL(Ctlp_Formula_t)) {
902        (void) fprintf(vis_stdout, "Fairness constraint not Buchi...");
903        (void) fprintf(vis_stdout, "don't know how to print.\n");
904      }
905       
906      Ctlp_FormulaPrint(vis_stdout,
907                        Fsm_FairnessReadFinallyInfFormula(constraint, 0, i));
908      (void) fprintf(vis_stdout, ";\n");
909    }
910  }
911
912  return 0;
913
914  usage:
915  (void) fprintf(vis_stderr, "usage: print_fairness [-h]\n");
916  (void) fprintf(vis_stderr, "   -h  print the command usage\n");
917  return 1;
918}
919
920
921/**Function********************************************************************
922
923  Synopsis    [Implements the print_img_info command.]
924
925  CommandName [print_img_info]
926
927  CommandSynopsis [print information about the image method currently
928  in use]
929
930  CommandArguments [\[-b\] \[-f\] \[-h\] ]
931
932  CommandDescription [Prints information about the image computation method
933  currently being used by the FSM. This includes the particular values of
934  parameters used by the method for initialization.  If the image information
935  does not exist, then this command forces the information to be
936  computed. If none of the flags (-b or -f) is set, forward
937  transition relation is computed. <p>
938
939  Command options: <p>
940
941  <dl>
942
943  <dt> -b
944  <dd> Compute the transition relation for backward image computation
945  (if needed).<p>
946
947  <dt> -f
948  <dd> Compute the transition relation for forward image computation
949  (if needed).<p>
950
951  <dt> -h
952  <dd> Print the command usage.<p>
953 
954  </dl>]
955
956  SideEffects []
957
958******************************************************************************/
959static int
960CommandPrintImageInfo(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
961{
962  int c;
963  Img_ImageInfo_t *imageInfo;
964  Fsm_Fsm_t       *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
965  int bwdImgFlag = 0;
966  int fwdImgFlag = 0;
967
968  util_getopt_reset();
969  while ((c = util_getopt(argc, argv, "bfh")) != EOF) {
970    switch(c) {
971      case 'b':
972        bwdImgFlag = 1;
973        break;
974      case 'f':
975        fwdImgFlag = 1;
976        break;
977      case 'h':
978        goto usage;
979      default:
980        goto usage;
981    }
982  }
983
984  if (fsm == NIL(Fsm_Fsm_t)) {
985    return 1;
986  }
987
988  if (!(bwdImgFlag || fwdImgFlag)){
989    fwdImgFlag = 1;
990  }
991
992  imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, bwdImgFlag, fwdImgFlag);
993  Img_ImageInfoPrintMethodParams(imageInfo, vis_stdout);
994  return 0;
995
996usage:
997  (void) fprintf(vis_stderr,"usage: print_image_method [-b] [-f] [-h]\n");
998  (void) fprintf(vis_stderr, "  -b  create the backward transition relation\n");
999  (void) fprintf(vis_stderr, "  -f  create the forward transition relation\n");
1000  (void) fprintf(vis_stderr, "  -h  print the command usage\n");
1001  return 1;
1002}
1003
1004/**Function********************************************************************
1005
1006  Synopsis    [Implements the print_hd_options command.]
1007
1008  CommandName [print_hd_options]
1009
1010  CommandSynopsis [print information about the HD options currently
1011  in use]
1012
1013  CommandArguments [\[-h\] ]
1014
1015  CommandDescription [Prints information about the current HD options.
1016  The HD method is an alternate method to compute a least fixpoint and
1017  is provided with the compute_reach and check_invariant commands.
1018  The method is described in Ravi and Somenzi, ICCAD95. The command
1019  can be used only when compiled with the CUDD package.  <p>
1020
1021  Command options: <p>
1022
1023  <dt> -h
1024  <dd> Print the command usage.<p>
1025 
1026  </dl>
1027
1028  Set parameters: The HD options are specified with the set command.
1029
1030  <dl>
1031  <dt> hd_frontier_approx_method &lt;method&gt;
1032  <dd> This option specifes
1033  the method to approximate the frontier set. <p>
1034
1035  Methods: <p>
1036  remap_ua : (Default) The BDD approximation method of DAC98 Ravi,
1037  Shiple, McMillan, Somenzi. <p>
1038  biased_rua : Approximation method similar to remap_ua, but uses
1039  a bias function. The bias function is set appropriate to the context. <p>
1040  under_approx : The BDD approximation method of Shiple's thesis. <p>
1041  heavy_branch : The BDD approximation method of ICCAD95 Ravi,
1042  Somenzi. <p>
1043  short_paths : The BDD approximation method of ICCAD95 Ravi,
1044  Somenzi. <p>
1045  compress : An approximation method that runs short_paths first
1046  and then remap_ua. <p>
1047
1048  <dt> hd_frontier_approx_threshold &lt;number&gt;
1049  <dd> This option specifes the size of the frontier to be used for
1050  image computation. The threshold for the various methods is
1051  approximate (not strictly adhered to). For the remap_ua and
1052  biased_rua method, this threshold is a lower bound and the default
1053  is 3500. For the short_paths and heavy_branch methods, this threshold
1054  is an upper bound. Therefore, a default of 2000 is set to obtain a
1055  meaningful result. Any value lower than 2000 is corrected to this
1056  default. This value is also relevant for dead-end computations. In a
1057  dead-end, the threshold for each image computation (of a disjunct of
1058  Reached) is five times the frontier approximation threshold. When
1059  the frontier approximation threshold is 0, the threshold for each
1060  dead-end image computation is 5000. <p>
1061
1062  <dt> hd_approx_quality &lt;double&gt
1063  <dd> This option specifies the quality factor for the under_approx
1064  and remap_ua methods. Default value is 1.0. The range is any
1065  double value greater than 0. Smaller quality factors produce smaller
1066  results. Meaningful values are between 1 and 2.  <p>
1067
1068  <dt> hd_approx_bias_quality &lt;double&gt
1069  <dd> This option specifies the quality factor for the biased_rua
1070  method. Default value is 0.5. The range is any
1071  double value greater than 0. Smaller quality factors produce smaller
1072  results. Meaningful values are between 0 and 1.<p>
1073
1074  <dt> hd_dead_end &lt;method&gt
1075  <dd> This option specifies the method used for dead-end
1076  computation. A "dead-end" is characterized by an empty
1077  frontier. A dead-end computation involves generating new states from
1078  the reached set. <p>
1079
1080  Methods:<p>
1081  brute_force : Computes the image of the entire reached
1082  set. May be fatal if the reached set is very large. <p>
1083  conjuncts : (Default) Computes the image of reached by
1084  decomposing into parts. <p>
1085  hybrid : Computes the image of a subset of reached. If no
1086  new states, then the reaminder is decomposed in parts. <p>
1087
1088  <dt> hd_dead_end_approx_method &lt;method&gt;
1089  <dd> This option allows the specification of the approximation
1090  method to use to compute the subset of Reached at the dead-end. The
1091  threshold used is the same as hd_frontier_approx_threshold.<p>
1092
1093  For methods, refer hd_frontier_approx_method methods. Default is remap_ua.<p>
1094
1095  <dt> hd_no_scrap_states
1096  <dd> This allows the option of not adding the "scrap" states. Scrap
1097  states are residues from the approximation of the frontier set.
1098  Default is to add the scrap states. <p>
1099
1100  <dt> hd_new_only
1101  <dd> This allows the option of adding considering only new states of
1102  each iteration for image computation. The default is to take a set in
1103  the interval of the new states and the reached set. <p>
1104
1105  <dt> hd_only_partial_image
1106  <dd> This allows the option of HD with partial image computation
1107  only (no approximation of the frontier set).  Default is to allow both
1108  partial images and approximation of the frontier set. <p>
1109
1110  <dt> Partial Image options: <p>
1111
1112  <dt> hd_partial_image_method &lt;method&gt
1113  <dd> This option allows the image computation to approximate the
1114  image with the specified method. <p>
1115  Methods:<p>
1116  approx : (Default) Computes a partial image by
1117  under-approximating the intermediate products of image computation.
1118  <p>
1119  clipping : Computes a partial image by "clipping" the
1120  depth of recursion of the and-abstract computations during image
1121  computation. <p>
1122
1123  <dt> hd_partial_image_threshold &lt;number&gt
1124  <dd> This options allows the specification of a threshold (in terms
1125  of bdd node size of the intermediate product) that will trigger
1126  approximation of the intermediate product. Default is 200000. This
1127  option has to be used in conjunction with hd_partial_image_size. If
1128  the value of hd_partial_image_size is larger than this option, then
1129  the approximation of the intermediate size will be as large as the
1130  hd_partial_image_size number. <p>
1131
1132  <dt> hd_partial_image_size &lt;number&gt
1133  <dd> This options allows the specification of a size (in terms of
1134  bdd node size of the intermediate product) that is the target size
1135  of the approximated intermediate product. Default is 100000. For the
1136  short_paths and heavy_branch methods, the size of the approximation
1137  is corrected to 10000 if the size specified is lower. This is
1138  because the short_paths and heavy_branch methods consider this size
1139  as an upper bound on the approximation. This option has to be used
1140  in conjunction with hd_partial_image_threshold. If the value of
1141  hd_partial_image_threshold is much larger than this option, then the
1142  desired size will not be obtained as approximation may not be
1143  triggered.<p>
1144
1145  <dt> hd_partial_image_approx &lt;method&gt
1146  <dd> This options allows the specification of the method to be used
1147  to approximate the intermediate product. <p>
1148
1149  For methods, refer hd_frontier_approx_method methods. Default is remap_ua.<p>
1150
1151  <dt> hd_partial_image_approx_quality &lt;double&gt
1152  <dd> This option specifies the quality factor for the under_approx
1153  and remap_ua methods for partial image computation. Default value is
1154  1.0. Range of values is any double greater than 0. Smaller quality
1155  factors produce smaller results. Meaningful values are between 1 and
1156  2.  <p>
1157
1158  <dt> hd_partial_image_approx_bias_quality &lt;double&gt
1159  <dd> This option specifies the quality factor for the biased_rua
1160  method for partial image computation. Default value is
1161  0.5. Range of values is any double greater than 0. Smaller quality
1162  factors produce smaller results. Meaningful values are between 0 and
1163  1. <p>
1164
1165  <dt> hd_partial_image_clipping_depth &lt;double&gt
1166  <dd> This option allows the specification of the depth at which the
1167  recursion can be clipped when _hd_partial_image_method_ is
1168  clipping. Range of values is between 0 and 1. The clipping depth is
1169  then calculated as the specified fraction of the number of
1170  variables. Default is 0.4. <p>
1171 
1172  </dl>
1173  ]
1174 
1175  SideEffects []
1176
1177******************************************************************************/
1178static int
1179CommandPrintHdOptions(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
1180{
1181  int c;
1182
1183  if (*hmgr == NULL) {
1184    fprintf(vis_stderr,"** hrc error: Hierarchy manager is empty\n");
1185    return 1;
1186  }
1187
1188  util_getopt_reset();
1189  while ((c = util_getopt(argc, argv, "h")) != EOF) {
1190    switch(c) {
1191      case 'h':
1192        goto usage;
1193      default:
1194        goto usage;
1195    }
1196     /* NOT REACHED */
1197 }
1198
1199  /* print hd options */
1200  FsmHdPrintOptions();
1201  return 0;
1202
1203usage:
1204  (void) fprintf(vis_stderr,"usage: print_hd_options [-h]\n");
1205  (void) fprintf(vis_stderr, "  -h  print the command usage\n");
1206  return 1;
1207} /* end of CommandPrintHdOptions */
1208
1209
1210/**Function********************************************************************
1211
1212  Synopsis    [Implements the print_ardc_options command.]
1213
1214  CommandName [print_ardc_options]
1215
1216  CommandSynopsis [print information about the ARDC options currently
1217  in use]
1218
1219  CommandArguments [\[-h\] \[-H\]]
1220
1221  CommandDescription [Prints information about the current ARDC options.
1222  <p>
1223
1224  Command options: <p>
1225
1226  <dl>
1227
1228  <dt> -h
1229  <dd> Print the command usage.<p>
1230
1231  <dt> -H
1232  <dd> Print the ARDC set command usage.<p>
1233 
1234  </dl>
1235
1236  Set parameters: The ARDC options are specified with the set command.
1237
1238  <dl>
1239
1240  <dt> ardc_traversal_method <code> &lt;method&gt; </code>
1241  <dd> Specify a method for approximate FSM traversal.
1242  <p>
1243  <dd>
1244  <code> method </code> must be one of the following:
1245  <p>
1246
1247  <code> 0 </code>: MBM (machine by machine). <p>
1248  <code> 1 </code>: RFBF(reached frame by frame). <p>
1249  <code> 2 </code>: TFBF(to frame by frame). <p>
1250  <code> 3 </code>: TMBM(combination of MBM and TFBF). <p>
1251  <code> 4 </code>: LMBM(least fixpoint MBM, default). <p>
1252  <code> 5 </code>: TLMBM(combination of LMBM and TFBF). <p>
1253
1254  <dt> ardc_group_size <code> &lt;size&gt; </code>
1255  <dd> Specify the number of latches per group for ARDCS.
1256  <p>
1257  <dd>
1258  <code> size </code> must be a positive integer (default = 8).
1259  <p>
1260
1261  <dt> ardc_affinity_factor <code> &lt;affinity&gt; </code>
1262  <dd> Specify affinity factor to make a group for ARDCs.
1263       The available factor is from 0.0(use only correlation) to 1.0(use only
1264       dependency).
1265  <p>
1266  <dd>
1267  <code> affinity </code> must be a positive real (default = 0.5).
1268  <p>
1269
1270  <dt> ardc_max_iteration <code> &lt;iteration&gt; </code>
1271  <dd> Specify the maximum iteration count during approximate FSM traversal.
1272  Default is 0 which means infinite.
1273  <p>
1274  <dd>
1275  <code> iteration </code> must be a positive integer or zero.
1276  <p>
1277
1278  <dt> ardc_constrain_target <code> &lt;target&gt; </code>
1279  <dd> Specify where image constraining will be applied to.
1280  <p>
1281  <dd>
1282  <code> target </code> must be one of the following:
1283  <p>
1284
1285  <code> 0 </code>: constrain transition relation (default). <p>
1286  <code> 1 </code>: constrain initial states. <p>
1287  <code> 2 </code>: constrain both. <p>
1288
1289  <dt> ardc_constrain_method <code> &lt;method&gt; </code>
1290  <dd> Specify an image constraining method to compute ARDCs.
1291  <p>
1292  <dd>
1293  <code> method </code> must be one of the following:
1294  <p>
1295
1296  <code> 0 </code>: restrict (default). <p>
1297  <code> 1 </code>: constrain <p>
1298  <code> 2 </code>: compact (currently supported by only CUDD) <p>
1299  <code> 3 </code>: squeeze (currently supported by only CUDD) <p>
1300
1301  <dt> ardc_constrain_reorder <code> &lt;method&gt; </code>
1302  <dd> Specify whether to enable variable reorderings during consecutive
1303  image constraining operations.
1304  <p>
1305  <dd>
1306  <code> method </code> must be one of the following:
1307  <p>
1308
1309  <code> yes </code>: allow variable reorderings during consecutive image
1310                      constraining operations (default) <p>
1311  <code> no  </code>: don't allow variable reorderings during consecutive
1312                      image constraining operations <p>
1313
1314  <dt> ardc_abstract_pseudo_input <code> &lt;method&gt; </code>
1315  <dd> Specify when to abstract pseudo primary input variables out
1316  from transition relation.
1317  <p>
1318  <dd>
1319  <code> method </code> must be one of the following:
1320  <p>
1321
1322  <code> 0 </code>: do not abstract pseudo input variables <p>
1323  <code> 1 </code>: abstract pseudo inputs before image computation (default)<p>
1324  <code> 2 </code>: abstract pseudo inputs at every end of image computation <p>
1325  <code> 3 </code>: abstract pseudo inputs at the end of approximate traversal<p>
1326
1327  <dt> ardc_decompose_flag <code> &lt;method&gt; </code>
1328  <dd> Specify whether to use decomposed approximate reachable states or
1329       single conjuncted reachable states.
1330  <p>
1331  <dd>
1332  <code> method </code> must be one of the following:
1333  <p>
1334
1335  <code> yes </code>: keep decomposed reachable stateses (default) <p>
1336  <code> no  </code>: make a conjunction of reachable states of all submachines <p>
1337
1338  <dt> ardc_projected_initial_flag <code> &lt;method&gt; </code>
1339  <dd> Specify which initial states is going to be used.
1340  <p>
1341  <dd>
1342  <code> method </code> must be one of the following:
1343  <p>
1344
1345  <code> yes </code>: use projected initial states for submachine (default) <p>
1346  <code> no  </code>: use original initial states for submachine <p>
1347
1348  <dt> ardc_image_method <code> &lt;method&gt; </code>
1349  <dd> Specify image_mathod during computing reachable states of submachines.
1350  <p>
1351  <dd>
1352  <code> method </code> must be one of the following:
1353  <p>
1354
1355  <code> monolithic </code>: use monolithic image computation <p>
1356  <code> iwls95     </code>: use iwls95 image computation (default) <p>
1357  <code> mlp        </code>: use mlp image computation <p>
1358  <code> tfm        </code>: use tfm image computation <p>
1359  <code> hybrid     </code>: use hybrid image computation <p>
1360
1361  <dt> ardc_use_high_density <code> &lt;method&gt; </code>
1362  <dd> Specify whether to use high density in computing reachable states
1363  of submachines.
1364  <p>
1365  <dd>
1366  <code> method </code> must be one of the following:
1367  <p>
1368
1369  <code> yes </code>: use High Density for reachable states of submachines <p>
1370  <code> no  </code>: use BFS for reachable states of submachines (default) <p>
1371
1372  <dt> ardc_reorder_ptr <code> &lt;method&gt; </code>
1373  <dd> Specify whether to reorder partitioned transition relation after
1374  constraining fanin submachines.
1375  <p>
1376  <dd>
1377  <code> method </code> must be one of the following:
1378  <p>
1379
1380  <code> yes </code>: whenever partitioned transition relation changes,
1381  reorders partitioned transition relation <p>
1382  <code> no  </code>: no reordering of partitioned transition relation (default) <p>
1383
1384  <dt> ardc_fanin_constrain_mode <code> &lt;method&gt; </code>
1385  <dd> Specify which method will be used in constraining fanin submachines. <p>
1386  <dd>
1387  <code> method </code> must be one of the following:
1388  <p>
1389
1390  <code> 0 </code>: constrain w.r.t. the reachable states of fanin submachines
1391  (default) <p>
1392  <code> 1 </code>: constrain w.r.t. the reachable states of both fanin
1393  submachines and itself <p>
1394
1395  <dt> ardc_create_pseudo_var_mode <code> &lt;method&gt; </code>
1396  <dd> Specify which method will be used to create pseudo input
1397  variables of submachines.
1398  <p>
1399  <dd>
1400  <code> method </code> must be one of the following:
1401  <p>
1402
1403  <code> 0 </code>: makes pseudo input variables with exact support
1404  (default) <p>
1405  <code> 1 </code>: makes pseudo input variables from all state
1406  variables of the other submachines <p>
1407  <code> 2 </code>: makes pseudo input variables from all state
1408  variables of fanin submachines <p>
1409
1410  <dt> ardc_lmbm_initial_mode <code> &lt;method&gt; </code>
1411  <dd> Specify which method will be used as initial states in LMBM
1412  computation.
1413  <p>
1414  <dd>
1415  <code> method </code> must be one of the following:
1416  <p>
1417
1418  <code> 0 </code>: use given initial states all the time <p>
1419  <code> 1 </code>: use current reached states as initial states (default) <p>
1420  <code> 2 </code>: use current frontier as initial states <p>
1421
1422  <dt> set ardc_mbm_reuse_tr <code> &lt;method&gt; </code>
1423  <dd> Specify whether to reuse already constrained transition relation
1424  for next iteratrion in MBM. <p>
1425  <dd>
1426  <code> method </code> must be one of the following:
1427  <p>
1428
1429  <code> yes </code>: use constrained transition relation for next iteration <p>
1430  <code> no  </code>: use original transition relation for next iteration
1431                      (default) <p>
1432
1433  <dt> ardc_read_group <code> &lt;filename&gt; </code>
1434  <dd> Specify a filename containing grouping information <p>
1435  <dd>
1436  <code> filename </code> containing grouping information
1437  <p>
1438
1439  <dt> ardc_write_group <code> &lt;filename&gt; </code>
1440  <dd> Specify a filename to write grouping information <p>
1441  <dd>
1442  <code> filename </code> to write grouping information
1443  <p>
1444
1445  <dt> ardc_verbosity <code> &lt;verbosity&gt; </code>
1446  <dd> Specify the level of printing information during computing ARDCs.
1447  <p>
1448  <dd>
1449  <code> verbosity </code> must be 0 - 3 (default = 0).
1450  <p>
1451 
1452  </dl>
1453
1454  The default settings correspond to the fast variants of LMBM and
1455  MBM.  MBM never produces a more accurate approximation than LMBM for
1456  the same state-space decomposition.  However, the corresponding
1457  statement does not hold for the fast versions.  (That is, FastMBM
1458  will occasionally outperform FastLMBM.)  To get the slower, but more
1459  accurate versions of LMBM and MBM use the following settings:
1460
1461  <ul>
1462  <li> set ardc_constrain_method 1
1463  <li> set ardc_constrain_reorder no
1464  <li> set ardc_abstract_pseudo_input 0
1465  </ul>
1466 
1467  ]
1468 
1469  SideEffects []
1470
1471******************************************************************************/
1472static int
1473CommandPrintArdcOptions(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
1474{
1475  int c;
1476
1477  if (*hmgr == NULL) {
1478    fprintf(vis_stderr,"** hrc error: Hierarchy manager is empty\n");
1479    return 1;
1480  }
1481
1482  util_getopt_reset();
1483  while ((c = util_getopt(argc, argv, "hH")) != EOF) {
1484    switch(c) {
1485      case 'h':
1486        goto usage;
1487      case 'H':
1488        goto usage_ardc;
1489      default:
1490        goto usage;
1491    }
1492    /* NOT REACHED */
1493  }
1494
1495  /* print ARDC options */
1496  FsmArdcPrintOptions();
1497  return 0;
1498
1499usage:
1500  (void) fprintf(vis_stderr,"usage: print_ardc_options [-h] [-H]\n");
1501  (void) fprintf(vis_stderr, "  -h  print the command usage\n");
1502  (void) fprintf(vis_stderr, "  -H  print the ARDC set command usage\n");
1503  return 1;
1504usage_ardc:
1505  (void) fprintf(vis_stderr, "   set ardc_traversal_method <m>\n");
1506  (void) fprintf(vis_stderr, "       m = 0 : MBM (machine by machine)\n");
1507  (void) fprintf(vis_stderr, "       m = 1 : RFBF(reached frame by frame)\n");
1508  (void) fprintf(vis_stderr, "       m = 2 : TFBF(to frame by frame)\n");
1509  (void) fprintf(vis_stderr, "       m = 3 : TMBM(TFBF + MBM)\n");
1510  (void) fprintf(vis_stderr, "       m = 4 : LMBM(least fixpoint MBM, default)\n");
1511  (void) fprintf(vis_stderr, "       m = 5 : TLMBM(TFBF + LMBM)\n");
1512  (void) fprintf(vis_stderr, "   set ardc_group_size <n>\n");
1513  (void) fprintf(vis_stderr, "       n (default = 8)\n");
1514  (void) fprintf(vis_stderr, "   set ardc_affinity_factor <f>\n");
1515  (void) fprintf(vis_stderr, "       f = 0.0 - 1.0 (default = 0.5)\n");
1516  (void) fprintf(vis_stderr, "   set ardc_max_iteration <n>\n");
1517  (void) fprintf(vis_stderr, "       n (default = 0(infinity))\n");
1518  (void) fprintf(vis_stderr, "   set ardc_constrain_target <m>\n");
1519  (void) fprintf(vis_stderr, "       m = 0 : constrain transition relation (default)\n");
1520  (void) fprintf(vis_stderr, "       m = 1 : constrain initial states\n");
1521  (void) fprintf(vis_stderr, "       m = 2 : constrain both\n");
1522  (void) fprintf(vis_stderr, "   set ardc_constrain_method <m>\n");
1523  (void) fprintf(vis_stderr, "       m = 0 : restrict (default)\n");
1524  (void) fprintf(vis_stderr, "       m = 1 : constrain\n");
1525  (void) fprintf(vis_stderr,
1526                 "       m = 2 : compact (currently supported by only CUDD)\n");
1527  (void) fprintf(vis_stderr,
1528                 "       m = 3 : squeeze (currently supported by only CUDD)\n");
1529  (void) fprintf(vis_stderr, "   set ardc_constrain_reorder <m>\n");
1530  (void) fprintf(vis_stderr, "       m = yes : allow variable reorderings during consecutive\n");
1531  (void) fprintf(vis_stderr, "                 image constraining operations (default)\n");
1532  (void) fprintf(vis_stderr, "       m = no  : don't allow variable reorderings during consecutive\n");
1533  (void) fprintf(vis_stderr, "                 image constraining operations\n");
1534  (void) fprintf(vis_stderr, "   set ardc_abstract_pseudo_input <m>\n");
1535  (void) fprintf(vis_stderr, "       m = 0 : do not abstract pseudo input variables\n");
1536  (void) fprintf(vis_stderr, "       m = 1 : abstract pseudo inputs before image computation (default)\n");
1537  (void) fprintf(vis_stderr, "       m = 2 : abstract pseudo inputs at every end of image computation\n");
1538  (void) fprintf(vis_stderr, "       m = 3 : abstract pseudo inputs at the end of approximate traversal\n");
1539  (void) fprintf(vis_stderr, "   set ardc_decompose_flag <m>\n");
1540  (void) fprintf(vis_stderr, "       m = yes : keep decomposed reachable stateses (default)\n");
1541  (void) fprintf(vis_stderr, "       m = no  : make a conjunction of reachable states of all submachines\n");
1542  (void) fprintf(vis_stderr, "   set ardc_projected_initial_flag <m>\n");
1543  (void) fprintf(vis_stderr, "       m = yes : use projected initial states for submachine (default)\n");
1544  (void) fprintf(vis_stderr, "       m = no  : use original initial states for submachine\n");
1545  (void) fprintf(vis_stderr, "   set ardc_image_method <m>\n");
1546  (void) fprintf(vis_stderr, "       m = monolithic : use monolithic image computation for submachines\n");
1547  (void) fprintf(vis_stderr, "       m = iwls95     : use iwls95 image computation for submachines (default)\n");
1548  (void) fprintf(vis_stderr, "       m = mlp        : use mlp image computation for submachines\n");
1549  (void) fprintf(vis_stderr, "       m = tfm        : use tfm image computation for submachines\n");
1550  (void) fprintf(vis_stderr, "       m = hybrid     : use hybrid image computation for submachines\n");
1551  (void) fprintf(vis_stderr, "   set ardc_use_high_density <m>\n");
1552  (void) fprintf(vis_stderr, "       m = yes : use High Density for reachable states of submachines\n");
1553  (void) fprintf(vis_stderr, "       m = no  : use BFS for reachable states of submachines (default)\n");
1554  (void) fprintf(vis_stderr, "   set ardc_create_pseudo_var_mode <m>\n");
1555  (void) fprintf(vis_stderr, "       m = 0 : makes pseudo input variables with exact support (default)\n");
1556  (void) fprintf(vis_stderr, "       m = 1 : makes pseudo input variables from all state variables of\n");
1557  (void) fprintf(vis_stderr, "               the other machines\n");
1558  (void) fprintf(vis_stderr, "       m = 2 : makes pseudo input variables from all state variables of\n");
1559  (void) fprintf(vis_stderr, "               fanin machines\n");
1560  (void) fprintf(vis_stderr, "   set ardc_reorder_ptr <m>\n");
1561  (void) fprintf(vis_stderr, "       m = yes : whenever partitioned transition relation changes,\n");
1562  (void) fprintf(vis_stderr, "                 reorders partitioned transition relation\n");
1563  (void) fprintf(vis_stderr, "       m = no  : no reordering of partitioned transition relation (default)\n");
1564  (void) fprintf(vis_stderr, "   set ardc_fanin_constrain_mode <m>\n");
1565  (void) fprintf(vis_stderr, "       m = 0 : constrains w.r.t. the reachable states of fanin machines\n");
1566  (void) fprintf(vis_stderr, "               (default)\n");
1567  (void) fprintf(vis_stderr, "       m = 1 : constrains w.r.t. the reachable states of both fanin machines\n");
1568  (void) fprintf(vis_stderr, "               and itself\n");
1569  (void) fprintf(vis_stderr, "   set ardc_lmbm_initial_mode <m>\n");
1570  (void) fprintf(vis_stderr, "       m = 0 : use given initial states all the time\n");
1571  (void) fprintf(vis_stderr, "       m = 1 : use current reached states as initial states (default)\n");
1572  (void) fprintf(vis_stderr, "       m = 2 : use current frontier as initial states\n");
1573  (void) fprintf(vis_stderr, "   set ardc_mbm_reuse_tr <m>\n");
1574  (void) fprintf(vis_stderr, "       m = yes : use constrained transition relation for next iteration\n");
1575  (void) fprintf(vis_stderr, "       m = no  : use original transition relation for next iteration (default)\n");
1576  (void) fprintf(vis_stderr, "   set ardc_read_group <filename>\n");
1577  (void) fprintf(vis_stderr, "       <filename> file containing grouping information\n");
1578  (void) fprintf(vis_stderr, "   set ardc_write_group <filename>\n");
1579  (void) fprintf(vis_stderr, "       <filename> file to write grouping information\n");
1580  (void) fprintf(vis_stderr, "   set ardc_verbosity <n>\n");
1581  (void) fprintf(vis_stderr, "       n = 0 - 3 (default = 0)\n");
1582  return 1;
1583} /* end of CommandPrintArdcOptions */
1584
1585
1586/**Function********************************************************************
1587
1588  Synopsis    [Implements the print_tfm_options command.]
1589
1590  CommandName [print_tfm_options]
1591
1592  CommandSynopsis [print information about the transition function based
1593  image computation options currently in use]
1594
1595  CommandArguments [\[-h\] \[-H\]]
1596
1597  CommandDescription [Prints information about the current transition function
1598  based image computation options.
1599  <p>
1600
1601  Command options: <p>
1602
1603  <dl>
1604
1605  <dt> -h
1606  <dd> Print the command usage.<p>
1607
1608  <dt> -H
1609  <dd> Print the transition function based image computation set command usage.
1610  <p>
1611 
1612  </dl>
1613
1614  Set parameters: The transition function based image computation options are
1615  specified with the set command.
1616
1617  <dl>
1618
1619  <dt> tfm_split_method <code> &lt;method&gt; </code>
1620  <dd> Specify a splitting method. <p>
1621  <dd>
1622  <code> method </code> must be one of the following:
1623  <p>
1624
1625  <code> 0 </code>: input splitting (default) <p>
1626  <code> 1 </code>: output splitting <p>
1627  <code> 2 </code>: mixed (input split + output split) <p>
1628
1629  <dt> tfm_input_split <code> &lt;method&gt; </code>
1630  <dd> Specify an input splitting method. <p>
1631  <dd>
1632  <code> method </code> must be one of the following:
1633  <p>
1634
1635  <code> 0 </code>: support before splitting (default) <p>
1636  <code> 1 </code>: support after splitting <p>
1637  <code> 2 </code>: estimate BDD size after splitting <p>
1638  <code> 3 </code>: top variable <p>
1639
1640  <dt> tfm_pi_split_flag <code> &lt;method&gt; </code>
1641  <dd> Specify whether to allow primary input variables to be chosen
1642       as a splitting variable. <p>
1643  <dd>
1644  <code> method </code> must be one of the following:
1645  <p>
1646
1647  <code> yes </code>: choose either state or input variable as splitting
1648                      variable (default) <p>
1649  <code> no  </code>: choose only state variable as splitting variable <p>
1650
1651  <dt> tfm_range_comp <code> &lt;method&gt; </code>
1652  <dd> Specify a method whether to convert image to range computataion. <p>
1653  <dd>
1654  <code> method </code> must be one of the following:
1655  <p>
1656
1657  <code> 0 </code>: do not convert to range computation <p>
1658  <code> 1 </code>: convert image to range computation (default) <p>
1659  <code> 2 </code>: use a threshold (tfm_range_threshold, default for
1660  hybrid) <p>
1661
1662  <dt> tfm_range_threshold &lt;number&gt;
1663  <dd> This option is valid only when the tfm_range_comp is set to 2. This
1664  threshold is used to determine whether to convert to range computation
1665  by comparing the shared BDD size of function vector after constraining
1666  w.r.t. from set to its original size. If the size is less than the origianl
1667  size * <number>, then we convert to range computation. The default value
1668  is 10. <p>
1669
1670  <dt> tfm_range_try_threshold &lt;number&gt;
1671  <dd> This option is valid only when the tfm_range_comp is set to 2. This
1672  option is used to disable checking the condition if it fails to convert
1673  consecutively <number> times. The default value is 2. <p>
1674
1675  <dt> tfm_range_check_reorder <code> &lt;method&gt; </code>
1676  <dd> Specify whether to force to call variable reordering after constraining
1677  function vector w.r.t. from set and before checking the condition. <p>
1678  <dd>
1679  <code> method </code> must be one of the following:
1680  <p>
1681
1682  <code> yes </code>: force to reorder before checking tfm_range_threshold <p>
1683  <code> no  </code>: do not reorder (default) <p>
1684
1685  <dt> tfm_tie_break_mode <code> &lt;method&gt; </code>
1686  <dd> Specify a tie breaking method when we have a tie in choosing
1687  a splitting variable in input and output splitting method. <p>
1688  <dd>
1689  <code> method </code> must be one of the following:
1690  <p>
1691
1692  <code> 0 </code>: the closest variable to top (default) <p>
1693  <code> 1 </code>: the smallest BDD size after splitting <p>
1694
1695  <dt> tfm_output_split <code> &lt;method&gt; </code>
1696  <dd> Specify an output splitting method. <p>
1697  <dd>
1698  <code> method </code> must be one of the following:
1699  <p>
1700
1701  <code> 0 </code>: smallest BDD size (default) <p>
1702  <code> 1 </code>: largest BDD size <p>
1703  <code> 2 </code>: top variable <p>
1704
1705  <dt> tfm_turn_depth &lt;number&gt;
1706  <dd> This option is valid only when mixed or hybrid method is chosen.
1707  This is used to determine when to switch to the other method at which
1708  depth of recursion. The default is 5 for tfm and -1 for hybrid method. <p>
1709
1710  <dt> tfm_find_decomp_var <code> &lt;method&gt; </code>
1711  <dd> Specify a method whether to try to find a decomposable variable
1712  (meaning articulation point) first if any. <p>
1713  <dd>
1714  <code> method </code> must be one of the following:
1715  <p>
1716
1717  <code> yes </code>: try to find a decomposable variable (articulation point)
1718  <p>
1719  <code> no  </code>: do not try (default) <p>
1720
1721  <dt> tfm_sort_vector_flag <code> &lt;method&gt; </code>
1722  <dd> Specify a method whether to sort function vectors to increase cache
1723  performance. <p>
1724  <dd>
1725  <code> method </code> must be one of the following:
1726  <p>
1727
1728  <code> yes </code>: sort function vectors (default for tfm) <p>
1729  <code> no  </code>: do not sort (default for hybrid) <p>
1730
1731  <dt> tfm_print_stats <code> &lt;method&gt; </code>
1732  <dd> Specify a method whether to print statistics for cache and recursions
1733  at the end of job.<p>
1734  <dd>
1735  <code> method </code> must be one of the following:
1736  <p>
1737
1738  <code> yes </code>: print statistics <p>
1739  <code> no  </code>: do not print (default) <p>
1740
1741  <dt> tfm_print_bdd_size <code> &lt;method&gt; </code>
1742  <dd> Specify a method whether to print the BDD size of all intermediate
1743  product. <p>
1744  <dd>
1745  <code> method </code> must be one of the following:
1746  <p>
1747
1748  <code> yes </code>: print BDD size <p>
1749  <code> no  </code>: do not print (default) <p>
1750
1751  <dt> tfm_split_cube_func <code> &lt;method&gt; </code>
1752  <dd> Specify a method whether to try to find a cube in function vector
1753  in input splitting, then perform output splitting once w.r.t. the cube. <p>
1754 
1755  <dd>
1756  <code> method </code> must be one of the following:
1757  <p>
1758
1759  <code> yes </code>: try cube splitting <p>
1760  <code> no  </code>: do not try (default) <p>
1761
1762  <dt> tfm_find_essential <code> &lt;method&gt; </code>
1763  <dd> Specify a method whether to try to find essential variables in from set.
1764  If a variable occurs in all cubes of a BDD, the variable is called essential.
1765  If exists, minimize both function vector and the from set with the essential
1766  cube. <p>
1767  <dd>
1768  <code> method </code> must be one of the following:
1769  <p>
1770
1771  <code> 0 </code>: do not try (default) <p>
1772  <code> 1 </code>: try to find essential variables <p>
1773  <code> 2 </code>: on and off dynamically <p>
1774
1775  <dt> tfm_print_essential <code> &lt;method&gt; </code>
1776  <dd> Specify a method whether to print information about essential variables.
1777  <p>
1778  <dd>
1779  <code> method </code> must be one of the following:
1780  <p>
1781
1782  <code> 0 </code>: do not print (default) <p>
1783  <code> 1 </code>: print only at end <p>
1784  <code> 2 </code>: print at every image computation <p>
1785
1786  <dt> tfm_use_cache <code> &lt;method&gt; </code>
1787  <dd> Specify whether to use an image cache. <p>
1788  <dd>
1789  <code> method </code> must be one of the following:
1790  <p>
1791
1792  <code> 0 </code>: do not use cache (default for hybrid) <p>
1793  <code> 1 </code>: use cache (default) <p>
1794  <code> 2 </code>: store all intermediate results <p>
1795
1796  <dt> tfm_global_cache <code> &lt;method&gt; </code>
1797  <dd> Specify a method whether to use one global image cache, or one image
1798  cache per each machine. <p>
1799  <dd>
1800  <code> method </code> must be one of the following:
1801  <p>
1802
1803  <code> yes </code>: use only one global cache (default) <p>
1804  <code> no  </code>: use one cache per machine <p>
1805
1806  <dt> tfm_max_chain_length &lt;number&gt;
1807  <dd> This option is used to set the maximum number of items in a slot for
1808  conflict. The default is 2. <p>
1809
1810  <dt> tfm_init_cache_size &lt;number&gt;
1811  <dd> This option is used to set the initial cache size. The number is
1812  recommended to be a prime number. Currently, we do not resize the cache size,
1813  but for the future extension, we named initial. The default is 1001. <p>
1814
1815  <dt> tfm_auto_flush_cache <code> &lt;method&gt; </code>
1816  <dd> Specify a method to flush image cache. <p>
1817  <dd>
1818  <code> method </code> must be one of the following:
1819  <p>
1820
1821  <code> 0 </code>: flush cache only when requested <p>
1822  <code> 1 </code>: flush cache at the end of image computation (default) <p>
1823  <code> 2 </code>: flush cache before reordering <p>
1824
1825  <dt> tfm_compose_intermediate_vars <code> &lt;method&gt; </code>
1826  <dd> Specify a method whether to compose all intermediate variables.  <p>
1827  <dd>
1828  <code> method </code> must be one of the following:
1829  <p>
1830
1831  <code> yes </code>: compose all <p>
1832  <code> no  </code>: do not compose (default) <p>
1833
1834  <dt> tfm_pre_split_method <code> &lt;method&gt; </code>
1835  <dd> Specify a splitting method for preimage computation. <p>
1836  <dd>
1837  <code> method </code> must be one of the following:
1838  <p>
1839
1840  <code> 0 </code>: input splitting (domain cofactoring, default) <p>
1841  <code> 1 </code>: output splitting (constraint cofactoring) <p>
1842  <code> 2 </code>: mixed (input split + output split) <p>
1843  <code> 3 </code>: substitution <p>
1844
1845  <dt> tfm_pre_input_split <code> &lt;method&gt; </code>
1846  <dd> Specify an input splitting method for preimage computation. <p>
1847  <dd>
1848  <code> method </code> must be one of the following:
1849  <p>
1850
1851  <code> 0 </code>: support before splitting (default) <p>
1852  <code> 1 </code>: support after splitting <p>
1853  <code> 2 </code>: estimate BDD size after splitting <p>
1854  <code> 3 </code>: top variable <p>
1855
1856  <dt> tfm_pre_output_split <code> &lt;method&gt; </code>
1857  <dd> Specify an output splitting method for preimage computation. <p>
1858  <dd>
1859  <code> method </code> must be one of the following:
1860  <p>
1861
1862  <code> 0 </code>: smallest BDD size (default) <p>
1863  <code> 1 </code>: largest BDD size <p>
1864  <code> 2 </code>: top variable <p>
1865
1866  <dt> tfm_pre_dc_leaf_method <code> &lt;method&gt; </code>
1867  <dd> Specify a method to switch to another method to complete preimage
1868  computation in domain cofactoring method when no more splitting variable
1869  exist. <p>
1870  <dd>
1871  <code> method </code> must be one of the following:
1872  <p>
1873
1874  <code> 0 </code>: substitution (default) <p>
1875  <code> 1 </code>: constraint cofactoring <p>
1876  <code> 2 </code>: hybrid <p>
1877
1878  <dt> tfm_pre_minimize <code> &lt;method&gt; </code>
1879  <dd> Specify a method whether to minimize transition function vector
1880  w.r.t a chosen function in constraint cofactoring method. This
1881  option is recommended to use when image cache is disabled, because
1882  even though this option can minimize the BDD size of function vector,
1883  this may degrade cache performance. <p>
1884  <dd>
1885  <code> method </code> must be one of the following:
1886  <p>
1887
1888  <code> yes </code>: minimize function vector w.r.t. a chosen function
1889                in constraint cofactoring <p>
1890  <code> no  </code>: do not minimize (default) <p>
1891
1892  <dt> tfm_verbosity <code> &lt;verbosity&gt; </code>
1893  <dd> Specify the level of printing information related with transition
1894  function method.
1895  <p>
1896  <dd>
1897  <code> verbosity </code> must be 0 - 2 (default = 0).
1898  <p>
1899
1900  </dl>
1901  ]
1902 
1903  SideEffects []
1904
1905******************************************************************************/
1906static int
1907CommandPrintTfmOptions(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
1908{
1909  int c;
1910
1911  if (*hmgr == NULL) {
1912    fprintf(vis_stderr,"** hrc error: Hierarchy manager is empty\n");
1913    return 1;
1914  }
1915
1916  util_getopt_reset();
1917  while ((c = util_getopt(argc, argv, "hH")) != EOF) {
1918    switch(c) {
1919      case 'h':
1920        goto usage;
1921      case 'H':
1922        goto usage_tfm;
1923      default:
1924        goto usage;
1925    }
1926     /* NOT REACHED */
1927 }
1928
1929  /* print transition function based image computation options */
1930  Img_PrintTfmOptions();
1931  return 0;
1932
1933usage:
1934  (void) fprintf(vis_stderr,"usage: print_tfm_options [-h] [-H]\n");
1935  (void) fprintf(vis_stderr, "  -h  print the command usage\n");
1936  (void) fprintf(vis_stderr, "  -H  print the transition function based ");
1937  (void) fprintf(vis_stderr, "image computation set command usage\n");
1938  return 1;
1939usage_tfm:
1940  (void) fprintf(vis_stderr, "   set tfm_split_method <m>\n");
1941  (void) fprintf(vis_stderr, "       m = 0 : input splitting (default)\n");
1942  (void) fprintf(vis_stderr, "       m = 1 : output splitting\n");
1943  (void) fprintf(vis_stderr, "       m = 2 : mixed (input split + output split)\n");
1944  (void) fprintf(vis_stderr, "   set tfm_input_split <m>\n");
1945  (void) fprintf(vis_stderr, "       m = 0 : support before splitting (default)\n");
1946  (void) fprintf(vis_stderr, "       m = 1 : support after splitting\n");
1947  (void) fprintf(vis_stderr, "       m = 2 : estimate BDD size after splitting\n");
1948  (void) fprintf(vis_stderr, "       m = 3 : top variable\n");
1949  (void) fprintf(vis_stderr, "   set tfm_pi_split_flag <m>\n");
1950  (void) fprintf(vis_stderr, "       m = yes : choose either state or input variable as splitting variable\n");
1951  (void) fprintf(vis_stderr, "                 (default)\n");
1952  (void) fprintf(vis_stderr, "       m = no  : choose only state variable as splitting variable\n");
1953  (void) fprintf(vis_stderr, "   set tfm_range_comp <m>\n");
1954  (void) fprintf(vis_stderr, "       m = 0 : do not convert to range computation\n");
1955  (void) fprintf(vis_stderr, "       m = 1 : convert image to range computation (default)\n");
1956  (void) fprintf(vis_stderr, "       m = 2 : use a threshold (tfm_range_threshold, default for hybrid)\n");
1957  (void) fprintf(vis_stderr, "   set tfm_range_threshold <n>\n");
1958  (void) fprintf(vis_stderr, "       n (default = 10)\n");
1959  (void) fprintf(vis_stderr, "   set tfm_range_try_threshold <n>\n");
1960  (void) fprintf(vis_stderr, "       n (default = 2)\n");
1961  (void) fprintf(vis_stderr, "   set tfm_range_check_reorder <m>\n");
1962  (void) fprintf(vis_stderr, "       m = yes : force to reorder before checking tfm_range_threshold\n");
1963  (void) fprintf(vis_stderr, "       m = no  : do not reorder (default)\n");
1964  (void) fprintf(vis_stderr, "   set tfm_tie_break_mode <m>\n");
1965  (void) fprintf(vis_stderr, "       m = 0 : the closest variable to top (default)\n");
1966  (void) fprintf(vis_stderr, "       m = 1 : the smallest BDD size after splitting\n");
1967  (void) fprintf(vis_stderr, "   set tfm_output_split <m>\n");
1968  (void) fprintf(vis_stderr, "       m = 0 : smallest BDD size (default)\n");
1969  (void) fprintf(vis_stderr, "       m = 1 : largest BDD size\n");
1970  (void) fprintf(vis_stderr, "       m = 2 : top variable\n");
1971  (void) fprintf(vis_stderr, "   set tfm_turn_depth <n>\n");
1972  (void) fprintf(vis_stderr, "       n (default = 5, -1 for hybrid)\n");
1973  (void) fprintf(vis_stderr, "   set tfm_find_decomp_var <m>\n");
1974  (void) fprintf(vis_stderr, "       m = yes : try to find a decomposable variable (articulation point)\n");
1975  (void) fprintf(vis_stderr, "       m = no  : do not try (default)\n");
1976  (void) fprintf(vis_stderr, "   set tfm_sort_vector_flag <m>\n");
1977  (void) fprintf(vis_stderr, "       m = yes : sort function vectors to utilize cache (default for tfm)\n");
1978  (void) fprintf(vis_stderr, "       m = no  : do not sort (default for hybrid)\n");
1979  (void) fprintf(vis_stderr, "   set tfm_print_stats <m>\n");
1980  (void) fprintf(vis_stderr, "       m = yes : print statistics for cache and recursions\n");
1981  (void) fprintf(vis_stderr, "       m = no  : do not print (default)\n");
1982  (void) fprintf(vis_stderr, "   set tfm_print_bdd_size <m>\n");
1983  (void) fprintf(vis_stderr, "       m = yes : print BDD size of all intermediate product\n");
1984  (void) fprintf(vis_stderr, "       m = no  : do not print (default)\n");
1985  (void) fprintf(vis_stderr, "   set tfm_split_cube_func <m>\n");
1986  (void) fprintf(vis_stderr, "       m = yes : find a cube function element,\n");
1987  (void) fprintf(vis_stderr, "                 then apply output splitting in input splitting\n");
1988  (void) fprintf(vis_stderr, "       m = no  : do not try (default)\n");
1989  (void) fprintf(vis_stderr, "   set tfm_find_essential <m>\n");
1990  (void) fprintf(vis_stderr, "       m = 0 : do not try (default)\n");
1991  (void) fprintf(vis_stderr, "       m = 1 : try to find essential variables\n");
1992  (void) fprintf(vis_stderr, "       m = 2 : on and off dynamically\n");
1993  (void) fprintf(vis_stderr, "   set tfm_print_essential <m>\n");
1994  (void) fprintf(vis_stderr, "       m = 0 : do not print (default)\n");
1995  (void) fprintf(vis_stderr, "       m = 1 : print only at end\n");
1996  (void) fprintf(vis_stderr, "       m = 2 : print at every image computation\n");
1997  (void) fprintf(vis_stderr, "   set tfm_use_cache <m>\n");
1998  (void) fprintf(vis_stderr, "       m = 0 : do not use cache (default for hybrid)\n");
1999  (void) fprintf(vis_stderr, "       m = 1 : use cache (default)\n");
2000  (void) fprintf(vis_stderr, "       m = 2 : store all intermediate results\n");
2001  (void) fprintf(vis_stderr, "   set tfm_global_cache <m>\n");
2002  (void) fprintf(vis_stderr, "       m = yes : use only one global cache (default)\n");
2003  (void) fprintf(vis_stderr, "       m = no  : use one cache per machine\n");
2004  (void) fprintf(vis_stderr, "   set tfm_max_chain_length <n>\n");
2005  (void) fprintf(vis_stderr, "       n (default = 2)\n");
2006  (void) fprintf(vis_stderr, "   set tfm_init_cache_size <n>\n");
2007  (void) fprintf(vis_stderr, "       n (default = 1001)\n");
2008  (void) fprintf(vis_stderr, "   set tfm_auto_flush_cache <m>\n");
2009  (void) fprintf(vis_stderr, "       m = 0 : flush cache only when requested\n");
2010  (void) fprintf(vis_stderr, "       m = 1 : flush cache at the end of image computation (default)\n");
2011  (void) fprintf(vis_stderr, "       m = 2 : flush cache before reordering\n");
2012  (void) fprintf(vis_stderr, "   set tfm_compose_intermediate_vars <m>\n");
2013  (void) fprintf(vis_stderr, "       m = yes : compose all intermediate vars\n");
2014  (void) fprintf(vis_stderr, "       m = no  : do not compose (default)\n");
2015  (void) fprintf(vis_stderr, "   set tfm_pre_split_method <m>\n");
2016  (void) fprintf(vis_stderr, "       m = 0 : input splitting (domain cofactoring, default)\n");
2017  (void) fprintf(vis_stderr, "       m = 1 : output splitting (constraint cofactoring)\n");
2018  (void) fprintf(vis_stderr, "       m = 2 : mixed (input split + output split)\n");
2019  (void) fprintf(vis_stderr, "       m = 3 : substitution\n");
2020  (void) fprintf(vis_stderr, "   set tfm_pre_input_split <m>\n");
2021  (void) fprintf(vis_stderr, "       m = 0 : support before splitting (default)\n");
2022  (void) fprintf(vis_stderr, "       m = 1 : support after splitting\n");
2023  (void) fprintf(vis_stderr, "       m = 2 : estimate BDD size after splitting\n");
2024  (void) fprintf(vis_stderr, "       m = 3 : top variable\n");
2025  (void) fprintf(vis_stderr, "   set tfm_pre_output_split <m>\n");
2026  (void) fprintf(vis_stderr, "       m = 0 : smallest BDD size (default)\n");
2027  (void) fprintf(vis_stderr, "       m = 1 : largest BDD size\n");
2028  (void) fprintf(vis_stderr, "       m = 2 : top variable\n");
2029  (void) fprintf(vis_stderr, "   set tfm_pre_dc_leaf_method <m>\n");
2030  (void) fprintf(vis_stderr, "       m = 0 : substitution (default)\n");
2031  (void) fprintf(vis_stderr, "       m = 1 : constraint cofactoring\n");
2032  (void) fprintf(vis_stderr, "       m = 2 : hybrid\n");
2033  (void) fprintf(vis_stderr, "   set tfm_pre_minimize <m>\n");
2034  (void) fprintf(vis_stderr, "       m = yes : minimize function vector w.r.t. a chosen function\n");
2035  (void) fprintf(vis_stderr, "                 in constraint cofactoring\n");
2036  (void) fprintf(vis_stderr, "       m = no  : do not minimize (default)\n");
2037  (void) fprintf(vis_stderr, "   set tfm_verbosity <n>\n");
2038  (void) fprintf(vis_stderr, "       n = 0 - 2 (default = 0)\n");
2039  return 1;
2040} /* end of CommandPrintTfmOptions */
2041
2042
2043/**Function********************************************************************
2044
2045  Synopsis    [Implements the print_hybrid_options command.]
2046
2047  CommandName [print_hybrid_options]
2048
2049  CommandSynopsis [print information about the hybrid image computation options
2050  currently in use]
2051
2052  CommandArguments [\[-h\] \[-H\]]
2053
2054  CommandDescription [Prints information about the current hybrid image
2055  computation options.
2056  <p>
2057
2058  Command options: <p>
2059
2060  <dl>
2061
2062  <dt> -h
2063  <dd> Print the command usage.<p>
2064
2065  <dt> -H
2066  <dd> Print the hybrid image computation set command usage.<p>
2067 
2068  </dl>
2069
2070  Set parameters: The hybrid image computation options are specified with the
2071  set command.
2072
2073  <dl>
2074
2075  <dt> hybrid_mode <code> <m>&lt;mode<m>&gt; </code>
2076  <dd> Specify a mode how to start hybrid computation. <p>
2077  <dd>
2078  <code> mode </code> must be one of the following:
2079  <p>
2080
2081  <code> 0 </code>: start with only transition function and build transition
2082  relation on demand <p>
2083  <code> 1 </code>: start with both transition function and relation (default)
2084  <p>
2085  <code> 2 </code>: start with only transition relation. Only this mode
2086  can deal with nondeterminism.<p>
2087
2088  <dt> hybrid_tr_split_method <code> <m>&lt;method<m>&gt; </code>
2089  <dd> Specify a method to choose a splitting variable in hybrid mode = 2. <p>
2090  <dd>
2091  <code> method </code> must be one of the following:
2092  <p>
2093
2094  <code> 0 </code>: use support (default) <p>
2095  <code> 1 </code>: use estimate BDD size <p>
2096
2097  <dt> hybrid_build_partial_tr <code> <m>&lt;method<m>&gt; </code>
2098  <dd> Specify whether to build full or partial transition relation in
2099  hybrid mode = 2.
2100  This option is used to use less memory. When we use partial transition
2101  relation, for the variables excluded in the transition relation, we build
2102  each bit transition relation on demand. When nondeterminism exists in
2103  the circuit, this can not be used.
2104  <dd>
2105  <code> method </code> must be one of the following:
2106  <p>
2107
2108  <code> yes </code>: build partial transition relation <p>
2109  <code> no  </code>: build full transition relation (default) <p>
2110
2111  <dt> hybrid_partial_num_vars &lt;number&gt;
2112  <dd> Specify how many variables are going to be excluded in building
2113  partial transition relation. The default is 8. <p>
2114
2115  <dt> hybrid_partial_method <code> <m>&lt;method<m>&gt; </code>
2116  <dd> Specify a method to choose variables to be excluded in building
2117  partial transition relation. <p>
2118  <dd>
2119  <code> method </code> must be one of the following:
2120  <p>
2121
2122  <code> 0 </code>: use BDD size (default) <p>
2123  <code> 1 </code>: use support <p>
2124
2125  <dt> hybrid_delayed_split <code> <m>&lt;method<m>&gt; </code>
2126  <dd> Specify a method whether to split transition relation immediately or
2127  just all at once before AndExist. <p>
2128  <dd>
2129  <code> method </code> must be one of the following:
2130  <p>
2131
2132  <code> yes </code>: apply splitting to transition relation at once <p>
2133  <code> no  </code>: do not apply (default) <p>
2134
2135  <dt> hybrid_split_min_depth &lt;number&gt;
2136  <dd> Specify the minimum depth to apply dynamic hybrid method. If a depth
2137  is smaller than this minimum depth, just split. The default is 1. <p>
2138
2139  <dt> hybrid_split_max_depth &lt;number&gt;
2140  <dd> Specify the maximum depth to apply dynamic hybrid method. If a depth
2141  is bigger than this maximum depth, just conjoin. The default is 5. <p>
2142
2143  <dt> hybrid_pre_split_min_depth &lt;number&gt;
2144  <dd> Specify the minimum depth to apply dynamic hybrid method in preimage
2145  computation. If a depth is smaller than this minimum depth, just split.
2146  The default is 0. <p>
2147
2148  <dt> hybrid_pre_split_max_depth &lt;number&gt;
2149  <dd> Specify the maximum depth to apply dynamic hybrid method in preimage
2150  computation. If a depth is bigger than this maximum depth, just conjoin.
2151  The default is 4. <p>
2152
2153  <dt> hybrid_lambda_threshold &lt;number&gt;
2154  <dd> Specify a threshold in floating between 0.0 and 1.0 to determine
2155  to split or to conjoin after computing variable lifetime lambda for
2156  image computation.
2157  If lambda is equal or smaller than this threshold, we conjoin.
2158  Otherwise we split. The default is 0.6 <p>
2159
2160  <dt> hybrid_pre_lambda_threshold &lt;number&gt;
2161  <dd> Specify a threshold in floating between 0.0 and 1.0 to determine
2162  to split or to conjoin after computing variable lifetime lambda for
2163  preimage computation.
2164  If lambda is equal or smaller than this threshold, we conjoin.
2165  Otherwise we split. The default is 0.65 <p>
2166
2167  <dt> hybrid_conjoin_vector_size &lt;number&gt;
2168  <dd> If the number of components in transition function vector is equal or
2169  smaller than this threshold, we just conjoin. This check is performed before
2170  computing lambda. The default is 10. <p>
2171
2172  <dt> hybrid_conjoin_relation_size &lt;number&gt;
2173  <dd> If the number of clusters in transition relation is equal or smaller
2174  than this threshold, we just conjoin. This check is performed before
2175  computing lambda. The default is 2. <p>
2176
2177  <dt> hybrid_conjoin_relation_bdd_size &lt;number&gt;
2178  <dd> If the shared BDD size of transition relation is equal or smaller than
2179  this threshold, we conjoin. This check is performed before computing lambda.
2180  The default is 200. <p>
2181
2182  <dt> hybrid_improve_lambda &lt;number&gt;
2183  <dd> When variable lifetime lambda is bigger than lambda threshold,
2184  if the difference between previous and current lambda is equal or smaller
2185  than this threshold, then we conjoin. The default is 0.1. <p>
2186
2187  <dt> hybrid_improve_vector_size &lt;number&gt;
2188  <dd> When variable lifetime lambda is bigger than lambda threshold,
2189  if the difference between the previous and current number of components
2190  in transition function vector is equal or smaller than this threshold,
2191  then we conjoin. The default is 3. <p>
2192
2193  <dt> hybrid_improve_vector_bdd_size &lt;number&gt;
2194  <dd> When variable lifetime lambda is bigger than lambda threshold,
2195  if the difference between the previous and current shared BDD size of
2196  transition function vector is equal or smaller than this threshold,
2197  then we conjoin. The default is 30.0. <p>
2198
2199  <dt> hybrid_decide_mode <code> <m>&lt;method<m>&gt; </code>
2200  <dd> Specify a method to decide whether to split or to conjoin. <p>
2201  <dd>
2202  <code> method </code> must be one of the following:
2203  <p>
2204
2205  <code> 0 </code>: use only lambda <p>
2206  <code> 1 </code>: use lambda and also special checks to conjoin <p>
2207  <code> 2 </code>: use lambda and also improvement <p>
2208  <code> 3 </code>: use all (default) <p>
2209
2210  <dt> hybrid_reorder_with_from <code> <m>&lt;method<m>&gt; </code>
2211  <dd> Specify a method to reorder transition relation to conjoin in image
2212  computation, whether to include from set in the computation. <p>
2213  <dd>
2214  <code> method </code> must be one of the following:
2215  <p>
2216
2217  <code> yes </code>: reorder relation array with from to conjoin (default) <p>
2218  <code> no  </code>: reorder relation array without from to conjoin <p>
2219
2220  <dt> hybrid_pre_reorder_with_from <code> <m>&lt;method<m>&gt; </code>
2221  <dd> Specify a method to reorder transition relation to conjoin in preimage
2222  computation, whether to include from set in the computation. <p>
2223  <dd>
2224  <code> method </code> must be one of the following:
2225  <p>
2226
2227  <code> yes </code>: reorder relation array with from to conjoin <p>
2228  <code> no  </code>: reorder relation array without from to conjoin (default)
2229  <p>
2230
2231  <dt> hybrid_lambda_mode <code> <m>&lt;method<m>&gt; </code>
2232  <dd> Specify a method to decide which variable lifetime to be used for
2233  image computation. <p>
2234  <dd>
2235  <code> method </code> must be one of the following:
2236  <p>
2237
2238  <code> 0 </code>: total lifetime with ps/pi variables (default) <p>
2239  <code> 1 </code>: active lifetime with ps/pi variables <p>
2240  <code> 2 </code>: total lifetime with ps/ns/pi variables <p>
2241
2242  <dt> hybrid_pre_lambda_mode <code> <m>&lt;method<m>&gt; </code>
2243  <dd> Specify a method to decide which variable lifetime to be used for
2244  preimage computation. <p>
2245  <dd>
2246  <code> method </code> must be one of the following:
2247  <p>
2248
2249  <code> 0 </code>: total lifetime with ns/pi variables <p>
2250  <code> 1 </code>: active lifetime with ps/pi variables <p>
2251  <code> 2 </code>: total lifetime with ps/ns/pi variables (default) <p>
2252  <code> 3 </code>: total lifetime with ps/pi variables <p>
2253
2254  <dt> hybrid_lambda_with_from <code> <m>&lt;method<m>&gt; </code>
2255  <dd> Specify a method to compute variable lifetime lambda, whether
2256  to include from set in the computation. <p>
2257  <dd>
2258  <code> method </code> must be one of the following:
2259  <p>
2260
2261  <code> yes </code>: include from set in lambda computation (default) <p>
2262  <code> no  </code>: do not include <p>
2263
2264  <dt> hybrid_lambda_with_tr <code> <m>&lt;method<m>&gt; </code>
2265  <dd> Specify a method to compute variable lifetime lambda, whether
2266  to use transition relation or transition function vector, when both
2267  exist. <p>
2268  <dd>
2269  <code> method </code> must be one of the following:
2270  <p>
2271
2272  <code> yes </code>: use transition relation (default) <p>
2273  <code> no  </code>: use transition function vector <p>
2274
2275  <dt> hybrid_lambda_with_clustering <code> <m>&lt;method<m>&gt; </code>
2276  <dd> Specify a method whether to include clustering to compute variable
2277  lifetime lambda. <p>
2278  <dd>
2279  <code> method </code> must be one of the following:
2280  <p>
2281
2282  <code> yes </code>: compute lambda after clustering <p>
2283  <code> no  </code>: do not cluster (default) <p>
2284
2285  <dt> hybrid_synchronize_tr <code> <m>&lt;method<m>&gt; </code>
2286  <dd> Specify a method to keep transition relation. This option is only for
2287  when hybrid mode is 1. <p>
2288  <dd>
2289  <code> method </code> must be one of the following:
2290  <p>
2291
2292  <code> yes </code>: rebuild transition relation from function vector
2293  whenever the function vector changes <p>
2294  <code> no  </code>: do not rebuild (default) <p>
2295
2296  <dt> hybrid_img_keep_pi <code> <m>&lt;method<m>&gt; </code>
2297  <dd> Specify a method to build forward transition relation. <p>
2298  <dd>
2299  <code> method </code> must be one of the following:
2300  <p>
2301
2302  <code> yes </code>: keep all primary input variables in forward transition
2303  relation. <p>
2304  <code> no  </code>: quantify out local primary input variables from the
2305  transition relation. (default) <p>
2306
2307  <dt> hybrid_pre_keep_pi <code> <m>&lt;method<m>&gt; </code>
2308  <dd> Specify a method to build backward transition relation. <p>
2309  <dd>
2310  <code> method </code> must be one of the following:
2311  <p>
2312
2313  <code> yes </code>: keep all primary input variables in backward transition
2314  relation and preimages. <p>
2315  <code> no  </code>: quantify out local primary input variables from the
2316  transition relation. (default) <p>
2317
2318  <dt> hybrid_pre_canonical <code> <m>&lt;method<m>&gt; </code>
2319  <dd> Specify a method whether to canonicalize the function vector for
2320  preimage computation. <p>
2321  <dd>
2322  <code> method </code> must be one of the following:
2323  <p>
2324
2325  <code> yes </code>: canonicalize the function vector <p>
2326  <code> no  </code>: do not canonicalize (default) <p>
2327
2328  <dt> hybrid_tr_method <code> <m>lt;method<m>gt; </code>
2329  <dd> Specify an image method for AndExist operation in hybrid method. <p>
2330  <dd>
2331  <code> method </code> must be one of the following:
2332  <p>
2333
2334  <code> iwls95 (default) <p>
2335  <code> mlp <p>
2336
2337  </dl>
2338  ]
2339 
2340  SideEffects []
2341
2342******************************************************************************/
2343static int
2344CommandPrintHybridOptions(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
2345{
2346  int c;
2347
2348  if (*hmgr == NULL) {
2349    fprintf(vis_stderr,"** hrc error: Hierarchy manager is empty\n");
2350    return 1;
2351  }
2352
2353  util_getopt_reset();
2354  while ((c = util_getopt(argc, argv, "hH")) != EOF) {
2355    switch(c) {
2356      case 'h':
2357        goto usage;
2358      case 'H':
2359        goto usage_hybrid;
2360      default:
2361        goto usage;
2362    }
2363  }
2364
2365  /* print hybrid image computation options */
2366  Img_PrintHybridOptions();
2367  return 0;
2368
2369usage:
2370  (void) fprintf(vis_stderr,"usage: print_hybrid_options [-h] [-H]\n");
2371  (void) fprintf(vis_stderr, "  -h  print the command usage\n");
2372  (void) fprintf(vis_stderr,
2373                "  -H  print the hybrid image computation set command usage\n");
2374  return 1;
2375usage_hybrid:
2376  (void) fprintf(vis_stderr, "   set hybrid_mode <m>\n");
2377  (void) fprintf(vis_stderr, "       m = 0 : start with only transition function\n");
2378  (void) fprintf(vis_stderr, "       m = 1 : start with both transition function and relation at the beginning (default)\n");
2379  (void) fprintf(vis_stderr, "       m = 2 : start with only transition relation\n");
2380  (void) fprintf(vis_stderr, "   set hybrid_tr_split_method <m>\n");
2381  (void) fprintf(vis_stderr, "       m = 0 : use support (default)\n");
2382  (void) fprintf(vis_stderr, "       m = 1 : use estimate BDD size\n");
2383  (void) fprintf(vis_stderr, "   set hybrid_build_partial_tr <m>\n");
2384  (void) fprintf(vis_stderr, "       m = yes : build partial transition relation\n");
2385  (void) fprintf(vis_stderr, "       m = no  : build full transition relation (default)\n");
2386  (void) fprintf(vis_stderr, "   set hybrid_partial_num_vars <n>\n");
2387  (void) fprintf(vis_stderr, "       n (default = 8)\n");
2388  (void) fprintf(vis_stderr, "   set hybrid_partial_method <m>\n");
2389  (void) fprintf(vis_stderr, "       m = 0 : use BDD size (default)\n");
2390  (void) fprintf(vis_stderr, "       m = 1 : use support\n");
2391  (void) fprintf(vis_stderr, "   set hybrid_delayed_split <m>\n");
2392  (void) fprintf(vis_stderr, "       m = yes : apply splitting to transition relation at once\n");
2393  (void) fprintf(vis_stderr, "       m = no  : do not apply (default)\n");
2394  (void) fprintf(vis_stderr, "   set hybrid_split_min_depth <n>\n");
2395  (void) fprintf(vis_stderr, "       n (default = 1)\n");
2396  (void) fprintf(vis_stderr, "   set hybrid_split_max_depth <n>\n");
2397  (void) fprintf(vis_stderr, "       n (default = 5)\n");
2398  (void) fprintf(vis_stderr, "   set hybrid_pre_split_min_depth <n>\n");
2399  (void) fprintf(vis_stderr, "       n (default = 0)\n");
2400  (void) fprintf(vis_stderr, "   set hybrid_pre_split_max_depth <n>\n");
2401  (void) fprintf(vis_stderr, "       n (default = 4)\n");
2402  (void) fprintf(vis_stderr, "   set hybrid_lambda_threshold <f>\n");
2403  (void) fprintf(vis_stderr, "       f (default = 0.6)\n");
2404  (void) fprintf(vis_stderr, "   set hybrid_pre_lambda_threshold <f>\n");
2405  (void) fprintf(vis_stderr, "       f (default = 0.65)\n");
2406  (void) fprintf(vis_stderr, "   set hybrid_conjoin_vector_size <n>\n");
2407  (void) fprintf(vis_stderr, "       n (default = 10)\n");
2408  (void) fprintf(vis_stderr, "   set hybrid_conjoin_relation_size <n>\n");
2409  (void) fprintf(vis_stderr, "       n (default = 2)\n");
2410  (void) fprintf(vis_stderr, "   set hybrid_conjoin_relation_bdd_size <n>\n");
2411  (void) fprintf(vis_stderr, "       n (default = 200)\n");
2412  (void) fprintf(vis_stderr, "   set hybrid_improve_lambda <f>\n");
2413  (void) fprintf(vis_stderr, "       f (default = 0.1)\n");
2414  (void) fprintf(vis_stderr, "   set hybrid_improve_vector_size <n>\n");
2415  (void) fprintf(vis_stderr, "       n (default = 3)\n");
2416  (void) fprintf(vis_stderr, "   set hybrid_improve_vector_bdd_size <f>\n");
2417  (void) fprintf(vis_stderr, "       f (default = 30.0)\n");
2418  (void) fprintf(vis_stderr, "   set hybrid_decide_mode <m>\n");
2419  (void) fprintf(vis_stderr, "       m = 0 : use only lambda\n");
2420  (void) fprintf(vis_stderr, "       m = 1 : use lambda and special checks\n");
2421  (void) fprintf(vis_stderr, "       m = 2 : use lambda and improvement\n");
2422  (void) fprintf(vis_stderr, "       m = 3 : use all (default)\n");
2423  (void) fprintf(vis_stderr, "   set hybrid_reorder_with_from <m>\n");
2424  (void) fprintf(vis_stderr, "       m = yes : include from set in reordering relation array (default)\n");
2425  (void) fprintf(vis_stderr, "       m = no  : do not include\n");
2426  (void) fprintf(vis_stderr, "   set hybrid_pre_reorder_with_from <m>\n");
2427  (void) fprintf(vis_stderr, "       m = yes : include from set in reordering relation array\n");
2428  (void) fprintf(vis_stderr, "       m = no  : do not include (default)\n");
2429  (void) fprintf(vis_stderr, "   set hybrid_lambda_mode <m>\n");
2430  (void) fprintf(vis_stderr, "       m = 0 : total lifetime with ps/pi variables (default)\n");
2431  (void) fprintf(vis_stderr, "       m = 1 : active lifetime with ps/pi variables\n");
2432  (void) fprintf(vis_stderr, "       m = 2 : total lifetime with ps/ns/pi variables\n");
2433  (void) fprintf(vis_stderr, "   set hybrid_pre_lambda_mode <m>\n");
2434  (void) fprintf(vis_stderr, "       m = 0 : total lifetime with ns/pi variables\n");
2435  (void) fprintf(vis_stderr, "       m = 1 : active lifetime with ps/pi variables\n");
2436  (void) fprintf(vis_stderr, "       m = 2 : total lifetime with ps/ns/pi variables (default)\n");
2437  (void) fprintf(vis_stderr, "       m = 3 : total lifetime with ps/pi variables\n");
2438  (void) fprintf(vis_stderr, "   set hybrid_lambda_with_from <m>\n");
2439  (void) fprintf(vis_stderr, "       m = yes : include from set in lambda computation (default)\n");
2440  (void) fprintf(vis_stderr, "       m = no  : do not include\n");
2441  (void) fprintf(vis_stderr, "   set hybrid_lambda_with_clustering <m>\n");
2442  (void) fprintf(vis_stderr, "       m = yes : compute lambda after clustering\n");
2443  (void) fprintf(vis_stderr, "       m = no  : do not cluster (default)\n");
2444  (void) fprintf(vis_stderr, "   set hybrid_synchronize_tr <m>\n");
2445  (void) fprintf(vis_stderr, "       m = yes : rebuild transition relation whenever function vector changes\n");
2446  (void) fprintf(vis_stderr, "       m = no  : do not rebuild (default)\n");
2447  (void) fprintf(vis_stderr, "   set hybrid_img_keep_pi <m>\n");
2448  (void) fprintf(vis_stderr, "       m = yes : keep all pi variables in forward tr\n");
2449  (void) fprintf(vis_stderr, "       m = no  : quantify out local pi variables (default)\n");
2450  (void) fprintf(vis_stderr, "   set hybrid_pre_keep_pi <m>\n");
2451  (void) fprintf(vis_stderr, "       m = yes : keep all pi variables in backward tr and preimages\n");
2452  (void) fprintf(vis_stderr, "       m = no  : quantify out local pi variables (default)\n");
2453  (void) fprintf(vis_stderr, "   set hybrid_pre_canonical <m>\n");
2454  (void) fprintf(vis_stderr, "       m = yes : canonicalize the function vector for preimage\n");
2455  (void) fprintf(vis_stderr, "       m = no  : do not canonicalize (default)\n");
2456  (void) fprintf(vis_stderr, "   set hybrid_tr_method <m>\n");
2457  (void) fprintf(vis_stderr, "       m = iwls95 (default)\n");
2458  (void) fprintf(vis_stderr, "       m = mlp\n");
2459  return 1;
2460} /* end of CommandPrintHybridOptions */
2461
2462
2463/**Function********************************************************************
2464
2465  Synopsis    [Implements the print_mlp_options command.]
2466
2467  CommandName [print_mlp_options]
2468
2469  CommandSynopsis [print information about the MLP image computation options
2470  currently in use]
2471
2472  CommandArguments [\[-h\] \[-H\]]
2473
2474  CommandDescription [Prints information about the current MLP image
2475  computation options.
2476  <p>
2477
2478  Command options: <p>
2479
2480  <dl>
2481
2482  <dt> -h
2483  <dd> Print the command usage.<p>
2484
2485  <dt> -H
2486  <dd> Print the MLP image computation set command usage.<p>
2487 
2488  </dl>
2489
2490  Set parameters: The MLP image computation options are specified with the
2491  set command.
2492
2493  <dl>
2494
2495  <dt> mlp_cluster <code> <m>&lt;method<m>&gt; </code>
2496  <dd> Specify a method for clustering. <p>
2497  <dd>
2498  <code> method </code> must be one of the following:
2499  <p>
2500
2501  <code> 0 </code>: linear clustering <p>
2502  <code> 1 </code>: affinity based tree clustering (default) <p>
2503
2504  <dt> mlp_reorder <code> <m>&lt;method<m>&gt; </code>
2505  <dd> Specify a method for reordering after clustering for image
2506  computation. <p>
2507  <dd>
2508  <code> method </code> must be one of the following:
2509  <p>
2510
2511  <code> 0 </code>: no reordering after clustering (default) <p>
2512  <code> 1 </code>: reorder using MLP after clustering (inside) <p>
2513  <code> 2 </code>: reorder using MLP after clustering (outside) <p>
2514  <code> 3 </code>: reorder using IWLS95 after clustering <p>
2515
2516  <dt> mlp_pre_reorder <code> <m>&lt;method<m>&gt; </code>
2517  <dd> Specify a method for reordering after clustering for preimage
2518  computation. <p>
2519  <dd>
2520  <code> method </code> must be one of the following:
2521  <p>
2522
2523  <code> 0 </code>: no reordering after clustering (default) <p>
2524  <code> 1 </code>: reorder using MLP after clustering (inside) <p>
2525  <code> 2 </code>: reorder using MLP after clustering (outside) <p>
2526  <code> 3 </code>: reorder using IWLS95 after clustering <p>
2527
2528  <dt> mlp_postprocess <code> <m>&lt;method<m>&gt; </code>
2529  <dd> Specify when to do postprocessing. <p>
2530  <dd>
2531  <code> method </code> must be one of the following:
2532  <p>
2533
2534  <code> 0 </code>: no postprocessing (default) <p>
2535  <code> 1 </code>: do postprocesing after ordering <p>
2536  <code> 2 </code>: do postprocesing after clustering or reordering <p>
2537  <code> 3 </code>: do both 1 and 2 <p>
2538
2539  </dl>
2540  ]
2541 
2542  SideEffects []
2543
2544******************************************************************************/
2545static int
2546CommandPrintMlpOptions(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
2547{
2548  int c;
2549
2550  if (*hmgr == NULL) {
2551    fprintf(vis_stderr,"** hrc error: Hierarchy manager is empty\n");
2552    return 1;
2553  }
2554
2555  util_getopt_reset();
2556  while ((c = util_getopt(argc, argv, "hH")) != EOF) {
2557    switch(c) {
2558      case 'h':
2559        goto usage;
2560      case 'H':
2561        goto usage_mlp;
2562      default:
2563        goto usage;
2564    }
2565  }
2566
2567  /* print hybrid image computation options */
2568  Img_PrintMlpOptions();
2569  return 0;
2570
2571usage:
2572  (void) fprintf(vis_stderr,"usage: print_mlp_options [-h] [-H]\n");
2573  (void) fprintf(vis_stderr, "  -h  print the command usage\n");
2574  (void) fprintf(vis_stderr,
2575                "  -H  print the MLP image computation set command usage\n");
2576  return 1;
2577usage_mlp:
2578  (void) fprintf(vis_stderr, "   set mlp_cluster <m>\n");
2579  (void) fprintf(vis_stderr, "       m = 0 : linear clustering\n");
2580  (void) fprintf(vis_stderr, "       m = 1 : affinity based tree clustering (default)\n");
2581  (void) fprintf(vis_stderr, "   set mlp_reorder <m>\n");
2582  (void) fprintf(vis_stderr, "       m = 0 : no reordering after clustering (default)\n");
2583  (void) fprintf(vis_stderr, "       m = 1 : reorder using MLP after clustering (inside)\n");
2584  (void) fprintf(vis_stderr, "       m = 2 : reorder using MLP after clustering (outside)\n");
2585  (void) fprintf(vis_stderr, "       m = 3 : reorder using IWLS95 after clustering\n");
2586  (void) fprintf(vis_stderr, "   set mlp_pre_reorder <m>\n");
2587  (void) fprintf(vis_stderr, "       m = 0 : no reordering after clustering (default)\n");
2588  (void) fprintf(vis_stderr, "       m = 1 : reorder using MLP after clustering (inside)\n");
2589  (void) fprintf(vis_stderr, "       m = 2 : reorder using MLP after clustering (outside)\n");
2590  (void) fprintf(vis_stderr, "       m = 3 : reorder using IWLS95 after clustering\n");
2591  (void) fprintf(vis_stderr, "   set mlp_postprocess <m>\n");
2592  (void) fprintf(vis_stderr, "       m = 0 : no postprocessing (default)\n");
2593  (void) fprintf(vis_stderr, "       m = 1 : do postprocessing after ordering\n");
2594  (void) fprintf(vis_stderr, "       m = 2 : do postprocessing after clustering or reordering\n");
2595  (void) fprintf(vis_stderr, "       m = 3 : do both 1 and 2\n");
2596  return 1;
2597} /* end of CommandPrintMlpOptions */
2598
2599
2600/**Function********************************************************************
2601
2602  Synopsis    [Implements the print_guided_search_options command.]
2603
2604  CommandName [print_guided_search_options]
2605
2606  CommandSynopsis [print information about guided_search_options in use]
2607
2608  CommandArguments [\[-h\] ]
2609
2610  CommandDescription [Prints information about current Guided Search
2611  options. Guided search is an alternate method to compute fixpoints
2612  by modifying the fixpoint computation with restrictions. It is
2613  applicable to the <tt>compute_reach</tt>, <tt>check_invariant</tt>
2614  and <tt>model_check</tt> commands (refer to their help pages on the
2615  use of guided search). See also for details: Ravi and Somenzi, Hints
2616  to accelerate symbolic traversal. CHARME'99; Bloem, Ravi, and
2617  Somenzi, Efficient Decision Procedures for Model Checking of Linear
2618  Time Logic Properties, CAV'99; Bloem, Ravi, and Somenzi, Symbolic
2619  Guided Search for CTL Model Checking, DAC'00. Not allowed with -A 2
2620  or -i, and will only work with iwls95 or monolithic image methods.
2621  The description of some options can be found in the help page for
2622  set. <p>
2623
2624  Command options: <p>
2625
2626  <dl>
2627  <dt>guided_search_hint_type</dt>
2628 
2629  <dd>Choose from local (default) or global.  If this flag is set to
2630  local, then every subformula is evaluated to completion, using all
2631  hints in order, before the next subformula is started. For pure ACTL
2632  or pure ECTL formulae, we can also set guided_search_hint_type to
2633  global, in which case the entire formula is evaluated for one hint
2634  before moving on to the next hint, using underapproximations.</dd>
2635
2636  <dt>guided_search_underapprox_minimize_method</dt>
2637
2638  <dd>Choose from "constrain" and "and" (default).  Sets the method with which
2639  the transition relation is minimized when underapproximations are used.  The
2640  option constrain is incompatible with hints that use signals other than
2641  inputs.</dd>
2642
2643  <dt>guided_search_overapprox_minimize_method</dt>
2644
2645  <dd>Choose from "squeeze" and "ornot" (default).  Sets the method with which
2646  the transition relation is minimized when underapproximations are used.  The
2647  option squeeze is incompatible with hints that use signals other than inputs.
2648  Ornot implies that the transition relation will be disjoined with the
2649  negation of the hint: T' = T + ~h, whereas squeeze will find a small BDD
2650  between T and T'.</dd>
2651
2652  <dt>guided_search_sequence</dt>
2653
2654  <dd>For compute_reach and check_invariant only.  Set this flag to a list of
2655  comma-separated integers <code>i1,i2,...,in</code>, with <code>n</code> at
2656  most the number of hints that you specify .  The <code>k</code>'th hint will
2657  be used for <code>ik</code> iterations (images).  A value of <code>0</code>
2658  causes the hint to be applied to convergence.  Not setting this option is
2659  like setting it to <code>0,0,...,0</code>.  If length of the specified
2660  sequence is less than the number of hints, the sequence is padded with
2661  zeroes.   
2662  </dl>
2663
2664  Guided search also uses the High Density traversal options that are
2665  germane to dead-ends. The relevant flags are hd_dead_end,
2666  hd_dead_end_approx_method, hd_frontier_approx_threshold,
2667  hd_approx_quality, hd_approx_bias_quality. Use help on the
2668  print_hd_options command for explanation of these flags. If guided
2669  search is used with HD using the -A 1 options in
2670  <tt>compute_reach</tt> and <tt>check_invariant</tt>, the HD options
2671  are used by both HD and guided search. ]
2672
2673 
2674  SideEffects []
2675
2676******************************************************************************/
2677static int
2678CommandPrintGuidedSearchOptions(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
2679{
2680  int c;
2681  if (*hmgr == NULL) {
2682    fprintf(vis_stderr,"** hrc error: Hierarchy manager is empty\n");
2683    return 1;
2684  }
2685
2686  util_getopt_reset();
2687  while ((c = util_getopt(argc, argv, "h")) != EOF) {
2688    switch(c) {
2689      case 'h':
2690        goto usage;
2691      default:
2692        goto usage;
2693    }
2694     /* NOT REACHED */
2695  }
2696
2697  FsmGuidedSearchPrintOptions();
2698  return 0;
2699 usage:
2700  (void) fprintf(vis_stderr,"usage: print_guided_search_options [-h]\n");
2701  (void) fprintf(vis_stderr, "  -h  print the command usage\n");
2702  return 1;
2703
2704} /* end of CommandGuidedSearchPrintOptions */
2705
2706
2707/**Function********************************************************************
2708
2709  Synopsis    [Handle function for timeout.]
2710
2711  Description [This function is called when the time out occurs.]
2712
2713  SideEffects []
2714
2715******************************************************************************/
2716static void
2717TimeOutHandle(void)
2718{
2719  longjmp(timeOutEnv, 1);
2720}
Note: See TracBrowser for help on using the repository browser.