source: vis_dev/vis-2.3/share/help/print_hybrid_optionsCmd.txt @ 87

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

vis2.3
File size: 9.8 KB
Line 
1
2  print_hybrid_options - print information about the hybrid image computation
3  options currently in use
4     _________________________________________________________________
5
6   print_hybrid_options [-h] [-H]
7
8   Prints information about the current hybrid image computation options.
9
10   Command options:
11
12   -h
13          Print the command usage.
14
15   -H
16          Print the hybrid image computation set command usage.
17
18   Set parameters: The hybrid image computation options are specified with the
19   set command.
20
21   hybrid_mode <mode>
22          Specify a mode how to start hybrid computation.
23
24          mode must be one of the following:
25
26          0 : start with only transition function and build transition relation
27          on demand
28
29          1 : start with both transition function and relation (default)
30
31          2 : start with only transition relation. Only this mode can deal with
32          nondeterminism.
33
34   hybrid_tr_split_method <method>
35          Specify a method to choose a splitting variable in hybrid mode = 2.
36
37          method must be one of the following:
38
39          0 : use support (default)
40
41          1 : use estimate BDD size
42
43   hybrid_build_partial_tr <method>
44          Specify whether to build full or partial transition relation in
45          hybrid mode = 2. This option is used to use less memory. When we use
46          partial  transition relation, for the variables excluded in the
47          transition relation, we build each bit transition relation on demand.
48          When nondeterminism exists in the circuit, this can not be used.
49          method must be one of the following:
50
51          yes : build partial transition relation
52
53          no : build full transition relation (default)
54
55   hybrid_partial_num_vars <number>
56          Specify how many variables are going to be excluded in building
57          partial transition relation. The default is 8.
58
59   hybrid_partial_method <method>
60          Specify a method to choose variables to be excluded in building
61          partial transition relation.
62
63          method must be one of the following:
64
65          0 : use BDD size (default)
66
67          1 : use support
68
69   hybrid_delayed_split <method>
70          Specify a method whether to split transition relation immediately or
71          just all at once before AndExist.
72
73          method must be one of the following:
74
75          yes : apply splitting to transition relation at once
76
77          no : do not apply (default)
78
79   hybrid_split_min_depth <number>
80          Specify the minimum depth to apply dynamic hybrid method. If a depth
81          is smaller than this minimum depth, just split. The default is 1.
82
83   hybrid_split_max_depth <number>
84          Specify the maximum depth to apply dynamic hybrid method. If a depth
85          is bigger than this maximum depth, just conjoin. The default is 5.
86
87   hybrid_pre_split_min_depth <number>
88          Specify the minimum depth to apply dynamic hybrid method in preimage
89          computation. If a depth is smaller than this minimum depth, just
90          split. The default is 0.
91
92   hybrid_pre_split_max_depth <number>
93          Specify the maximum depth to apply dynamic hybrid method in preimage
94          computation. If a depth is bigger than this maximum depth, just
95          conjoin. The default is 4.
96
97   hybrid_lambda_threshold <number>
98          Specify a threshold in floating between 0.0 and 1.0 to determine to
99          split or to conjoin after computing variable lifetime lambda for
100          image computation. If lambda is equal or smaller than this threshold,
101          we conjoin. Otherwise we split. The default is 0.6
102
103   hybrid_pre_lambda_threshold <number>
104          Specify a threshold in floating between 0.0 and 1.0 to determine to
105          split or to conjoin after computing variable lifetime lambda for
106          preimage  computation.  If lambda is equal or smaller than this
107          threshold, we conjoin. Otherwise we split. The default is 0.65
108
109   hybrid_conjoin_vector_size <number>
110          If the number of components in transition function vector is equal or
111          smaller than this threshold, we just conjoin. This check is performed
112          before computing lambda. The default is 10.
113
114   hybrid_conjoin_relation_size <number>
115          If the number of clusters in transition relation is equal or smaller
116          than this threshold, we just conjoin. This check is performed before
117          computing lambda. The default is 2.
118
119   hybrid_conjoin_relation_bdd_size <number>
120          If the shared BDD size of transition relation is equal or smaller
121          than this threshold, we conjoin. This check is performed before
122          computing lambda. The default is 200.
123
124   hybrid_improve_lambda <number>
125          When variable lifetime lambda is bigger than lambda threshold, if the
126          difference between previous and current lambda is equal or smaller
127          than this threshold, then we conjoin. The default is 0.1.
128
129   hybrid_improve_vector_size <number>
130          When variable lifetime lambda is bigger than lambda threshold, if the
131          difference between the previous and current number of components in
132          transition function vector is equal or smaller than this threshold,
133          then we conjoin. The default is 3.
134
135   hybrid_improve_vector_bdd_size <number>
136          When variable lifetime lambda is bigger than lambda threshold, if the
137          difference  between the previous and current shared BDD size of
138          transition function vector is equal or smaller than this threshold,
139          then we conjoin. The default is 30.0.
140
141   hybrid_decide_mode <method>
142          Specify a method to decide whether to split or to conjoin.
143
144          method must be one of the following:
145
146          0 : use only lambda
147
148          1 : use lambda and also special checks to conjoin
149
150          2 : use lambda and also improvement
151
152          3 : use all (default)
153
154   hybrid_reorder_with_from <method>
155          Specify a method to reorder transition relation to conjoin in image
156          computation, whether to include from set in the computation.
157
158          method must be one of the following:
159
160          yes : reorder relation array with from to conjoin (default)
161
162          no : reorder relation array without from to conjoin
163
164   hybrid_pre_reorder_with_from <method>
165          Specify  a  method to reorder transition relation to conjoin in
166          preimage computation, whether to include from set in the computation.
167
168          method must be one of the following:
169
170          yes : reorder relation array with from to conjoin
171
172          no : reorder relation array without from to conjoin (default)
173
174   hybrid_lambda_mode <method>
175          Specify a method to decide which variable lifetime to be used for
176          image computation.
177
178          method must be one of the following:
179
180          0 : total lifetime with ps/pi variables (default)
181
182          1 : active lifetime with ps/pi variables
183
184          2 : total lifetime with ps/ns/pi variables
185
186   hybrid_pre_lambda_mode <method>
187          Specify a method to decide which variable lifetime to be used for
188          preimage computation.
189
190          method must be one of the following:
191
192          0 : total lifetime with ns/pi variables
193
194          1 : active lifetime with ps/pi variables
195
196          2 : total lifetime with ps/ns/pi variables (default)
197
198          3 : total lifetime with ps/pi variables
199
200   hybrid_lambda_with_from <method>
201          Specify a method to compute variable lifetime lambda, whether to
202          include from set in the computation.
203
204          method must be one of the following:
205
206          yes : include from set in lambda computation (default)
207
208          no : do not include
209
210   hybrid_lambda_with_tr <method>
211          Specify a method to compute variable lifetime lambda, whether to use
212          transition relation or transition function vector, when both exist.
213
214          method must be one of the following:
215
216          yes : use transition relation (default)
217
218          no : use transition function vector
219
220   hybrid_lambda_with_clustering <method>
221          Specify a method whether to include clustering to compute variable
222          lifetime lambda.
223
224          method must be one of the following:
225
226          yes : compute lambda after clustering
227
228          no : do not cluster (default)
229
230   hybrid_synchronize_tr <method>
231          Specify a method to keep transition relation. This option is only for
232          when hybrid mode is 1.
233
234          method must be one of the following:
235
236          yes : rebuild transition relation from function vector whenever the
237          function vector changes
238
239          no : do not rebuild (default)
240
241   hybrid_img_keep_pi <method>
242          Specify a method to build forward transition relation.
243
244          method must be one of the following:
245
246          yes  :  keep  all primary input variables in forward transition
247          relation.
248
249          no : quantify out local primary input variables from the transition
250          relation. (default)
251
252   hybrid_pre_keep_pi <method>
253          Specify a method to build backward transition relation.
254
255          method must be one of the following:
256
257          yes  :  keep all primary input variables in backward transition
258          relation and preimages.
259
260          no : quantify out local primary input variables from the transition
261          relation. (default)
262
263   hybrid_pre_canonical <method>
264          Specify a method whether to canonicalize the function vector for
265          preimage computation.
266
267          method must be one of the following:
268
269          yes : canonicalize the function vector
270
271          no : do not canonicalize (default)
272
273   hybrid_tr_method lt;methodgt;
274          Specify an image method for AndExist operation in hybrid method.
275
276          method must be one of the following:
277
278          iwls95 (default)
279
280          mlp
281     _________________________________________________________________
282
283   Last updated on 20100410 00h02
Note: See TracBrowser for help on using the repository browser.