| 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 |
|---|