source: vis_dev/vis-2.1/share/vis/help/print_hybrid_optionsCmd.txt @ 11

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

Add vis

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