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