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