source: vis_dev/vis-2.3/share/help/print_hd_optionsCmd.txt @ 101

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

vis2.3
File size: 7.7 KB
Line 
1
2  print_hd_options - print information about the HD options currently in use
3     _________________________________________________________________
4
5   print_hd_options [-h]
6
7   Prints  information  about the current HD options. The HD method is an
8   alternate  method to compute a least fixpoint and is provided with the
9   compute_reach and check_invariant commands. The method is described in Ravi
10   and Somenzi, ICCAD95. The command can be used only when compiled with the
11   CUDD package.
12
13   Command options:
14
15   -h
16   Print the command usage.
17
18   Set parameters: The HD options are specified with the set command.
19
20   hd_frontier_approx_method <method>
21          This option specifes the method to approximate the frontier set.
22
23          Methods:
24
25          remap_ua : (Default) The BDD approximation method of DAC98 Ravi,
26          Shiple, McMillan, Somenzi.
27
28          biased_rua : Approximation method similar to remap_ua, but uses a
29          bias function. The bias function is set appropriate to the context.
30
31          under_approx : The BDD approximation method of Shiple's thesis.
32
33          heavy_branch : The BDD approximation method of ICCAD95 Ravi, Somenzi.
34
35          short_paths : The BDD approximation method of ICCAD95 Ravi, Somenzi.
36
37          compress : An approximation method that runs short_paths first and
38          then remap_ua.
39
40   hd_frontier_approx_threshold <number>
41          This option specifes the size of the frontier to be used for image
42          computation. The threshold for the various methods is approximate
43          (not strictly adhered to). For the remap_ua and biased_rua method,
44          this threshold is a lower bound and the default is 3500. For the
45          short_paths and heavy_branch methods, this threshold is an upper
46          bound. Therefore, a default of 2000 is set to obtain a meaningful
47          result. Any value lower than 2000 is corrected to this default. This
48          value is also relevant for dead-end computations. In a dead-end, the
49          threshold for each image computation (of a disjunct of Reached) is
50          five times the frontier approximation threshold. When the frontier
51          approximation threshold is 0, the threshold for each dead-end image
52          computation is 5000.
53
54   hd_approx_quality <double>
55          This option specifies the quality factor for the under_approx and
56          remap_ua methods. Default value is 1.0. The range is any double value
57          greater than 0. Smaller quality factors produce smaller results.
58          Meaningful values are between 1 and 2.
59
60   hd_approx_bias_quality <double>
61          This option specifies the quality factor for the biased_rua method.
62          Default value is 0.5. The range is any double value greater than 0.
63          Smaller quality factors produce smaller results. Meaningful values
64          are between 0 and 1.
65
66   hd_dead_end <method>
67          This option specifies the method used for dead-end computation. A
68          "dead-end"  is  characterized  by an empty frontier. A dead-end
69          computation involves generating new states from the reached set.
70
71          Methods:
72
73          brute_force : Computes the image of the entire reached set. May be
74          fatal if the reached set is very large.
75
76          conjuncts : (Default) Computes the image of reached by decomposing
77          into parts.
78
79          hybrid : Computes the image of a subset of reached. If no new states,
80          then the reaminder is decomposed in parts.
81
82   hd_dead_end_approx_method <method>
83          This option allows the specification of the approximation method to
84          use to compute the subset of Reached at the dead-end. The threshold
85          used is the same as hd_frontier_approx_threshold.
86
87          For methods, refer hd_frontier_approx_method methods. Default is
88          remap_ua.
89
90   hd_no_scrap_states
91          This allows the option of not adding the "scrap" states. Scrap states
92          are residues from the approximation of the frontier set. Default is
93          to add the scrap states.
94
95   hd_new_only
96          This allows the option of adding considering only new states of each
97          iteration for image computation. The default is to take a set in the
98          interval of the new states and the reached set.
99
100   hd_only_partial_image
101          This allows the option of HD with partial image computation only (no
102          approximation of the frontier set). Default is to allow both partial
103          images and approximation of the frontier set.
104
105   Partial Image options:
106
107   hd_partial_image_method <method>
108          This option allows the image computation to approximate the image
109          with the specified method.
110
111          Methods:
112
113          approx : (Default) Computes a partial image by under-approximating
114          the intermediate products of image computation.
115
116          clipping  : Computes a partial image by "clipping" the depth of
117          recursion of the and-abstract computations during image computation.
118
119   hd_partial_image_threshold <number>
120          This options allows the specification of a threshold (in terms of bdd
121          node  size  of  the  intermediate  product)  that  will trigger
122          approximation of the intermediate product. Default is 200000. This
123          option has to be used in conjunction with hd_partial_image_size. If
124          the value of hd_partial_image_size is larger than this option, then
125          the approximation of the intermediate size will be as large as the
126          hd_partial_image_size number.
127
128   hd_partial_image_size <number>
129          This options allows the specification of a size (in terms of bdd node
130          size of the intermediate product) that is the target size of the
131          approximated  intermediate  product. Default is 100000. For the
132          short_paths and heavy_branch methods, the size of the approximation
133          is corrected to 10000 if the size specified is lower. This is because
134          the short_paths and heavy_branch methods consider this size as an
135          upper bound on the approximation. This option has to be used in
136          conjunction  with  hd_partial_image_threshold.  If the value of
137          hd_partial_image_threshold is much larger than this option, then the
138          desired  size  will not be obtained as approximation may not be
139          triggered.
140
141   hd_partial_image_approx <method>
142          This options allows the specification of the method to be used to
143          approximate the intermediate product.
144
145          For methods, refer hd_frontier_approx_method methods. Default is
146          remap_ua.
147
148   hd_partial_image_approx_quality <double>
149          This option specifies the quality factor for the under_approx and
150          remap_ua methods for partial image computation. Default value is 1.0.
151          Range of values is any double greater than 0. Smaller quality factors
152          produce smaller results. Meaningful values are between 1 and 2.
153
154   hd_partial_image_approx_bias_quality <double>
155          This option specifies the quality factor for the biased_rua method
156          for partial image computation. Default value is 0.5. Range of values
157          is any double greater than 0. Smaller quality factors produce smaller
158          results. Meaningful values are between 0 and 1.
159
160   hd_partial_image_clipping_depth <double>
161          This  option allows the specification of the depth at which the
162          recursion can be clipped when _hd_partial_image_method_ is clipping.
163          Range  of values is between 0 and 1. The clipping depth is then
164          calculated as the specified fraction of the number of variables.
165          Default is 0.4.
166     _________________________________________________________________
167
168   Last updated on 20100410 00h02
Note: See TracBrowser for help on using the repository browser.