[14] | 1 | |
---|
| 2 | print_guided_search_options - print information about guided_search_options |
---|
| 3 | in use |
---|
| 4 | _________________________________________________________________ |
---|
| 5 | |
---|
| 6 | print_guided_search_options [-h] |
---|
| 7 | |
---|
| 8 | Prints information about current Guided Search options. Guided search is an |
---|
| 9 | alternate method to compute fixpoints by modifying the fixpoint computation |
---|
| 10 | with restrictions. It is applicable to the compute_reach, check_invariant |
---|
| 11 | and model_check commands (refer to their help pages on the use of guided |
---|
| 12 | search). See also for details: Ravi and Somenzi, Hints to accelerate |
---|
| 13 | symbolic traversal. CHARME'99; Bloem, Ravi, and Somenzi, Efficient Decision |
---|
| 14 | Procedures for Model Checking of Linear Time Logic Properties, CAV'99; |
---|
| 15 | Bloem, Ravi, and Somenzi, Symbolic Guided Search for CTL Model Checking, |
---|
| 16 | DAC'00. Not allowed with -A 2 or -i, and will only work with iwls95 or |
---|
| 17 | monolithic image methods. The description of some options can be found in |
---|
| 18 | the help page for set. |
---|
| 19 | |
---|
| 20 | Command options: |
---|
| 21 | |
---|
| 22 | guided_search_hint_type |
---|
| 23 | Choose from local (default) or global. If this flag is set to local, |
---|
| 24 | then every subformula is evaluated to completion, using all hints in |
---|
| 25 | order, before the next subformula is started. For pure ACTL or pure |
---|
| 26 | ECTL formulae, we can also set guided_search_hint_type to global, in |
---|
| 27 | which case the entire formula is evaluated for one hint before moving |
---|
| 28 | on to the next hint, using underapproximations. |
---|
| 29 | |
---|
| 30 | guided_search_underapprox_minimize_method |
---|
| 31 | Choose from "constrain" and "and" (default). Sets the method with |
---|
| 32 | which the transition relation is minimized when underapproximations |
---|
| 33 | are used. The option constrain is incompatible with hints that use |
---|
| 34 | signals other than inputs. |
---|
| 35 | |
---|
| 36 | guided_search_overapprox_minimize_method |
---|
| 37 | Choose from "squeeze" and "ornot" (default). Sets the method with |
---|
| 38 | which the transition relation is minimized when underapproximations |
---|
| 39 | are used. The option squeeze is incompatible with hints that use |
---|
| 40 | signals other than inputs. Ornot implies that the transition relation |
---|
| 41 | will be disjoined with the negation of the hint: T' = T + ~h, whereas |
---|
| 42 | squeeze will find a small BDD between T and T'. |
---|
| 43 | |
---|
| 44 | guided_search_sequence |
---|
| 45 | For compute_reach and check_invariant only. Set this flag to a list |
---|
| 46 | of comma-separated integers i1,i2,...,in, with n at most the number |
---|
| 47 | of hints that you specify . The k'th hint will be used for ik |
---|
| 48 | iterations (images). A value of 0 causes the hint to be applied to |
---|
| 49 | convergence. Not setting this option is like setting it to 0,0,...,0. |
---|
| 50 | If length of the specified sequence is less than the number of hints, |
---|
| 51 | the sequence is padded with zeroes. |
---|
| 52 | |
---|
| 53 | Guided search also uses the High Density traversal options that are germane |
---|
| 54 | to dead-ends. The relevant flags are hd_dead_end, hd_dead_end_approx_method, |
---|
| 55 | hd_frontier_approx_threshold,hd_approx_quality,hd_approx_bias_quality.Use |
---|
| 56 | help on the print_hd_options command for explanation of these flags. If |
---|
| 57 | guided search is used with HD using the -A 1 options in compute_reach and |
---|
| 58 | check_invariant, the HD options are used by both HD and guided search. |
---|
| 59 | _________________________________________________________________ |
---|
| 60 | |
---|
| 61 | Last updated on 20100410 00h02 |
---|