source: vis_dev/vis-2.1/share/help/print_tfm_optionsCmd.txt @ 14

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

Add vis
File size: 9.8 KB
Line 
1
2  print_tfm_options - print information about the transition function based
3  image computation options currently in use
4     _________________________________________________________________
5
6   print_tfm_options [-h] [-H]
7
8   Prints  information  about the current transition function based image
9   computation options.
10
11   Command options:
12
13   -h
14          Print the command usage.
15
16   -H
17          Print  the  transition  function  based  image  computation set
18          command usage.
19
20   Set  parameters:  The  transition  function  based  image  computation
21   options are specified with the set command.
22
23   tfm_split_method <method>
24          Specify a splitting method.
25
26          method must be one of the following:
27
28          0 : input splitting (default)
29
30          1 : output splitting
31
32          2 : mixed (input split + output split)
33
34   tfm_input_split <method>
35          Specify an input splitting method.
36
37          method must be one of the following:
38
39          0 : support before splitting (default)
40
41          1 : support after splitting
42
43          2 : estimate BDD size after splitting
44
45          3 : top variable
46
47   tfm_pi_split_flag <method>
48          Specify  whether  to allow primary input variables to be chosen
49          as a splitting variable.
50
51          method must be one of the following:
52
53          yes  :  choose  either  state  or  input  variable as splitting
54          variable (default)
55
56          no : choose only state variable as splitting variable
57
58   tfm_range_comp <method>
59          Specify   a   method   whether   to   convert  image  to  range
60          computataion.
61
62          method must be one of the following:
63
64          0 : do not convert to range computation
65
66          1 : convert image to range computation (default)
67
68          2 : use a threshold (tfm_range_threshold, default for hybrid)
69
70   tfm_range_threshold <number>
71          This  option is valid only when the tfm_range_comp is set to 2.
72          This threshold is used to determine whether to convert to range
73          computation by comparing the shared BDD size of function vector
74          after constraining w.r.t. from set to its original size. If the
75          size  is  less  than  the  origianl size * , then we convert to
76          range computation. The default value is 10.
77
78   tfm_range_try_threshold <number>
79          This  option is valid only when the tfm_range_comp is set to 2.
80          This  option  is  used  to disable checking the condition if it
81          fails to convert consecutively times. The default value is 2.
82
83   tfm_range_check_reorder <method>
84          Specify  whether  to  force  to  call variable reordering after
85          constraining   function  vector  w.r.t.  from  set  and  before
86          checking the condition.
87
88          method must be one of the following:
89
90          yes : force to reorder before checking tfm_range_threshold
91
92          no : do not reorder (default)
93
94   tfm_tie_break_mode <method>
95          Specify  a tie breaking method when we have a tie in choosing a
96          splitting variable in input and output splitting method.
97
98          method must be one of the following:
99
100          0 : the closest variable to top (default)
101
102          1 : the smallest BDD size after splitting
103
104   tfm_output_split <method>
105          Specify an output splitting method.
106
107          method must be one of the following:
108
109          0 : smallest BDD size (default)
110
111          1 : largest BDD size
112
113          2 : top variable
114
115   tfm_turn_depth <number>
116          This  option  is  valid  only  when  mixed  or hybrid method is
117          chosen.  This  is used to determine when to switch to the other
118          method  at  which  depth of recursion. The default is 5 for tfm
119          and -1 for hybrid method.
120
121   tfm_find_decomp_var <method>
122          Specify a method whether to try to find a decomposable variable
123          (meaning articulation point) first if any.
124
125          method must be one of the following:
126
127          yes : try to find a decomposable variable (articulation point)
128
129          no : do not try (default)
130
131   tfm_sort_vector_flag <method>
132          Specify  a  method whether to sort function vectors to increase
133          cache performance.
134
135          method must be one of the following:
136
137          yes : sort function vectors (default for tfm)
138
139          no : do not sort (default for hybrid)
140
141   tfm_print_stats <method>
142          Specify  a  method  whether  to  print statistics for cache and
143          recursions at the end of job.
144
145          method must be one of the following:
146
147          yes : print statistics
148
149          no : do not print (default)
150
151   tfm_print_bdd_size <method>
152          Specify  a  method  whether  to  print  the  BDD  size  of  all
153          intermediate product.
154
155          method must be one of the following:
156
157          yes : print BDD size
158
159          no : do not print (default)
160
161   tfm_split_cube_func <method>
162          Specify  a  method  whether  to  try to find a cube in function
163          vector  in  input splitting, then perform output splitting once
164          w.r.t. the cube.
165
166          method must be one of the following:
167
168          yes : try cube splitting
169
170          no : do not try (default)
171
172   tfm_find_essential <method>
173          Specify  a method whether to try to find essential variables in
174          from  set.  If  a  variable  occurs  in all cubes of a BDD, the
175          variable is called essential. If exists, minimize both function
176          vector and the from set with the essential cube.
177
178          method must be one of the following:
179
180          0 : do not try (default)
181
182          1 : try to find essential variables
183
184          2 : on and off dynamically
185
186   tfm_print_essential <method>
187          Specify  a  method whether to print information about essential
188          variables.
189
190          method must be one of the following:
191
192          0 : do not print (default)
193
194          1 : print only at end
195
196          2 : print at every image computation
197
198   tfm_use_cache <method>
199          Specify whether to use an image cache.
200
201          method must be one of the following:
202
203          0 : do not use cache (default for hybrid)
204
205          1 : use cache (default)
206
207          2 : store all intermediate results
208
209   tfm_global_cache <method>
210          Specify  a method whether to use one global image cache, or one
211          image cache per each machine.
212
213          method must be one of the following:
214
215          yes : use only one global cache (default)
216
217          no : use one cache per machine
218
219   tfm_max_chain_length <number>
220          This  option  is  used  to set the maximum number of items in a
221          slot for conflict. The default is 2.
222
223   tfm_init_cache_size <number>
224          This  option  is used to set the initial cache size. The number
225          is  recommended  to  be  a  prime  number. Currently, we do not
226          resize  the  cache size, but for the future extension, we named
227          initial. The default is 1001.
228
229   tfm_auto_flush_cache <method>
230          Specify a method to flush image cache.
231
232          method must be one of the following:
233
234          0 : flush cache only when requested
235
236          1 : flush cache at the end of image computation (default)
237
238          2 : flush cache before reordering
239
240   tfm_compose_intermediate_vars <method>
241          Specify a method whether to compose all intermediate variables.
242
243          method must be one of the following:
244
245          yes : compose all
246
247          no : do not compose (default)
248
249   tfm_pre_split_method <method>
250          Specify a splitting method for preimage computation.
251
252          method must be one of the following:
253
254          0 : input splitting (domain cofactoring, default)
255
256          1 : output splitting (constraint cofactoring)
257
258          2 : mixed (input split + output split)
259
260          3 : substitution
261
262   tfm_pre_input_split <method>
263          Specify an input splitting method for preimage computation.
264
265          method must be one of the following:
266
267          0 : support before splitting (default)
268
269          1 : support after splitting
270
271          2 : estimate BDD size after splitting
272
273          3 : top variable
274
275   tfm_pre_output_split <method>
276          Specify an output splitting method for preimage computation.
277
278          method must be one of the following:
279
280          0 : smallest BDD size (default)
281
282          1 : largest BDD size
283
284          2 : top variable
285
286   tfm_pre_dc_leaf_method <method>
287          Specify  a  method  to  switch  to  another  method to complete
288          preimage  computation in domain cofactoring method when no more
289          splitting variable exist.
290
291          method must be one of the following:
292
293          0 : substitution (default)
294
295          1 : constraint cofactoring
296
297          2 : hybrid
298
299   tfm_pre_minimize <method>
300          Specify a method whether to minimize transition function vector
301          w.r.t  a chosen function in constraint cofactoring method. This
302          option  is  recommended  to  use  when image cache is disabled,
303          because  even  though  this option can minimize the BDD size of
304          function vector, this may degrade cache performance.
305
306          method must be one of the following:
307
308          yes  :  minimize  function  vector  w.r.t. a chosen function in
309          constraint cofactoring
310
311          no : do not minimize (default)
312
313   tfm_verbosity <verbosity>
314          Specify   the   level  of  printing  information  related  with
315          transition function method.
316
317          verbosity must be 0 - 2 (default = 0).
318     _________________________________________________________________
319
320   Last updated on 20050519 10h16
Note: See TracBrowser for help on using the repository browser.