[14] | 1 | |
---|
| 2 | print_hd_options - print information about the HD options currently in use |
---|
| 3 | _________________________________________________________________ |
---|
| 4 | |
---|
| 5 | print_hd_options [-h] |
---|
| 6 | |
---|
| 7 | Prints information about the current HD options. The HD method is an |
---|
| 8 | alternate method to compute a least fixpoint and is provided with the |
---|
| 9 | compute_reach and check_invariant commands. The method is described in Ravi |
---|
| 10 | and Somenzi, ICCAD95. The command can be used only when compiled with the |
---|
| 11 | CUDD package. |
---|
| 12 | |
---|
| 13 | Command options: |
---|
| 14 | |
---|
| 15 | -h |
---|
| 16 | Print the command usage. |
---|
| 17 | |
---|
| 18 | Set parameters: The HD options are specified with the set command. |
---|
| 19 | |
---|
| 20 | hd_frontier_approx_method <method> |
---|
| 21 | This option specifes the method to approximate the frontier set. |
---|
| 22 | |
---|
| 23 | Methods: |
---|
| 24 | |
---|
| 25 | remap_ua : (Default) The BDD approximation method of DAC98 Ravi, |
---|
| 26 | Shiple, McMillan, Somenzi. |
---|
| 27 | |
---|
| 28 | biased_rua : Approximation method similar to remap_ua, but uses a |
---|
| 29 | bias function. The bias function is set appropriate to the context. |
---|
| 30 | |
---|
| 31 | under_approx : The BDD approximation method of Shiple's thesis. |
---|
| 32 | |
---|
| 33 | heavy_branch : The BDD approximation method of ICCAD95 Ravi, Somenzi. |
---|
| 34 | |
---|
| 35 | short_paths : The BDD approximation method of ICCAD95 Ravi, Somenzi. |
---|
| 36 | |
---|
| 37 | compress : An approximation method that runs short_paths first and |
---|
| 38 | then remap_ua. |
---|
| 39 | |
---|
| 40 | hd_frontier_approx_threshold <number> |
---|
| 41 | This option specifes the size of the frontier to be used for image |
---|
| 42 | computation. The threshold for the various methods is approximate |
---|
| 43 | (not strictly adhered to). For the remap_ua and biased_rua method, |
---|
| 44 | this threshold is a lower bound and the default is 3500. For the |
---|
| 45 | short_paths and heavy_branch methods, this threshold is an upper |
---|
| 46 | bound. Therefore, a default of 2000 is set to obtain a meaningful |
---|
| 47 | result. Any value lower than 2000 is corrected to this default. This |
---|
| 48 | value is also relevant for dead-end computations. In a dead-end, the |
---|
| 49 | threshold for each image computation (of a disjunct of Reached) is |
---|
| 50 | five times the frontier approximation threshold. When the frontier |
---|
| 51 | approximation threshold is 0, the threshold for each dead-end image |
---|
| 52 | computation is 5000. |
---|
| 53 | |
---|
| 54 | hd_approx_quality <double> |
---|
| 55 | This option specifies the quality factor for the under_approx and |
---|
| 56 | remap_ua methods. Default value is 1.0. The range is any double value |
---|
| 57 | greater than 0. Smaller quality factors produce smaller results. |
---|
| 58 | Meaningful values are between 1 and 2. |
---|
| 59 | |
---|
| 60 | hd_approx_bias_quality <double> |
---|
| 61 | This option specifies the quality factor for the biased_rua method. |
---|
| 62 | Default value is 0.5. The range is any double value greater than 0. |
---|
| 63 | Smaller quality factors produce smaller results. Meaningful values |
---|
| 64 | are between 0 and 1. |
---|
| 65 | |
---|
| 66 | hd_dead_end <method> |
---|
| 67 | This option specifies the method used for dead-end computation. A |
---|
| 68 | "dead-end" is characterized by an empty frontier. A dead-end |
---|
| 69 | computation involves generating new states from the reached set. |
---|
| 70 | |
---|
| 71 | Methods: |
---|
| 72 | |
---|
| 73 | brute_force : Computes the image of the entire reached set. May be |
---|
| 74 | fatal if the reached set is very large. |
---|
| 75 | |
---|
| 76 | conjuncts : (Default) Computes the image of reached by decomposing |
---|
| 77 | into parts. |
---|
| 78 | |
---|
| 79 | hybrid : Computes the image of a subset of reached. If no new states, |
---|
| 80 | then the reaminder is decomposed in parts. |
---|
| 81 | |
---|
| 82 | hd_dead_end_approx_method <method> |
---|
| 83 | This option allows the specification of the approximation method to |
---|
| 84 | use to compute the subset of Reached at the dead-end. The threshold |
---|
| 85 | used is the same as hd_frontier_approx_threshold. |
---|
| 86 | |
---|
| 87 | For methods, refer hd_frontier_approx_method methods. Default is |
---|
| 88 | remap_ua. |
---|
| 89 | |
---|
| 90 | hd_no_scrap_states |
---|
| 91 | This allows the option of not adding the "scrap" states. Scrap states |
---|
| 92 | are residues from the approximation of the frontier set. Default is |
---|
| 93 | to add the scrap states. |
---|
| 94 | |
---|
| 95 | hd_new_only |
---|
| 96 | This allows the option of adding considering only new states of each |
---|
| 97 | iteration for image computation. The default is to take a set in the |
---|
| 98 | interval of the new states and the reached set. |
---|
| 99 | |
---|
| 100 | hd_only_partial_image |
---|
| 101 | This allows the option of HD with partial image computation only (no |
---|
| 102 | approximation of the frontier set). Default is to allow both partial |
---|
| 103 | images and approximation of the frontier set. |
---|
| 104 | |
---|
| 105 | Partial Image options: |
---|
| 106 | |
---|
| 107 | hd_partial_image_method <method> |
---|
| 108 | This option allows the image computation to approximate the image |
---|
| 109 | with the specified method. |
---|
| 110 | |
---|
| 111 | Methods: |
---|
| 112 | |
---|
| 113 | approx : (Default) Computes a partial image by under-approximating |
---|
| 114 | the intermediate products of image computation. |
---|
| 115 | |
---|
| 116 | clipping : Computes a partial image by "clipping" the depth of |
---|
| 117 | recursion of the and-abstract computations during image computation. |
---|
| 118 | |
---|
| 119 | hd_partial_image_threshold <number> |
---|
| 120 | This options allows the specification of a threshold (in terms of bdd |
---|
| 121 | node size of the intermediate product) that will trigger |
---|
| 122 | approximation of the intermediate product. Default is 200000. This |
---|
| 123 | option has to be used in conjunction with hd_partial_image_size. If |
---|
| 124 | the value of hd_partial_image_size is larger than this option, then |
---|
| 125 | the approximation of the intermediate size will be as large as the |
---|
| 126 | hd_partial_image_size number. |
---|
| 127 | |
---|
| 128 | hd_partial_image_size <number> |
---|
| 129 | This options allows the specification of a size (in terms of bdd node |
---|
| 130 | size of the intermediate product) that is the target size of the |
---|
| 131 | approximated intermediate product. Default is 100000. For the |
---|
| 132 | short_paths and heavy_branch methods, the size of the approximation |
---|
| 133 | is corrected to 10000 if the size specified is lower. This is because |
---|
| 134 | the short_paths and heavy_branch methods consider this size as an |
---|
| 135 | upper bound on the approximation. This option has to be used in |
---|
| 136 | conjunction with hd_partial_image_threshold. If the value of |
---|
| 137 | hd_partial_image_threshold is much larger than this option, then the |
---|
| 138 | desired size will not be obtained as approximation may not be |
---|
| 139 | triggered. |
---|
| 140 | |
---|
| 141 | hd_partial_image_approx <method> |
---|
| 142 | This options allows the specification of the method to be used to |
---|
| 143 | approximate the intermediate product. |
---|
| 144 | |
---|
| 145 | For methods, refer hd_frontier_approx_method methods. Default is |
---|
| 146 | remap_ua. |
---|
| 147 | |
---|
| 148 | hd_partial_image_approx_quality <double> |
---|
| 149 | This option specifies the quality factor for the under_approx and |
---|
| 150 | remap_ua methods for partial image computation. Default value is 1.0. |
---|
| 151 | Range of values is any double greater than 0. Smaller quality factors |
---|
| 152 | produce smaller results. Meaningful values are between 1 and 2. |
---|
| 153 | |
---|
| 154 | hd_partial_image_approx_bias_quality <double> |
---|
| 155 | This option specifies the quality factor for the biased_rua method |
---|
| 156 | for partial image computation. Default value is 0.5. Range of values |
---|
| 157 | is any double greater than 0. Smaller quality factors produce smaller |
---|
| 158 | results. Meaningful values are between 0 and 1. |
---|
| 159 | |
---|
| 160 | hd_partial_image_clipping_depth <double> |
---|
| 161 | This option allows the specification of the depth at which the |
---|
| 162 | recursion can be clipped when _hd_partial_image_method_ is clipping. |
---|
| 163 | Range of values is between 0 and 1. The clipping depth is then |
---|
| 164 | calculated as the specified fraction of the number of variables. |
---|
| 165 | Default is 0.4. |
---|
| 166 | _________________________________________________________________ |
---|
| 167 | |
---|
| 168 | Last updated on 20100410 00h02 |
---|