[11] | 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 |
---|